diff --git a/src/util/Makefile b/src/util/Makefile
index baaa4ab5bba..1628e6b325b 100644
--- a/src/util/Makefile
+++ b/src/util/Makefile
@@ -71,6 +71,7 @@ SRC = allocate_objects.cpp \
       simplify_expr_array.cpp \
       simplify_expr_boolean.cpp \
       simplify_expr_floatbv.cpp \
+      simplify_expr_if.cpp \
       simplify_expr_int.cpp \
       simplify_expr_pointer.cpp \
       simplify_expr_struct.cpp \
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index f19d6fdfce9..7d81fef9756 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -103,34 +103,29 @@ simplify_exprt::resultt<> simplify_exprt::simplify_abs(const abs_exprt &expr)
   return unchanged(expr);
 }
 
-bool simplify_exprt::simplify_sign(exprt &expr)
+simplify_exprt::resultt<> simplify_exprt::simplify_sign(const sign_exprt &expr)
 {
-  if(expr.operands().size()!=1)
-    return true;
-
-  if(expr.op0().is_constant())
+  if(expr.op().is_constant())
   {
-    const typet &type = expr.op0().type();
+    const typet &type = expr.op().type();
 
     if(type.id()==ID_floatbv)
     {
-      ieee_floatt value(to_constant_expr(expr.op0()));
-      expr = make_boolean_expr(value.get_sign());
-      return false;
+      ieee_floatt value(to_constant_expr(expr.op()));
+      return make_boolean_expr(value.get_sign());
     }
     else if(type.id()==ID_signedbv ||
             type.id()==ID_unsignedbv)
     {
-      const auto value = numeric_cast<mp_integer>(expr.op0());
+      const auto value = numeric_cast<mp_integer>(expr.op());
       if(value.has_value())
       {
-        expr = make_boolean_expr(*value >= 0);
-        return false;
+        return make_boolean_expr(*value >= 0);
       }
     }
   }
 
-  return true;
+  return unchanged(expr);
 }
 
 simplify_exprt::resultt<>
@@ -650,7 +645,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
           from_integer(*sub_size, size_type()),
           typecast_exprt(expr.op().op1(), size_type()));
 
-      simplify_rec(new_expr.op()); // rec. call
+      new_expr.op() = simplify_rec(new_expr.op()); // rec. call
 
       return changed(simplify_typecast(new_expr)); // rec. call
     }
@@ -734,8 +729,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
         }
       }
 
-      simplify_rec(new_expr);
-      return std::move(new_expr);
+      return changed(simplify_rec(new_expr)); // recursive call
     }
   }
 
@@ -1074,8 +1068,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
       auto result =
         address_of_exprt(index_exprt(o, from_integer(0, size_type())));
 
-      simplify_rec(result);
-      return std::move(result);
+      return changed(simplify_rec(result)); // recursive call
     }
   }
 
@@ -1111,8 +1104,7 @@ simplify_exprt::simplify_dereference(const dereference_exprt &expr)
   {
     exprt tmp=to_address_of_expr(pointer).object();
     // one address_of is gone, try again
-    simplify_rec(tmp);
-    return tmp;
+    return changed(simplify_rec(tmp));
   }
   // rewrite *(&a[0] + x) to a[x]
   else if(pointer.id()==ID_plus &&
@@ -1130,386 +1122,9 @@ simplify_exprt::simplify_dereference(const dereference_exprt &expr)
           old.array(),
           pointer_offset_sum(old.index(), pointer.op1()),
           old.array().type().subtype());
-        simplify_rec(idx);
-        return idx;
-      }
-    }
-  }
-
-  return unchanged(expr);
-}
-
-bool simplify_exprt::simplify_if_implies(
-  exprt &expr,
-  const exprt &cond,
-  bool truth,
-  bool &new_truth)
-{
-  if(expr==cond)
-  {
-    new_truth = truth;
-    return false;
-  }
-
-  if(truth && cond.id()==ID_lt && expr.id()==ID_lt)
-  {
-    if(cond.op0()==expr.op0() &&
-       cond.op1().is_constant() &&
-       expr.op1().is_constant() &&
-       cond.op1().type()==expr.op1().type())
-    {
-      mp_integer i1, i2;
-
-      if(
-        !to_integer(to_constant_expr(cond.op1()), i1) &&
-        !to_integer(to_constant_expr(expr.op1()), i2))
-      {
-        if(i1 >= i2)
-        {
-          new_truth = true;
-          return false;
-        }
-      }
-    }
-
-    if(cond.op1()==expr.op1() &&
-       cond.op0().is_constant() &&
-       expr.op0().is_constant() &&
-       cond.op0().type()==expr.op0().type())
-    {
-      mp_integer i1, i2;
-
-      if(
-        !to_integer(to_constant_expr(cond.op0()), i1) &&
-        !to_integer(to_constant_expr(expr.op0()), i2))
-      {
-        if(i1 <= i2)
-        {
-          new_truth = true;
-          return false;
-        }
-      }
-    }
-  }
-
-  return true;
-}
-
-bool simplify_exprt::simplify_if_recursive(
-  exprt &expr,
-  const exprt &cond,
-  bool truth)
-{
-  if(expr.type().id()==ID_bool)
-  {
-    bool new_truth;
-
-    if(!simplify_if_implies(expr, cond, truth, new_truth))
-    {
-      if(new_truth)
-      {
-        expr=true_exprt();
-        return false;
-      }
-      else
-      {
-        expr=false_exprt();
-        return false;
-      }
-    }
-  }
-
-  bool result = true;
-
-  Forall_operands(it, expr)
-    result = simplify_if_recursive(*it, cond, truth) && result;
-
-  return result;
-}
-
-bool simplify_exprt::simplify_if_conj(
-  exprt &expr,
-  const exprt &cond)
-{
-  forall_operands(it, cond)
-  {
-    if(expr==*it)
-    {
-      expr=true_exprt();
-      return false;
-    }
-  }
-
-  bool result=true;
-
-  Forall_operands(it, expr)
-    result=simplify_if_conj(*it, cond) && result;
-
-  return result;
-}
-
-bool simplify_exprt::simplify_if_disj(
-  exprt &expr,
-  const exprt &cond)
-{
-  forall_operands(it, cond)
-  {
-    if(expr==*it)
-    {
-      expr=false_exprt();
-      return false;
-    }
-  }
-
-  bool result=true;
-
-  Forall_operands(it, expr)
-    result=simplify_if_disj(*it, cond) && result;
-
-  return result;
-}
-
-bool simplify_exprt::simplify_if_branch(
-  exprt &trueexpr,
-  exprt &falseexpr,
-  const exprt &cond)
-{
-  bool tresult = true;
-  bool fresult = true;
-
-  if(cond.id()==ID_and)
-  {
-    tresult = simplify_if_conj(trueexpr, cond) && tresult;
-    fresult = simplify_if_recursive(falseexpr, cond, false) && fresult;
-  }
-  else if(cond.id()==ID_or)
-  {
-    tresult = simplify_if_recursive(trueexpr, cond, true) && tresult;
-    fresult = simplify_if_disj(falseexpr, cond) && fresult;
-  }
-  else
-  {
-    tresult = simplify_if_recursive(trueexpr, cond, true) && tresult;
-    fresult = simplify_if_recursive(falseexpr, cond, false) && fresult;
-  }
-
-  if(!tresult)
-    simplify_rec(trueexpr);
-  if(!fresult)
-    simplify_rec(falseexpr);
-
-  return tresult && fresult;
-}
-
-bool simplify_exprt::simplify_if_cond(exprt &expr)
-{
-  bool result=true;
-  bool tmp=false;
-
-  while(!tmp)
-  {
-    tmp=true;
-
-    if(expr.id()==ID_and)
-    {
-      if(expr.has_operands())
-      {
-        exprt::operandst &operands = expr.operands();
-        for(exprt::operandst::iterator it1=operands.begin();
-            it1!=operands.end(); it1++)
-        {
-          for(exprt::operandst::iterator it2=operands.begin();
-              it2!=operands.end(); it2++)
-          {
-            if(it1!=it2)
-              tmp=simplify_if_recursive(*it1, *it2, true) && tmp;
-          }
-        }
-      }
-    }
-
-    if(!tmp)
-      simplify_rec(expr);
-
-    result=tmp && result;
-  }
-
-  return result;
-}
-
-bool simplify_exprt::simplify_if_preorder(if_exprt &expr)
-{
-  exprt &cond=expr.cond();
-  exprt &truevalue=expr.true_case();
-  exprt &falsevalue=expr.false_case();
-
-  // we first want to look at the condition
-  bool result=simplify_rec(cond);
-
-  // 1 ? a : b -> a  and  0 ? a : b -> b
-  if(cond.is_constant())
-  {
-    exprt tmp=cond.is_true()?truevalue:falsevalue;
-    simplify_rec(tmp);
-    expr.swap(tmp);
-    return false;
-  }
-
-  if(do_simplify_if)
-  {
-    if(cond.id()==ID_not)
-    {
-      exprt tmp;
-      tmp.swap(cond.op0());
-      cond.swap(tmp);
-      truevalue.swap(falsevalue);
-      result=false;
-    }
-
-#ifdef USE_LOCAL_REPLACE_MAP
-    replace_mapt map_before(local_replace_map);
-
-    // a ? b : c  --> a ? b[a/true] : c
-    if(cond.id()==ID_and)
-    {
-      forall_operands(it, cond)
-      {
-        if(it->id()==ID_not)
-          local_replace_map.insert(
-            std::make_pair(it->op0(), false_exprt()));
-        else
-          local_replace_map.insert(
-            std::make_pair(*it, true_exprt()));
-      }
-    }
-    else
-      local_replace_map.insert(std::make_pair(cond, true_exprt()));
-
-    result=simplify_rec(truevalue) && result;
-
-    local_replace_map=map_before;
-
-    // a ? b : c  --> a ? b : c[a/false]
-    if(cond.id()==ID_or)
-    {
-      forall_operands(it, cond)
-      {
-        if(it->id()==ID_not)
-          local_replace_map.insert(
-            std::make_pair(it->op0(), true_exprt()));
-        else
-          local_replace_map.insert(
-            std::make_pair(*it, false_exprt()));
+        return changed(simplify_rec(idx));
       }
     }
-    else
-      local_replace_map.insert(std::make_pair(cond, false_exprt()));
-
-    result=simplify_rec(falsevalue) && result;
-
-    local_replace_map.swap(map_before);
-#else
-    result=simplify_rec(truevalue) && result;
-    result=simplify_rec(falsevalue) && result;
-#endif
-  }
-  else
-  {
-    result=simplify_rec(truevalue) && result;
-    result=simplify_rec(falsevalue) && result;
-  }
-
-  return result;
-}
-
-simplify_exprt::resultt<> simplify_exprt::simplify_if(const if_exprt &expr)
-{
-  const exprt &cond = expr.cond();
-  const exprt &truevalue = expr.true_case();
-  const exprt &falsevalue = expr.false_case();
-
-  if(do_simplify_if)
-  {
-    #if 0
-    result = simplify_if_cond(cond) && result;
-    result = simplify_if_branch(truevalue, falsevalue, cond) && result;
-    #endif
-
-    if(expr.type()==bool_typet())
-    {
-      // a?b:c <-> (a && b) || (!a && c)
-
-      if(truevalue.is_true() && falsevalue.is_false())
-      {
-        // a?1:0 <-> a
-        return cond;
-      }
-      else if(truevalue.is_false() && falsevalue.is_true())
-      {
-        // a?0:1 <-> !a
-        exprt tmp = boolean_negate(cond);
-        simplify_node(tmp);
-        return std::move(tmp);
-      }
-      else if(falsevalue.is_false())
-      {
-        // a?b:0 <-> a AND b
-        and_exprt tmp(cond, truevalue);
-        simplify_node(tmp);
-        return std::move(tmp);
-      }
-      else if(falsevalue.is_true())
-      {
-        // a?b:1 <-> !a OR b
-        exprt tmp_not_cond = boolean_negate(cond);
-        simplify_node(tmp_not_cond);
-        or_exprt tmp(tmp_not_cond, truevalue);
-        simplify_node(tmp);
-        return std::move(tmp);
-      }
-      else if(truevalue.is_true())
-      {
-        // a?1:b <-> a||(!a && b) <-> a OR b
-        or_exprt tmp(cond, falsevalue);
-        simplify_node(tmp);
-        return std::move(tmp);
-      }
-      else if(truevalue.is_false())
-      {
-        // a?0:b <-> !a && b
-        exprt tmp_not_cond = boolean_negate(cond);
-        simplify_node(tmp_not_cond);
-        and_exprt tmp(tmp_not_cond, falsevalue);
-        simplify_node(tmp);
-        return std::move(tmp);
-      }
-    }
-  }
-
-  if(truevalue==falsevalue)
-    return truevalue;
-
-  // this pushes the if-then-else into struct and array constructors
-  if(((truevalue.id()==ID_struct && falsevalue.id()==ID_struct) ||
-      (truevalue.id()==ID_array && falsevalue.id()==ID_array)) &&
-     truevalue.operands().size()==falsevalue.operands().size())
-  {
-    exprt cond_copy=cond;
-    exprt falsevalue_copy=falsevalue;
-    exprt truevalue_copy = truevalue;
-
-    auto range_false = make_range(falsevalue_copy.operands());
-    auto range_true = make_range(truevalue_copy.operands());
-    auto new_expr = truevalue;
-    new_expr.operands().clear();
-
-    for(const auto &pair : range_true.zip(range_false))
-    {
-      new_expr.operands().push_back(
-        simplify_if(if_exprt(cond_copy, pair.first, pair.second)));
-    }
-
-    return std::move(new_expr);
   }
 
   return unchanged(expr);
@@ -1546,14 +1161,15 @@ simplify_exprt::resultt<> simplify_exprt::simplify_lambda(const exprt &expr)
   return unchanged(expr);
 }
 
