diff --git a/jbmc/regression/jbmc/symex_complexity/process.desc b/jbmc/regression/jbmc/symex_complexity/process.desc
index 4a915b7fce1..da27a208408 100644
--- a/jbmc/regression/jbmc/symex_complexity/process.desc
+++ b/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.
\ No newline at end of file
+slowly, high chance something has gone wrong.
diff --git a/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc b/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc
index d8f0a0e31c7..5be6851caf3 100644
--- a/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc
+++ b/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$
diff --git a/regression/cbmc/unreachable-goto2/test-vccs.desc b/regression/cbmc/unreachable-goto2/test-vccs.desc
index 75a82c3b065..f976984958e 100644
--- a/regression/cbmc/unreachable-goto2/test-vccs.desc
+++ b/regression/cbmc/unreachable-goto2/test-vccs.desc
@@ -2,7 +2,7 @@ CORE paths-lifo-expected-failure
 test.c
 --show-vcc --verbosity 8
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
-^\{1\} goto_symex::\\guard#1$
+^\{1\} ¬goto_symex::\\guard#1$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/solver-hardness/guards/test.desc b/regression/solver-hardness/guards/test.desc
index 6eac38ac4c8..a4b68755f03 100644
--- a/regression/solver-hardness/guards/test.desc
+++ b/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":".*"\}\}
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index 1745a8e445e..5a45e7dddfd 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -328,12 +328,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};
 
@@ -347,12 +346,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)