Symex guards: avoid unnecessary duplicate negation

We negated the right-hand side assigned to a guard symbol just so as to
then negate the use of the guard symbol. Remove this duplicate negation.

jbmc/regression/jbmc/symex_complexity/process.desc

@@ -1,7 +1,7 @@
 CORE
 ComplexClass
---function ComplexClass.process --symex-complexity-limit 2 --verbosity 9 --unwind 10 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
-^\[symex-complexity\] Branch considered too complex|\[symex-complexity\] Trying to enter blacklisted loop|\[symex-complexity\] Loop operations considered too complex$
+--function ComplexClass.process --symex-complexity-limit 1 --verbosity 9 --unwind 10 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
+^\[symex-complexity\] Branch considered too complex|\[symex-complexity\] Trying to enter blacklisted loop|\[symex-complexity\] Loop operations considered too complex
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
@@ -15,4 +15,4 @@ Loop blacklisting.
 
 When these don't work this test may take some time to run (and then fail), which is hard to
 restrict because this is the problem this feature is meant to solve. If this test is running
-slowly, high chance something has gone wrong.
+slowly, high chance something has gone wrong.

regression/cbmc/fault_localization-all_properties2/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE paths-lifo-expected-failure broken-smt-backend no-new-smt
 main.c
 --localize-faults
 ^EXIT=10$
@@ -7,5 +7,3 @@ line 9 function main$
 ^VERIFICATION FAILED$
 --
 --
-CBMC wrongly reports line 7 as the faulty statement when instead it should be
-line 9.

regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc

@@ -13,26 +13,26 @@ test::1::unconditionally_reachable_7[^\s]+ = 7$
 test::1::unconditionally_reachable_8[^\s]+ = 7$
 test::1::unconditionally_reachable_9[^\s]+ = 7$
 test::1::unconditionally_reachable_10[^\s]+ = 7$
-test::1::possibly_reachable_1[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_1[^\s]+\)$
-test::1::possibly_reachable_2[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_2[^\s]+\)$
-test::1::possibly_reachable_3[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_3[^\s]+\)$
-test::1::possibly_reachable_4[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_4[^\s]+\)$
-test::1::possibly_reachable_5[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_5[^\s]+\)$
-test::1::possibly_reachable_6[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_6[^\s]+\)$
-test::1::possibly_reachable_7[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_7[^\s]+\)$
+test::1::possibly_reachable_1[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_1[^\s]+ : 7\)$
+test::1::possibly_reachable_2[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_2[^\s]+ : 7\)$
+test::1::possibly_reachable_3[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_3[^\s]+ : 7\)$
+test::1::possibly_reachable_4[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_4[^\s]+ : 7\)$
+test::1::possibly_reachable_5[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_5[^\s]+ : 7\)$
+test::1::possibly_reachable_6[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_6[^\s]+ : 7\)$
+test::1::possibly_reachable_7[^\s]+ = \(goto_symex::\\guard[^\s]+ \? test::1::possibly_reachable_7[^\s]+ : 7\)$
 --
-test::1::unconditionally_reachable_1[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_1[^\s]+\)$
-test::1::unconditionally_reachable_2[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_2[^\s]+\)$
-test::1::unconditionally_reachable_3[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_3[^\s]+\)$
-test::1::unconditionally_reachable_4[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_4[^\s]+\)$
-test::1::unconditionally_reachable_5[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_5[^\s]+\)$
-test::1::unconditionally_reachable_6[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_6[^\s]+\)$
-test::1::unconditionally_reachable_7[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_7[^\s]+\)$
-test::1::unconditionally_reachable_8[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_8[^\s]+\)$
-test::1::unconditionally_reachable_9[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_9[^\s]+\)$
-test::1::unconditionally_reachable_10[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_10[^\s]+\)$
-test::1::unconditionally_reachable_11[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_11[^\s]+\)$
-test::1::unconditionally_reachable_12[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_12[^\s]+\)$
+test::1::unconditionally_reachable_1[^\s]+ = .+ \?
+test::1::unconditionally_reachable_2[^\s]+ = .+ \?
+test::1::unconditionally_reachable_3[^\s]+ = .+ \?
+test::1::unconditionally_reachable_4[^\s]+ = .+ \?
+test::1::unconditionally_reachable_5[^\s]+ = .+ \?
+test::1::unconditionally_reachable_6[^\s]+ = .+ \?
+test::1::unconditionally_reachable_7[^\s]+ = .+ \?
+test::1::unconditionally_reachable_8[^\s]+ = .+ \?
+test::1::unconditionally_reachable_9[^\s]+ = .+ \?
+test::1::unconditionally_reachable_10[^\s]+ = .+ \?
+test::1::unconditionally_reachable_11[^\s]+ = .+ \?
+test::1::unconditionally_reachable_12[^\s]+ = .+ \?
 test::1::unreachable_1[^\s]+ = 7$
 test::1::unreachable_2[^\s]+ = 7$
 test::1::unreachable_3[^\s]+ = 7$