-bool simplify_exprt::simplify_with(exprt &expr)
+simplify_exprt::resultt<> simplify_exprt::simplify_with(const exprt &expr)
 {
-  bool result=true;
+  bool no_change = true;
 
   if((expr.operands().size()%2)!=1)
-    return true;
+    return unchanged(expr);
 
-  auto &with_expr = to_with_expr(expr);
+  // copy
+  auto with_expr = to_with_expr(expr);
 
   const typet old_type_followed = ns.follow(with_expr.old().type());
 
@@ -1569,17 +1185,20 @@ bool simplify_exprt::simplify_with(exprt &expr)
           with_expr.where().get(ID_component_name);
 
         if(!to_struct_type(old_type_followed).has_component(component_name))
-          return result;
+          return unchanged(expr);
 
         std::size_t number =
           to_struct_type(old_type_followed).component_number(component_name);
 
+        if(number >= with_expr.old().operands().size())
+          return unchanged(expr);
+
         with_expr.old().operands()[number].swap(with_expr.new_value());
 
         with_expr.operands().erase(++with_expr.operands().begin());
         with_expr.operands().erase(++with_expr.operands().begin());
 
-        result=false;
+        no_change = false;
       }
     }
   }
@@ -1588,10 +1207,10 @@ bool simplify_exprt::simplify_with(exprt &expr)
     with_expr.old().type().id() == ID_vector)
   {
     if(
-      expr.op0().id() == ID_array || expr.op0().id() == ID_constant ||
-      expr.op0().id() == ID_vector)
+      with_expr.old().id() == ID_array || with_expr.old().id() == ID_constant ||
+      with_expr.old().id() == ID_vector)
     {
-      while(expr.operands().size()>1)
+      while(with_expr.operands().size() > 1)
       {
         const auto i = numeric_cast<mp_integer>(with_expr.where());
 
@@ -1607,26 +1226,24 @@ bool simplify_exprt::simplify_with(exprt &expr)
         with_expr.operands().erase(++with_expr.operands().begin());
         with_expr.operands().erase(++with_expr.operands().begin());
 
-        result=false;
+        no_change = false;
       }
     }
   }
 
-  if(expr.operands().size()==1)
-  {
-    exprt tmp;
-    tmp.swap(expr.op0());
-    expr.swap(tmp);
-    result=false;
-  }
+  if(with_expr.operands().size() == 1)
+    return with_expr.old();
 
-  return result;
+  if(no_change)
+    return unchanged(expr);
+  else
+    return std::move(with_expr);
 }
 
-bool simplify_exprt::simplify_update(exprt &expr)
+simplify_exprt::resultt<> simplify_exprt::simplify_update(const exprt &expr)
 {
   if(expr.operands().size()!=3)
-    return true;
+    return unchanged(expr);
 
   // this is to push updates into (possibly nested) constants
 
@@ -1645,10 +1262,10 @@ bool simplify_exprt::simplify_update(exprt &expr)
       const auto i = numeric_cast<mp_integer>(e.op0());
 
       if(!i.has_value())
-        return true;
+        return unchanged(expr);
 
       if(*i < 0 || *i >= value_ptr->operands().size())
-        return true;
+        return unchanged(expr);
 
       value_ptr = &value_ptr->operands()[numeric_cast_v<std::size_t>(*i)];
     }
@@ -1660,20 +1277,18 @@ bool simplify_exprt::simplify_update(exprt &expr)
       const struct_typet &value_ptr_struct_type =
         to_struct_type(value_ptr_type);
       if(!value_ptr_struct_type.has_component(component_name))
-        return true;
+        return unchanged(expr);
       auto &designator_as_struct_expr = to_struct_expr(*value_ptr);
       value_ptr = &designator_as_struct_expr.component(component_name, ns);
       CHECK_RETURN(value_ptr->is_not_nil());
     }
     else
-      return true; // give up, unknown designator
+      return unchanged(expr); // give up, unknown designator
   }
 
   // found, done
   *value_ptr=to_update_expr(expr).new_value();
-  expr.swap(updated_value);
-
-  return false;
+  return updated_value;
 }
 
 simplify_exprt::resultt<> simplify_exprt::simplify_object(const exprt &expr)
@@ -2194,9 +1809,7 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
     auto tmp = expr;
     tmp.op() = index_exprt(expr.op(), expr.offset());
     tmp.offset() = from_integer(0, expr.offset().type());
-    simplify_rec(tmp);
-
-    return std::move(tmp);
+    return changed(simplify_rec(tmp));
   }
 
   // extract bits of a constant
@@ -2242,8 +1855,7 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
   if(!subexpr.has_value() || subexpr.value() == expr)
     return unchanged(expr);
 
-  simplify_rec(subexpr.value());
-  return subexpr.value();
+  return changed(simplify_rec(subexpr.value())); // recursive call
 }
 
 simplify_exprt::resultt<>
@@ -2466,16 +2078,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
     }
 
     if(result_expr.is_not_nil())
-    {
-      simplify_rec(result_expr);
-      return result_expr;
-    }
-
-    if(result_expr.is_not_nil())
-    {
-      simplify_rec(result_expr);
-      return result_expr;
-    }
+      return changed(simplify_rec(result_expr));
   }
 
   // replace elements of array or struct expressions, possibly using
@@ -2519,7 +2122,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
             *offset_int + val_offset - m_offset_bits / 8, offset.type()),
           new_val);
 
-        simplify_rec(*it);
+        *it = simplify_rec(*it); // recursive call
 
         val_offset+=bytes_req;
       }
@@ -2533,7 +2136,8 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
   return unchanged(expr);
 }
 
-simplify_exprt::resultt<> simplify_exprt::simplify_complex(const exprt &expr)
+simplify_exprt::resultt<>
+simplify_exprt::simplify_complex(const unary_exprt &expr)
 {
   if(expr.id() == ID_complex_real)
   {
@@ -2570,8 +2174,14 @@ bool simplify_exprt::simplify_node_preorder(exprt &expr)
     if(expr.has_operands())
     {
       Forall_operands(it, expr)
-        if(!simplify_rec(*it)) // recursive call
+      {
+        auto r_it = simplify_rec(*it); // recursive call
+        if(r_it.has_changed())
+        {
+          *it = r_it.expr;
           result=false;
+        }
+      }
     }
   }
 
@@ -2603,8 +2213,7 @@ bool simplify_exprt::simplify_node(exprt &expr)
           expr.id()==ID_gt    || expr.id()==ID_lt ||
           expr.id()==ID_ge    || expr.id()==ID_le)
   {
-    if(!simplify_inequality(expr))
-      r = changed(expr);
+    r = simplify_inequality(expr);
   }
   else if(expr.id()==ID_if)
   {
@@ -2616,23 +2225,19 @@ bool simplify_exprt::simplify_node(exprt &expr)
   }
   else if(expr.id()==ID_with)
   {
-    if(!simplify_with(expr))
-      r = changed(expr);
+    r = simplify_with(expr);
   }
   else if(expr.id()==ID_update)
   {
-    if(!simplify_update(expr))
-      r = changed(expr);
+    r = simplify_update(expr);
   }
   else if(expr.id()==ID_index)
   {
-    if(!simplify_index(expr))
-      r = changed(expr);
+    r = simplify_index(to_index_expr(expr));
   }
   else if(expr.id()==ID_member)
   {
-    if(!simplify_member(expr))
-      r = changed(expr);
+    r = simplify_member(to_member_expr(expr));
   }
   else if(expr.id()==ID_byte_update_little_endian ||
           expr.id()==ID_byte_update_big_endian)
@@ -2646,7 +2251,7 @@ bool simplify_exprt::simplify_node(exprt &expr)
   }
   else if(expr.id()==ID_pointer_object)
   {
-    r = simplify_pointer_object(expr);
+    r = simplify_pointer_object(to_unary_expr(expr));
   }
   else if(expr.id() == ID_is_dynamic_object)
   {
@@ -2658,11 +2263,11 @@ bool simplify_exprt::simplify_node(exprt &expr)
   }
   else if(expr.id()==ID_object_size)
   {
-    r = simplify_object_size(expr);
+    r = simplify_object_size(to_unary_expr(expr));
   }
   else if(expr.id()==ID_good_pointer)
   {
-    r = simplify_good_pointer(expr);
+    r = simplify_good_pointer(to_unary_expr(expr));
   }
   else if(expr.id()==ID_div)
   {
@@ -2674,7 +2279,7 @@ bool simplify_exprt::simplify_node(exprt &expr)
   }
   else if(expr.id()==ID_bitnot)
   {
-    r = simplify_bitnot(expr);
+    r = simplify_bitnot(to_bitnot_expr(expr));
   }
   else if(expr.id()==ID_bitand ||
           expr.id()==ID_bitor ||
@@ -2715,15 +2320,15 @@ bool simplify_exprt::simplify_node(exprt &expr)
   }
   else if(expr.id()==ID_unary_minus)
   {
-    r = simplify_unary_minus(expr);
+    r = simplify_unary_minus(to_unary_minus_expr(expr));
   }
   else if(expr.id()==ID_unary_plus)
   {
-    r = simplify_unary_plus(expr);
+    r = simplify_unary_plus(to_unary_plus_expr(expr));
   }
   else if(expr.id()==ID_not)
   {
-    r = simplify_not(expr);
+    r = simplify_not(to_not_expr(expr));
   }
   else if(expr.id()==ID_implies ||
           expr.id()==ID_or      || expr.id()==ID_xor ||
@@ -2741,15 +2346,15 @@ bool simplify_exprt::simplify_node(exprt &expr)
   }
   else if(expr.id()==ID_pointer_offset)
   {
-    r = simplify_pointer_offset(expr);
+    r = simplify_pointer_offset(to_unary_expr(expr));
   }
   else if(expr.id()==ID_extractbit)
   {
-    r = simplify_extractbit(expr);
+    r = simplify_extractbit(to_extractbit_expr(expr));
   }
   else if(expr.id()==ID_concatenation)
   {
-    r = simplify_concatenation(expr);
+    r = simplify_concatenation(to_concatenation_expr(expr));
   }
   else if(expr.id()==ID_extractbits)
   {
@@ -2782,8 +2387,7 @@ bool simplify_exprt::simplify_node(exprt &expr)
   }
   else if(expr.id()==ID_sign)
   {
-    if(!simplify_sign(expr))
-      r = changed(expr);
+    r = simplify_sign(to_sign_expr(expr));
   }
   else if(expr.id() == ID_popcount)
   {
@@ -2795,7 +2399,7 @@ bool simplify_exprt::simplify_node(exprt &expr)
   }
   else if(expr.id() == ID_complex_real || expr.id() == ID_complex_imag)
   {
-    r = simplify_complex(expr);
+    r = simplify_complex(to_unary_expr(expr));
   }
 
   if(r.has_changed())
