diff --git a/src/goto-symex/goto_state.cpp b/src/goto-symex/goto_state.cpp
index dd6214f9351..eb1e2f001cb 100644
--- a/src/goto-symex/goto_state.cpp
+++ b/src/goto-symex/goto_state.cpp
@@ -46,11 +46,72 @@ void goto_statet::apply_condition(
 {
   if(condition.id() == ID_and)
   {
+    // A == B && C == D && E == F ...
+    // -->
+    // Apply each condition individually
     for(const auto &op : condition.operands())
       apply_condition(op, previous_state, ns);
   }
+  else if(condition.id() == ID_notequal &&
+          to_notequal_expr(condition).lhs().type() == bool_typet())
+  {
+    // A != (true|false)
+    // -->
+    // A == (false|true)
+    exprt lhs = to_notequal_expr(condition).lhs();
+    exprt rhs = to_notequal_expr(condition).rhs();
+    if(is_ssa_expr(rhs))
+      std::swap(lhs, rhs);
+
+    if(rhs.is_true())
+      apply_condition(equal_exprt(lhs, false_exprt()), previous_state, ns);
+    else if(rhs.is_false())
+      apply_condition(equal_exprt(lhs, true_exprt()), previous_state, ns);
+  }
+  else if(condition.id() == ID_not &&
+          to_not_expr(condition).op().id() == ID_notequal)
+  {
+    // !(A != B)
+    // -->
+    // A == B
+    const auto &notequal_expr = to_notequal_expr(to_not_expr(condition).op());
+    apply_condition(
+      equal_exprt(notequal_expr.lhs(), notequal_expr.rhs()),
+      previous_state,
+      ns);
+  }
+  else if(condition.id() == ID_not &&
+          to_not_expr(condition).op().id() == ID_equal)
+  {
+    // !(A == B)
+    // -->
+    // A != B
+    const auto &equal_expr = to_equal_expr(to_not_expr(condition).op());
+    apply_condition(
+      notequal_exprt(equal_expr.lhs(), equal_expr.rhs()),
+      previous_state,
+      ns);
+  }
+  else if(condition.id() == ID_not)
+  {
+    // !A
+    // -->
+    // A == false
+    apply_condition(
+      equal_exprt(to_not_expr(condition).op(), false_exprt()),
+      previous_state,
+      ns);
+  }
+  else if(condition.id() == ID_symbol && condition.type() == bool_typet())
+  {
+    // A
+    // -->
+    // A == true
+    apply_condition(equal_exprt(condition, true_exprt()), previous_state, ns);
+  }
   else if(condition.id() == ID_equal)
   {
+    // Base case: try to apply a single equality constraint
     exprt lhs = to_equal_expr(condition).lhs();
     exprt rhs = to_equal_expr(condition).rhs();
     if(is_ssa_expr(rhs))
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index 6a1c5ab50ce..6ba853838cd 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -55,21 +55,12 @@ void goto_symext::apply_goto_condition(
 
   jump_taken_state.apply_condition(new_guard, current_state, ns);
 
-  // Try to find a negative condition that implies an equality constraint on
-  // the branch-not-taken path.
   // Could use not_exprt + simplify, but let's avoid paying that cost on quite
   // a hot path:
-  if(new_guard.id() == ID_not)
-    jump_not_taken_state.apply_condition(
-      to_not_expr(new_guard).op(), current_state, ns);
-  else if(new_guard.id() == ID_notequal)
-  {
-    auto &not_equal_expr = to_notequal_expr(new_guard);
-    jump_not_taken_state.apply_condition(
-      equal_exprt(not_equal_expr.lhs(), not_equal_expr.rhs()),
-      current_state,
-      ns);
-  }
+  exprt negated_new_guard = new_guard.id() ==
+    ID_not ? to_not_expr(new_guard).op() : not_exprt(new_guard);
+  jump_not_taken_state.apply_condition(
+    negated_new_guard, current_state, ns);
 }
 
 /// Try to evaluate a simple pointer comparison.