diff --git a/regression/cbmc/atomic_section_seq1/test.desc b/regression/cbmc/atomic_section_seq1/test.desc
index 6de79559914..54b42c855cc 100644
--- a/regression/cbmc/atomic_section_seq1/test.desc
+++ b/regression/cbmc/atomic_section_seq1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=10$
@@ -6,3 +6,6 @@ main.c
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
+--
+This test involves empty structs, which the SMT2 back-end does not currently
+support.
diff --git a/regression/cbmc/trace-values/trace-values.c b/regression/cbmc/trace-values/trace-values.c
index 0b828f24e42..d54f6d64480 100644
--- a/regression/cbmc/trace-values/trace-values.c
+++ b/regression/cbmc/trace-values/trace-values.c
@@ -16,6 +16,7 @@ int main()
   int *q=&my_nested[1].f;
   int *null=0;
   int *junk;
+  struct S s;
 
   global_var=1;
   static_var=2;
@@ -34,6 +35,9 @@ int main()
   // assign entire struct
   my_nested[1]=my_nested[0];
 
+  // struct member
+  s.f = 42;
+
   // get a trace
   __CPROVER_assert(0, "");
 }
diff --git a/regression/cbmc/trace-values/trace-values.desc b/regression/cbmc/trace-values/trace-values.desc
index 67ae31afe4d..cfac2618a72 100644
--- a/regression/cbmc/trace-values/trace-values.desc
+++ b/regression/cbmc/trace-values/trace-values.desc
@@ -3,6 +3,7 @@ trace-values.c
 --trace
 ^EXIT=10$
 ^SIGNAL=0$
+^  s=\{ \.f=-?\d+, \.array=\{ -?\d+, -?\d+, -?\d+ \} \} \(\{ [01 ]+, \{ [01 ]+, [01 ]+, [01 ]+ \} \}\)$
 ^  global_var=1 .*$
 ^  static_var=2 .*$
 ^  local_var=3 .*$
@@ -12,6 +13,7 @@ trace-values.c
 ^  dynamic_object1\[1.*\]=8 .*$
 ^  my_nested\[1.*\](=\{ )?.f=0[ ,]
 ^  my_nested\[1.*\](=\{ .f=0, )?.array=\{ 0, 4, 0 \}
+^  s\.f=42 \([0 ]+ 00101010\)$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index 02afd8fead1..8c97da8e1b1 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -389,6 +389,8 @@ void symex_target_equationt::convert_decls(
       // The result is not used, these have no impact on
       // the satisfiability of the formula.
       decision_procedure.handle(step.cond_expr);
+      decision_procedure.handle(
+        equal_exprt{step.ssa_full_lhs, step.ssa_full_lhs});
       step.converted = true;
       with_solver_hardness(
         decision_procedure, hardness_register_ssa(step_index, step));