@@ -2820,8 +2424,7 @@ bool simplify_exprt::simplify_node(exprt &expr)
   return no_change;
 }
 
-/// \return returns true if expression unchanged; returns false if changed
-bool simplify_exprt::simplify_rec(exprt &expr)
+simplify_exprt::resultt<> simplify_exprt::simplify_rec(const exprt &expr)
 {
   // look up in cache
 
@@ -2867,34 +2470,45 @@ bool simplify_exprt::simplify_rec(exprt &expr)
   #endif
 #endif
 
-  if(!result)
+  if(result) // no change
+  {
+    return unchanged(expr);
+  }
+  else // change, new expression is 'tmp'
   {
-    POSTCONDITION(tmp.type() == expr.type());
-    expr.swap(tmp);
+    POSTCONDITION(as_const(tmp).type() == expr.type());
 
-    #ifdef USE_CACHE
+#ifdef USE_CACHE
     // save in cache
-    cache_result.first->second=expr;
-    #endif
-  }
+    cache_result.first->second = tmp;
+#endif
 
-  return result;
+    return std::move(tmp);
+  }
 }
 
+/// \return returns true if expression unchanged; returns false if changed
 bool simplify_exprt::simplify(exprt &expr)
 {
 #ifdef DEBUG_ON_DEMAND
   if(debug_on)
     std::cout << "TO-SIMP " << format(expr) << "\n";
 #endif
-  bool res=simplify_rec(expr);
+  auto result = simplify_rec(expr);
 #ifdef DEBUG_ON_DEMAND
   if(debug_on)
-    std::cout << "FULLSIMP " << format(expr) << "\n";
+    std::cout << "FULLSIMP " << format(result.expr) << "\n";
 #endif
-  return res;
+  if(result.has_changed())
+  {
+    expr = result.expr;
+    return false; // change
+  }
+  else
+    return true; // no change
 }
 
+/// \return returns true if expression unchanged; returns false if changed
 bool simplify(exprt &expr, const namespacet &ns)
 {
   return simplify_exprt(ns).simplify(expr);
diff --git a/src/util/simplify_expr_array.cpp b/src/util/simplify_expr_array.cpp
index 21cc09dc97e..67c10c854cb 100644
--- a/src/util/simplify_expr_array.cpp
+++ b/src/util/simplify_expr_array.cpp
@@ -15,13 +15,19 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "std_expr.h"
 #include "string_constant.h"
 
-bool simplify_exprt::simplify_index(exprt &expr)
+simplify_exprt::resultt<>
+simplify_exprt::simplify_index(const index_exprt &expr)
 {
   bool no_change = true;
 
+  // copy
+  auto new_expr = expr;
+
+  // references
+  auto &index = new_expr.index();
+  auto &array = new_expr.array();
+
   // extra arithmetic optimizations
-  const exprt &index=to_index_expr(expr).index();
-  const exprt &array=to_index_expr(expr).array();
 
   if(index.id()==ID_div &&
      index.operands().size()==2)
@@ -30,33 +36,29 @@ bool simplify_exprt::simplify_index(exprt &expr)
        index.op0().operands().size()==2 &&
        index.op0().op1()==index.op1())
     {
-      exprt tmp=index.op0().op0();
-      expr.op1()=tmp;
+      index = index.op0().op0();
       no_change = false;
     }
     else if(index.op0().id()==ID_mult &&
             index.op0().operands().size()==2 &&
             index.op0().op0()==index.op1())
     {
-      exprt tmp=index.op0().op1();
-      expr.op1()=tmp;
+      index = index.op0().op1();
       no_change = false;
     }
   }
 
-  if(array.id()==ID_lambda)
+  if(array.id() == ID_lambda)
   {
     // simplify (lambda i: e)(x) to e[i/x]
 
     const auto &comprehension = to_array_comprehension_expr(array);
 
-    if(expr.op1().type() == comprehension.arg().type())
+    if(index.type() == comprehension.arg().type())
     {
       exprt tmp = comprehension.body();
-      replace_expr(comprehension.arg(), expr.op1(), tmp);
-      expr.swap(tmp);
-      simplify_rec(expr);
-      return false;
+      replace_expr(comprehension.arg(), index, tmp);
+      return changed(simplify_rec(tmp));
     }
   }
   else if(array.id()==ID_with)
@@ -64,53 +66,45 @@ bool simplify_exprt::simplify_index(exprt &expr)
     // we have (a WITH [i:=e])[j]
 
     if(array.operands().size() != 3)
-      return true;
+      return unchanged(expr);
 
     const auto &with_expr = to_with_expr(array);
 
-    if(with_expr.where() == expr.op1())
+    if(with_expr.where() == index)
     {
       // simplify (e with [i:=v])[i] to v
-      exprt tmp = with_expr.new_value();
-      expr.swap(tmp);
-      return false;
+      return with_expr.new_value();
     }
     else
     {
       // Turn (a with i:=x)[j] into (i==j)?x:a[j].
       // watch out that the type of i and j might be different.
       const exprt rhs_casted =
-        typecast_exprt::conditional_cast(with_expr.where(), expr.op1().type());
-
-      equal_exprt equality_expr(expr.op1(), rhs_casted);
+        typecast_exprt::conditional_cast(with_expr.where(), index.type());
 
-      simplify_inequality(equality_expr);
+      exprt equality_expr = simplify_inequality(equal_exprt(index, rhs_casted));
 
-      index_exprt new_index_expr(with_expr.old(), expr.op1(), expr.type());
-
-      simplify_index(new_index_expr); // recursive call
+      exprt new_index_expr = simplify_index(
+        index_exprt(with_expr.old(), index, new_expr.type())); // recursive call
 
       if(equality_expr.is_true())
       {
-        expr = with_expr.new_value();
-        return false;
+        return with_expr.new_value();
       }
       else if(equality_expr.is_false())
       {
-        expr.swap(new_index_expr);
-        return false;
+        return new_index_expr;
       }
 
       if_exprt if_expr(equality_expr, with_expr.new_value(), new_index_expr);
-      expr = simplify_if(if_expr).expr;
-      return false;
+      return changed(simplify_if(if_expr));
     }
   }
   else if(
     array.id() == ID_constant || array.id() == ID_array ||
     array.id() == ID_vector)
   {
-    const auto i = numeric_cast<mp_integer>(expr.op1());
+    const auto i = numeric_cast<mp_integer>(index);
 
     if(!i.has_value())
     {
@@ -122,14 +116,12 @@ bool simplify_exprt::simplify_index(exprt &expr)
     else
     {
       // ok
-      exprt tmp = array.operands()[numeric_cast_v<std::size_t>(*i)];
-      expr.swap(tmp);
-      return false;
+      return array.operands()[numeric_cast_v<std::size_t>(*i)];
     }
   }
   else if(array.id()==ID_string_constant)
   {
-    const auto i = numeric_cast<mp_integer>(expr.op1());
+    const auto i = numeric_cast<mp_integer>(index);
 
     const std::string &value = id2string(to_string_constant(array).get_value());
 
@@ -145,18 +137,14 @@ bool simplify_exprt::simplify_index(exprt &expr)
       // terminating zero?
       const char v =
         (*i == value.size()) ? 0 : value[numeric_cast_v<std::size_t>(*i)];
-      exprt tmp=from_integer(v, expr.type());
-      expr.swap(tmp);
-      return false;
+      return from_integer(v, new_expr.type());
     }
   }
   else if(array.id()==ID_array_of)
   {
     if(array.operands().size()==1)
     {
-      exprt tmp=array.op0();
-      expr.swap(tmp);
-      return false;
+      return array.op0();
     }
   }
   else if(array.id() == ID_array_list)
@@ -168,9 +156,7 @@ bool simplify_exprt::simplify_index(exprt &expr)
       simplify(tmp_index);
       if(tmp_index==index)
       {
-        exprt tmp=array.operands()[i*2+1];
-        expr.swap(tmp);
-        return false;
+        return array.operands()[i * 2 + 1];
       }
     }
   }
@@ -190,7 +176,7 @@ bool simplify_exprt::simplify_index(exprt &expr)
 
       auto sub_size = pointer_offset_size(*subtype, ns);
       if(!sub_size.has_value())
-        return true;
+        return unchanged(expr);
 
       // add offset to index
       mult_exprt offset(from_integer(*sub_size, array.op1().type()), index);
@@ -199,11 +185,8 @@ bool simplify_exprt::simplify_index(exprt &expr)
 
       exprt result_expr(array.id(), expr.type());
       result_expr.add_to_operands(array.op0(), final_offset);
-      expr.swap(result_expr);
-
-      simplify_rec(expr);
 
-      return false;
+      return changed(simplify_rec(result_expr));
     }
   }
   else if(array.id()==ID_if)
@@ -214,13 +197,14 @@ bool simplify_exprt::simplify_index(exprt &expr)
     index_exprt idx_false=to_index_expr(expr);
     idx_false.array()=if_expr.false_case();
 
-    to_index_expr(expr).array()=if_expr.true_case();
-
-    expr=if_exprt(cond, expr, idx_false, expr.type());
-    simplify_rec(expr);
+    new_expr.array() = if_expr.true_case();
 
-    return false;
+    exprt result = if_exprt(cond, new_expr, idx_false, expr.type());
+    return changed(simplify_rec(result));
   }
 
-  return no_change;
+  if(no_change)
+    return unchanged(expr);
+  else
+    return std::move(new_expr);
 }
diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp
index 5bcf4678e68..35f30f7d528 100644
--- a/src/util/simplify_expr_boolean.cpp
+++ b/src/util/simplify_expr_boolean.cpp
@@ -27,20 +27,20 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
 
   if(expr.id()==ID_implies)
   {
+    const auto &implies_expr = to_implies_expr(expr);
+
     if(
-      expr.operands().size() != 2 ||
-      expr.operands().front().type().id() != ID_bool ||
-      expr.operands().back().type().id() != ID_bool)
+      implies_expr.op0().type().id() != ID_bool ||
+      implies_expr.op1().type().id() != ID_bool)
     {
       return unchanged(expr);
     }
 
     // turn a => b into !a || b
 
-    auto new_expr = expr;
+    binary_exprt new_expr = implies_expr;
     new_expr.id(ID_or);
     new_expr.op0() = boolean_negate(new_expr.op0());
-    simplify_node(new_expr.op0());
     simplify_node(new_expr);
     return std::move(new_expr);
   }
@@ -164,12 +164,9 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
   return unchanged(expr);
 }
 
