diff --git a/regression/cbmc/struct14/main.c b/regression/cbmc/struct14/main.c
new file mode 100644
index 0000000000..014d887616
--- /dev/null
+++ b/regression/cbmc/struct14/main.c
@@ -0,0 +1,14 @@
+struct S
+{
+  int x;
+};
+
+int main(int argc, char *argv[])
+{
+  struct S s;
+
+  if(argc > 3)
+    s.x = 42;
+
+  __CPROVER_assert(s.x == 42, "should fail");
+}
diff --git a/regression/cbmc/struct14/test.desc b/regression/cbmc/struct14/test.desc
new file mode 100644
index 0000000000..b69d909607
--- /dev/null
+++ b/regression/cbmc/struct14/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+With field-sensitive SSA encoding we need to make sure that each struct member
+is treated as non-deterministic unless initialised.
diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp
index 46ce421c40..660bd640d0 100644
--- a/src/goto-symex/symex_decl.cpp
+++ b/src/goto-symex/symex_decl.cpp
@@ -64,8 +64,17 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   }
 
   // L2 renaming
-  std::size_t generation = state.increase_generation(l1_identifier, ssa);
-  CHECK_RETURN(generation == 1);
+  const exprt fields = state.field_sensitivity.get_fields(ns, state, ssa);
+  std::set<symbol_exprt> fields_set;
+  find_symbols(fields, fields_set);
+
+  for(const auto &l1_symbol : fields_set)
+  {
+    ssa_exprt field_ssa = to_ssa_expr(l1_symbol);
+    std::size_t field_generation =
+      state.increase_generation(l1_symbol.get_identifier(), field_ssa);
+    CHECK_RETURN(field_generation == 1);
+  }
 
   const bool record_events=state.record_events;
   state.record_events=false;