diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp
index 281cc7f664d..0847ce7ad47 100644
--- a/src/analyses/custom_bitvector_analysis.cpp
+++ b/src/analyses/custom_bitvector_analysis.cpp
@@ -11,8 +11,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "custom_bitvector_analysis.h"
 
-#include <util/xml_expr.h>
+#include <util/expr_util.h>
 #include <util/simplify_expr.h>
+#include <util/xml_expr.h>
 
 #include <langapi/language_util.h>
 
@@ -527,7 +528,7 @@ void custom_bitvector_domaint::transform(
       // Comparing iterators is safe as the target must be within the same list
       // of instructions because this is a GOTO.
       if(to!=from->get_target())
-        guard.make_not();
+        guard = boolean_negate(guard);
 
       exprt result=eval(guard, cba);
       exprt result2=simplify_expr(result, ns);
diff --git a/src/analyses/flow_insensitive_analysis.cpp b/src/analyses/flow_insensitive_analysis.cpp
index 403b8777fc2..a6e045f31c6 100644
--- a/src/analyses/flow_insensitive_analysis.cpp
+++ b/src/analyses/flow_insensitive_analysis.cpp
@@ -14,8 +14,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <cassert>
 
-#include <util/std_expr.h>
+#include <util/expr_util.h>
 #include <util/std_code.h>
+#include <util/std_expr.h>
 
 exprt flow_insensitive_abstract_domain_baset::get_guard(
   locationt from,
@@ -28,11 +29,7 @@ exprt flow_insensitive_abstract_domain_baset::get_guard(
   next++;
 
   if(next==to)
-  {
-    exprt tmp(from->guard);
-    tmp.make_not();
-    return tmp;
-  }
+    return boolean_negate(from->guard);
 
   return from->guard;
 }
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index ce6f07672a3..8e32c7064b6 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -861,11 +861,9 @@ void goto_checkt::nan_check(
   else
     UNREACHABLE;
 
-  isnan.make_not();
-
   add_guarded_claim(
-    isnan,
-    "NaN on "+expr.id_string(),
+    boolean_negate(isnan),
+    "NaN on " + expr.id_string(),
     "NaN",
     expr.find_source_location(),
     expr,
diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp
index f775860ac32..835bcd9b359 100644
--- a/src/analyses/invariant_set.cpp
+++ b/src/analyses/invariant_set.cpp
@@ -13,16 +13,17 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <iostream>
 
+#include <util/arith_tools.h>
 #include <util/base_exceptions.h>
-#include <util/symbol_table.h>
+#include <util/base_type.h>
+#include <util/c_types.h>
+#include <util/expr_util.h>
 #include <util/namespace.h>
-#include <util/arith_tools.h>
-#include <util/std_expr.h>
 #include <util/simplify_expr.h>
-#include <util/base_type.h>
+#include <util/std_expr.h>
 #include <util/std_types.h>
+#include <util/symbol_table.h>
 
-#include <util/c_types.h>
 #include <langapi/language_util.h>
 
 void inv_object_storet::output(std::ostream &out) const
@@ -758,10 +759,9 @@ void invariant_sett::nnf(exprt &expr, bool negate)
       nnf(tmp, !negate);
       expr.swap(tmp);
     }
-    else
+    else if(negate)
     {
-      if(negate)
-        expr.make_not();
+      expr = boolean_negate(expr);
     }
   }
   else if(expr.id()==ID_le)
@@ -812,10 +812,9 @@ void invariant_sett::nnf(exprt &expr, bool negate)
     if(negate)
       expr.id(ID_equal);
   }
-  else
+  else if(negate)
   {
-    if(negate)
-      expr.make_not();
+    expr = boolean_negate(expr);
   }
 }
 
diff --git a/src/analyses/invariant_set_domain.cpp b/src/analyses/invariant_set_domain.cpp
index 416f57a945f..dce6d70401d 100644
--- a/src/analyses/invariant_set_domain.cpp
+++ b/src/analyses/invariant_set_domain.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "invariant_set_domain.h"
 