-simplify_exprt::resultt<> simplify_exprt::simplify_not(const exprt &expr)
+simplify_exprt::resultt<> simplify_exprt::simplify_not(const not_exprt &expr)
 {
-  if(expr.operands().size()!=1)
-    return unchanged(expr);
-
-  const exprt &op = expr.op0();
+  const exprt &op = expr.op();
 
   if(expr.type().id()!=ID_bool ||
      op.type().id()!=ID_bool)
diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h
index 28e03fbbfb4..fabeef6114c 100644
--- a/src/util/simplify_expr_class.h
+++ b/src/util/simplify_expr_class.h
@@ -30,12 +30,15 @@ class abs_exprt;
 class address_of_exprt;
 class array_exprt;
 class binary_relation_exprt;
+class bitnot_exprt;
 class bswap_exprt;
 class byte_extract_exprt;
 class byte_update_exprt;
+class concatenation_exprt;
 class dereference_exprt;
 class div_exprt;
 class exprt;
+class extractbit_exprt;
 class extractbits_exprt;
 class floatbv_typecast_exprt;
 class function_application_exprt;
@@ -47,12 +50,16 @@ class minus_exprt;
 class mod_exprt;
 class mult_exprt;
 class namespacet;
+class not_exprt;
 class plus_exprt;
 class popcount_exprt;
 class refined_string_exprt;
+class sign_exprt;
 class tvt;
 class typecast_exprt;
 class unary_exprt;
+class unary_minus_exprt;
+class unary_plus_exprt;
 
 #define forall_value_list(it, value_list) \
   for(simplify_exprt::value_listt::const_iterator it=(value_list).begin(); \
@@ -129,9 +136,9 @@ class simplify_exprt
   // These below all return 'true' if the simplification wasn't applicable.
   // If false is returned, the expression has changed.
   NODISCARD resultt<> simplify_typecast(const typecast_exprt &);
-  NODISCARD resultt<> simplify_extractbit(const exprt &);
+  NODISCARD resultt<> simplify_extractbit(const extractbit_exprt &);
   NODISCARD resultt<> simplify_extractbits(const extractbits_exprt &);
-  NODISCARD resultt<> simplify_concatenation(const exprt &);
+  NODISCARD resultt<> simplify_concatenation(const concatenation_exprt &);
   NODISCARD resultt<> simplify_mult(const mult_exprt &);
   NODISCARD resultt<> simplify_div(const div_exprt &);
   NODISCARD resultt<> simplify_mod(const mod_exprt &);
@@ -144,40 +151,40 @@ class simplify_exprt
   NODISCARD resultt<> simplify_bitwise(const exprt &);
   bool simplify_if_preorder(if_exprt &expr);
   NODISCARD resultt<> simplify_if(const if_exprt &);
-  NODISCARD resultt<> simplify_bitnot(const exprt &);
-  NODISCARD resultt<> simplify_not(const exprt &);
+  NODISCARD resultt<> simplify_bitnot(const bitnot_exprt &);
+  NODISCARD resultt<> simplify_not(const not_exprt &);
   NODISCARD resultt<> simplify_boolean(const exprt &);
-  bool simplify_inequality(exprt &expr);
+  NODISCARD resultt<> simplify_inequality(const exprt &);
   NODISCARD resultt<>
   simplify_ieee_float_relation(const binary_relation_exprt &);
   NODISCARD resultt<> simplify_lambda(const exprt &);
-  bool simplify_with(exprt &expr);
-  bool simplify_update(exprt &expr);
-  bool simplify_index(exprt &expr);
-  bool simplify_member(exprt &expr);
+  NODISCARD resultt<> simplify_with(const exprt &);
+  NODISCARD resultt<> simplify_update(const exprt &);
+  NODISCARD resultt<> simplify_index(const index_exprt &);
+  NODISCARD resultt<> simplify_member(const member_exprt &);
   NODISCARD resultt<> simplify_byte_update(const byte_update_exprt &);
   NODISCARD resultt<> simplify_byte_extract(const byte_extract_exprt &);
-  NODISCARD resultt<> simplify_pointer_object(const exprt &);
-  NODISCARD resultt<> simplify_object_size(const exprt &);
-  bool simplify_dynamic_size(exprt &expr);
+  NODISCARD resultt<> simplify_pointer_object(const unary_exprt &);
+  NODISCARD resultt<> simplify_object_size(const unary_exprt &);
+  NODISCARD resultt<> simplify_dynamic_size(const unary_exprt &);
   NODISCARD resultt<> simplify_is_dynamic_object(const exprt &expr);
   NODISCARD resultt<> simplify_is_invalid_pointer(const exprt &expr);
-  NODISCARD resultt<> simplify_same_object(const exprt &);
-  NODISCARD resultt<> simplify_good_pointer(const exprt &);
+  NODISCARD resultt<> simplify_same_object(const unary_exprt &);
+  NODISCARD resultt<> simplify_good_pointer(const unary_exprt &);
   NODISCARD resultt<> simplify_object(const exprt &);
-  NODISCARD resultt<> simplify_unary_minus(const exprt &);
-  NODISCARD resultt<> simplify_unary_plus(const exprt &);
+  NODISCARD resultt<> simplify_unary_minus(const unary_minus_exprt &);
+  NODISCARD resultt<> simplify_unary_plus(const unary_plus_exprt &);
   NODISCARD resultt<> simplify_dereference(const dereference_exprt &);
   NODISCARD resultt<> simplify_address_of(const address_of_exprt &);
-  NODISCARD resultt<> simplify_pointer_offset(const exprt &);
+  NODISCARD resultt<> simplify_pointer_offset(const unary_exprt &);
   NODISCARD resultt<> simplify_bswap(const bswap_exprt &);
   NODISCARD resultt<> simplify_isinf(const unary_exprt &);
   NODISCARD resultt<> simplify_isnan(const unary_exprt &);
   NODISCARD resultt<> simplify_isnormal(const unary_exprt &);
   NODISCARD resultt<> simplify_abs(const abs_exprt &);
-  bool simplify_sign(exprt &expr);
+  NODISCARD resultt<> simplify_sign(const sign_exprt &);
   NODISCARD resultt<> simplify_popcount(const popcount_exprt &);
-  NODISCARD resultt<> simplify_complex(const exprt &);
+  NODISCARD resultt<> simplify_complex(const unary_exprt &);
 
   /// Attempt to simplify mathematical function applications if we have
   /// enough information to do so. Currently focused on constant comparisons.
@@ -196,16 +203,16 @@ class simplify_exprt
   static tvt objects_equal(const exprt &a, const exprt &b);
   static tvt objects_equal_address_of(const exprt &a, const exprt &b);
   NODISCARD resultt<> simplify_address_of_arg(const exprt &);
-  bool simplify_inequality_both_constant(exprt &);
-  bool simplify_inequality_no_constant(exprt &);
-  bool simplify_inequality_rhs_is_constant(exprt &);
-  bool simplify_inequality_address_of(exprt &expr);
-  bool simplify_inequality_pointer_object(exprt &expr);
+  NODISCARD resultt<> simplify_inequality_both_constant(const exprt &);
+  NODISCARD resultt<> simplify_inequality_no_constant(const exprt &);
+  NODISCARD resultt<> simplify_inequality_rhs_is_constant(const exprt &);
+  NODISCARD resultt<> simplify_inequality_address_of(const exprt &);
+  NODISCARD resultt<> simplify_inequality_pointer_object(const exprt &);
 
   // main recursion
   bool simplify_node(exprt &expr);
   bool simplify_node_preorder(exprt &expr);
-  bool simplify_rec(exprt &expr);
+  NODISCARD resultt<> simplify_rec(const exprt &);
 
   virtual bool simplify(exprt &expr);
 
diff --git a/src/util/simplify_expr_if.cpp b/src/util/simplify_expr_if.cpp
new file mode 100644
index 00000000000..e019cff7e34
--- /dev/null
+++ b/src/util/simplify_expr_if.cpp
@@ -0,0 +1,420 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include "simplify_expr_class.h"
+
+#include "arith_tools.h"
+#include "expr_util.h"
+#include "range.h"
+#include "std_expr.h"
+
+bool simplify_exprt::simplify_if_implies(
+  exprt &expr,
+  const exprt &cond,
+  bool truth,
+  bool &new_truth)
+{
+  if(expr == cond)
+  {
+    new_truth = truth;
+    return false;
+  }
+
+  if(truth && cond.id() == ID_lt && expr.id() == ID_lt)
+  {
+    if(
+      cond.op0() == expr.op0() && cond.op1().is_constant() &&
+      expr.op1().is_constant() && cond.op1().type() == expr.op1().type())
+    {
+      mp_integer i1, i2;
+
+      if(
+        !to_integer(to_constant_expr(cond.op1()), i1) &&
+        !to_integer(to_constant_expr(expr.op1()), i2))
+      {
+        if(i1 >= i2)
+        {
+          new_truth = true;
+          return false;
+        }
+      }
+    }
+
+    if(
+      cond.op1() == expr.op1() && cond.op0().is_constant() &&
+      expr.op0().is_constant() && cond.op0().type() == expr.op0().type())
+    {
+      mp_integer i1, i2;
+
+      if(
+        !to_integer(to_constant_expr(cond.op0()), i1) &&
+        !to_integer(to_constant_expr(expr.op0()), i2))
+      {
+        if(i1 <= i2)
+        {
+          new_truth = true;
+          return false;
+        }
+      }
+    }
+  }
+
+  return true;
+}
+
+bool simplify_exprt::simplify_if_recursive(
+  exprt &expr,
+  const exprt &cond,
+  bool truth)
+{
+  if(expr.type().id() == ID_bool)
+  {
+    bool new_truth;
+
+    if(!simplify_if_implies(expr, cond, truth, new_truth))
+    {
+      if(new_truth)
+      {
+        expr = true_exprt();
+        return false;
+      }
+      else
+      {
+        expr = false_exprt();
+        return false;
+      }
+    }
+  }
+
+  bool no_change = true;
+
+  Forall_operands(it, expr)
+    no_change = simplify_if_recursive(*it, cond, truth) && no_change;
+
+  return no_change;
+}
+
+bool simplify_exprt::simplify_if_conj(exprt &expr, const exprt &cond)
+{
+  forall_operands(it, cond)
+  {
+    if(expr == *it)
+    {
+      expr = true_exprt();
+      return false;
+    }
+  }
+
+  bool no_change = true;
+
+  Forall_operands(it, expr)
+    no_change = simplify_if_conj(*it, cond) && no_change;
+
+  return no_change;
+}
+
+bool simplify_exprt::simplify_if_disj(exprt &expr, const exprt &cond)
+{
+  forall_operands(it, cond)
+  {
+    if(expr == *it)
+    {
+      expr = false_exprt();
+      return false;
+    }
+  }
+
+  bool no_change = true;
+
+  Forall_operands(it, expr)
+    no_change = simplify_if_disj(*it, cond) && no_change;
+
+  return no_change;
+}
+
+bool simplify_exprt::simplify_if_branch(
+  exprt &trueexpr,
+  exprt &falseexpr,
+  const exprt &cond)
+{
+  bool tno_change = true;
+  bool fno_change = true;
+
+  if(cond.id() == ID_and)
+  {
+    tno_change = simplify_if_conj(trueexpr, cond) && tno_change;
+    fno_change = simplify_if_recursive(falseexpr, cond, false) && fno_change;
+  }
+  else if(cond.id() == ID_or)
+  {
+    tno_change = simplify_if_recursive(trueexpr, cond, true) && tno_change;
+    fno_change = simplify_if_disj(falseexpr, cond) && fno_change;
+  }
+  else
+  {
+    tno_change = simplify_if_recursive(trueexpr, cond, true) && tno_change;
+    fno_change = simplify_if_recursive(falseexpr, cond, false) && fno_change;
+  }
+
+  if(!tno_change)
+    trueexpr = simplify_rec(trueexpr); // recursive call
+  if(!fno_change)
+    falseexpr = simplify_rec(falseexpr); // recursive call
+
+  return tno_change && fno_change;
+}
+
+bool simplify_exprt::simplify_if_cond(exprt &expr)
+{
+  bool no_change = true;
+  bool tmp = false;
+
+  while(!tmp)
+  {
+    tmp = true;
+
+    if(expr.id() == ID_and)
+    {
+      if(expr.has_operands())
+      {
+        exprt::operandst &operands = expr.operands();
+        for(exprt::operandst::iterator it1 = operands.begin();
+            it1 != operands.end();
+            it1++)
+        {
+          for(exprt::operandst::iterator it2 = operands.begin();
+              it2 != operands.end();
+              it2++)
+          {
+            if(it1 != it2)
+              tmp = simplify_if_recursive(*it1, *it2, true) && tmp;
+          }
+        }
+      }
+    }
+
+    if(!tmp)
+      expr = simplify_rec(expr); // recursive call
+
+    no_change = tmp && no_change;
+  }
+
+  return no_change;
+}
+
+bool simplify_exprt::simplify_if_preorder(if_exprt &expr)
+{
+  exprt &cond = expr.cond();
+  exprt &truevalue = expr.true_case();
+  exprt &falsevalue = expr.false_case();
+
+  bool no_change = true;
+
+  // we first want to look at the condition
+  auto r_cond = simplify_rec(cond);
+  if(r_cond.has_changed())
+  {
+    cond = r_cond.expr;
+    no_change = false;
+  }
+
+  // 1 ? a : b -> a  and  0 ? a : b -> b
+  if(cond.is_constant())
+  {
+    exprt tmp = cond.is_true() ? truevalue : falsevalue;
+    tmp = simplify_rec(tmp);
+    expr.swap(tmp);
+    return false;
+  }
+
+  if(do_simplify_if)
+  {
+    if(cond.id() == ID_not)
+    {
+      exprt tmp;
+      tmp.swap(cond.op0());
+      cond.swap(tmp);
+      truevalue.swap(falsevalue);
+      no_change = false;
+    }
+
+#ifdef USE_LOCAL_REPLACE_MAP
+    replace_mapt map_before(local_replace_map);
+
+    // a ? b : c  --> a ? b[a/true] : c
+    if(cond.id() == ID_and)
+    {
+      forall_operands(it, cond)
+      {
+        if(it->id() == ID_not)
+          local_replace_map.insert(std::make_pair(it->op0(), false_exprt()));
+        else
+          local_replace_map.insert(std::make_pair(*it, true_exprt()));
+      }
+    }
+    else
+      local_replace_map.insert(std::make_pair(cond, true_exprt()));
+
+    auto r_truevalue = simplify_rec(truevalue);
+    if(r_truevalue.has_changed())
+    {
+      truevalue = r_truevalue.expr;
+      no_change = false;
+    }
+
+    local_replace_map = map_before;
+
+    // a ? b : c  --> a ? b : c[a/false]
+    if(cond.id() == ID_or)
+    {
+      forall_operands(it, cond)
+      {
+        if(it->id() == ID_not)
+          local_replace_map.insert(std::make_pair(it->op0(), true_exprt()));
+        else
+          local_replace_map.insert(std::make_pair(*it, false_exprt()));
+      }
+    }
+    else
+      local_replace_map.insert(std::make_pair(cond, false_exprt()));
+
+    auto r_falsevalue = simplify_rec(falsevalue);
+    if(r_falsevalue.has_changed())
+    {
+      falsevalue = r_falsevalue.expr;
+      no_change = false;
+    }
+
+    local_replace_map.swap(map_before);
+#else
+    auto r_truevalue = simplify_rec(truevalue);
+    if(r_truevalue.has_changed())
+    {
+      truevalue = r_truevalue.expr;
+      no_change = false;
+    }
+    auto r_falsevalue = simplify_rec(falsevalue);
+    if(r_falsevalue.has_changed())
+    {
+      falsevalue = r_falsevalue.expr;
+      no_change = false;
+    }
+#endif
+  }
+  else
+  {
+    auto r_truevalue = simplify_rec(truevalue);
+    if(r_truevalue.has_changed())
+    {
+      truevalue = r_truevalue.expr;
+      no_change = false;
+    }
+    auto r_falsevalue = simplify_rec(falsevalue);
+    if(r_falsevalue.has_changed())
+    {
+      falsevalue = r_falsevalue.expr;
+      no_change = false;
+    }
+  }
+
+  return no_change;
+}
+
+simplify_exprt::resultt<> simplify_exprt::simplify_if(const if_exprt &expr)
+{
+  const exprt &cond = expr.cond();
+  const exprt &truevalue = expr.true_case();
+  const exprt &falsevalue = expr.false_case();
+
+  if(do_simplify_if)
+  {
+#if 0
+    no_change = simplify_if_cond(cond) && no_change;
+    no_change = simplify_if_branch(truevalue, falsevalue, cond) && no_change;
+#endif
+
+    if(expr.type() == bool_typet())
+    {
+      // a?b:c <-> (a && b) || (!a && c)
+
+      if(truevalue.is_true() && falsevalue.is_false())
+      {
+        // a?1:0 <-> a
+        return cond;
+      }
+      else if(truevalue.is_false() && falsevalue.is_true())
+      {
+        // a?0:1 <-> !a
+        exprt tmp = boolean_negate(cond);
+        simplify_node(tmp);
+        return std::move(tmp);
+      }
+      else if(falsevalue.is_false())
+      {
+        // a?b:0 <-> a AND b
+        and_exprt tmp(cond, truevalue);
+        simplify_node(tmp);
+        return std::move(tmp);
+      }
+      else if(falsevalue.is_true())
+      {
+        // a?b:1 <-> !a OR b
+        exprt tmp_not_cond = boolean_negate(cond);
+        simplify_node(tmp_not_cond);
+        or_exprt tmp(tmp_not_cond, truevalue);
+        simplify_node(tmp);
+        return std::move(tmp);
+      }
+      else if(truevalue.is_true())
+      {
+        // a?1:b <-> a||(!a && b) <-> a OR b
+        or_exprt tmp(cond, falsevalue);
+        simplify_node(tmp);
+        return std::move(tmp);
+      }
+      else if(truevalue.is_false())
+      {
+        // a?0:b <-> !a && b
+        exprt tmp_not_cond = boolean_negate(cond);
+        simplify_node(tmp_not_cond);
+        and_exprt tmp(tmp_not_cond, falsevalue);
+        simplify_node(tmp);
+        return std::move(tmp);
+      }
+    }
+  }
+
+  if(truevalue == falsevalue)
+    return truevalue;
+
+  // this pushes the if-then-else into struct and array constructors
+  if(
+    ((truevalue.id() == ID_struct && falsevalue.id() == ID_struct) ||
+     (truevalue.id() == ID_array && falsevalue.id() == ID_array)) &&
+    truevalue.operands().size() == falsevalue.operands().size())
+  {
+    exprt cond_copy = cond;
+    exprt falsevalue_copy = falsevalue;
+    exprt truevalue_copy = truevalue;
+
+    auto range_false = make_range(falsevalue_copy.operands());
+    auto range_true = make_range(truevalue_copy.operands());
+    auto new_expr = truevalue;
+    new_expr.operands().clear();
+
+    for(const auto &pair : range_true.zip(range_false))
+    {
+      new_expr.operands().push_back(
+        simplify_if(if_exprt(cond_copy, pair.first, pair.second)));
+    }
+
+    return std::move(new_expr);
+  }
+
+  return unchanged(expr);
+}
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index 0ea1ee50bb0..cd4aed6d928 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -771,20 +771,17 @@ simplify_exprt::resultt<> simplify_exprt::simplify_bitwise(const exprt &expr)
     return std::move(new_expr);
 }
 
-simplify_exprt::resultt<> simplify_exprt::simplify_extractbit(const exprt &expr)
+simplify_exprt::resultt<>
+simplify_exprt::simplify_extractbit(const extractbit_exprt &expr)
 {
-  PRECONDITION(expr.id() == ID_extractbit);
-  const auto &extractbit_expr = to_extractbit_expr(expr);
-
-  const typet &src_type = extractbit_expr.src().type();
+  const typet &src_type = expr.src().type();
 
   if(!is_bitvector_type(src_type))
     return unchanged(expr);
 
   const std::size_t src_bit_width = to_bitvector_type(src_type).get_width();
 
-  const auto index_converted_to_int =
-    numeric_cast<mp_integer>(extractbit_expr.index());
+  const auto index_converted_to_int = numeric_cast<mp_integer>(expr.index());
   if(
     !index_converted_to_int.has_value() || *index_converted_to_int < 0 ||
     *index_converted_to_int >= src_bit_width)
@@ -792,11 +789,11 @@ simplify_exprt::resultt<> simplify_exprt::simplify_extractbit(const exprt &expr)
     return unchanged(expr);
   }
 
-  if(!extractbit_expr.src().is_constant())
+  if(!expr.src().is_constant())
     return unchanged(expr);
 
   const bool bit = get_bvrep_bit(
-    to_constant_expr(extractbit_expr.src()).get_value(),
+    to_constant_expr(expr.src()).get_value(),
     src_bit_width,
     numeric_cast_v<std::size_t>(*index_converted_to_int));
 
@@ -804,7 +801,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_extractbit(const exprt &expr)
 }
 
 simplify_exprt::resultt<>