regression/cbmc/unreachable-goto2/test-vccs.desc

@@ -2,7 +2,7 @@ CORE paths-lifo-expected-failure
 test.c
 --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
-^\{1\} goto_symex::\\guard#1$
+^\{1\} ¬goto_symex::\\guard#1$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/solver-hardness/guards/test.desc

@@ -5,7 +5,7 @@ main.c
 ^SIGNAL=0$
 ^\[main.assertion.1\] line 12 should fail: FAILURE$
 ^VERIFICATION FAILED$
-\{"GOTO":"GOTO \d+","GOTO_ID":\d+,"SAT_hardness":\{"ClauseSet":\[\d+.*\],"Clauses":[1-9]\d*,"Literals":[1-9]\d*,"Variables":[1-9]\d*},"SSA_expr":"goto_symex::\\\\guard#1 ∧ goto_symex::\\\\guard#2","Source":\{"file":"main.c","function":"main","line":"\d+","workingDirectory":".*"\}\}
+\{"GOTO":"GOTO \d+","GOTO_ID":\d+,"SAT_hardness":\{"ClauseSet":\[\d+.*\],"Clauses":[1-9]\d*,"Literals":[1-9]\d*,"Variables":[1-9]\d*},"SSA_expr":"¬goto_symex::\\\\guard#1 ∧ ¬goto_symex::\\\\guard#2","Source":\{"file":"main.c","function":"main","line":"\d+","workingDirectory":".*"\}\}
 --
 ^warning: ignoring
 \{"GOTO":"GOTO \d+","GOTO_ID":\d+,"SAT_hardness":\{"ClauseSet":\[\d+.*\],"Clauses":[1-9]\d*,"Literals":[1-9]\d*,"Variables":[1-9]\d*},"SSA_expr":"true","Source":\{"file":"main.c","function":"main","line":"\d+","workingDirectory":".*"\}\}

src/goto-symex/symex_goto.cpp

@@ -490,12 +490,11 @@ void goto_symext::symex_goto(statet &state)
     {
       symbol_exprt guard_symbol_expr =
         symbol_exprt(statet::guard_identifier(), bool_typet());
-      exprt new_rhs = boolean_negate(new_guard);
 
       ssa_exprt new_lhs =
         state.rename_ssa<L1>(ssa_exprt{guard_symbol_expr}, ns).get();
       new_lhs =
-        state.assignment(std::move(new_lhs), new_rhs, ns, true, false).get();
+        state.assignment(std::move(new_lhs), new_guard, ns, true, false).get();
 
       guardt guard{true_exprt{}, guard_manager};
 
@@ -509,12 +508,14 @@ void goto_symext::symex_goto(statet &state)
 
       target.assignment(
         guard.as_expr(),
-        new_lhs, new_lhs, guard_symbol_expr,
-        new_rhs,
+        new_lhs,
+        new_lhs,
+        guard_symbol_expr,
+        new_guard,
         original_source,
         symex_targett::assignment_typet::GUARD);
 
-      guard_expr = state.rename(boolean_negate(guard_symbol_expr), ns).get();
+      guard_expr = state.rename(guard_symbol_expr, ns).get();
     }
 
     if(state.has_saved_jump_target)