diff --git a/regression/cbmc/trace-values/trace-values.c b/regression/cbmc/trace-values/trace-values.c
new file mode 100644
index 00000000000..d0560a76284
--- /dev/null
+++ b/regression/cbmc/trace-values/trace-values.c
@@ -0,0 +1,38 @@
+int global_var;
+
+struct S
+{
+  int f;
+  int array[3];
+} my_nested[2];
+
+int main()
+{
+  static int static_var;
+  int local_var;
+  int *p=&my_nested[0].array[1];
+  int *q=&my_nested[1].f;
+  int *null=0;
+  int *junk;
+
+  global_var=1;
+  static_var=2;
+  local_var=3;
+  *p=4;
+  *q=5;
+  *null=6;
+  *junk=7;
+
+  // dynamic
+  p=malloc(sizeof(int)*2);
+  p[1]=8;
+  
+  // not even a pointer variable
+  *(int *)0=9;
+
+  // assign entire struct
+  my_nested[1]=my_nested[0];
+
+  // get a trace
+  __CPROVER_assert(0, "");
+}
diff --git a/regression/cbmc/trace-values/trace-values.desc b/regression/cbmc/trace-values/trace-values.desc
new file mode 100644
index 00000000000..07063197241
--- /dev/null
+++ b/regression/cbmc/trace-values/trace-values.desc
@@ -0,0 +1,18 @@
+CORE
+trace-values.c
+--trace
+^EXIT=10$
+^SIGNAL=0$
+^  local_var=0 .*$
+^  global_var=1 .*$
+^  static_var=2 .*$
+^  local_var=3 .*$
+^  my_nested\[0.*\].array\[1.*\]=4 .*$
+^  my_nested\[1.*\].f=5 .*$
+^  null\$object=6 .*$
+^  junk\$object=7 .*$
+^  dynamic_object1\[1.*\]=8 .*$
+^  my_nested\[1.*\]={ .f=0, .array={ 0, 4, 0 } } .*$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp
index 1de01cc2bfe..3a23e0b8750 100644
--- a/src/goto-programs/goto_trace.cpp
+++ b/src/goto-programs/goto_trace.cpp
@@ -24,6 +24,25 @@ Author: Daniel Kroening
 
 #include "printf_formatter.h"
 
+static optionalt<symbol_exprt> get_object_rec(const exprt &src)
+{
+  if(src.id()==ID_symbol)
+    return to_symbol_expr(src);
+  else if(src.id()==ID_member)
+    return get_object_rec(to_member_expr(src).struct_op());
+  else if(src.id()==ID_index)
+    return get_object_rec(to_index_expr(src).array());
+  else if(src.id()==ID_typecast)
+    return get_object_rec(to_typecast_expr(src).op());
+  else
+    return {}; // give up
+}
+
+optionalt<symbol_exprt> goto_trace_stept::get_lhs_object() const
+{
+  return get_object_rec(full_lhs);
+}
+
 void goto_tracet::output(
   const class namespacet &ns,
   std::ostream &out) const