-simplify_exprt::simplify_concatenation(const exprt &expr)
+simplify_exprt::simplify_concatenation(const concatenation_exprt &expr)
 {
   bool no_change = true;
 
@@ -1111,25 +1108,20 @@ simplify_exprt::simplify_extractbits(const extractbits_exprt &expr)
   return unchanged(expr);
 }
 
-simplify_exprt::resultt<> simplify_exprt::simplify_unary_plus(const exprt &expr)
+simplify_exprt::resultt<>
+simplify_exprt::simplify_unary_plus(const unary_plus_exprt &expr)
 {
-  if(expr.operands().size()!=1)
-    return unchanged(expr);
-
   // simply remove, this is always 'nop'
-  return expr.op0();
+  return expr.op();
 }
 
 simplify_exprt::resultt<>
-simplify_exprt::simplify_unary_minus(const exprt &expr)
+simplify_exprt::simplify_unary_minus(const unary_minus_exprt &expr)
 {
-  if(expr.operands().size()!=1)
-    return unchanged(expr);
-
   if(!is_number(expr.type()))
     return unchanged(expr);
 
-  const exprt &operand = expr.op0();
+  const exprt &operand = expr.op();
 
   if(expr.type()!=operand.type())
     return unchanged(expr);
@@ -1137,23 +1129,21 @@ simplify_exprt::simplify_unary_minus(const exprt &expr)
   if(operand.id()==ID_unary_minus)
   {
     // cancel out "-(-x)" to "x"
-    if(operand.operands().size()!=1)
-      return unchanged(expr);
-
-    if(!is_number(operand.op0().type()))
+    if(!is_number(to_unary_minus_expr(operand).op().type()))
       return unchanged(expr);
 
-    return expr.op0().op0();
+    return to_unary_minus_expr(operand).op();
   }
   else if(operand.id()==ID_constant)
   {
     const irep_idt &type_id=expr.type().id();
+    const auto &constant_expr = to_constant_expr(operand);
 
     if(type_id==ID_integer ||
        type_id==ID_signedbv ||
        type_id==ID_unsignedbv)
     {
-      const auto int_value = numeric_cast<mp_integer>(expr.op0());
+      const auto int_value = numeric_cast<mp_integer>(constant_expr);
 
       if(!int_value.has_value())
         return unchanged(expr);
@@ -1163,20 +1153,20 @@ simplify_exprt::simplify_unary_minus(const exprt &expr)
     else if(type_id==ID_rational)
     {
       rationalt r;
-      if(to_rational(expr.op0(), r))
+      if(to_rational(constant_expr, r))
         return unchanged(expr);
 
       return from_rational(-r);
     }
     else if(type_id==ID_fixedbv)
     {
-      fixedbvt f(to_constant_expr(expr.op0()));
+      fixedbvt f(constant_expr);
       f.negate();
       return f.to_expr();
     }
     else if(type_id==ID_floatbv)
     {
-      ieee_floatt f(to_constant_expr(expr.op0()));
+      ieee_floatt f(constant_expr);
       f.negate();
       return f.to_expr();
     }
@@ -1185,14 +1175,10 @@ simplify_exprt::simplify_unary_minus(const exprt &expr)
   return unchanged(expr);
 }
 
-simplify_exprt::resultt<> simplify_exprt::simplify_bitnot(const exprt &expr)
+simplify_exprt::resultt<>
+simplify_exprt::simplify_bitnot(const bitnot_exprt &expr)
 {
-  const exprt::operandst &operands = expr.operands();
-
-  if(operands.size()!=1)
-    return unchanged(expr);
-
-  const exprt &op = operands.front();
+  const exprt &op = expr.op();
 
   const auto &type = expr.type();
 
@@ -1220,39 +1206,39 @@ simplify_exprt::resultt<> simplify_exprt::simplify_bitnot(const exprt &expr)
 }
 
 /// simplifies inequalities !=, <=, <, >=, >, and also ==
-bool simplify_exprt::simplify_inequality(exprt &expr)
+simplify_exprt::resultt<> simplify_exprt::simplify_inequality(const exprt &expr)
 {
-  exprt::operandst &operands=expr.operands();
+  const exprt::operandst &operands = expr.operands();
 
   if(expr.type().id()!=ID_bool)
-    return true;
+    return unchanged(expr);
 
   if(operands.size()!=2)
-    return true;
+    return unchanged(expr);
 
   exprt tmp0=expr.op0();
   exprt tmp1=expr.op1();
 
   // types must match
   if(tmp0.type() != tmp1.type())
-    return true;
+    return unchanged(expr);
 
   // if rhs is ID_if (and lhs is not), swap operands for == and !=
   if((expr.id()==ID_equal || expr.id()==ID_notequal) &&
      tmp0.id()!=ID_if &&
      tmp1.id()==ID_if)
   {
-    expr.op0().swap(expr.op1());
-    return simplify_inequality(expr);
+    auto new_expr = expr;
+    new_expr.op0().swap(new_expr.op1());
+    return changed(simplify_inequality(new_expr)); // recursive call
   }
 
   if(tmp0.id()==ID_if && tmp0.operands().size()==3)
   {
     if_exprt if_expr=lift_if(expr, 0);
-    simplify_inequality(if_expr.true_case());
-    simplify_inequality(if_expr.false_case());
-    expr = simplify_if(if_expr).expr;
-    return false;
+    if_expr.true_case() = simplify_inequality(if_expr.true_case());
+    if_expr.false_case() = simplify_inequality(if_expr.false_case());
+    return changed(simplify_if(if_expr));
   }
 
   // see if we are comparing pointers that are address_of
@@ -1261,12 +1247,16 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
       (tmp1.id()==ID_address_of ||
        (tmp1.id()==ID_typecast && tmp1.op0().id()==ID_address_of)) &&
       (expr.id()==ID_equal || expr.id()==ID_notequal))
+  {
     return simplify_inequality_address_of(expr);
+  }
 
   if(tmp0.id()==ID_pointer_object &&
      tmp1.id()==ID_pointer_object &&
      (expr.id()==ID_equal || expr.id()==ID_notequal))
+  {
     return simplify_inequality_pointer_object(expr);
+  }
 
   if(tmp0.type().id()==ID_c_enum_tag)
     tmp0.type()=ns.follow_tag(to_c_enum_tag_type(tmp0.type()));
@@ -1286,20 +1276,21 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
   {
     // we want the constant on the RHS
 
+    exprt new_expr = expr;
+
     if(expr.id()==ID_ge)
-      expr.id(ID_le);
+      new_expr.id(ID_le);
     else if(expr.id()==ID_le)
-      expr.id(ID_ge);
+      new_expr.id(ID_ge);
     else if(expr.id()==ID_gt)
-      expr.id(ID_lt);
+      new_expr.id(ID_lt);
     else if(expr.id()==ID_lt)
-      expr.id(ID_gt);
+      new_expr.id(ID_gt);
 
-    expr.op0().swap(expr.op1());
+    new_expr.op0().swap(new_expr.op1());
 
     // RHS is constant, LHS is not
-    simplify_inequality_rhs_is_constant(expr);
-    return false;
+    return changed(simplify_inequality_rhs_is_constant(new_expr));
   }
   else if(tmp1_const)
   {
@@ -1315,7 +1306,8 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
 
 /// simplifies inequalities for the case in which both sides
 /// of the inequality are constants
-bool simplify_exprt::simplify_inequality_both_constant(exprt &expr)
+simplify_exprt::resultt<>
+simplify_exprt::simplify_inequality_both_constant(const exprt &expr)
 {
   PRECONDITION(expr.operands().size() == 2);
 
@@ -1346,12 +1338,11 @@ bool simplify_exprt::simplify_inequality_both_constant(exprt &expr)
       {
         // if NULL is not zero on this platform, we really don't know what it
         // is and therefore cannot simplify
-        return true;
+        return unchanged(expr);
       }
       equal = tmp0_const.is_zero() && tmp1_const.is_zero();
     }
-    expr = make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
-    return false;
+    return make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
   }
 
   if(tmp0.type().id() == ID_fixedbv)
@@ -1360,17 +1351,15 @@ bool simplify_exprt::simplify_inequality_both_constant(exprt &expr)
     fixedbvt f1(tmp1_const);
 
     if(expr.id() == ID_ge)
-      expr = make_boolean_expr(f0 >= f1);
+      return make_boolean_expr(f0 >= f1);
     else if(expr.id() == ID_le)
-      expr = make_boolean_expr(f0 <= f1);
+      return make_boolean_expr(f0 <= f1);
     else if(expr.id() == ID_gt)
-      expr = make_boolean_expr(f0 > f1);
+      return make_boolean_expr(f0 > f1);
     else if(expr.id() == ID_lt)
-      expr = make_boolean_expr(f0 < f1);
+      return make_boolean_expr(f0 < f1);
     else
       UNREACHABLE;
-
-    return false;
   }
   else if(tmp0.type().id() == ID_floatbv)
   {
@@ -1378,65 +1367,59 @@ bool simplify_exprt::simplify_inequality_both_constant(exprt &expr)
     ieee_floatt f1(tmp1_const);
 
     if(expr.id() == ID_ge)
-      expr = make_boolean_expr(f0 >= f1);
+      return make_boolean_expr(f0 >= f1);
     else if(expr.id() == ID_le)
-      expr = make_boolean_expr(f0 <= f1);
+      return make_boolean_expr(f0 <= f1);
     else if(expr.id() == ID_gt)
-      expr = make_boolean_expr(f0 > f1);
+      return make_boolean_expr(f0 > f1);
     else if(expr.id() == ID_lt)
-      expr = make_boolean_expr(f0 < f1);
+      return make_boolean_expr(f0 < f1);
     else
       UNREACHABLE;
-
-    return false;
   }
   else if(tmp0.type().id() == ID_rational)
   {
     rationalt r0, r1;
 
     if(to_rational(tmp0, r0))
-      return true;
+      return unchanged(expr);
 
     if(to_rational(tmp1, r1))
-      return true;
+      return unchanged(expr);
 
     if(expr.id() == ID_ge)
-      expr = make_boolean_expr(r0 >= r1);
+      return make_boolean_expr(r0 >= r1);
     else if(expr.id() == ID_le)
-      expr = make_boolean_expr(r0 <= r1);
+      return make_boolean_expr(r0 <= r1);
     else if(expr.id() == ID_gt)
-      expr = make_boolean_expr(r0 > r1);
+      return make_boolean_expr(r0 > r1);
     else if(expr.id() == ID_lt)
-      expr = make_boolean_expr(r0 < r1);
+      return make_boolean_expr(r0 < r1);
     else
       UNREACHABLE;
-
-    return false;
   }
   else
   {
     const auto v0 = numeric_cast<mp_integer>(tmp0_const);
 
     if(!v0.has_value())
-      return true;
+      return unchanged(expr);
 
     const auto v1 = numeric_cast<mp_integer>(tmp1_const);
 
     if(!v1.has_value())
-      return true;
+      return unchanged(expr);
 
     if(expr.id() == ID_ge)
-      expr = make_boolean_expr(*v0 >= *v1);
+      return make_boolean_expr(*v0 >= *v1);
     else if(expr.id() == ID_le)
-      expr = make_boolean_expr(*v0 <= *v1);
+      return make_boolean_expr(*v0 <= *v1);
     else if(expr.id() == ID_gt)
-      expr = make_boolean_expr(*v0 > *v1);
+      return make_boolean_expr(*v0 > *v1);
     else if(expr.id() == ID_lt)
-      expr = make_boolean_expr(*v0 < *v1);
+      return make_boolean_expr(*v0 < *v1);
     else
       UNREACHABLE;
-
-    return false;
   }
 }
 
