goto-symex: assumed pointer equalities must update value set

regression/cbmc/Pointer_Assume2/main.c

@@ -0,0 +1,27 @@
+int main()
+{
+  int *r;
+  int *a;
+#if 1
+  _Bool tmp_if_expr;
+  if(r == 0)
+  {
+    tmp_if_expr = 0;
+  }
+  else
+  {
+    r = __CPROVER_allocate(sizeof(int), 0);
+    tmp_if_expr = 1;
+  }
+
+  __CPROVER_assume(tmp_if_expr);
+#else
+  // this works, because we constant-propagate r as an address-of expression
+  __CPROVER_assume(r != 0);
+  r = __CPROVER_allocate(sizeof(int), 0);
+#endif
+  __CPROVER_assume(r != 0);
+  __CPROVER_assume(r == a);
+  __CPROVER_assert(r == a, " r == a before");
+  __CPROVER_assert(*r == *a, "*r == *a before");
+}

regression/cbmc/Pointer_Assume2/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

src/goto-symex/goto_state.cpp

@@ -92,19 +92,20 @@
     if(is_ssa_expr(rhs))
       std::swap(lhs, rhs);
 
-    if(is_ssa_expr(lhs) && goto_symex_can_forward_propagatet(ns)(rhs))
+    if(is_ssa_expr(lhs))
     {
       const ssa_exprt &ssa_lhs = to_ssa_expr(lhs);
       INVARIANT(
         !ssa_lhs.get_level_2().empty(),
         "apply_condition operand should be L2 renamed");
+      const ssa_exprt l1_lhs = remove_level_2(ssa_lhs);
 
       if(
-        previous_state.threads.size() == 1 ||
-        previous_state.write_is_shared(ssa_lhs, ns) !=
-          goto_symex_statet::write_is_shared_resultt::SHARED)
+        goto_symex_can_forward_propagatet(ns)(rhs) &&
+        (previous_state.threads.size() == 1 ||
+         previous_state.write_is_shared(ssa_lhs, ns) !=
+           goto_symex_statet::write_is_shared_resultt::SHARED))
       {
-        const ssa_exprt l1_lhs = remove_level_2(ssa_lhs);
         const irep_idt &l1_identifier = l1_lhs.get_identifier();
 
         level2.increase_generation(
@@ -118,6 +119,20 @@
 
         value_set.assign(l1_lhs, rhs, ns, true, false);
       }
+      else if(is_ssa_expr(rhs))
+      {
+        const ssa_exprt &ssa_rhs = to_ssa_expr(rhs);
+        INVARIANT(
+          !ssa_rhs.get_level_2().empty(),
+          "apply_condition operand should be L2 renamed");
+        const ssa_exprt l1_rhs = remove_level_2(ssa_rhs);
+
+        // We have a condition a == b. Make both a's and b's value sets the
+        // union of their previous value sets (the last "true" argument makes
+        // sure we add rather than replace value sets).
+        value_set.assign(l1_lhs, l1_rhs, ns, true, true);
+        value_set.assign(l1_rhs, l1_lhs, ns, true, true);
+      }
     }
   }
   else if(