goto_checkt: keep same-assertion for different expressions

Purging redundant assertions results in surprising user output as it
would seem that certain properties aren't being checked.

Author: tautschnig

regression/cbmc/Pointer_byte_extract5/test.desc

@@ -4,7 +4,7 @@ main.i
 ^EXIT=10$
 ^SIGNAL=0$
 array\.List dynamic object upper bound in p->List\[2\]: FAILURE
-\*\* 1 of 14 failed
+\*\* 1 of \d+ failed
 --
 ^warning: ignoring
 --

regression/cbmc/Undefined_Shift1/test.desc

@@ -4,11 +4,12 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*\] line 4 shift operand is negative in .*: SUCCESS$
+^\[.*\] line 5 shift operand is negative in .*: SUCCESS$
 ^\[.*\] line 7 shift distance too large in .*: FAILURE$
 ^\[.*\] line 15 shift distance is negative in .*: FAILURE$
 ^\[.*\] line 15 shift distance too large in .*: SUCCESS$
 ^\[.*\] line 20 shift operand is negative in .*: FAILURE$
-^\*\* 3 of 5 failed
+^\*\* 3 of 6 failed
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc/pointer-overflow3/no-simplify.desc

@@ -0,0 +1,16 @@
+CORE broken-smt-backend
+main.c
+--pointer-overflow-check --no-simplify
+^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside dynamic object bounds in p \+ \(signed (long (long )?)?int\)10: FAILURE
+^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside dynamic object bounds in p - \(signed (long (long )?)?int\)10: FAILURE
+^\[main.pointer_arithmetic.\d+\] line 10 pointer arithmetic: pointer outside object bounds in arr \+ \(signed (long (long )?)?int\)10: FAILURE
+^\[main.pointer_arithmetic.\d+\] line 11 pointer arithmetic: pointer outside object bounds in arr - \(signed (long (long )?)?int\)10: FAILURE
+^\*\* 4 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+Invariant check failed
+--
+Uses --no-simplify to avoid removing repeated ASSERT FALSE statements.

regression/cbmc/pointer-overflow3/test.desc

@@ -1,6 +1,6 @@
-CORE broken-smt-backend
+CORE
 main.c
---pointer-overflow-check --no-simplify
+--pointer-overflow-check
 ^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside dynamic object bounds in p \+ \(signed (long (long )?)?int\)10: FAILURE
 ^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside dynamic object bounds in p - \(signed (long (long )?)?int\)10: FAILURE
 ^\[main.pointer_arithmetic.\d+\] line 10 pointer arithmetic: pointer outside object bounds in arr \+ \(signed (long (long )?)?int\)10: FAILURE
@@ -12,5 +12,3 @@ main.c
 --
 ^warning: ignoring
 Invariant check failed
---
-Uses --no-simplify to avoid removing repeated ASSERT FALSE statements.

src/analyses/goto_check.cpp

@@ -242,7 +242,7 @@ class goto_checkt
     const guardt &guard);
 
   goto_programt new_code;
-  typedef std::set<exprt> assertionst;
+  typedef std::set<std::pair<exprt, exprt>> assertionst;
   assertionst assertions;
 
   /// Remove all assertions containing the symbol in \p lhs as well as all
@@ -333,8 +333,12 @@ void goto_checkt::invalidate(const exprt &lhs)
 
     for(auto it = assertions.begin(); it != assertions.end();)
     {
-      if(has_symbol(*it, find_symbols_set) || has_subexpr(*it, ID_dereference))
+      if(
+        has_symbol(it->second, find_symbols_set) ||
+        has_subexpr(it->second, ID_dereference))
+      {
         it = assertions.erase(it);
+      }
       else
         ++it;
     }
@@ -1545,7 +1549,7 @@ void goto_checkt::add_guarded_property(
       ? std::move(simplified_expr)
       : implies_exprt{guard.as_expr(), std::move(simplified_expr)};
 
-  if(assertions.insert(guarded_expr).second)
+  if(assertions.insert(std::make_pair(src_expr, guarded_expr)).second)
   {
     auto t = new_code.add(
       enable_assert_to_assume ? goto_programt::make_assumption(