@@ -1488,50 +1471,53 @@ bool simplify_exprt::eliminate_common_addends(
   return true;
 }
 
-bool simplify_exprt::simplify_inequality_no_constant(exprt &expr)
+simplify_exprt::resultt<>
+simplify_exprt::simplify_inequality_no_constant(const exprt &expr)
 {
-  exprt::operandst &operands=expr.operands();
-
   // pretty much all of the simplifications below are unsound
   // for IEEE float because of NaN!
 
   if(expr.op0().type().id() == ID_floatbv)
-    return true;
+    return unchanged(expr);
 
   // eliminate strict inequalities
   if(expr.id()==ID_notequal)
   {
-    expr.id(ID_equal);
-    simplify_inequality_no_constant(expr);
-    expr = boolean_negate(expr);
-    simplify_node(expr);
-    return false;
+    auto new_expr = expr;
+    new_expr.id(ID_equal);
+    new_expr = simplify_inequality_no_constant(new_expr);
+    new_expr = boolean_negate(new_expr);
+    simplify_node(new_expr);
+    return std::move(new_expr);
   }
   else if(expr.id()==ID_gt)
   {
-    expr.id(ID_ge);
+    auto new_expr = expr;
+    new_expr.id(ID_ge);
     // swap operands
-    expr.op0().swap(expr.op1());
-    simplify_inequality_no_constant(expr);
-    expr = boolean_negate(expr);
-    simplify_node(expr);
-    return false;
+    new_expr.op0().swap(new_expr.op1());
+    new_expr = simplify_inequality_no_constant(new_expr);
+    new_expr = boolean_negate(new_expr);
+    simplify_node(new_expr);
+    return std::move(new_expr);
   }
   else if(expr.id()==ID_lt)
   {
-    expr.id(ID_ge);
-    simplify_inequality_no_constant(expr);
-    expr = boolean_negate(expr);
-    simplify_node(expr);
-    return false;
+    auto new_expr = expr;
+    new_expr.id(ID_ge);
+    new_expr = simplify_inequality_no_constant(new_expr);
+    new_expr = boolean_negate(new_expr);
+    simplify_node(new_expr);
+    return std::move(new_expr);
   }
   else if(expr.id()==ID_le)
   {
-    expr.id(ID_ge);
+    auto new_expr = expr;
+    new_expr.id(ID_ge);
     // swap operands
-    expr.op0().swap(expr.op1());
-    simplify_inequality_no_constant(expr);
-    return false;
+    new_expr.op0().swap(new_expr.op1());
+    new_expr = simplify_inequality_no_constant(new_expr);
+    return std::move(new_expr);
   }
 
   // now we only have >=, =
@@ -1542,11 +1528,8 @@ bool simplify_exprt::simplify_inequality_no_constant(exprt &expr)
 
   // syntactically equal?
 
-  if(operands.front()==operands.back())
-  {
-    expr=true_exprt();
-    return false;
-  }
+  if(expr.op0() == expr.op1())
+    return true_exprt();
 
   // try constants
 
@@ -1594,8 +1577,7 @@ bool simplify_exprt::simplify_inequality_no_constant(exprt &expr)
 
     if(ok)
     {
-      expr = make_boolean_expr(result);
-      return false;
+      return make_boolean_expr(result);
     }
   }
 
@@ -1603,22 +1585,24 @@ bool simplify_exprt::simplify_inequality_no_constant(exprt &expr)
   // On bit-vectors, this is only sound on '='.
   if(expr.id()==ID_equal)
   {
-    if(!eliminate_common_addends(expr.op0(), expr.op1()))
+    auto new_expr = expr;
+    if(!eliminate_common_addends(new_expr.op0(), new_expr.op1()))
     {
       // remove zeros
-      simplify_node(expr.op0());
-      simplify_node(expr.op1());
-      simplify_inequality(expr); // recursive call
-      return false;
+      simplify_node(new_expr.op0());
+      simplify_node(new_expr.op1());
+      new_expr = simplify_inequality(new_expr); // recursive call
+      return std::move(new_expr);
     }
   }
 
-  return true;
+  return unchanged(expr);
 }
 
 /// \par expr: an inequality where the RHS is a constant
 /// and the LHS is not
-bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr)
+simplify_exprt::resultt<>
+simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr)
 {
   // the constant is always on the RHS
   PRECONDITION(expr.op1().is_constant());
@@ -1626,10 +1610,11 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr)
   if(expr.op0().id()==ID_if && expr.op0().operands().size()==3)
   {
     if_exprt if_expr=lift_if(expr, 0);
-    simplify_inequality_rhs_is_constant(if_expr.true_case());
-    simplify_inequality_rhs_is_constant(if_expr.false_case());
-    expr = simplify_if(if_expr);
-    return false;
+    if_expr.true_case() =
+      simplify_inequality_rhs_is_constant(if_expr.true_case());
+    if_expr.false_case() =
+      simplify_inequality_rhs_is_constant(if_expr.false_case());
+    return changed(simplify_if(if_expr));
   }
 
   // do we deal with pointers?
@@ -1637,11 +1622,12 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr)
   {
     if(expr.id()==ID_notequal)
     {
-      expr.id(ID_equal);
-      simplify_inequality_rhs_is_constant(expr);
-      expr = boolean_negate(expr);
-      simplify_node(expr);
-      return false;
+      auto new_expr = expr;
+      new_expr.id(ID_equal);
+      new_expr = simplify_inequality_rhs_is_constant(new_expr);
+      new_expr = boolean_negate(new_expr);
+      simplify_node(new_expr);
+      return std::move(new_expr);
     }
 
     // very special case for pointers
@@ -1661,8 +1647,7 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr)
           expr.op0().op0().id() == ID_index ||
           expr.op0().op0().id() == ID_string_constant)
         {
-          expr=false_exprt();
-          return false;
+          return false_exprt();
         }
       }
       else if(expr.op0().id()==ID_typecast &&
@@ -1678,8 +1663,7 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr)
           expr.op0().op0().op0().id() == ID_index ||
           expr.op0().op0().op0().id() == ID_string_constant)
         {
-          expr=false_exprt();
-          return false;
+          return false_exprt();
         }
       }
       else if(expr.op0().id()==ID_typecast &&
@@ -1691,18 +1675,18 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr)
         // (type)ptr == NULL -> ptr == NULL
         // note that 'ptr' may be an integer
         exprt op=expr.op0().op0();
