diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 266de986ac4..72f14f16115 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -2824,6 +2824,10 @@ simplify_exprt::simplify_node_preorder(const exprt &expr)
   {
     result = simplify_unary_pointer_predicate_preorder(to_unary_expr(expr));
   }
+  else if(expr.id() == ID_not)
+  {
+    result = simplify_not_preorder(to_not_expr(expr));
+  }
   else if(expr.has_operands())
   {
     std::optional<exprt::operandst> new_operands;
diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp
index 569c91ef837..a62fedfea0d 100644
--- a/src/util/simplify_expr_boolean.cpp
+++ b/src/util/simplify_expr_boolean.cpp
@@ -377,3 +377,66 @@ simplify_exprt::resultt<> simplify_exprt::simplify_not(const not_exprt &expr)
 
   return unchanged(expr);
 }
+
+simplify_exprt::resultt<>
+simplify_exprt::simplify_not_preorder(const not_exprt &expr)
+{
+  const exprt &op = expr.op();
+
+  if(!expr.is_boolean() || !op.is_boolean())
+  {
+    return unchanged(expr);
+  }
+
+  if(op.id() == ID_not) // (not not a) == a
+  {
+    return changed(simplify_rec(to_not_expr(op).op()));
+  }
+  else if(op.is_false())
+  {
+    return true_exprt{};
+  }
+  else if(op.is_true())
+  {
+    return false_exprt{};
+  }
+  else if(op.id() == ID_and || op.id() == ID_or)
+  {
+    exprt tmp = op;
+
+    Forall_operands(it, tmp)
+    {
+      *it = boolean_negate(*it);
+    }
+
+    tmp.id(tmp.id() == ID_and ? ID_or : ID_and);
+
+    return changed(simplify_rec(tmp));
+  }
+  else if(op.id() == ID_notequal) // !(a!=b) <-> a==b
+  {
+    exprt tmp = op;
+    tmp.id(ID_equal);
+    return changed(simplify_rec(tmp));
+  }
+  else if(op.id() == ID_exists) // !(exists: a) <-> forall: not a
+  {
+    auto const &op_as_exists = to_exists_expr(op);
+    return changed(simplify_rec(
+      forall_exprt{op_as_exists.symbol(), not_exprt{op_as_exists.where()}}));
+  }
+  else if(op.id() == ID_forall) // !(forall: a) <-> exists: not a
+  {
+    auto const &op_as_forall = to_forall_expr(op);
+    return changed(simplify_rec(
+      exists_exprt{op_as_forall.symbol(), not_exprt{op_as_forall.where()}}));
+  }
+
+  auto op_result = simplify_rec(op);
+  if(!op_result.has_changed())
+    return unchanged(expr);
+
+  not_exprt tmp = expr;
+  tmp.op() = std::move(op_result.expr);
+  return std::move(tmp);
+}
diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h
index 2e7341be03b..6a1a9721be5 100644
--- a/src/util/simplify_expr_class.h
+++ b/src/util/simplify_expr_class.h
@@ -167,6 +167,7 @@ class simplify_exprt
   [[nodiscard]] resultt<> simplify_if(const if_exprt &);
   [[nodiscard]] resultt<> simplify_bitnot(const bitnot_exprt &);
   [[nodiscard]] resultt<> simplify_not(const not_exprt &);
+  [[nodiscard]] resultt<> simplify_not_preorder(const not_exprt &expr);
   [[nodiscard]] resultt<> simplify_boolean(const exprt &);
   [[nodiscard]] resultt<> simplify_inequality(const binary_relation_exprt &);
   [[nodiscard]] resultt<>