@@ -217,15 +236,15 @@ std::string trace_numeric_value(
 void trace_value(
   std::ostream &out,
   const namespacet &ns,
-  const ssa_exprt &lhs_object,
+  const optionalt<symbol_exprt> &lhs_object,
   const exprt &full_lhs,
   const exprt &value,
   const trace_optionst &options)
 {
   irep_idt identifier;
 
-  if(lhs_object.is_not_nil())
-    identifier=lhs_object.get_object_name();
+  if(lhs_object.has_value())
+    identifier=lhs_object->get_identifier();
 
   std::string value_string;
 
@@ -346,7 +365,7 @@ void show_full_goto_trace(
       if(step.pc->is_assign() ||
          step.pc->is_return() || // returns have a lhs!
          step.pc->is_function_call() ||
-         (step.pc->is_other() && step.lhs_object.is_not_nil()))
+         (step.pc->is_other() && step.full_lhs.is_not_nil()))
       {
         if(prev_step_nr!=step.step_nr || first_step)
         {
@@ -356,23 +375,13 @@ void show_full_goto_trace(
             out, ns, step, step.pc->source_location, step.step_nr, options);
         }
 
-        // see if the full lhs is something clean
-        if(is_index_member_symbol(step.full_lhs))
-          trace_value(
-            out,
-            ns,
-            step.lhs_object,
-            step.full_lhs,
-            step.full_lhs_value,
-            options);
-        else
-          trace_value(
-            out,
-            ns,
-            step.lhs_object,
-            step.lhs_object,
-            step.lhs_object_value,
-            options);
+       trace_value(
+         out,
+         ns,
+         step.get_lhs_object(),
+         step.full_lhs,
+         step.full_lhs_value,
+         options);
       }
       break;
 
@@ -386,7 +395,7 @@ void show_full_goto_trace(
       }
 
       trace_value(
-        out, ns, step.lhs_object, step.full_lhs, step.full_lhs_value, options);
+        out, ns, step.get_lhs_object(), step.full_lhs, step.full_lhs_value, options);
       break;
 
     case goto_trace_stept::typet::OUTPUT:
diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h
index e550e3e1535..b00579c569b 100644
--- a/src/goto-programs/goto_trace.h
+++ b/src/goto-programs/goto_trace.h
@@ -104,14 +104,14 @@ class goto_trace_stept
   // for assert
   std::string comment;
 
-  // the object being assigned
-  ssa_exprt lhs_object;
-
-  // the full, original lhs expression
+  // the full, original lhs expression, after dereferencing
   exprt full_lhs;
 
-  // A constant with the new value
-  exprt lhs_object_value, full_lhs_value;
+  // the object being assigned
+  optionalt<symbol_exprt> get_lhs_object() const;
+
+  // A constant with the new value of the lhs
+  exprt full_lhs_value;
 
   // for INPUT/OUTPUT
   irep_idt format_string, io_id;
@@ -141,8 +141,6 @@ class goto_trace_stept
     cond_value(false),
     formatted(false)
   {
-    lhs_object.make_nil();
-    lhs_object_value.make_nil();
     full_lhs.make_nil();
     full_lhs_value.make_nil();
     cond_expr.make_nil();
@@ -245,9 +243,10 @@ void show_goto_trace(
 void trace_value(
   std::ostream &out,
   const namespacet &,
-  const ssa_exprt &lhs_object,
+  const optionalt<symbol_exprt> &lhs_object,
   const exprt &full_lhs,
-  const exprt &value);
+  const exprt &value,
+  const trace_optionst &);
 
 #define OPT_GOTO_TRACE                                                         \
   "(trace-json-extended)"                                                      \
diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index ccae6ad7e55..2c382d76f98 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -278,24 +278,17 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
         }
 
         if(it->type==goto_trace_stept::typet::ASSIGNMENT &&
-           it->lhs_object_value.is_not_nil() &&
+           it->full_lhs_value.is_not_nil() &&
            it->full_lhs.is_not_nil())
         {
-          if(!it->lhs_object_value.is_constant() ||
-             !it->lhs_object_value.has_operands() ||
-             !has_prefix(id2string(it->lhs_object_value.op0().get(ID_value)),
-                         "INVALID-"))
-          {
-            xmlt &val=edge.new_element("data");
-            val.set_attribute("key", "assumption");
-            code_assignt assign(it->lhs_object, it->lhs_object_value);
-            irep_idt identifier=it->lhs_object.get_identifier();
-            val.data=convert_assign_rec(identifier, assign);
-
-            xmlt &val_s=edge.new_element("data");
-            val_s.set_attribute("key", "assumption.scope");
-            val_s.data=id2string(it->pc->source_location.get_function());
-          }
+          xmlt &val=edge.new_element("data");
+          val.set_attribute("key", "assumption");
+          val.data=from_expr(ns, it->pc->function, it->full_lhs)+" = "+
+                   from_expr(ns, it->pc->function, it->full_lhs_value)+";";
+
+          xmlt &val_s=edge.new_element("data");
+          val_s.set_attribute("key", "assumption.scope");
+          val_s.data=id2string(it->pc->source_location.get_function());
         }
         else if(it->type==goto_trace_stept::typet::GOTO &&
                 it->pc->is_goto())
diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
index 8882ff5cdb8..fa9617dfb0b 100644
--- a/src/goto-programs/interpreter.cpp
+++ b/src/goto-programs/interpreter.cpp
@@ -677,15 +677,7 @@ void interpretert::execute_assign()
       goto_trace_stept &trace_step=steps.get_last_step();
       assign(address, rhs);
       trace_step.full_lhs=code_assign.lhs();
-
-      // TODO: need to look at other cases on ssa_exprt
-      // (dereference should be handled on ssa)
-      if(ssa_exprt::can_build_identifier(trace_step.full_lhs))
-      {
-        trace_step.lhs_object=ssa_exprt(trace_step.full_lhs);
-      }
       trace_step.full_lhs_value=get_value(trace_step.full_lhs.type(), rhs);
-      trace_step.lhs_object_value=trace_step.full_lhs_value;
     }
   }
   else if(code_assign.rhs().id()==ID_side_effect)
diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp
index a02738f289d..508d8104d5e 100644
--- a/src/goto-programs/json_goto_trace.cpp
+++ b/src/goto-programs/json_goto_trace.cpp
@@ -77,7 +77,10 @@ void convert_decl(
   const jsont &json_location = conversion_dependencies.location;
   const namespacet &ns = conversion_dependencies.ns;
 
-  irep_idt identifier = step.lhs_object.get_identifier();
+  auto lhs_object=step.get_lhs_object();
+
+  irep_idt identifier =
+    lhs_object.has_value()?lhs_object->get_identifier():irep_idt();
 
   json_assignment["stepType"] = json_stringt("assignment");
 
diff --git a/src/goto-programs/vcd_goto_trace.cpp b/src/goto-programs/vcd_goto_trace.cpp
index 9e736033df1..3f6d1ec778b 100644
--- a/src/goto-programs/vcd_goto_trace.cpp
+++ b/src/goto-programs/vcd_goto_trace.cpp
@@ -89,16 +89,20 @@ void output_vcd(
   {
     if(step.is_assignment())
     {
-      irep_idt identifier=step.lhs_object.get_identifier();
-      const typet &type=step.lhs_object.type();
+      auto lhs_object=step.get_lhs_object();
+      if(lhs_object.has_value())
+      {
+        irep_idt identifier=lhs_object->get_identifier();
+        const typet &type=lhs_object->type();
 
-      const auto number=n.number(identifier);
+        const auto number=n.number(identifier);
 
-      const mp_integer width = pointer_offset_bits(type, ns);
+        const mp_integer width = pointer_offset_bits(type, ns);
 
-      if(width>=1)
-        out << "$var reg " << width << " V" << number << " "
-            << identifier << " $end" << "\n";
+        if(width>=1)
+          out << "$var reg " << width << " V" << number << " "
+              << identifier << " $end" << "\n";
+      }
     }
   }
 
@@ -113,30 +117,34 @@ void output_vcd(
     {
     case goto_trace_stept::typet::ASSIGNMENT:
       {
-        irep_idt identifier=step.lhs_object.get_identifier();
-        const typet &type=step.lhs_object.type();
-
-        out << '#' << timestamp << "\n";
-        timestamp++;
-
-        const auto number=n.number(identifier);
-
-        // booleans are special in VCD
-        if(type.id()==ID_bool)
+        auto lhs_object=step.get_lhs_object();
+        if(lhs_object.has_value())
         {
-          if(step.lhs_object_value.is_true())
-            out << "1" << "V" << number << "\n";
-          else if(step.lhs_object_value.is_false())
-            out << "0" << "V" << number << "\n";
+          irep_idt identifier=lhs_object->get_identifier();
+          const typet &type=lhs_object->type();
+
+          out << '#' << timestamp << "\n";
+          timestamp++;
+
+          const auto number=n.number(identifier);
+
+          // booleans are special in VCD
+          if(type.id()==ID_bool)
+          {
+            if(step.full_lhs_value.is_true())
+              out << "1" << "V" << number << "\n";
+            else if(step.full_lhs_value.is_false())
+              out << "0" << "V" << number << "\n";
+            else
+              out << "x" << "V" << number << "\n";
+          }
           else
-            out << "x" << "V" << number << "\n";
-        }
-        else
-        {
-          std::string binary=as_vcd_binary(step.lhs_object_value, ns);
+          {
+            std::string binary=as_vcd_binary(step.full_lhs_value, ns);
 
-          if(binary!="")
-            out << "b" << binary << " V" << number << " " << "\n";
+            if(binary!="")
+              out << "b" << binary << " V" << number << " " << "\n";
+          }
         }
       }
       break;
diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp
index 933acebe443..e0850a489ac 100644
--- a/src/goto-programs/xml_goto_trace.cpp
+++ b/src/goto-programs/xml_goto_trace.cpp
@@ -71,17 +71,33 @@ void convert(
     case goto_trace_stept::typet::ASSIGNMENT:
     case goto_trace_stept::typet::DECL:
       {
-        irep_idt identifier=step.lhs_object.get_identifier();
+        auto lhs_object=step.get_lhs_object();
+        irep_idt identifier=
+          lhs_object.has_value()?lhs_object->get_identifier():irep_idt();
         xmlt &xml_assignment=dest.new_element("assignment");
 
         if(xml_location.name!="")
           xml_assignment.new_element().swap(xml_location);
 
-        std::string value_string, type_string,
-                    full_lhs_string, full_lhs_value_string;
+        {
+          auto lhs_object=step.get_lhs_object();
+
+          const symbolt *symbol;
+
+          if(lhs_object.has_value() &&
+             !ns.lookup(lhs_object->get_identifier(), symbol))
+          {
+            std::string type_string=from_type(ns, symbol->name, symbol->type);
 
-        if(step.lhs_object_value.is_not_nil())
-          value_string=from_expr(ns, identifier, step.lhs_object_value);
+            xml_assignment.set_attribute("mode", id2string(symbol->mode));
+            xml_assignment.set_attribute("identifier", id2string(symbol->name));
+            xml_assignment.set_attribute("base_name", id2string(symbol->base_name));
+            xml_assignment.set_attribute("display_name", id2string(symbol->display_name()));
+            xml_assignment.new_element("type").data=type_string;
+          }
+        }
+
+        std::string full_lhs_string, full_lhs_value_string;
 
         if(step.full_lhs.is_not_nil())
           full_lhs_string=from_expr(ns, identifier, step.full_lhs);
@@ -90,43 +106,17 @@ void convert(
           full_lhs_value_string=
             from_expr(ns, identifier, step.full_lhs_value);
 
-        if(step.lhs_object_value.type().is_not_nil())
-          type_string=
-            from_type(ns, identifier, step.lhs_object_value.type());
-
-        const symbolt *symbol;
-        irep_idt base_name, display_name;
-
-        if(!ns.lookup(identifier, symbol))
-        {
-          base_name=symbol->base_name;
-          display_name=symbol->display_name();
-          if(type_string=="")
-            type_string=from_type(ns, identifier, symbol->type);
-
-          xml_assignment.set_attribute("mode", id2string(symbol->mode));
-        }
-
-        xml_assignment.new_element("type").data=type_string;
         xml_assignment.new_element("full_lhs").data=full_lhs_string;
         xml_assignment.new_element("full_lhs_value").data=full_lhs_value_string;
-        xml_assignment.new_element("value").data=value_string;
 
         xml_assignment.set_attribute_bool("hidden", step.hidden);
         xml_assignment.set_attribute("thread", std::to_string(step.thread_nr));
-        xml_assignment.set_attribute("identifier", id2string(identifier));
-        xml_assignment.set_attribute("base_name", id2string(base_name));
-        xml_assignment.set_attribute("display_name", id2string(display_name));
         xml_assignment.set_attribute("step_nr", std::to_string(step.step_nr));
 
         xml_assignment.set_attribute("assignment_type",
           step.assignment_type==
             goto_trace_stept::assignment_typet::ACTUAL_PARAMETER?
           "actual_parameter":"state");
-
-        if(step.lhs_object_value.is_not_nil())
-          xml_assignment.new_element("value_expression").
-            new_element(xml(step.lhs_object_value, ns));
       }
       break;
 
diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
index 2e0ec908a94..40523caaba3 100644
--- a/src/goto-symex/build_goto_trace.cpp
+++ b/src/goto-symex/build_goto_trace.cpp
@@ -295,16 +295,6 @@ void build_goto_trace(
       goto_trace_step.thread_nr = SSA_step.source.thread_nr;
       goto_trace_step.pc = SSA_step.source.pc;
       goto_trace_step.comment = SSA_step.comment;
-      if(SSA_step.ssa_lhs.is_not_nil())
-      {
-        goto_trace_step.lhs_object =
-          ssa_exprt(SSA_step.ssa_lhs.get_original_expr());
-      }
-      else
-      {
-        goto_trace_step.lhs_object.make_nil();
-      }
-
       goto_trace_step.type = SSA_step.type;
       goto_trace_step.hidden = SSA_step.hidden;
       goto_trace_step.format_string = SSA_step.format_string;
@@ -334,9 +324,6 @@ void build_goto_trace(
           prop_conv, ns, SSA_step.original_full_lhs, SSA_step.ssa_full_lhs);
       }
 
-      if(SSA_step.ssa_lhs.is_not_nil())
-        goto_trace_step.lhs_object_value = prop_conv.get(SSA_step.ssa_lhs);
-
       if(SSA_step.ssa_full_lhs.is_not_nil())
       {
         goto_trace_step.full_lhs_value = prop_conv.get(SSA_step.ssa_full_lhs);