-        expr.op0().swap(op);
-        if(expr.op0().type().id()!=ID_pointer)
-          expr.op1()=from_integer(0, expr.op0().type());
+        auto new_expr = expr;
+        new_expr.op0().swap(op);
+        if(new_expr.op0().type().id() != ID_pointer)
+          new_expr.op1() = from_integer(0, new_expr.op0().type());
         else
-          expr.op1().type()=expr.op0().type();
-        simplify_inequality(expr); // do again!
-        return false;
+          new_expr.op1().type() = new_expr.op0().type();
+        return changed(simplify_inequality(new_expr)); // do again!
       }
     }
 
     // all we are doing with pointers
-    return true;
+    return unchanged(expr);
   }
 
   // is it a separation predicate?
@@ -1714,9 +1698,10 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr)
     if(expr.id()==ID_equal || expr.id()==ID_notequal)
     {
       mp_integer constant=0;
-      bool changed=false;
+      bool op_changed = false;
+      auto new_expr = expr;
 
-      Forall_operands(it, expr.op0())
+      Forall_operands(it, new_expr.op0())
       {
         if(it->is_constant())
         {
@@ -1725,21 +1710,21 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr)
           {
             constant+=i;
             *it=from_integer(0, it->type());
-            changed=true;
+            op_changed = true;
           }
         }
       }
 
-      if(changed)
+      if(op_changed)
       {
         // adjust the constant on the RHS
-        mp_integer i = numeric_cast_v<mp_integer>(to_constant_expr(expr.op1()));
+        mp_integer i =
+          numeric_cast_v<mp_integer>(to_constant_expr(new_expr.op1()));
         i-=constant;
-        expr.op1()=from_integer(i, expr.op1().type());
+        new_expr.op1() = from_integer(i, new_expr.op1().type());
 
-        expr.op0() = simplify_plus(to_plus_expr(expr.op0()));
-        simplify_inequality(expr);
-        return false;
+        new_expr.op0() = simplify_plus(to_plus_expr(new_expr.op0()));
+        return changed(simplify_inequality(new_expr));
       }
     }
   }
@@ -1765,8 +1750,7 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr)
       exprt result=expr;
       result.op0()=expr.op0().op0();
       result.op1()=const_val_converted.to_expr();
-      expr.swap(result);
-      return false;
+      return std::move(result);
     }
   }
   #endif
@@ -1779,11 +1763,11 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr)
        expr.op0().type().id()==ID_unsignedbv)
     {
       // zero is always smaller or equal something unsigned
-      expr=true_exprt();
-      return false;
+      return true_exprt();
     }
 
-    exprt &operand=expr.op0();
+    auto new_expr = expr;
+    exprt &operand = new_expr.op0();
 
     if(expr.id()==ID_equal)
     {
@@ -1791,11 +1775,13 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr)
       if(operand.id()==ID_unary_minus)
       {
         if(operand.operands().size()!=1)
-          return true;
+          return unchanged(expr);
+
         exprt tmp;
         tmp.swap(operand.op0());
         operand.swap(tmp);
-        return false;
+
+        return std::move(new_expr);
       }
       else if(operand.id()==ID_plus)
       {
@@ -1815,8 +1801,7 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr)
             tmp.operands().resize(2);
             tmp.op0().swap(operand.op0());
             tmp.op1().swap(operand.op1().op0());
-            expr.swap(tmp);
-            return false;
+            return std::move(tmp);
           }
         }
       }
@@ -1831,15 +1816,13 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr)
     // we re-write (TYPE)boolean == 0 -> !boolean
     if(expr.op1().is_zero() && expr.id()==ID_equal)
     {
-      expr = boolean_negate(expr.op0().op0());
-      return false;
+      return boolean_negate(expr.op0().op0());
     }
 
     // we re-write (TYPE)boolean != 0 -> boolean
     if(expr.op1().is_zero() && expr.id()==ID_notequal)
     {
-      expr=expr.op0().op0();
-      return false;
+      return expr.op0().op0();
     }
   }
 
@@ -1853,11 +1836,12 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr)
 
     if(expr.id()==ID_notequal)
     {
-      expr.id(ID_equal);
-      simplify_inequality_rhs_is_constant(expr);
-      expr = boolean_negate(expr);
-      simplify_node(expr);
-      return false;
+      auto new_expr = expr;
+      new_expr.id(ID_equal);
+      new_expr = simplify_inequality_rhs_is_constant(new_expr);
+      new_expr = boolean_negate(new_expr);
+      simplify_node(new_expr);
+      return std::move(new_expr);
     }
     else if(expr.id()==ID_gt)
     {
@@ -1865,23 +1849,23 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr)
 
       if(i==max)
       {
-        expr=false_exprt();
-        return false;
+        return false_exprt();
       }
 
-      expr.id(ID_ge);
+      auto new_expr = expr;
+      new_expr.id(ID_ge);
       ++i;
-      expr.op1()=from_integer(i, expr.op1().type());
-      simplify_inequality_rhs_is_constant(expr);
-      return false;
+      new_expr.op1() = from_integer(i, new_expr.op1().type());
+      return changed(simplify_inequality_rhs_is_constant(new_expr));
     }
     else if(expr.id()==ID_lt)
     {
-      expr.id(ID_ge);
-      simplify_inequality_rhs_is_constant(expr);
-      expr = boolean_negate(expr);
-      simplify_node(expr);
-      return false;
+      auto new_expr = expr;
+      new_expr.id(ID_ge);
+      new_expr = simplify_inequality_rhs_is_constant(new_expr);
+      new_expr = boolean_negate(new_expr);
+      simplify_node(new_expr);
+      return std::move(new_expr);
     }
     else if(expr.id()==ID_le)
     {
@@ -1889,19 +1873,19 @@ bool simplify_exprt::simplify_inequality_rhs_is_constant(exprt &expr)
 
       if(i==max)
       {
-        expr=true_exprt();
-        return false;
+        return true_exprt();
       }
 
-      expr.id(ID_ge);
+      auto new_expr = expr;
+      new_expr.id(ID_ge);
       ++i;
-      expr.op1()=from_integer(i, expr.op1().type());
-      simplify_inequality_rhs_is_constant(expr);
-      expr = boolean_negate(expr);
-      simplify_node(expr);
-      return false;
+      new_expr.op1() = from_integer(i, new_expr.op1().type());
+      new_expr = simplify_inequality_rhs_is_constant(new_expr);
+      new_expr = boolean_negate(new_expr);
+      simplify_node(new_expr);
+      return std::move(new_expr);
     }
   }
 #endif
-  return true;
+  return unchanged(expr);
 }
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
index 51cba08f5ab..a9bf5919bcc 100644
--- a/src/util/simplify_expr_pointer.cpp
+++ b/src/util/simplify_expr_pointer.cpp
@@ -69,8 +69,13 @@ simplify_exprt::simplify_address_of_arg(const exprt &expr)
       new_index_expr.array() = array_result.expr;
     }
 
-    if(!simplify_rec(new_index_expr.index()))
+    auto index_result = simplify_rec(new_index_expr.index());
+
+    if(index_result.has_changed())
+    {
       no_change = false;
+      new_index_expr.index() = index_result.expr;
+    }
 
     // rewrite (*(type *)int) [index] by
     // pushing the index inside
@@ -148,8 +153,12 @@ simplify_exprt::simplify_address_of_arg(const exprt &expr)
   else if(expr.id()==ID_dereference)
   {
     auto new_expr = to_dereference_expr(expr);
-    if(!simplify_rec(new_expr.pointer()))
+    auto r_pointer = simplify_rec(new_expr.pointer());
+    if(r_pointer.has_changed())
+    {
+      new_expr.pointer() = r_pointer.expr;
       return std::move(new_expr);
+    }
   }
   else if(expr.id()==ID_if)
   {
@@ -157,8 +166,12 @@ simplify_exprt::simplify_address_of_arg(const exprt &expr)
 
     bool no_change = true;
 
-    if(!simplify_rec(new_if_expr.cond()))
+    auto r_cond = simplify_rec(new_if_expr.cond());
+    if(r_cond.has_changed())
+    {
+      new_if_expr.cond() = r_cond.expr;
       no_change = false;
+    }
 
     auto true_result = simplify_address_of_arg(new_if_expr.true_case());
     if(true_result.has_changed())
@@ -231,18 +244,17 @@ simplify_exprt::simplify_address_of(const address_of_exprt &expr)
 }
 
 simplify_exprt::resultt<>
-simplify_exprt::simplify_pointer_offset(const exprt &expr)
+simplify_exprt::simplify_pointer_offset(const unary_exprt &expr)
 {
-  if(expr.operands().size()!=1)
-    return unchanged(expr);
-
-  const exprt &ptr = expr.op0();
+  const exprt &ptr = expr.op();
 
   if(ptr.id()==ID_if && ptr.operands().size()==3)
   {
     if_exprt if_expr=lift_if(expr, 0);
-    if_expr.true_case() = simplify_pointer_offset(if_expr.true_case());
-    if_expr.false_case() = simplify_pointer_offset(if_expr.false_case());
+    if_expr.true_case() =
+      simplify_pointer_offset(to_unary_expr(if_expr.true_case()));
+    if_expr.false_case() =
+      simplify_pointer_offset(to_unary_expr(if_expr.false_case()));
     return changed(simplify_if(if_expr));
   }
 
@@ -271,7 +283,7 @@ simplify_exprt::simplify_pointer_offset(const exprt &expr)
       // Cast from pointer to pointer.
       // This just passes through, remove typecast.
       auto new_expr = expr;
-      new_expr.op0() = ptr.op0();
+      new_expr.op() = ptr.op0();
 
       simplify_node(new_expr); // recursive call
       return new_expr;
@@ -421,7 +433,8 @@ simplify_exprt::simplify_pointer_offset(const exprt &expr)
   return unchanged(expr);
 }
 
-bool simplify_exprt::simplify_inequality_address_of(exprt &expr)
+simplify_exprt::resultt<>
+simplify_exprt::simplify_inequality_address_of(const exprt &expr)
 {
   PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
   PRECONDITION(expr.type().id() == ID_bool);
@@ -444,9 +457,9 @@ bool simplify_exprt::simplify_inequality_address_of(exprt &expr)
   INVARIANT(tmp1.id() == ID_address_of, "id must be ID_address_of");
 
   if(tmp0.operands().size()!=1)
-    return true;
+    return unchanged(expr);
   if(tmp1.operands().size()!=1)
-    return true;
+    return unchanged(expr);
 
   if(tmp0.op0().id()==ID_symbol &&
      tmp1.op0().id()==ID_symbol)
@@ -454,9 +467,7 @@ bool simplify_exprt::simplify_inequality_address_of(exprt &expr)
     bool equal = to_symbol_expr(tmp0.op0()).get_identifier() ==
                  to_symbol_expr(tmp1.op0()).get_identifier();
 
-    expr = make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
-
-    return false;
+    return make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
   }
   else if(
     tmp0.op0().id() == ID_dynamic_object &&
@@ -465,23 +476,20 @@ bool simplify_exprt::simplify_inequality_address_of(exprt &expr)
     bool equal = to_dynamic_object_expr(tmp0.op0()).get_instance() ==
                  to_dynamic_object_expr(tmp1.op0()).get_instance();
 
-    expr = make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
-
-    return false;
+    return make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
   }
   else if(
     (tmp0.op0().id() == ID_symbol && tmp1.op0().id() == ID_dynamic_object) ||
     (tmp0.op0().id() == ID_dynamic_object && tmp1.op0().id() == ID_symbol))
   {
-    expr = make_boolean_expr(expr.id() != ID_equal);
-
-    return false;
+    return make_boolean_expr(expr.id() != ID_equal);
   }
 
-  return true;
+  return unchanged(expr);
 }
 
-bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr)
+simplify_exprt::resultt<>
+simplify_exprt::simplify_inequality_pointer_object(const exprt &expr)
 {
   PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
   PRECONDITION(expr.type().id() == ID_bool);
@@ -502,12 +510,12 @@ bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr)
         (op.op0().id() != ID_symbol && op.op0().id() != ID_dynamic_object &&
          op.op0().id() != ID_string_constant))
       {
-        return true;
+        return unchanged(expr);
       }
     }
     else if(op.id() != ID_constant || !op.is_zero())
     {
-      return true;
+      return unchanged(expr);
     }
 
     if(new_inequality_ops.empty())
@@ -520,18 +528,17 @@ bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr)
     }
   }
 
-  expr.operands() = std::move(new_inequality_ops);
-  simplify_inequality(expr);
-  return false;
+  auto new_expr = expr;
+
+  new_expr.operands() = std::move(new_inequality_ops);
+
+  return changed(simplify_inequality(new_expr));
 }
 
 simplify_exprt::resultt<>
-simplify_exprt::simplify_pointer_object(const exprt &expr)
+simplify_exprt::simplify_pointer_object(const unary_exprt &expr)
 {
-  if(expr.operands().size()!=1)
-    return unchanged(expr);
-
-  const exprt &op = expr.op0();
+  const exprt &op = expr.op();
 
   auto op_result = simplify_object(op);
 
@@ -547,15 +554,13 @@ simplify_exprt::simplify_pointer_object(const exprt &expr)
     p_o_true.op0() = if_expr.true_case();
 
     auto new_expr = if_exprt(cond, p_o_true, p_o_false, expr.type());
-    simplify_rec(new_expr);
-
-    return new_expr;
+    return changed(simplify_rec(new_expr));
   }
 
   if(op_result.has_changed())
   {
     auto new_expr = expr;
-    new_expr.op0() = op_result;
+    new_expr.op() = op_result;
     return std::move(new_expr);
   }
   else
@@ -705,14 +710,11 @@ tvt simplify_exprt::objects_equal_address_of(const exprt &a, const exprt &b)
 }
 
 simplify_exprt::resultt<>
-simplify_exprt::simplify_object_size(const exprt &expr)
+simplify_exprt::simplify_object_size(const unary_exprt &expr)
 {
-  if(expr.operands().size()!=1)
-    return unchanged(expr);
-
   auto new_expr = expr;
   bool no_change = true;
-  exprt &op = new_expr.op0();
+  exprt &op = new_expr.op();
   auto op_result = simplify_object(op);
 
   if(op_result.has_changed())
@@ -757,13 +759,10 @@ simplify_exprt::simplify_object_size(const exprt &expr)
 }
 
 simplify_exprt::resultt<>
-simplify_exprt::simplify_good_pointer(const exprt &expr)
+simplify_exprt::simplify_good_pointer(const unary_exprt &expr)
 {
-  if(expr.operands().size()!=1)
-    return unchanged(expr);
-
   // we expand the definition
-  exprt def=good_pointer_def(expr.op0(), ns);
+  exprt def = good_pointer_def(expr.op(), ns);
 
   // recursive call
   simplify_node(def);
diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp
index 4d1067b271e..4e19c95b93a 100644
--- a/src/util/simplify_expr_struct.cpp
+++ b/src/util/simplify_expr_struct.cpp
@@ -15,15 +15,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "pointer_offset_size.h"
 #include "std_expr.h"
 
-bool simplify_exprt::simplify_member(exprt &expr)
+simplify_exprt::resultt<>
+simplify_exprt::simplify_member(const member_exprt &expr)
 {
-  if(expr.operands().size()!=1)
-    return true;
-
   const irep_idt &component_name=
     to_member_expr(expr).get_component_name();
 
-  exprt &op=expr.op0();
+  const exprt &op = expr.compound();
   const typet &op_type=ns.follow(op.type());
 
   if(op.id()==ID_with)
@@ -34,12 +32,12 @@ bool simplify_exprt::simplify_member(exprt &expr)
     if(op.operands().size()>=3 &&
        op_type.id()==ID_struct)
     {
-      exprt::operandst &operands=op.operands();
+      exprt::operandst new_operands = op.operands();
 
-      while(operands.size()>1)
+      while(new_operands.size() > 1)
       {
-        exprt &op1=operands[operands.size()-2];
-        exprt &op2=operands[operands.size()-1];
+        exprt &op1 = new_operands[new_operands.size() - 2];
+        exprt &op2 = new_operands[new_operands.size() - 1];
 
         if(op1.get(ID_component_name)==component_name)
         {
@@ -49,27 +47,20 @@ bool simplify_exprt::simplify_member(exprt &expr)
             "member expression type must match component type");
           exprt tmp;
           tmp.swap(op2);
-          expr.swap(tmp);
 
           // do this recursively
-          simplify_rec(expr);
-
-          return false;
+          return changed(simplify_rec(tmp));
         }
         else // something else, get rid of it
-          operands.resize(operands.size()-2);
+          new_operands.resize(new_operands.size() - 2);
       }
 
-      if(op.operands().size()==1)
-      {
-        exprt tmp;
-        tmp.swap(op.op0());
-        op.swap(tmp);
-        // do this recursively
-        simplify_member(expr);
-      }
+      DATA_INVARIANT(new_operands.size() == 1, "post-condition of loop");
 
-      return false;
+      auto new_member_expr = expr;
+      new_member_expr.struct_op() = new_operands.front();
+      // do this recursively
+      return changed(simplify_member(new_member_expr));
     }
     else if(op_type.id()==ID_union)
     {
@@ -78,12 +69,10 @@ bool simplify_exprt::simplify_member(exprt &expr)
       if(with_expr.where().get(ID_component_name)==component_name)
       {
         // WITH(s, .m, v).m -> v
-        expr=with_expr.new_value();
+        auto tmp = with_expr.new_value();
 
         // do this recursively
-        simplify_rec(expr);
-
-        return false;
+        return changed(simplify_rec(tmp));
       }
     }
   }
@@ -103,25 +92,20 @@ bool simplify_exprt::simplify_member(exprt &expr)
         {
           // UPDATE(s, .m, v).m -> v
           exprt tmp=update_expr.new_value();
-          expr.swap(tmp);
 
           // do this recursively
-          simplify_rec(expr);
-
-          return false;
+          return changed(simplify_rec(tmp));
         }
         // the following optimization only works on structs,
         // and not on unions
         else if(op_type.id()==ID_struct)
         {
           // UPDATE(s, .m1, v).m2 -> s.m2
-          exprt tmp=update_expr.old();
-          op.swap(tmp);
+          auto new_expr = expr;
+          new_expr.struct_op() = update_expr.old();
 
           // do this recursively
-          simplify_rec(expr);
-
-          return false;
+          return changed(simplify_rec(new_expr));
         }
       }
     }
@@ -139,10 +123,7 @@ bool simplify_exprt::simplify_member(exprt &expr)
         DATA_INVARIANT(
           op.operands()[number].type() == expr.type(),
           "member expression type must match component type");
-        exprt tmp;
-        tmp.swap(op.operands()[number]);
-        expr.swap(tmp);
-        return false;
+        return op.operands()[number];
       }
     }
   }
@@ -162,13 +143,13 @@ bool simplify_exprt::simplify_member(exprt &expr)
         component.is_nil() || component.type().id() == ID_c_bit_field ||
         component.type().id() == ID_bool)
       {
-        return true;
+        return unchanged(expr);
       }
 
       // add member offset to index
       auto offset_int = member_offset(struct_type, component_name, ns);
       if(!offset_int.has_value())
-        return true;
+        return unchanged(expr);
 
       const exprt &struct_offset=op.op1();
       exprt member_offset = from_integer(*offset_int, struct_offset.type());
@@ -176,11 +157,8 @@ bool simplify_exprt::simplify_member(exprt &expr)
       simplify_node(final_offset);
 
       byte_extract_exprt result(op.id(), op.op0(), final_offset, expr.type());
-      expr.swap(result);
-
-      simplify_rec(expr);
 
-      return false;
+      return changed(simplify_rec(result)); // recursive call
     }
     else if(op_type.id() == ID_union)
     {
@@ -193,12 +171,7 @@ bool simplify_exprt::simplify_member(exprt &expr)
         const typet &subtype = union_type.component_type(component_name);
 
         if(subtype == byte_extract_expr.op().type())
-        {
-          exprt tmp = byte_extract_expr.op();
-          expr.swap(tmp);
-
-          return false;
-        }
+          return byte_extract_expr.op();
       }
     }
   }
@@ -206,11 +179,7 @@ bool simplify_exprt::simplify_member(exprt &expr)
   {
     // trivial?
     if(to_union_expr(op).op().type() == expr.type())
-    {
-      exprt tmp=to_union_expr(op).op();
-      expr.swap(tmp);
-      return false;
-    }
+      return to_union_expr(op).op();
 
     // need to convert!
     auto target_size = pointer_offset_size(expr.type(), ns);
@@ -229,10 +198,7 @@ bool simplify_exprt::simplify_member(exprt &expr)
         auto tmp = bits2expr(bits_cut, expr.type(), true);
 
         if(tmp.has_value())
-        {
-          expr = *tmp;
-          return false;
-        }
+          return std::move(*tmp);
       }
     }
   }
@@ -242,9 +208,9 @@ bool simplify_exprt::simplify_member(exprt &expr)
     // identical types:
     if(op_type == op.op0().type())
     {
-      expr.op0() = op.op0();
-      simplify_member(expr);
-      return false;
+      auto new_expr = expr;
+      new_expr.struct_op() = op.op0();
+      return changed(simplify_member(new_expr));
     }
 
     // Try to translate into an equivalent member (perhaps nested) of the type
@@ -267,9 +233,8 @@ bool simplify_exprt::simplify_member(exprt &expr)
           equivalent_member.value().id() != ID_byte_extract_little_endian &&
           equivalent_member.value().id() != ID_byte_extract_big_endian)
         {
-          expr = equivalent_member.value();
-          simplify_rec(expr);
-          return false;
+          auto tmp = equivalent_member.value();
+          return changed(simplify_rec(tmp));
         }
       }
     }
@@ -282,12 +247,11 @@ bool simplify_exprt::simplify_member(exprt &expr)
     member_exprt member_false=to_member_expr(expr);
     member_false.compound()=if_expr.false_case();
 
-    to_member_expr(expr).compound()=if_expr.true_case();
-
-    expr=if_exprt(cond, expr, member_false, expr.type());
-    simplify_rec(expr);
+    member_exprt member_true = to_member_expr(expr);
+    member_true.compound() = if_expr.true_case();
 
-    return false;
+    auto tmp = if_exprt(cond, member_true, member_false, expr.type());
+    return changed(simplify_rec(tmp));
   }
   else if(op.id() == ID_let)
   {
@@ -297,13 +261,12 @@ bool simplify_exprt::simplify_member(exprt &expr)
     // let x = 1 in x
     member_exprt pushed_in_member = to_member_expr(expr);
     pushed_in_member.op() = to_let_expr(op).where();
-    expr = op;
-    to_let_expr(expr).where() = pushed_in_member;
-    to_let_expr(expr).type() = to_let_expr(expr).where().type();
+    auto new_expr = op;
+    to_let_expr(new_expr).where() = pushed_in_member;
+    to_let_expr(new_expr).type() = to_let_expr(new_expr).where().type();
 
-    simplify_rec(expr);
-    return false;
+    return changed(simplify_rec(new_expr));
   }
 
-  return true;
+  return unchanged(expr);
 }
diff --git a/src/util/simplify_utils.cpp b/src/util/simplify_utils.cpp
index fcbe1f232ae..7244f8fb3ef 100644
--- a/src/util/simplify_utils.cpp
+++ b/src/util/simplify_utils.cpp
@@ -7,6 +7,7 @@ Author: Daniel Kroening, kroening@kroening.com
 \*******************************************************************/
 
 #include "simplify_utils.h"
+#include "as_const.h"
 
 #include <algorithm>
 
@@ -126,8 +127,8 @@ bool sort_and_join(exprt &expr)
   if(!expr.has_operands())
     return true;
 
-  const struct saj_tablet &saj_entry=
-    sort_and_join(expr.id(), expr.type().id());
+  const struct saj_tablet &saj_entry =
+    sort_and_join(expr.id(), as_const(expr).type().id());
   if(saj_entry.id.empty())
     return true;