diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp
index a65d87b5fad..8fb3099aeb5 100644
--- a/src/goto-symex/symex_decl.cpp
+++ b/src/goto-symex/symex_decl.cpp
@@ -54,10 +54,10 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   target.decl(
     state.guard.as_expr(),
     ssa,
+    state.field_sensitivity.apply(ns, state, ssa, false),
     state.source,
-    hidden?
-      symex_targett::assignment_typet::HIDDEN:
-      symex_targett::assignment_typet::STATE);
+    hidden ? symex_targett::assignment_typet::HIDDEN
+           : symex_targett::assignment_typet::STATE);
 
   if(path_storage.dirty(ssa.get_object_name()) && state.atomic_section_id == 0)
     target.shared_write(
diff --git a/src/goto-symex/symex_target.h b/src/goto-symex/symex_target.h
index aead9ecc075..982ef67e255 100644
--- a/src/goto-symex/symex_target.h
+++ b/src/goto-symex/symex_target.h
@@ -127,6 +127,7 @@ class symex_targett
   /// Declare a fresh variable. The `cond_expr` is _lhs==lhs_.
   /// \param guard: Precondition for a declaration of this variable
   /// \param ssa_lhs: Variable to be declared, must be symbol (and not nil)
+  /// \param initializer: Initial value
   /// \param source: Pointer to location in the input GOTO program of this
   ///  declaration
   /// \param assignment_type: To distinguish between different types of
@@ -134,8 +135,9 @@ class symex_targett
   virtual void decl(
     const exprt &guard,
     const ssa_exprt &ssa_lhs,
+    const exprt &initializer,
     const sourcet &source,
-    assignment_typet assignment_type)=0;
+    assignment_typet assignment_type) = 0;
 
   /// Remove a variable from the scope.
   /// \param guard: Precondition for removal of this variable
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index ff7e1f6a382..f07e03235b2 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -128,6 +128,7 @@ void symex_target_equationt::assignment(
 void symex_target_equationt::decl(
   const exprt &guard,
   const ssa_exprt &ssa_lhs,
+  const exprt &initializer,
   const sourcet &source,
   assignment_typet assignment_type)
 {
@@ -138,7 +139,7 @@ void symex_target_equationt::decl(
 
   SSA_step.guard=guard;
   SSA_step.ssa_lhs=ssa_lhs;
-  SSA_step.ssa_full_lhs=ssa_lhs;
+  SSA_step.ssa_full_lhs = initializer;
   SSA_step.original_full_lhs=ssa_lhs.get_original_expr();
   SSA_step.hidden=(assignment_type!=assignment_typet::STATE);
 
diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h
index 1106d1001f1..7e65328639b 100644
--- a/src/goto-symex/symex_target_equation.h
+++ b/src/goto-symex/symex_target_equation.h
@@ -73,6 +73,7 @@ class symex_target_equationt:public symex_targett
   virtual void decl(
     const exprt &guard,
     const ssa_exprt &ssa_lhs,
+    const exprt &initializer,
     const sourcet &source,
     assignment_typet assignment_type);