diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 1b1591e81b1..54c2a6948c3 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "simplify_expr.h"
 
-#include <cassert>
 #include <algorithm>
 
 #include "arith_tools.h"
@@ -19,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "endianness_map.h"
 #include "expr_util.h"
 #include "fixedbv.h"
+#include "invariant.h"
 #include "namespace.h"
 #include "pointer_offset_size.h"
 #include "rational.h"
@@ -225,7 +225,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
     inequality.add_source_location()=expr.source_location();
     inequality.lhs()=expr.op0();
     inequality.rhs()=from_integer(0, op_type);
-    assert(inequality.rhs().is_not_nil());
+    CHECK_RETURN(inequality.rhs().is_not_nil());
     simplify_node(inequality);
     expr.swap(inequality);
     return false;
@@ -260,7 +260,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
     inequality.add_source_location()=expr.source_location();
     inequality.lhs()=expr.op0();
     inequality.rhs()=from_integer(0, op_type);
-    assert(inequality.rhs().is_not_nil());
+    CHECK_RETURN(inequality.rhs().is_not_nil());
     simplify_node(inequality);
     expr.op0()=inequality;
     simplify_typecast(expr); // recursive call
@@ -488,13 +488,13 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
         if(operand.is_true())
         {
           expr=from_integer(1, expr_type);
-          assert(expr.is_not_nil());
+          CHECK_RETURN(expr.is_not_nil());
           return false;
         }
         else if(operand.is_false())
         {
           expr=from_integer(0, expr_type);
-          assert(expr.is_not_nil());
+          CHECK_RETURN(expr.is_not_nil());
           return false;
         }
       }
@@ -1365,17 +1365,12 @@ bool simplify_exprt::simplify_update(exprt &expr)
     {
       const irep_idt &component_name=
         e.get(ID_component_name);
-
-      if(!to_struct_type(value_ptr_type).
-         has_component(component_name))
+      const struct_typet &value_ptr_struct_type=to_struct_type(value_ptr_type);
+      if(!value_ptr_struct_type.has_component(component_name))
         return true;
-
-      std::size_t number=to_struct_type(value_ptr_type).
-        component_number(component_name);
-
-      assert(number<value_ptr->operands().size());
-
-      value_ptr=&value_ptr->operands()[number];
+      auto &designator_as_struct_expr = to_struct_expr(*value_ptr);
+      value_ptr = &designator_as_struct_expr.component(component_name, ns);
+      CHECK_RETURN(value_ptr->id() != ID_nil);
     }
     else
       return true; // give up, unknown designator