+#include <util/expr_util.h>
 #include <util/simplify_expr.h>
 
 void invariant_set_domaint::transform(
@@ -32,7 +33,7 @@ void invariant_set_domaint::transform(
       goto_programt::const_targett next=from_l;
       next++;
       if(next==to_l)
-        tmp.make_not();
+        tmp = boolean_negate(from_l->guard);
 
       simplify(tmp, ns);
       invariant_set.strengthen(tmp);
diff --git a/src/analyses/static_analysis.cpp b/src/analyses/static_analysis.cpp
index 10400301709..5b3aad1d8af 100644
--- a/src/analyses/static_analysis.cpp
+++ b/src/analyses/static_analysis.cpp
@@ -15,8 +15,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cassert>
 #include <memory>
 
-#include <util/std_expr.h>
+#include <util/expr_util.h>
 #include <util/std_code.h>
+#include <util/std_expr.h>
 
 #include "is_threaded.h"
 
@@ -31,11 +32,7 @@ exprt static_analysis_baset::get_guard(
   next++;
 
   if(next==to)
-  {
-    exprt tmp(from->guard);
-    tmp.make_not();
-    return tmp;
-  }
+    return boolean_negate(from->guard);
 
   return from->guard;
 }
diff --git a/src/goto-instrument/branch.cpp b/src/goto-instrument/branch.cpp
index 913bf526b31..378a64d0b4e 100644
--- a/src/goto-instrument/branch.cpp
+++ b/src/goto-instrument/branch.cpp
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "branch.h"
 
 #include <util/cprover_prefix.h>
+#include <util/expr_util.h>
 #include <util/prefix.h>
 
 #include "function.h"
@@ -48,7 +49,7 @@ void branch(
          !i_it->guard.is_constant())
       {
         // negate condition
-        i_it->guard.make_not();
+        i_it->guard = boolean_negate(i_it->guard);
 
         goto_programt::targett t1=body.insert_after(i_it);
         t1->make_function_call(
diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp
index 74aa57557c1..b6078d043a0 100644
--- a/src/goto-instrument/code_contracts.cpp
+++ b/src/goto-instrument/code_contracts.cpp
@@ -13,6 +13,7 @@ Date: February 2016
 
 #include "code_contracts.h"
 
+#include <util/expr_util.h>
 #include <util/fresh_symbol.h>
 #include <util/replace_symbol.h>
 
@@ -158,7 +159,7 @@ static void check_apply_invariants(
   if(loop_head->is_goto())
     loop_end->guard.make_false();
   else
-    loop_end->guard.make_not();
+    loop_end->guard = boolean_negate(loop_end->guard);
 }
 
 void code_contractst::apply_contract(
diff --git a/src/goto-instrument/cover_instrument_mcdc.cpp b/src/goto-instrument/cover_instrument_mcdc.cpp
index e1b1ab7a52f..78bb86b8341 100644
--- a/src/goto-instrument/cover_instrument_mcdc.cpp
+++ b/src/goto-instrument/cover_instrument_mcdc.cpp
@@ -11,6 +11,8 @@ Author: Daniel Kroening
 
 #include "cover_instrument.h"
 
+#include <util/expr_util.h>
+
 #include <langapi/language_util.h>
 
 #include <algorithm>
@@ -73,7 +75,7 @@ void collect_mcdc_controlling_rec(
           new_conditions.push_back(conjunction(o));
           result.insert(conjunction(new_conditions));
 
-          o[i].make_not();
+          o[i] = boolean_negate(op);
           new_conditions.back() = conjunction(o);
           result.insert(conjunction(new_conditions));
         }
@@ -279,25 +281,24 @@ std::set<signed> sign_of_expr(const exprt &e, const exprt &E)
   // In the general case, we analyze each operand of ''E''.
   std::vector<exprt> ops;
   collect_operands(E, ops);
-  for(auto &x : ops)
+  for(const auto &x : ops)
   {
-    exprt y(x);
-    if(y == e)
+    if(x == e)
       signs.insert(+1);
-    else if(y.id() == ID_not)
+    else if(x.id() == ID_not)
     {
-      y.make_not();
-      if(y == e)
+      const exprt &x_op = to_not_expr(x).op();
+      if(x_op == e)
         signs.insert(-1);
-      if(!is_condition(y))
+      if(!is_condition(x_op))
       {
-        std::set<signed> re = sign_of_expr(e, y);
+        std::set<signed> re = sign_of_expr(e, x_op);
         signs.insert(re.begin(), re.end());
       }
     }
-    else if(!is_condition(y))
+    else if(!is_condition(x))
     {
-      std::set<signed> re = sign_of_expr(e, y);
+      std::set<signed> re = sign_of_expr(e, x);
       signs.insert(re.begin(), re.end());
     }
   }
@@ -420,9 +421,7 @@ bool eval_expr(const std::map<exprt, signed> &atomic_exprs, const exprt &src)
   // src is NOT
   else if(src.id() == ID_not)
   {
-    exprt no_op(src);
-    no_op.make_not();
-    return !eval_expr(atomic_exprs, no_op);
+    return !eval_expr(atomic_exprs, to_not_expr(src).op());
   }
   else // if(is_condition(src))
   {
diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp
index a7ef29eb16d..c206047de81 100644
--- a/src/goto-instrument/unwind.cpp
+++ b/src/goto-instrument/unwind.cpp
@@ -16,8 +16,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <iostream>
 #endif
 
+#include <util/expr_util.h>
 #include <util/std_expr.h>
 #include <util/string_utils.h>
+
 #include <goto-programs/goto_functions.h>
 
 #include "loop_utils.h"
@@ -127,8 +129,7 @@ void goto_unwindt::unwind(
 
     if(!t->guard.is_true()) // cond in backedge
     {
-      exit_cond=t->guard;
-      exit_cond.make_not();
+      exit_cond = boolean_negate(t->guard);
     }
     else if(loop_head->is_goto())
     {
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index 4cf08cabf27..5a4bf829d56 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -980,8 +980,7 @@ void goto_convertt::convert_for(
 
   // v: if(!c) goto z;
   v->make_goto(z);
-  v->guard=cond;
-  v->guard.make_not();
+  v->guard = boolean_negate(cond);
   v->source_location=cond.source_location();
 
   // do the w label
diff --git a/src/goto-programs/goto_convert_function_call.cpp b/src/goto-programs/goto_convert_function_call.cpp
index 82f46145b4d..0c8e5309b68 100644
--- a/src/goto-programs/goto_convert_function_call.cpp
+++ b/src/goto-programs/goto_convert_function_call.cpp
@@ -12,10 +12,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "goto_convert_class.h"
 
 
-#include <util/replace_expr.h>
-#include <util/source_location.h>
 #include <util/cprover_prefix.h>
+#include <util/expr_util.h>
 #include <util/prefix.h>
+#include <util/replace_expr.h>
+#include <util/source_location.h>
 #include <util/std_expr.h>
 
 #include <util/c_types.h>
@@ -135,8 +136,7 @@ void goto_convertt::do_function_call_if(
 
   // v: if(!c) goto y;
   v->make_goto(y);
-  v->guard=function.cond();
-  v->guard.make_not();
+  v->guard = boolean_negate(function.cond());
   v->source_location=function.cond().source_location();
 
   // w: f();
diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp
index 4e1bf9a7208..e21948b84fd 100644
--- a/src/goto-programs/string_abstraction.cpp
+++ b/src/goto-programs/string_abstraction.cpp
@@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/exception_utils.h>
+#include <util/expr_util.h>
 #include <util/pointer_predicates.h>
 #include <util/type_eq.h>
 
@@ -1273,8 +1274,7 @@ goto_programt::targett string_abstractiont::value_assignments_if(
 
   goto_else->function=target->function;
   goto_else->source_location=target->source_location;
-  goto_else->make_goto(else_target, rhs.cond());
-  goto_else->guard.make_not();
+  goto_else->make_goto(else_target, boolean_negate(rhs.cond()));
 
   goto_out->function=target->function;
   goto_out->source_location=target->source_location;
diff --git a/src/goto-symex/slice_by_trace.cpp b/src/goto-symex/slice_by_trace.cpp
index 6078b0fb7f8..716fb85b336 100644
--- a/src/goto-symex/slice_by_trace.cpp
+++ b/src/goto-symex/slice_by_trace.cpp
@@ -88,14 +88,12 @@ void symex_slice_by_tracet::slice_by_trace(
 
     if(g_copy.id()==ID_symbol || g_copy.id() == ID_not)
     {
-      g_copy.make_not();
-      simplify(g_copy, ns);
+      g_copy = simplify_expr(boolean_negate(g_copy), ns);
       implications.insert(g_copy);
     }
     else if(g_copy.id()==ID_and)
     {
-      exprt copy_last(g_copy.operands().back());
-      copy_last.make_not();
+      exprt copy_last = boolean_negate(g_copy.operands().back());
       simplify(copy_last, ns);
       implications.insert(copy_last);
     }
@@ -408,8 +406,7 @@ void symex_slice_by_tracet::slice_SSA_steps(
 
     if((guard.id()==ID_symbol) || (guard.id() == ID_not))
     {
-      guard.make_not();
-      simplify(guard, ns);
+      guard = simplify_expr(boolean_negate(guard), ns);
 
       if(implications.count(guard)!=0)
       {
@@ -426,8 +423,7 @@ void symex_slice_by_tracet::slice_SSA_steps(
     {
       Forall_operands(git, guard)
       {
-        exprt neg_expr=*git;
-        neg_expr.make_not();
+        exprt neg_expr = boolean_negate(*git);
         simplify(neg_expr, ns);
 
         if(implications.count(neg_expr)!=0)
@@ -466,8 +462,7 @@ void symex_slice_by_tracet::slice_SSA_steps(
         }
         else
         {
-          cond_copy.make_not();
-          simplify(cond_copy, ns);
+          cond_copy = simplify_expr(boolean_negate(cond_copy), ns);
           if(implications.count(cond_copy)!=0)
           {
             sliced_conds++;
@@ -622,8 +617,7 @@ bool symex_slice_by_tracet::implies_false(const exprt e)
       i=imps.begin();
       i!=imps.end(); i++)
   {
-    exprt i_copy(*i);
-    i_copy.make_not();
+    exprt i_copy = boolean_negate(*i);
     simplify(i_copy, ns);
     if(imps.count(i_copy)!=0)
       return true;
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index ec7f61a3f43..73e129361c4 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <algorithm>
 
 #include <util/exception_utils.h>
+#include <util/expr_util.h>
 #include <util/invariant.h>
 #include <util/pointer_offset_size.h>
 #include <util/range.h>
@@ -242,8 +243,7 @@ void goto_symext::symex_goto(statet &state)
     {
       symbol_exprt guard_symbol_expr=
         symbol_exprt(guard_identifier, bool_typet());
-      exprt new_rhs=new_guard;
-      new_rhs.make_not();
+      exprt new_rhs = boolean_negate(new_guard);
 
       ssa_exprt new_lhs(guard_symbol_expr);
       state.rename(new_lhs, ns, goto_symex_statet::L1);
@@ -266,8 +266,7 @@ void goto_symext::symex_goto(statet &state)
         original_source,
         symex_targett::assignment_typet::GUARD);
 
-      guard_expr=guard_symbol_expr;
-      guard_expr.make_not();
+      guard_expr = boolean_negate(guard_symbol_expr);
       state.rename(guard_expr, ns);
     }
 
@@ -276,10 +275,7 @@ void goto_symext::symex_goto(statet &state)
       if(!backward)
         state.guard.add(guard_expr);
       else
-      {
-        guard_expr.make_not();
-        state.guard.add(guard_expr);
-      }
+        state.guard.add(boolean_negate(guard_expr));
     }
     else
     {
@@ -287,14 +283,12 @@ void goto_symext::symex_goto(statet &state)
       if(!backward)
       {
         new_state.guard.add(guard_expr);
-        guard_expr.make_not();
-        state.guard.add(guard_expr);
+        state.guard.add(boolean_negate(guard_expr));
       }
       else
       {
         state.guard.add(guard_expr);
-        guard_expr.make_not();
-        new_state.guard.add(guard_expr);
+        new_state.guard.add(boolean_negate(guard_expr));
       }
     }
   }
diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/src/pointer-analysis/goto_program_dereference.cpp
index 0e716aa8a43..35921242fdd 100644
--- a/src/pointer-analysis/goto_program_dereference.cpp
+++ b/src/pointer-analysis/goto_program_dereference.cpp
@@ -76,7 +76,7 @@ void goto_program_dereferencet::dereference_failure(
 
   if(assertions.insert(guard_expr).second)
   {
-    guard_expr.make_not();
+    guard_expr = boolean_negate(guard_expr);
 
     // first try simplifier on it
     if(options.get_bool_option("simplify"))
@@ -127,11 +127,7 @@ void goto_program_dereferencet::dereference_rec(
         dereference_rec(op, guard, value_set_dereferencet::modet::READ);
 
       if(expr.id()==ID_or)
-      {
-        exprt tmp(op);
-        tmp.make_not();
-        guard.add(tmp);
-      }
+        guard.add(boolean_negate(op));
       else
         guard.add(op);
     }
@@ -169,9 +165,7 @@ void goto_program_dereferencet::dereference_rec(
     if(o2)
     {
       guardt old_guard=guard;
-      exprt tmp(expr.op0());
-      tmp.make_not();
-      guard.add(tmp);
+      guard.add(boolean_negate(expr.op0()));
       dereference_rec(expr.op2(), guard, mode);
       guard.swap(old_guard);
     }
diff --git a/src/util/expr.cpp b/src/util/expr.cpp
index 7322e124895..ac4172c0fb8 100644
--- a/src/util/expr.cpp
+++ b/src/util/expr.cpp
@@ -78,38 +78,6 @@ void exprt::make_typecast(const typet &_type)
   swap(new_expr);
 }
 
-/// Negate the expression.
-/// Simplifications:
-///   - If the expression is trivially true, make it false, and vice versa.
-///   - If the expression is an `ID_not`, remove the not.
-/// \deprecated use constructors instead
-void exprt::make_not()
-{
-  if(is_true())
-  {
-    *this=false_exprt();
-    return;
-  }
-  else if(is_false())
-  {
-    *this=true_exprt();
-    return;
-  }
-
-  exprt new_expr;
-
-  if(id()==ID_not && operands().size()==1)
-  {
-    new_expr.swap(operands().front());
-  }
-  else
-  {
-    new_expr = not_exprt(*this);
-  }
-
-  swap(new_expr);
-}
-
 /// Return whether the expression is a constant.
 /// \return True if is a constant, false otherwise
 bool exprt::is_constant() const
diff --git a/src/util/expr.h b/src/util/expr.h
index 358e106d3fa..a8c0b74dc82 100644
--- a/src/util/expr.h
+++ b/src/util/expr.h
@@ -213,7 +213,6 @@ class exprt:public irept
   }
 
   void make_typecast(const typet &_type);
-  void make_not();
 
   void make_true();
   void make_false();
diff --git a/src/util/guard.cpp b/src/util/guard.cpp
index 9da74db2dcd..320d98031c8 100644
--- a/src/util/guard.cpp
+++ b/src/util/guard.cpp
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <ostream>
 
+#include "expr_util.h"
 #include "invariant.h"
 #include "simplify_utils.h"
 #include "std_expr.h"
@@ -27,8 +28,7 @@ void guardt::guard_expr(exprt &dest) const
   {
     if(dest.is_false())
     {
-      dest=as_expr();
-      dest.make_not();
+      dest = boolean_negate(as_expr());
     }
     else
     {
@@ -110,8 +110,7 @@ guardt &operator |= (guardt &g1, const guardt &g2)
 
   if(g1.id()!=ID_and || g2.id()!=ID_and)
   {
-    exprt tmp(g2);
-    tmp.make_not();
+    exprt tmp(boolean_negate(g2));
 
     if(tmp==g1)
       g1.make_true();
@@ -166,8 +165,7 @@ guardt &operator |= (guardt &g1, const guardt &g2)
 
   g1=conjunction(op1);
 
-  exprt tmp(and_expr2);
-  tmp.make_not();
+  exprt tmp(boolean_negate(and_expr2));
 
   if(tmp!=and_expr1)
   {
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 3be87c69f00..e7adb108138 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -1105,9 +1105,7 @@ bool simplify_exprt::simplify_if(if_exprt &expr)
       else if(truevalue.is_false() && falsevalue.is_true())
       {
         // a?0:1 <-> !a
-        exprt tmp;
-        tmp.swap(cond);
-        tmp.make_not();
+        exprt tmp = boolean_negate(cond);
         simplify_node(tmp);
         expr.swap(tmp);
         return false;
@@ -1123,8 +1121,7 @@ bool simplify_exprt::simplify_if(if_exprt &expr)
       else if(falsevalue.is_true())
       {
         // a?b:1 <-> !a OR b
-        or_exprt tmp(cond, truevalue);
-        tmp.op0().make_not();
+        or_exprt tmp(boolean_negate(cond), truevalue);
         simplify_node(tmp.op0());
         simplify_node(tmp);
         expr.swap(tmp);
@@ -1141,8 +1138,7 @@ bool simplify_exprt::simplify_if(if_exprt &expr)
       else if(truevalue.is_false())
       {
         // a?0:b <-> !a && b
-        and_exprt tmp(cond, falsevalue);
-        tmp.op0().make_not();
+        and_exprt tmp(boolean_negate(cond), falsevalue);
         simplify_node(tmp.op0());
         simplify_node(tmp);
         expr.swap(tmp);
diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp
index 89003be5d4a..23b57744efe 100644
--- a/src/util/simplify_expr_boolean.cpp
+++ b/src/util/simplify_expr_boolean.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <unordered_set>
 
 #include "expr.h"
+#include "expr_util.h"
 #include "invariant.h"
 #include "namespace.h"
 #include "std_expr.h"
@@ -35,7 +36,7 @@ bool simplify_exprt::simplify_boolean(exprt &expr)
     // turn a => b into !a || b
 
     expr.id(ID_or);
-    expr.op0().make_not();
+    expr.op0() = boolean_negate(expr.op0());
     simplify_node(expr.op0());
     simplify_node(expr);
     return false;
@@ -80,7 +81,7 @@ bool simplify_exprt::simplify_boolean(exprt &expr)
     {
       exprt tmp(operands.front());
       if(negate)
-        tmp.make_not();
+        tmp = boolean_negate(operands.front());
       expr.swap(tmp);
       return false;
     }
@@ -195,7 +196,7 @@ bool simplify_exprt::simplify_not(exprt &expr)
 
     Forall_operands(it, expr)
     {
-      it->make_not();
+      *it = boolean_negate(*it);
       simplify_node(*it);
     }
 
diff --git a/src/util/simplify_expr_floatbv.cpp b/src/util/simplify_expr_floatbv.cpp
index f4a2aea43b6..13990e46db3 100644
--- a/src/util/simplify_expr_floatbv.cpp
+++ b/src/util/simplify_expr_floatbv.cpp
@@ -392,13 +392,13 @@ bool simplify_exprt::simplify_ieee_float_relation(exprt &expr)
   if(expr.op0()==expr.op1())
   {
     // x!=x is the same as saying isnan(op)
-    isnan_exprt isnan(expr.op0());
+    exprt isnan = isnan_exprt(expr.op0());
 
     if(expr.id()==ID_ieee_float_notequal)
     {
     }
     else if(expr.id()==ID_ieee_float_equal)
-      isnan.make_not();
+      isnan = not_exprt(isnan);
     else
       UNREACHABLE;
 
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index 1e2bb3ceb62..88af3ce1173 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -1558,7 +1558,7 @@ bool simplify_exprt::simplify_inequality_not_constant(exprt &expr)
   {
     expr.id(ID_equal);
     simplify_inequality_not_constant(expr);
-    expr.make_not();
+    expr = boolean_negate(expr);
     simplify_node(expr);
     return false;
   }
@@ -1568,7 +1568,7 @@ bool simplify_exprt::simplify_inequality_not_constant(exprt &expr)
     // swap operands
     expr.op0().swap(expr.op1());
     simplify_inequality_not_constant(expr);
-    expr.make_not();
+    expr = boolean_negate(expr);
     simplify_node(expr);
     return false;
   }
@@ -1576,7 +1576,7 @@ bool simplify_exprt::simplify_inequality_not_constant(exprt &expr)
   {
     expr.id(ID_ge);
     simplify_inequality_not_constant(expr);
-    expr.make_not();
+    expr = boolean_negate(expr);
     simplify_node(expr);
     return false;
   }
@@ -1695,7 +1695,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
     {
       expr.id(ID_equal);
       simplify_inequality_constant(expr);
-      expr.make_not();
+      expr = boolean_negate(expr);
       simplify_node(expr);
       return false;
     }
@@ -1886,8 +1886,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
     // we re-write (TYPE)boolean == 0 -> !boolean
     if(expr.op1().is_zero() && expr.id()==ID_equal)
     {
-      expr=expr.op0().op0();
-      expr.make_not();
+      expr = boolean_negate(expr.op0().op0());
       return false;
     }
 
@@ -1912,7 +1911,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
     {
       expr.id(ID_equal);
       simplify_inequality_constant(expr);
-      expr.make_not();
+      expr = boolean_negate(expr);
       simplify_node(expr);
       return false;
     }
@@ -1936,7 +1935,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
     {
       expr.id(ID_ge);
       simplify_inequality_constant(expr);
-      expr.make_not();
+      expr = boolean_negate(expr);
       simplify_node(expr);
       return false;
     }
@@ -1954,7 +1953,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
       ++i;
       expr.op1()=from_integer(i, expr.op1().type());
       simplify_inequality_constant(expr);
-      expr.make_not();
+      expr = boolean_negate(expr);
       simplify_node(expr);
       return false;
     }