@@ -1407,16 +1402,13 @@ bool simplify_exprt::simplify_object(exprt &expr)
   }
   else if(expr.id()==ID_typecast)
   {
-    const typet &op_type=ns.follow(expr.op0().type());
-
-    assert(expr.operands().size()==1);
+    auto const& typecast_expr = to_typecast_expr(expr);
+    const typet &op_type=ns.follow(typecast_expr.op().type());
 
     if(op_type.id()==ID_pointer)
     {
       // cast from pointer to pointer
-      exprt tmp;
-      tmp.swap(expr.op0());
-      expr.swap(tmp);
+      expr = typecast_expr.op();
       simplify_object(expr);
       return false;
     }
@@ -1427,10 +1419,10 @@ bool simplify_exprt::simplify_object(exprt &expr)
       // We do a bit of special treatment for (TYPE *)(a+(int)&o) and
       // (TYPE *)(a+(int)((T*)&o+x)), which are re-written to '&o'.
 
-      exprt tmp=expr.op0();
-      if(tmp.id()==ID_plus && tmp.operands().size()==2)
+      exprt casted_expr=typecast_expr.op();
+      if(casted_expr.id()==ID_plus && casted_expr.operands().size()==2)
       {
-        exprt cand=tmp.op0().id()==ID_typecast?tmp.op0():tmp.op1();
+        exprt cand=casted_expr.op0().id()==ID_typecast?casted_expr.op0():casted_expr.op1();
 
         if(cand.id()==ID_typecast &&
            cand.operands().size()==1 &&
@@ -1545,7 +1537,7 @@ exprt simplify_exprt::bits2expr(
     for(const auto &component : components)
     {
       mp_integer m_size=pointer_offset_bits(component.type(), ns);
-      assert(m_size>=0);
+      CHECK_RETURN(m_size >= 0);
 
       std::string comp_bits=
         std::string(
@@ -1573,7 +1565,7 @@ exprt simplify_exprt::bits2expr(
 
     std::size_t el_size=
       integer2size_t(pointer_offset_bits(type.subtype(), ns));
-    assert(el_size>0);
+    CHECK_RETURN(el_size > 0);
 
     array_exprt result(array_type);
     result.reserve_operands(n_el);
@@ -1677,7 +1669,7 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
     expr.offset()=plus_exprt(
       to_byte_extract_expr(expr.op()).offset(),
       expr.offset());
-    simplify_plus(expr.offset());
+    expr.offset() = simplify_plus(to_plus_expr(expr.offset())).simplified_expr;
 
     expr.op()=to_byte_extract_expr(expr.op()).op();
     simplify_byte_extract(expr);
@@ -1829,10 +1821,10 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
         op_type_ptr->id()==ID_array;
         op_type_ptr=&(ns.follow(*op_type_ptr).subtype()))
     {
-      // no arrays of zero-sized objects
-      assert(el_size>0);
-      // no arrays of non-byte sized objects
-      assert(el_size%8==0);
+      DATA_INVARIANT(el_size > 0, "arrays must not have zero-sized objects");
+      DATA_INVARIANT(
+        el_size % 8 == 0,
+        "array elements have a size in bits which is a multiple of bytes");
       mp_integer el_bytes=el_size/8;
 
       if(base_type_eq(expr.type(), op_type_ptr->subtype(), ns) ||
@@ -2225,6 +2217,18 @@ bool simplify_exprt::simplify_node_preorder(exprt &expr)
   return result;
 }
 
+inline bool adjust_with_simplify_result(
+  exprt &out,
+  const simplify_exprt::simplify_resultt &in)
+{
+  bool changed = in.was_changed == simplify_exprt::was_changedt::Changed;
+  if(changed)
+  {
+    out = in.simplified_expr;
+  }
+  return !changed;
+}
+
 bool simplify_exprt::simplify_node(exprt &expr)
 {
   if(!expr.has_operands())
@@ -2289,7 +2293,11 @@ bool simplify_exprt::simplify_node(exprt &expr)
   else if(expr.id()==ID_power)
     result=simplify_power(expr) && result;
   else if(expr.id()==ID_plus)
-    result=simplify_plus(expr) && result;
+  {
+    result =
+      adjust_with_simplify_result(expr, simplify_plus(to_plus_expr(expr))) &&
+      result;
+  }
   else if(expr.id()==ID_minus)
     result=simplify_minus(expr) && result;
   else if(expr.id()==ID_mult)
@@ -2300,7 +2308,12 @@ bool simplify_exprt::simplify_node(exprt &expr)
           expr.id()==ID_floatbv_div)
     result=simplify_floatbv_op(expr) && result;
   else if(expr.id()==ID_floatbv_typecast)
-    result=simplify_floatbv_typecast(expr) && result;
+  {
+    result =
+      adjust_with_simplify_result(
+        expr, simplify_floatbv_typecast(to_floatbv_typecast_expr(expr))) &&
+      result;
+  }
   else if(expr.id()==ID_unary_minus)
     result=simplify_unary_minus(expr) && result;
   else if(expr.id()==ID_unary_plus)
diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp
index 99a548927e1..207dcddb56e 100644
--- a/src/util/simplify_expr_boolean.cpp
+++ b/src/util/simplify_expr_boolean.cpp
@@ -8,10 +8,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "simplify_expr_class.h"
 
-#include <cassert>
 #include <unordered_set>
 
 #include "expr.h"
+#include "invariant.h"
 #include "namespace.h"
 #include "std_expr.h"
 
@@ -245,13 +245,12 @@ bool simplify_exprt::simplify_not(exprt &expr)
   }
   else if(op.id()==ID_exists) // !(exists: a) <-> forall: not a
   {
-    assert(op.operands().size()==2);
-    exprt tmp;
-    tmp.swap(op);
-    expr.swap(tmp);
-    expr.id(ID_forall);
-    expr.op1().make_not();
-    simplify_node(expr.op1());
+    auto const& op_as_exists = to_exists_expr(op);
+    forall_exprt rewritten_op(op_as_exists.symbol()
+      , op_as_exists.where());
+    rewritten_op.where().make_not();
+    simplify_node(rewritten_op.where());
+    expr = rewritten_op;
     return false;
   }
 
diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h
index 5e192292666..1e75e87f9ee 100644
--- a/src/util/simplify_expr_class.h
+++ b/src/util/simplify_expr_class.h
@@ -16,6 +16,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #endif
 
 #include <set>
+#include <util/expr.h>
+#include <util/std_expr.h>
 
 #include "type.h"
 #include "mp_arith.h"
@@ -62,6 +64,16 @@ class simplify_exprt
 
   bool do_simplify_if;
 
+  enum class was_changedt
+  {
+    Changed,
+    Unchanged
+  };
+  struct simplify_resultt
+  {
+    exprt simplified_expr;
+    was_changedt was_changed;
+  };
   // These below all return 'true' if the simplification wasn't applicable.
   // If false is returned, the expression has changed.
 
@@ -72,10 +84,11 @@ class simplify_exprt
   bool simplify_mult(exprt &expr);
   bool simplify_div(exprt &expr);
   bool simplify_mod(exprt &expr);
-  bool simplify_plus(exprt &expr);
+  simplify_resultt simplify_plus(const plus_exprt &expr);
   bool simplify_minus(exprt &expr);
   bool simplify_floatbv_op(exprt &expr);
-  bool simplify_floatbv_typecast(exprt &expr);
+  simplify_resultt
+  simplify_floatbv_typecast(const floatbv_typecast_exprt &expr);
   bool simplify_shifts(exprt &expr);
   bool simplify_power(exprt &expr);
   bool simplify_bitwise(exprt &expr);
diff --git a/src/util/simplify_expr_floatbv.cpp b/src/util/simplify_expr_floatbv.cpp
index 22623c518a9..1f0df30fbdc 100644
--- a/src/util/simplify_expr_floatbv.cpp
+++ b/src/util/simplify_expr_floatbv.cpp
@@ -8,13 +8,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "simplify_expr_class.h"
 
-#include <cassert>
-
+#include "arith_tools.h"
 #include "expr.h"
-#include "namespace.h"
 #include "ieee_float.h"
+#include "invariant.h"
+#include "namespace.h"
 #include "std_expr.h"
-#include "arith_tools.h"
 
 bool simplify_exprt::simplify_isinf(exprt &expr)
 {
@@ -138,11 +137,9 @@ bool simplify_exprt::simplify_sign(exprt &expr)
 }
 #endif
 
-bool simplify_exprt::simplify_floatbv_typecast(exprt &expr)
+simplify_exprt::simplify_resultt
+simplify_exprt::simplify_floatbv_typecast(const floatbv_typecast_exprt &expr)
 {
-  // These casts usually reduce precision, and thus, usually round.
-
-  assert(expr.operands().size()==2);
 
   const typet &dest_type=ns.follow(expr.type());
   const typet &src_type=ns.follow(expr.op0().type());
@@ -150,12 +147,11 @@ bool simplify_exprt::simplify_floatbv_typecast(exprt &expr)
   // eliminate redundant casts
   if(dest_type==src_type)
   {
-    expr=expr.op0();
-    return false;
+    return {expr.op0(), was_changedt::Changed};
   }
 
-  exprt op0=expr.op0();
-  exprt op1=expr.op1(); // rounding mode
+  exprt casted_expr = expr.op0();
+  exprt rounding_mode_expr = expr.op1(); // rounding mode
 
   // We can soundly re-write (float)((double)x op (double)y)
   // to x op y. True for any rounding mode!
@@ -188,34 +184,32 @@ bool simplify_exprt::simplify_floatbv_typecast(exprt &expr)
   #endif
 
   // constant folding
-  if(op0.is_constant() && op1.is_constant())
+  if(casted_expr.is_constant() && rounding_mode_expr.is_constant())
   {
     mp_integer rounding_mode;
-    if(!to_integer(op1, rounding_mode))
+    if(!to_integer(rounding_mode_expr, rounding_mode))
     {
       if(src_type.id()==ID_floatbv)
       {
         if(dest_type.id()==ID_floatbv) // float to float
         {
-          ieee_floatt result(to_constant_expr(op0));
+          ieee_floatt result(to_constant_expr(casted_expr));
           result.rounding_mode=
             (ieee_floatt::rounding_modet)integer2size_t(rounding_mode);
           result.change_spec(
             ieee_float_spect(to_floatbv_type(dest_type)));
-          expr=result.to_expr();
-          return false;
+          return {result.to_expr(), was_changedt::Changed};
         }
         else if(dest_type.id()==ID_signedbv ||
                 dest_type.id()==ID_unsignedbv)
         {
           if(rounding_mode==ieee_floatt::ROUND_TO_ZERO)
           {
-            ieee_floatt result(to_constant_expr(op0));
+            ieee_floatt result(to_constant_expr(casted_expr));
             result.rounding_mode=
               (ieee_floatt::rounding_modet)integer2size_t(rounding_mode);
             mp_integer value=result.to_integer();
-            expr=from_integer(value, dest_type);
-            return false;
+            return {from_integer(value, dest_type), was_changedt::Changed};
           }
         }
       }
@@ -223,7 +217,7 @@ bool simplify_exprt::simplify_floatbv_typecast(exprt &expr)
               src_type.id()==ID_unsignedbv)
       {
         mp_integer value;
-        if(!to_integer(op0, value))
+        if(!to_integer(casted_expr, value))
         {
           if(dest_type.id()==ID_floatbv) // int to float
           {
@@ -231,8 +225,7 @@ bool simplify_exprt::simplify_floatbv_typecast(exprt &expr)
             result.rounding_mode=
               (ieee_floatt::rounding_modet)integer2size_t(rounding_mode);
             result.from_integer(value);
-            expr=result.to_expr();
-            return false;
+            return {result.to_expr(), was_changedt::Changed};
           }
         }
       }
@@ -262,24 +255,32 @@ bool simplify_exprt::simplify_floatbv_typecast(exprt &expr)
   }
   #endif
 
-  return true;
+  return {expr, was_changedt::Unchanged};
 }
 
 bool simplify_exprt::simplify_floatbv_op(exprt &expr)
 {
   const typet &type=ns.follow(expr.type());
 
-  if(type.id()!=ID_floatbv)
-    return true;
-
-  assert(expr.operands().size()==3);
+  PRECONDITION(type.id() == ID_floatbv);
+  PRECONDITION(
+    expr.id() == ID_floatbv_plus || expr.id() == ID_floatbv_minus ||
+    expr.id() == ID_floatbv_mult || expr.id() == ID_floatbv_div);
+  DATA_INVARIANT(
+    expr.operands().size() == 3,
+    "binary operations have two operands, here an addtional parameter "
+    "is for the rounding mode");
 
   exprt op0=expr.op0();
   exprt op1=expr.op1();
   exprt op2=expr.op2(); // rounding mode
 
-  assert(ns.follow(op0.type())==type);
-  assert(ns.follow(op1.type())==type);
+  INVARIANT(
+    ns.follow(op0.type()) == type,
+    "expression type of operand must match type of expression");
+  INVARIANT(
+    ns.follow(op1.type()) == type,
+    "expression type of operand must match type of expression");
 
   // Remember that floating-point addition is _NOT_ associative.
   // Thus, we don't re-sort the operands.
@@ -330,8 +331,8 @@ bool simplify_exprt::simplify_floatbv_op(exprt &expr)
 
 bool simplify_exprt::simplify_ieee_float_relation(exprt &expr)
 {
-  assert(expr.id()==ID_ieee_float_equal ||
-         expr.id()==ID_ieee_float_notequal);
+  PRECONDITION(
+    expr.id() == ID_ieee_float_equal || expr.id() == ID_ieee_float_notequal);
 
   exprt::operandst &operands=expr.operands();
 
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index 6856c6a38fc..e26a8eede66 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -42,7 +42,10 @@ bool simplify_exprt::simplify_bswap(bswap_exprt &expr)
     mp_integer new_value=0;
     for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
     {
-      assert(!bytes.empty());
+      INVARIANT(
+        !bytes.empty(),
+        "bytes is not empty because we just pushed just as many elements on "
+        "top of it as we are popping now");
       new_value+=bytes.back()<<bit;
       bytes.pop_back();
     }
@@ -179,7 +182,7 @@ bool simplify_exprt::simplify_mult(exprt &expr)
   exprt::operandst::iterator constant;
 
   // true if we have found a constant
-  bool found = false;
+  bool constant_found = false;
 
   typet c_sizeof_type=nil_typet();
 
@@ -211,7 +214,7 @@ bool simplify_exprt::simplify_mult(exprt &expr)
         c_sizeof_type=
           static_cast<const typet &>(it->find(ID_C_c_sizeof_type));
 
-      if(found)
+      if(constant_found)
       {
         // update the constant factor
         if(!mul_expr(to_constant_expr(*constant), to_constant_expr(*it)))
@@ -221,7 +224,7 @@ bool simplify_exprt::simplify_mult(exprt &expr)
       {
         // set it as the constant factor if this is the first
         constant=it;
-        found=true;
+        constant_found = true;
       }
     }
 
@@ -237,7 +240,10 @@ bool simplify_exprt::simplify_mult(exprt &expr)
 
   if(c_sizeof_type.is_not_nil())
   {
-    assert(found);
+    INVARIANT(
+      constant_found,
+      "c_sizeof_type is only set to a non-nil value "
+      "if a constant has been found");
     constant->set(ID_C_c_sizeof_type, c_sizeof_type);
   }
 
@@ -251,7 +257,7 @@ bool simplify_exprt::simplify_mult(exprt &expr)
   else
   {
     // if the constant is a one and there are other factors
-    if(found && constant->is_one())
+    if(constant_found && constant->is_one())
     {
       // just delete it
       operands.erase(constant);
@@ -437,21 +443,19 @@ bool simplify_exprt::simplify_mod(exprt &expr)
   return true;
 }
 
-bool simplify_exprt::simplify_plus(exprt &expr)
+simplify_exprt::simplify_resultt
+simplify_exprt::simplify_plus(const plus_exprt &expr)
 {
   if(!is_number(expr.type()) &&
      expr.type().id()!=ID_pointer)
-    return true;
-
-  bool result=true;
+    return {expr, was_changedt::Unchanged};
 
-  exprt::operandst &operands=expr.operands();
-
-  assert(expr.id()==ID_plus);
+  was_changedt was_changed = was_changedt::Unchanged;
+  plus_exprt intermediary_plus_expr = expr;
+  exprt::operandst &operands = intermediary_plus_expr.operands();
 
   // floating-point addition is _NOT_ associative; thus,
   // there is special case for float
-
   if(ns.follow(expr.type()).id()==ID_floatbv)
   {
     // we only merge neighboring constants!
@@ -475,29 +479,37 @@ bool simplify_exprt::simplify_plus(exprt &expr)
   else
   {
     // ((T*)p+a)+b -> (T*)p+(a+b)
-    if(expr.type().id()==ID_pointer &&
-       expr.operands().size()==2 &&
-       expr.op0().id()==ID_plus &&
-       expr.op0().operands().size()==2)
+    if(
+      intermediary_plus_expr.type().id() == ID_pointer &&
+      intermediary_plus_expr.operands().size() == 2 &&
+      intermediary_plus_expr.op0().id() == ID_plus &&
+      intermediary_plus_expr.op0().operands().size() == 2)
     {
-      exprt op0=expr.op0();
+      plus_exprt &pointer_sum_expr = to_plus_expr(intermediary_plus_expr.op0());
 
-      if(expr.op0().op1().id()==ID_plus)
-        op0.op1().copy_to_operands(expr.op1());
+      if(pointer_sum_expr.op1().id() == ID_plus)
+        pointer_sum_expr.op1().copy_to_operands(intermediary_plus_expr.op1());
       else
-        op0.op1()=plus_exprt(op0.op1(), expr.op1());
+        pointer_sum_expr.op1() =
+          plus_exprt(pointer_sum_expr.op1(), intermediary_plus_expr.op1());
 
-      expr.swap(op0);
+      intermediary_plus_expr.swap(pointer_sum_expr);
 
-      simplify_plus(expr.op1());
-      simplify_plus(expr);
+      auto simplify_op_result =
+        simplify_plus(to_plus_expr(intermediary_plus_expr.op1()));
+      if(simplify_op_result.was_changed == was_changedt::Changed)
+      {
+        intermediary_plus_expr.op1() = simplify_op_result.simplified_expr;
+      }
+      auto simplify_intermediary_result = simplify_plus(intermediary_plus_expr);
 
-      return false;
+      return {simplify_intermediary_result.simplified_expr,
+              was_changedt::Changed};
     }
 
     // count the constants
     size_t count=0;
-    forall_operands(it, expr)
+    forall_operands(it, intermediary_plus_expr)
       if(is_number(it->type()) && it->is_constant())
         count++;
 
@@ -507,7 +519,7 @@ bool simplify_exprt::simplify_plus(exprt &expr)
       exprt::operandst::iterator const_sum;
       bool const_sum_set=false;
 
-      Forall_operands(it, expr)
+      Forall_operands(it, intermediary_plus_expr)
       {
         if(is_number(it->type()) && it->is_constant())
         {
@@ -522,8 +534,8 @@ bool simplify_exprt::simplify_plus(exprt &expr)
                          to_constant_expr(*it)))
             {
               *it=from_integer(0, it->type());
-              assert(it->is_not_nil());
-              result=false;
+              CHECK_RETURN(it->is_not_nil());
+              was_changed = was_changedt::Changed;
             }
           }
         }
@@ -553,11 +565,11 @@ bool simplify_exprt::simplify_plus(exprt &expr)
 
       if(itm!=expr_map.end())
       {
-        *(itm->second)=from_integer(0, expr.type());
-        *it=from_integer(0, expr.type());
-        assert(it->is_not_nil());
+        *(itm->second) = from_integer(0, intermediary_plus_expr.type());
+        *it = from_integer(0, intermediary_plus_expr.type());
+        CHECK_RETURN(it->is_not_nil());
         expr_map.erase(itm);
-        result=false;
+        was_changed = was_changedt::Changed;
       }
     }
 
@@ -572,7 +584,7 @@ bool simplify_exprt::simplify_plus(exprt &expr)
       if(is_number(it->type()) && it->is_zero())
       {
         it=operands.erase(it);
-        result=false;
+        was_changed = was_changedt::Changed;
       }
       else
         it++;
@@ -581,30 +593,28 @@ bool simplify_exprt::simplify_plus(exprt &expr)
 
   if(operands.empty())
   {
-    expr=from_integer(0, expr.type());
-    assert(expr.is_not_nil());
-    return false;
+    auto result = from_integer(0, expr.type());
+    CHECK_RETURN(result.is_not_nil());
+    return {result, was_changedt::Changed};
   }
   else if(operands.size()==1)
   {
-    exprt tmp(operands.front());
-    expr.swap(tmp);
-    return false;
+    return {operands.front(), was_changedt::Changed};
   }
 
-  return result;
+  return {intermediary_plus_expr, was_changed};
 }
 
 bool simplify_exprt::simplify_minus(exprt &expr)
 {
+  PRECONDITION(expr.id() == ID_minus);
+
   if(!is_number(expr.type()) &&
      expr.type().id()!=ID_pointer)
     return true;
 
   exprt::operandst &operands=expr.operands();
 
-  assert(expr.id()==ID_minus);
-
   if(operands.size()!=2)
     return true;
 
@@ -631,9 +641,8 @@ bool simplify_exprt::simplify_minus(exprt &expr)
     simplify_unary_minus(tmp2);
 
     plus_exprt tmp(operands[0], tmp2);
-    simplify_plus(tmp);
-
-    expr.swap(tmp);
+    auto result = simplify_plus(tmp);
+    expr.swap(result.simplified_expr);
     return false;
   }
   else if(is_number(expr.type()) &&
@@ -645,7 +654,7 @@ bool simplify_exprt::simplify_minus(exprt &expr)
     if(operands[0]==operands[1])
     {
       exprt zero=from_integer(0, expr.type());
-      assert(zero.is_not_nil());
+      CHECK_RETURN(zero.is_not_nil());
       expr=zero;
       return false;
     }
@@ -740,7 +749,9 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
     if(expr.op1().type()!=expr.type())
       break;
 
-    assert(a_str.size()==b_str.size());
+    INVARIANT(
+      a_str.size() == b_str.size(),
+      "bitvectors of the same type have the same size");
 
     constant_exprt new_op(expr.type());
     std::string new_value;
@@ -848,32 +859,41 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
 
 bool simplify_exprt::simplify_extractbit(exprt &expr)
 {
-  const typet &op0_type=expr.op0().type();
-
-  if(!is_bitvector_type(op0_type))
-    return true;
+  PRECONDITION(expr.id() == ID_extractbit);
+  auto &extractbit_expr = to_extractbit_expr(expr);
 
-  std::size_t width=to_bitvector_type(op0_type).get_width();
+  const typet &src_type = extractbit_expr.src().type();
 
-  assert(expr.operands().size()==2);
+  if(!is_bitvector_type(src_type))
+    return true;
 
-  mp_integer i;
+  const std::size_t src_bit_width = to_bitvector_type(src_type).get_width();
 
-  if(to_integer(expr.op1(), i))
+  const auto index_converted_to_int =
+    numeric_cast<mp_integer>(extractbit_expr.index());
+  if(!index_converted_to_int.has_value())
+  {
     return true;
-
-  if(!expr.op0().is_constant())
+  }
+  const mp_integer index_as_int = index_converted_to_int.value();
+  if(!extractbit_expr.src().is_constant())
     return true;
 
-  if(i<0 || i>=width)
+  if(index_as_int < 0 || index_as_int >= src_bit_width)
     return true;
 
-  const irep_idt &value=expr.op0().get(ID_value);
+  const irep_idt &src_value =
+    to_constant_expr(extractbit_expr.src()).get_value();
+
+
+  std::string src_value_as_string=id2string(src_value);
 
-  if(value.size()!=width)
+  if(src_value_as_string.size() != src_bit_width)
     return true;
 
-  bool bit=(id2string(value)[width-integer2size_t(i)-1]=='1');
+  const bool bit =
+    (src_value_as_string
+       [src_bit_width - numeric_cast_v<std::size_t>(index_as_int) - 1]=='1');
 
   expr.make_bool(bit);
 
@@ -1581,7 +1601,9 @@ bool simplify_exprt::simplify_inequality_not_constant(exprt &expr)
 
   // now we only have >=, =
 
-  assert(expr.id()==ID_ge || expr.id()==ID_equal);
+  INVARIANT(
+    expr.id() == ID_ge || expr.id() == ID_equal,
+    "we previously converted all other cases to >= or ==");
 
   // syntactically equal?
 
@@ -1663,7 +1685,7 @@ bool simplify_exprt::simplify_inequality_not_constant(exprt &expr)
 bool simplify_exprt::simplify_inequality_constant(exprt &expr)
 {
   // the constant is always on the RHS
-  assert(expr.op1().is_constant());
+  PRECONDITION(expr.op1().is_constant());
 
   if(expr.op0().id()==ID_if && expr.op0().operands().size()==3)
   {
@@ -1767,7 +1789,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
           {
             constant+=i;
             *it=from_integer(0, it->type());
-            assert(it->is_not_nil());
+            CHECK_RETURN(it->is_not_nil());
             changed=true;
           }
         }
@@ -1781,7 +1803,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
         i-=constant;
         expr.op1()=from_integer(i, expr.op1().type());
 
-        simplify_plus(expr.op0());
+        expr.op0() = simplify_plus(to_plus_expr(expr.op0())).simplified_expr;
         simplify_inequality(expr);
         return false;
       }
@@ -1907,9 +1929,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
     }
     else if(expr.id()==ID_gt)
     {
-      mp_integer i;
-      if(to_integer(expr.op1(), i))
-        throw "bit-vector constant unexpectedly non-integer";
+      mp_integer i = numeric_cast_v<mp_integer>(expr.op1());
 
       if(i==max)
       {
@@ -1933,9 +1953,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
     }
     else if(expr.id()==ID_le)
     {
-      mp_integer i;
-      if(to_integer(expr.op1(), i))
-        throw "bit-vector constant unexpectedly non-integer";
+      mp_integer i = numeric_cast_v<mp_integer>(expr.op1());
 
       if(i==max)
       {
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
index b183c81890b..1d8ad4c820a 100644
--- a/src/util/simplify_expr_pointer.cpp
+++ b/src/util/simplify_expr_pointer.cpp
@@ -196,9 +196,8 @@ bool simplify_exprt::simplify_address_of(exprt &expr)
   else if(object.id()==ID_dereference)
   {
     // simplify &*p to p
-    assert(object.operands().size()==1);
-    exprt tmp=object.op0();
-    expr=tmp;
+    auto const &object_as_dereference_expr = to_dereference_expr(object);
+    expr = object_as_dereference_expr.pointer();
     return false;
   }
 
@@ -410,9 +409,10 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
 
 bool simplify_exprt::simplify_inequality_address_of(exprt &expr)
 {
-  assert(expr.type().id()==ID_bool);
-  assert(expr.operands().size()==2);
-  assert(expr.id()==ID_equal || expr.id()==ID_notequal);
+  PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
+  PRECONDITION(expr.type().id() == ID_bool);
+  DATA_INVARIANT(
+    expr.operands().size() == 2, "(in)equalities have two operands");
 
   exprt tmp0=expr.op0();
   if(tmp0.id()==ID_typecast)
@@ -426,8 +426,8 @@ bool simplify_exprt::simplify_inequality_address_of(exprt &expr)
   if(tmp1.op0().id()==ID_index &&
      to_index_expr(tmp1.op0()).index().is_zero())
     tmp1=address_of_exprt(to_index_expr(tmp1.op0()).array());
-  assert(tmp0.id()==ID_address_of);
-  assert(tmp1.id()==ID_address_of);
+  INVARIANT(tmp0.id() == ID_address_of, "id must be ID_address_of");
+  INVARIANT(tmp1.id() == ID_address_of, "id must be ID_address_of");
 
   if(tmp0.operands().size()!=1)
     return true;
@@ -450,14 +450,15 @@ bool simplify_exprt::simplify_inequality_address_of(exprt &expr)
 
 bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr)
 {
-  assert(expr.type().id()==ID_bool);
-  assert(expr.operands().size()==2);
-  assert(expr.id()==ID_equal || expr.id()==ID_notequal);
+  PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
+  PRECONDITION(expr.type().id() == ID_bool);
+  DATA_INVARIANT(
+    expr.operands().size() == 2, "(in)equalities have two operands");
 
   forall_operands(it, expr)
   {
-    assert(it->id()==ID_pointer_object);
-    assert(it->operands().size()==1);
+    PRECONDITION(it->id() == ID_pointer_object);
+    PRECONDITION(it->operands().size() == 1);
     const exprt &op=it->op0();
 
     if(op.id()==ID_address_of)
diff --git a/src/util/ssa_expr.h b/src/util/ssa_expr.h
index e04325b4caf..02f50537c69 100644
--- a/src/util/ssa_expr.h
+++ b/src/util/ssa_expr.h
@@ -153,9 +153,9 @@ class ssa_exprt:public symbol_exprt
 */
 inline const ssa_exprt &to_ssa_expr(const exprt &expr)
 {
-  assert(expr.id()==ID_symbol &&
-         expr.get_bool(ID_C_SSA_symbol) &&
-         !expr.has_operands());
+  PRECONDITION(
+    expr.id() == ID_symbol && expr.get_bool(ID_C_SSA_symbol) &&
+    !expr.has_operands());
   return static_cast<const ssa_exprt &>(expr);
 }
 
@@ -164,9 +164,9 @@ inline const ssa_exprt &to_ssa_expr(const exprt &expr)
 */
 inline ssa_exprt &to_ssa_expr(exprt &expr)
 {
-  assert(expr.id()==ID_symbol &&
-         expr.get_bool(ID_C_SSA_symbol) &&
-         !expr.has_operands());
+  PRECONDITION(
+    expr.id() == ID_symbol && expr.get_bool(ID_C_SSA_symbol) &&
+    !expr.has_operands());
   return static_cast<ssa_exprt &>(expr);
 }
 
diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp
index ac7139113df..e9ed0585ee3 100644
--- a/src/util/std_expr.cpp
+++ b/src/util/std_expr.cpp
@@ -74,7 +74,7 @@ static void build_object_descriptor_rec(
     build_object_descriptor_rec(ns, index.array(), dest);
 
     exprt sub_size=size_of_expr(expr.type(), ns);
-    assert(sub_size.is_not_nil());
+    CHECK_RETURN(sub_size.is_not_nil());
 
     dest.offset()=
       plus_exprt(dest.offset(),
@@ -89,7 +89,7 @@ static void build_object_descriptor_rec(
     build_object_descriptor_rec(ns, struct_op, dest);
 
     exprt offset=member_offset_expr(member, ns);
-    assert(offset.is_not_nil());
+    CHECK_RETURN(offset.is_not_nil());
 
     dest.offset()=
       plus_exprt(dest.offset(),
@@ -124,7 +124,7 @@ void object_descriptor_exprt::build(
   const exprt &expr,
   const namespacet &ns)
 {
-  assert(object().id()==ID_unknown);
+  PRECONDITION(object().id() == ID_unknown);
   object()=expr;
 
   if(offset().id()==ID_unknown)
@@ -132,7 +132,7 @@ void object_descriptor_exprt::build(
 
   build_object_descriptor_rec(ns, expr, *this);
 
-  assert(root_object().type().id()!=ID_empty);
+  POSTCONDITION(root_object().type().id() != ID_empty);
 }
 
 shift_exprt::shift_exprt(
@@ -158,7 +158,7 @@ extractbits_exprt::extractbits_exprt(
   const typet &_type):
   exprt(ID_extractbits, _type)
 {
-  assert(_upper>=_lower);
+  PRECONDITION(_upper >= _lower);
   operands().resize(3);
   src()=_src;
   upper()=from_integer(_upper, integer_typet());
@@ -204,7 +204,8 @@ const exprt &object_descriptor_exprt::root_object() const
 
   while(p->id() == ID_member || p->id() == ID_index)
   {
-    assert(!p->operands().empty());
+    DATA_INVARIANT(
+      p->has_operands(), "member and index expressions have operands");
     p = &p->op0();
   }
 
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index 85ca4a6b3a2..5e3a06ed40d 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -4376,6 +4376,22 @@ class exists_exprt:public quantifier_exprt
   }
 };
 
+inline const exists_exprt &to_exists_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_exists);
+  DATA_INVARIANT(expr.operands().size()== 2,
+    "exists expressions have exactly two operands");
+  return static_cast<const exists_exprt&>(expr);
+}
+
+inline exists_exprt &to_exists_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_exists);
+  DATA_INVARIANT(expr.operands().size()== 2,
+                 "exists expressions have exactly two operands");
+  return static_cast<exists_exprt&>(expr);
+}
+
 /// \brief The popcount (counting the number of bits set to 1) expression
 class popcount_exprt: public unary_exprt
 {
diff --git a/src/util/std_types.cpp b/src/util/std_types.cpp
index 0712ad7cbe1..3df1bdaeb0f 100644
--- a/src/util/std_types.cpp
+++ b/src/util/std_types.cpp
@@ -19,14 +19,14 @@ Author: Daniel Kroening, kroening@kroening.com
 std::size_t fixedbv_typet::get_integer_bits() const
 {
   const irep_idt integer_bits=get(ID_integer_bits);
-  assert(!integer_bits.empty());
+  DATA_INVARIANT(!integer_bits.empty(), "integer bits should be set");
   return unsafe_string2unsigned(id2string(integer_bits));
 }
 
 std::size_t floatbv_typet::get_f() const
 {
   const irep_idt &f=get(ID_f);
-  assert(!f.empty());
+  DATA_INVARIANT(!f.empty(), "the mantissa should be set");
   return unsafe_string2unsigned(id2string(f));
 }
 
@@ -75,7 +75,7 @@ typet struct_union_typet::component_type(
   const irep_idt &component_name) const
 {
   const exprt c=get_component(component_name);
-  assert(c.is_not_nil());
+  CHECK_RETURN(c.is_not_nil());
   return c.type();
 }
 
diff --git a/src/util/string_constant.h b/src/util/string_constant.h
index 84588b58cd9..d62b42bc1c7 100644
--- a/src/util/string_constant.h
+++ b/src/util/string_constant.h
@@ -31,13 +31,13 @@ class string_constantt:public exprt
 
 inline const string_constantt &to_string_constant(const exprt &expr)
 {
-  assert(expr.id()==ID_string_constant);
+  PRECONDITION(expr.id() == ID_string_constant);
   return static_cast<const string_constantt &>(expr);
 }
 
 inline string_constantt &to_string_constant(exprt &expr)
 {
-  assert(expr.id()==ID_string_constant);
+  PRECONDITION(expr.id() == ID_string_constant);
   return static_cast<string_constantt &>(expr);
 }
 
diff --git a/src/util/string_utils.cpp b/src/util/string_utils.cpp
index 7ba55a73fb5..1bf384b9f29 100644
--- a/src/util/string_utils.cpp
+++ b/src/util/string_utils.cpp
@@ -109,8 +109,8 @@ void split_string(
   std::vector<std::string> result;
 
   split_string(s, delim, result, strip);
-  if(result.size()!=2)
-    throw "split string did not generate exactly 2 parts";
+  CHECK_RETURN(
+    result.size() == 2, "split string must generate exactly 2 parts");
 
   left=result[0];
   right=result[1];