diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
index 9675e9a9c31..8b249aafb63 100644
--- a/jbmc/src/java_bytecode/java_object_factory.cpp
+++ b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -1087,8 +1087,12 @@ void java_object_factoryt::gen_nondet_init(
       else
       {
         exprt within_bounds = interval.make_contains_expr(expr);
-        if(!within_bounds.is_true())
+        if(
+          !within_bounds.is_constant() ||
+          !to_constant_expr(within_bounds).is_true())
+        {
           assignments.add(code_assumet(std::move(within_bounds)));
+        }
       }
 
       if(
diff --git a/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp b/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp
index ae9f2272db1..ab49dc15896 100644
--- a/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp
+++ b/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp
@@ -69,7 +69,8 @@ static bool is_call_to(
 
 static bool is_assume_false(goto_programt::const_targett inst)
 {
-  return inst->is_assume() && inst->condition().is_false();
+  return inst->is_assume() && inst->condition().is_constant() &&
+         to_constant_expr(inst->condition()).is_false();
 }
 
 /// Interpret `program`, resolving classid comparisons assuming any actual
@@ -90,17 +91,20 @@ static goto_programt::const_targett interpret_classid_comparison(
     {
       exprt guard = pc->condition();
       guard = resolve_classid_test(guard, actual_class_id, ns);
-      if(guard.is_true())
+      if(!guard.is_constant())
+      {
+        // Can't resolve the test, so exit here:
+        return pc;
+      }
+      else if(to_constant_expr(guard).is_true())
       {
         REQUIRE(pc->targets.begin() != pc->targets.end());
         pc = *(pc->targets.begin());
       }
-      else if(guard.is_false())
-        ++pc;
       else
       {
-        // Can't resolve the test, so exit here:
-        return pc;
+        CHECK_RETURN(to_constant_expr(guard).is_false());
+        ++pc;
       }
     }
     else if(pc->type() == SKIP)
diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
index 80b9c778a45..e0e2efbd816 100644
--- a/src/analyses/constant_propagator.cpp
+++ b/src/analyses/constant_propagator.cpp
@@ -183,8 +183,8 @@ void constant_propagator_domaint::transform(
     else
       g = not_exprt(from->condition());
     partial_evaluate(values, g, ns);
-    if(g.is_false())
-     values.set_to_bottom();
+    if(g.is_constant() && to_constant_expr(g).is_false())
+      values.set_to_bottom();
     else
       two_way_propagate_rec(g, ns, cp);
   }
@@ -376,7 +376,7 @@ bool constant_propagator_domaint::two_way_propagate_rec(
 
     // x != FALSE ==> x == TRUE
 
-    if(rhs.is_zero() || rhs.is_false())
+    if(to_constant_expr(rhs).is_zero() || to_constant_expr(rhs).is_false())
       rhs = from_integer(1, rhs.type());
     else
       rhs = from_integer(0, rhs.type());
diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp
index 7687ee51e5c..7efe922c09d 100644
--- a/src/analyses/custom_bitvector_analysis.cpp
+++ b/src/analyses/custom_bitvector_analysis.cpp
@@ -349,7 +349,7 @@ void custom_bitvector_domaint::transform(
             {
               if(
                 lhs.is_constant() &&
-                is_null_pointer(to_constant_expr(lhs))) // NULL means all
+                to_constant_expr(lhs).is_null_pointer()) // NULL means all
               {
                 if(mode==modet::CLEAR_MAY)
                 {
@@ -478,7 +478,7 @@ void custom_bitvector_domaint::transform(
         {
           if(
             lhs.is_constant() &&
-            is_null_pointer(to_constant_expr(lhs))) // NULL means all
+            to_constant_expr(lhs).is_null_pointer()) // NULL means all
           {
             if(mode==modet::CLEAR_MAY)
             {
@@ -530,7 +530,7 @@ void custom_bitvector_domaint::transform(
 
       const exprt result2 = simplify_expr(eval(guard, cba), ns);
 
-      if(result2.is_false())
+      if(result2.is_constant() && to_constant_expr(result2).is_false())
         make_bottom();
     }
     break;
@@ -716,7 +716,7 @@ exprt custom_bitvector_domaint::eval(
 
       if(
         pointer.is_constant() &&
-        is_null_pointer(to_constant_expr(pointer))) // NULL means all
+        to_constant_expr(pointer).is_null_pointer()) // NULL means all
       {
         if(src.id() == ID_get_may)
         {
@@ -814,12 +814,12 @@ void custom_bitvector_analysist::check(
       if(use_xml)
       {
         out << "<result status=\"";
-        if(result.is_true())
+        if(!result.is_constant())
+          out << "UNKNOWN";
+        else if(to_constant_expr(result).is_true())
           out << "SUCCESS";
-        else if(result.is_false())
-          out << "FAILURE";
         else
-          out << "UNKNOWN";
+          out << "FAILURE";
         out << "\">\n";
         out << xml(i_it->source_location());
         out << "<description>"
@@ -838,12 +838,12 @@ void custom_bitvector_analysist::check(
         out << '\n';
       }
 
-      if(result.is_true())
+      if(!result.is_constant())
+        unknown++;
+      else if(to_constant_expr(result).is_true())
         pass++;
-      else if(result.is_false())
-        fail++;
       else
-        unknown++;
+        fail++;
     }
 
     if(!use_xml)
diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
index a47497dddc4..55605acf716 100644
--- a/src/analyses/goto_rw.cpp
+++ b/src/analyses/goto_rw.cpp
@@ -116,17 +116,17 @@ void rw_range_sett::get_objects_if(
   const range_spect &range_start,
   const range_spect &size)
 {
-  if(if_expr.cond().is_false())
-    get_objects_rec(mode, if_expr.false_case(), range_start, size);
-  else if(if_expr.cond().is_true())
-    get_objects_rec(mode, if_expr.true_case(), range_start, size);
-  else
+  if(!if_expr.cond().is_constant())
   {
     get_objects_rec(get_modet::READ, if_expr.cond());
 
     get_objects_rec(mode, if_expr.false_case(), range_start, size);
     get_objects_rec(mode, if_expr.true_case(), range_start, size);
   }
+  else if(to_constant_expr(if_expr.cond()).is_false())
+    get_objects_rec(mode, if_expr.false_case(), range_start, size);
+  else
+    get_objects_rec(mode, if_expr.true_case(), range_start, size);
 }
 
 void rw_range_sett::get_objects_dereference(
@@ -735,11 +735,7 @@ void rw_guarded_range_set_value_sett::get_objects_if(
   const range_spect &range_start,
   const range_spect &size)
 {
-  if(if_expr.cond().is_false())
-    get_objects_rec(mode, if_expr.false_case(), range_start, size);
-  else if(if_expr.cond().is_true())
-    get_objects_rec(mode, if_expr.true_case(), range_start, size);
-  else
+  if(!if_expr.cond().is_constant())
   {
     get_objects_rec(get_modet::READ, if_expr.cond());
 
@@ -753,6 +749,10 @@ void rw_guarded_range_set_value_sett::get_objects_if(
     get_objects_rec(mode, if_expr.true_case(), range_start, size);
     guard = std::move(copy);
   }
+  else if(to_constant_expr(if_expr.cond()).is_false())
+    get_objects_rec(mode, if_expr.false_case(), range_start, size);
+  else
+    get_objects_rec(mode, if_expr.true_case(), range_start, size);
 }
 
 void rw_guarded_range_set_value_sett::add(
diff --git a/src/analyses/guard_bdd.cpp b/src/analyses/guard_bdd.cpp
index 1e69cb65a1a..55131d7b9da 100644
--- a/src/analyses/guard_bdd.cpp
+++ b/src/analyses/guard_bdd.cpp
@@ -44,7 +44,7 @@ exprt guard_bddt::guard_expr(exprt expr) const
   }
   else
   {
-    if(expr.is_false())
+    if(expr.is_constant() && to_constant_expr(expr).is_false())
     {
       return boolean_negate(as_expr());
     }
diff --git a/src/analyses/guard_expr.cpp b/src/analyses/guard_expr.cpp
index b44e4e726fe..94ee1371dc7 100644
--- a/src/analyses/guard_expr.cpp
+++ b/src/analyses/guard_expr.cpp
@@ -24,7 +24,7 @@ exprt guard_exprt::guard_expr(exprt expr) const
   }
   else
   {
-    if(expr.is_false())
+    if(expr.is_constant() && to_constant_expr(expr).is_false())
     {
       return boolean_negate(as_expr());
     }
@@ -39,9 +39,10 @@ void guard_exprt::add(const exprt &expr)
 {
   PRECONDITION(expr.is_boolean());
 
-  if(is_false() || expr.is_true())
+  if(is_false() || (expr.is_constant() && to_constant_expr(expr).is_true()))
     return;
-  else if(is_true() || expr.is_false())
+  else if(
+    is_true() || (expr.is_constant() && to_constant_expr(expr).is_false()))
   {
     this->expr = expr;
 
@@ -198,7 +199,9 @@ guard_exprt &operator|=(guard_exprt &g1, const guard_exprt &g2)
 
   if(tmp != and_expr1)
   {
-    if(and_expr1.is_true() || and_expr2.is_true())
+    if(
+      (and_expr1.is_constant() && to_constant_expr(and_expr1).is_true()) ||
+      (and_expr2.is_constant() && to_constant_expr(and_expr2).is_true()))
     {
     }
     else
diff --git a/src/analyses/guard_expr.h b/src/analyses/guard_expr.h
index ea5d227eee7..3d89ee1d6d0 100644
--- a/src/analyses/guard_expr.h
+++ b/src/analyses/guard_expr.h
@@ -12,7 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_ANALYSES_GUARD_EXPR_H
 #define CPROVER_ANALYSES_GUARD_EXPR_H
 
-#include <util/expr.h>
+#include <util/std_expr.h>
 
 /// This is unused by this implementation of guards, but can be used by other
 /// implementations of the same interface.
@@ -59,12 +59,12 @@ class guard_exprt
 
   bool is_true() const
   {
-    return expr.is_true();
+    return expr.is_constant() && to_constant_expr(expr).is_true();
   }
 
   bool is_false() const
   {
-    return expr.is_false();
+    return expr.is_constant() && to_constant_expr(expr).is_false();
   }
 
   friend guard_exprt &operator-=(guard_exprt &g1, const guard_exprt &g2);
diff --git a/src/analyses/interval_analysis.cpp b/src/analyses/interval_analysis.cpp
index f9cc3cf1906..755904f19bb 100644
--- a/src/analyses/interval_analysis.cpp
+++ b/src/analyses/interval_analysis.cpp
@@ -46,7 +46,10 @@ void instrument_intervals(
     {
       goto_programt::const_targett previous = std::prev(i_it);
 
-      if(previous->is_goto() && !previous->condition().is_true())
+      if(
+        previous->is_goto() &&
+        (!previous->condition().is_constant() ||
+         !to_constant_expr(previous->condition()).is_true()))
       {
         // we follow a branch, instrument
       }
@@ -69,7 +72,7 @@ void instrument_intervals(
     for(const auto &symbol_expr : symbols)
     {
       exprt tmp=d.make_expression(symbol_expr);
-      if(!tmp.is_true())
+      if(!tmp.is_constant() || !to_constant_expr(tmp).is_true())
         assertion.push_back(tmp);
     }
 
diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp
index 4594a4d2e94..8c15050968a 100644
--- a/src/analyses/interval_domain.cpp
+++ b/src/analyses/interval_domain.cpp
@@ -501,7 +501,8 @@ bool interval_domaint::ai_simplify(
                                           //  of when condition is true
     if(!a.join(d))                        // If d (this) is included in a...
     {                                     // Then the condition is always true
-      unchanged=condition.is_true();
+      unchanged =
+        condition.is_constant() && to_constant_expr(condition).is_true();
       condition = true_exprt();
     }
   }
@@ -514,7 +515,8 @@ bool interval_domaint::ai_simplify(
     d.assume(not_exprt(condition), ns);   // Restrict to when condition is false
     if(d.is_bottom())                     // If there there are none...
     {                                     // Then the condition is always true
-      unchanged=condition.is_true();
+      unchanged =
+        condition.is_constant() && to_constant_expr(condition).is_true();
       condition = true_exprt();
     }
   }
diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp
index 49c3c8b2324..a8bc6086ea0 100644
--- a/src/analyses/invariant_set.cpp
+++ b/src/analyses/invariant_set.cpp
@@ -121,7 +121,7 @@ std::string inv_object_storet::build_string(const exprt &expr) const
   if(expr.is_constant())
   {
     // NULL?
-    if(is_null_pointer(to_constant_expr(expr)))
+    if(to_constant_expr(expr).is_null_pointer())
       return "0";
 
     const auto i = numeric_cast<mp_integer>(expr);
@@ -394,14 +394,17 @@ void invariant_sett::strengthen_rec(const exprt &expr)
     return;
   }
 
-  if(expr.is_true())
-  {
-    // do nothing, it's useless
-  }
-  else if(expr.is_false())
+  if(expr.is_constant())
   {
-    // wow, that's strong
-    make_false();
+    if(to_constant_expr(expr).is_true())
+    {
+      // do nothing, it's useless
+    }
+    else
+    {
+      // wow, that's strong
+      make_false();
+    }
   }
   else if(expr.id()==ID_not)
   {
@@ -596,7 +599,7 @@ tvt invariant_sett::implies_rec(const exprt &expr) const
   if(is_false) // can't get any stronger
     return tvt(true);
 
-  if(expr.is_true())
+  if(expr.is_constant() && to_constant_expr(expr).is_true())
     return tvt(true);
   else if(expr.id()==ID_not)
   {
@@ -701,15 +704,18 @@ void invariant_sett::nnf(exprt &expr, bool negate)
   if(!expr.is_boolean())
     throw "nnf: non-Boolean expression";
 
-  if(expr.is_true())
-  {
-    if(negate)
-      expr=false_exprt();
-  }
-  else if(expr.is_false())
+  if(expr.is_constant())
   {
-    if(negate)
-      expr=true_exprt();
+    if(to_constant_expr(expr).is_true())
+    {
+      if(negate)
+        expr = false_exprt();
+    }
+    else
+    {
+      if(negate)
+        expr = true_exprt();
+    }
   }
   else if(expr.id()==ID_not)
   {
diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp
index 59d0e110f23..e7f8e89a937 100644
--- a/src/analyses/local_bitvector_analysis.cpp
+++ b/src/analyses/local_bitvector_analysis.cpp
@@ -115,7 +115,7 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
 {
   if(rhs.is_constant())
   {
-    if(rhs.is_zero())
+    if(to_constant_expr(rhs).is_zero())
       return flagst::mk_null();
     else
       return flagst::mk_integer_address();
diff --git a/src/analyses/local_cfg.cpp b/src/analyses/local_cfg.cpp
index 60bcabb783f..f7645461b85 100644
--- a/src/analyses/local_cfg.cpp
+++ b/src/analyses/local_cfg.cpp
@@ -35,8 +35,12 @@ void local_cfgt::build(const goto_programt &goto_program)
     switch(instruction.type())
     {
     case GOTO:
-      if(!instruction.condition().is_true())
+      if(
+        !instruction.condition().is_constant() ||
+        !to_constant_expr(instruction.condition()).is_true())
+      {
         node.successors.push_back(loc_nr+1);
+      }
 
       for(const auto &target : instruction.targets)
       {
diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp
index d55b5d57293..f5249308af8 100644
--- a/src/analyses/local_may_alias.cpp
+++ b/src/analyses/local_may_alias.cpp
@@ -171,7 +171,7 @@ void local_may_aliast::get_rec(
 {
   if(rhs.is_constant())
   {
-    if(rhs.is_zero())
+    if(to_constant_expr(rhs).is_zero())
       dest.insert(objects.number(exprt(ID_null_object)));
     else
       dest.insert(objects.number(exprt(ID_integer_address_object)));
diff --git a/src/analyses/variable-sensitivity/abstract_environment.cpp b/src/analyses/variable-sensitivity/abstract_environment.cpp
index 4eedf918105..461b8fe59ff 100644
--- a/src/analyses/variable-sensitivity/abstract_environment.cpp
+++ b/src/analyses/variable-sensitivity/abstract_environment.cpp
@@ -269,7 +269,7 @@ bool abstract_environmentt::assume(const exprt &expr, const namespacet &ns)
     // Should be of the right type
     INVARIANT(assumption.is_boolean(), "simplification preserves type");
 
-    if(assumption.is_false())
+    if(assumption.is_constant() && to_constant_expr(assumption).is_false())
     {
       bool currently_bottom = is_bottom();
       make_bottom();
@@ -573,10 +573,10 @@ static auto inverse_operations =
 
 static exprt invert_result(const exprt &result)
 {
-  if(!result.is_boolean())
+  if(!result.is_boolean() || !result.is_constant())
     return result;
 
-  if(result.is_true())
+  if(to_constant_expr(result).is_true())
     return false_exprt();
   return true_exprt();
 }
@@ -634,7 +634,7 @@ exprt assume_and(
   for(auto const &operand : and_expr.operands())
   {
     auto result = env.do_assume(operand, ns);
-    if(result.is_false())
+    if(result.is_constant() && to_constant_expr(result).is_false())
       return result;
     nil |= result.is_nil();
   }
@@ -827,7 +827,7 @@ exprt assume_less_than(
   auto reduced_le_expr =
     binary_relation_exprt(left_lower, expr.id(), right_upper);
   auto result = env.eval(reduced_le_expr, ns)->to_constant();
-  if(result.is_true())
+  if(result.is_constant() && to_constant_expr(result).is_true())
   {
     if(is_assignable(operands.lhs))
     {
diff --git a/src/analyses/variable-sensitivity/abstract_value_object.cpp b/src/analyses/variable-sensitivity/abstract_value_object.cpp
index 2b339a3f5f3..e2e47a79cec 100644
--- a/src/analyses/variable-sensitivity/abstract_value_object.cpp
+++ b/src/analyses/variable-sensitivity/abstract_value_object.cpp
@@ -664,8 +664,10 @@ class value_set_evaluator
     for(const auto &v : condition)
     {
       auto expr = v->to_constant();
-      all_true = all_true && expr.is_true();
-      all_false = all_false && expr.is_false();
+      all_true =
+        all_true && expr.is_constant() && to_constant_expr(expr).is_true();
+      all_false =
+        all_false && expr.is_constant() && to_constant_expr(expr).is_false();
     }
     auto indeterminate = !all_true && !all_false;
 
diff --git a/src/analyses/variable-sensitivity/full_array_abstract_object.cpp b/src/analyses/variable-sensitivity/full_array_abstract_object.cpp
index 1d766adf82a..0db1689bcd2 100644
--- a/src/analyses/variable-sensitivity/full_array_abstract_object.cpp
+++ b/src/analyses/variable-sensitivity/full_array_abstract_object.cpp
@@ -426,7 +426,7 @@ exprt full_array_abstract_objectt::to_predicate_internal(
     auto index = index_exprt(name, ii);
     auto field_expr = field.second->to_predicate(index);
 
-    if(!field_expr.is_true())
+    if(!field_expr.is_constant() || !to_constant_expr(field_expr).is_true())
       all_predicates.push_back(field_expr);
   }
 
diff --git a/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp b/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp
index ab1ae403d46..5158a773472 100644
--- a/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp
+++ b/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp
@@ -312,7 +312,7 @@ exprt full_struct_abstract_objectt::to_predicate_internal(
       member_exprt(name, compound_type.get_component(field.first));
     auto field_expr = field.second->to_predicate(field_name);
 
-    if(!field_expr.is_true())
+    if(!field_expr.is_constant() || !to_constant_expr(field_expr).is_true())
       all_predicates.push_back(field_expr);
   }
 
diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp
index 51f738c5109..2a23434e576 100644
--- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp
+++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp
@@ -45,8 +45,9 @@ class interval_index_ranget : public index_range_implementationt
   {
     index = next;
     next = next_element(next, ns);
-    return simplify_expr(binary_predicate_exprt(index, ID_le, upper), ns)
-      .is_true();
+    auto simp_expr =
+      simplify_expr(binary_predicate_exprt(index, ID_le, upper), ns);
+    return simp_expr.is_constant() && to_constant_expr(simp_expr).is_true();
   }
 
   index_range_implementation_ptrt reset() const override
@@ -239,11 +240,15 @@ bool new_interval_is_top(const constant_interval_exprt &e)
   if(e.is_top())
     return true;
 
-  if(e.get_lower().is_false() && e.get_upper().is_true())
+  if(!e.get_lower().is_constant() || !e.get_upper().is_constant())
+    return false;
+
+  const constant_exprt &lower = to_constant_expr(e.get_lower());
+  const constant_exprt &upper = to_constant_expr(e.get_upper());
+
+  if(lower.is_false() && upper.is_true())
     return true;
-  if(
-    e.type().id() == ID_c_bool && e.get_lower().is_zero() &&
-    e.get_upper().is_one())
+  if(e.type().id() == ID_c_bool && lower.is_zero() && upper.is_one())
     return true;
 
   return false;
diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp
index 5357fc3046a..5df5e2b2921 100644
--- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp
+++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp
@@ -441,11 +441,13 @@ static bool is_set_extreme(const typet &type, const abstract_object_sett &set)
       set,
       [](const abstract_value_objectt &value) {
         auto c = value.to_constant();
-        return c.is_false() || (c.id() == ID_min_value);
+        return (c.is_constant() && to_constant_expr(c).is_false()) ||
+               (c.id() == ID_min_value);
       },
       [](const abstract_value_objectt &value) {
         auto c = value.to_constant();
-        return c.is_true() || (c.id() == ID_max_value);
+        return (c.is_constant() && to_constant_expr(c).is_true()) ||
+               (c.id() == ID_max_value);
       });
   }
 
@@ -455,11 +457,13 @@ static bool is_set_extreme(const typet &type, const abstract_object_sett &set)
       set,
       [](const abstract_value_objectt &value) {
         auto c = value.to_constant();
-        return c.is_zero() || (c.id() == ID_min_value);
+        return (c.is_constant() && to_constant_expr(c).is_zero()) ||
+               (c.id() == ID_min_value);
       },
       [](const abstract_value_objectt &value) {
         auto c = value.to_constant();
-        return c.is_one() || (c.id() == ID_max_value);
+        return (c.is_constant() && to_constant_expr(c).is_one()) ||
+               (c.id() == ID_max_value);
       });
   }
 
diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp
index 873e857af8f..c978690da82 100644
--- a/src/ansi-c/c_typecast.cpp
+++ b/src/ansi-c/c_typecast.cpp
@@ -565,11 +565,11 @@ void c_typecastt::implicit_typecast_followed(
   {
     // special case: 0 == NULL
 
-    if(simplify_expr(expr, ns).is_zero() && (
-       src_type.id()==ID_unsignedbv ||
-       src_type.id()==ID_signedbv ||
-       src_type.id()==ID_natural ||
-       src_type.id()==ID_integer))
+    auto simp_expr = simplify_expr(expr, ns);
+    if(
+      simp_expr.is_constant() && to_constant_expr(simp_expr).is_zero() &&
+      (src_type.id() == ID_unsignedbv || src_type.id() == ID_signedbv ||
+       src_type.id() == ID_natural || src_type.id() == ID_integer))
     {
       expr = null_pointer_exprt{to_pointer_type(orig_dest_type)};
       return; // ok
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
index f11e08f7e14..b101d364a3b 100644
--- a/src/ansi-c/c_typecheck_base.cpp
+++ b/src/ansi-c/c_typecheck_base.cpp
@@ -312,7 +312,9 @@ static bool is_instantiation_of_flexible_array(
   return old_array_type.element_type() == new_array_type.element_type() &&
          old_array_type.get_bool(ID_C_flexible_array_member) &&
          new_array_type.get_bool(ID_C_flexible_array_member) &&
-         (old_array_type.size().is_nil() || old_array_type.size().is_zero());
+         (old_array_type.size().is_nil() ||
+          (old_array_type.size().is_constant() &&
+           to_constant_expr(old_array_type.size()).is_zero()));
 }
 
 void c_typecheck_baset::typecheck_redefinition_non_type(
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index 6e348392845..d10db37a819 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/src/ansi-c/c_typecheck_code.cpp
@@ -113,7 +113,7 @@ void c_typecheck_baset::typecheck_code(codet &code)
     implicit_typecast_bool(code.op0());
     make_constant(code.op0());
 
-    if(code.op0().is_false())
+    if(code.op0().is_constant() && to_constant_expr(code.op0()).is_false())
     {
       // failed
       error().source_location = code.find_source_location();
@@ -948,7 +948,7 @@ void c_typecheck_baset::typecheck_conditional_targets(
     auto &condition = conditional_target_group.condition();
     typecheck_spec_condition(condition);
 
-    if(condition.is_true())
+    if(condition.is_constant() && to_constant_expr(condition).is_true())
     {
       // if the condition is trivially true,
       // simplify expr and expose the bare expressions
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 5e398ab2698..fa77f0ef433 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -258,7 +258,7 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
     subtypes[1].remove(ID_C_volatile);
     subtypes[1].remove(ID_C_restricted);
 
-    expr = make_boolean_expr(gcc_types_compatible_p(subtypes[0], subtypes[1]));
+    expr = constant_exprt{gcc_types_compatible_p(subtypes[0], subtypes[1])};
     expr.add_source_location()=source_location;
   }
   else if(expr.id()==ID_clang_builtin_convertvector)
@@ -1435,18 +1435,24 @@ void c_typecheck_baset::typecheck_expr_rel(
   else
   {
     // pointer and zero
-    if(type0.id()==ID_pointer &&
-       simplify_expr(op1, *this).is_zero())
+    if(type0.id() == ID_pointer)
     {
-      op1 = null_pointer_exprt{to_pointer_type(type0)};
-      return;
+      auto simp_op1 = simplify_expr(op1, *this);
+      if(simp_op1.is_constant() && to_constant_expr(simp_op1).is_zero())
+      {
+        op1 = null_pointer_exprt{to_pointer_type(type0)};
+        return;
+      }
     }
 
-    if(type1.id()==ID_pointer &&
-       simplify_expr(op0, *this).is_zero())
+    if(type1.id() == ID_pointer)
     {
-      op0 = null_pointer_exprt{to_pointer_type(type1)};
-      return;
+      auto simp_op0 = simplify_expr(op0, *this);
+      if(simp_op0.is_constant() && to_constant_expr(simp_op0).is_zero())
+      {
+        op0 = null_pointer_exprt{to_pointer_type(type1)};
+        return;
+      }
     }
 
     // pointer and integer
@@ -1672,13 +1678,13 @@ void c_typecheck_baset::typecheck_expr_trinary(if_exprt &expr)
     // (at least that's how GCC behaves)
     if(
       to_pointer_type(operands[1].type()).base_type().id() == ID_empty &&
-      tmp1.is_constant() && is_null_pointer(to_constant_expr(tmp1)))
+      tmp1.is_constant() && to_constant_expr(tmp1).is_null_pointer())
     {
       implicit_typecast(operands[1], operands[2].type());
     }
     else if(
       to_pointer_type(operands[2].type()).base_type().id() == ID_empty &&
-      tmp2.is_constant() && is_null_pointer(to_constant_expr(tmp2)))
+      tmp2.is_constant() && to_constant_expr(tmp2).is_null_pointer())
     {
       implicit_typecast(operands[2], operands[1].type());
     }
@@ -3583,9 +3589,9 @@ exprt c_typecheck_baset::do_special_functions(
 
     mp_integer arg1;
 
-    if(expr.arguments()[1].is_true())
+    if(to_constant_expr(expr.arguments()[1]).is_true())
       arg1=1;
-    else if(expr.arguments()[1].is_false())
+    else if(to_constant_expr(expr.arguments()[1]).is_false())
       arg1=0;
     else if(to_integer(to_constant_expr(expr.arguments()[1]), arg1))
     {
@@ -3627,7 +3633,7 @@ exprt c_typecheck_baset::do_special_functions(
       typecast_exprt::conditional_cast(expr.arguments()[0], bool_typet());
     make_constant(arg0);
 
-    if(arg0.is_true())
+    if(to_constant_expr(arg0).is_true())
       return expr.arguments()[1];
     else
       return expr.arguments()[2];
diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp
index e17d59966c7..8d49ba2eead 100644
--- a/src/ansi-c/c_typecheck_initializer.cpp
+++ b/src/ansi-c/c_typecheck_initializer.cpp
@@ -405,8 +405,10 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
       if(index>=dest->operands().size())
       {
         if(
-          type.id() == ID_array && (to_array_type(type).size().is_zero() ||
-                                    to_array_type(type).size().is_nil()))
+          type.id() == ID_array &&
+          ((to_array_type(type).size().is_constant() &&
+            to_constant_expr(to_array_type(type).size()).is_zero()) ||
+           to_array_type(type).size().is_nil()))
         {
           const typet &element_type = to_array_type(type).element_type();
 
@@ -673,10 +675,11 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
 
       // in case of a variable-length array consume all remaining
       // initializer elements
-      if(vla_permitted &&
-         dest_type.id()==ID_array &&
-         (to_array_type(dest_type).size().is_zero() ||
-          to_array_type(dest_type).size().is_nil()))
+      if(
+        vla_permitted && dest_type.id() == ID_array &&
+        ((to_array_type(dest_type).size().is_constant() &&
+          to_constant_expr(to_array_type(dest_type).size()).is_zero()) ||
+         to_array_type(dest_type).size().is_nil()))
       {
         value.id(ID_initializer_list);
         value.operands().clear();
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
index 02e50709308..43a1a2f3a8e 100644
--- a/src/ansi-c/c_typecheck_type.cpp
+++ b/src/ansi-c/c_typecheck_type.cpp
@@ -1069,12 +1069,12 @@ void c_typecheck_baset::typecheck_compound_body(
       assertion = typecast_exprt(assertion, bool_typet());
       make_constant(assertion);
 
-      if(assertion.is_false())
+      if(to_constant_expr(assertion).is_false())
       {
         throw errort().with_location(it->source_location())
           << "failed _Static_assert";
       }
-      else if(!assertion.is_true())
+      else if(!to_constant_expr(assertion).is_true())
       {
         // should warn/complain
       }
@@ -1243,9 +1243,9 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
       typecheck_expr(tmp_v);
       add_rounding_mode(tmp_v);
       simplify(tmp_v, *this);
-      if(tmp_v.is_true())
+      if(tmp_v.is_constant() && to_constant_expr(tmp_v).is_true())
         value=1;
-      else if(tmp_v.is_false())
+      else if(tmp_v.is_constant() && to_constant_expr(tmp_v).is_false())
         value=0;
       else if(
         tmp_v.is_constant() && !to_integer(to_constant_expr(tmp_v), value))
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 3257a74f270..b7042177813 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -1268,7 +1268,8 @@ std::string expr2ct::convert_complex(
   unsigned precedence)
 {
   if(
-    src.operands().size() == 2 && to_binary_expr(src).op0().is_zero() &&
+    src.operands().size() == 2 && to_binary_expr(src).op0().is_constant() &&
+    to_constant_expr(to_binary_expr(src).op0()).is_zero() &&
     to_binary_expr(src).op1().is_constant())
   {
     // This is believed to be gcc only; check if this is sensible
@@ -1983,7 +1984,7 @@ std::string expr2ct::convert_constant(
   }
   else if(type.id()==ID_pointer)
   {
-    if(is_null_pointer(src))
+    if(src.is_null_pointer())
     {
       if(configuration.use_library_macros)
         dest = "NULL";
@@ -3531,7 +3532,7 @@ std::string expr2ct::convert_conditional_target_group(const exprt &src)
   std::string dest;
   unsigned p;
   const auto &cond = src.operands().front();
-  if(!cond.is_true())
+  if(!cond.is_constant() || !to_constant_expr(cond).is_true())
   {
     dest += convert_with_precedence(cond, p);
     dest += ": ";
@@ -3751,8 +3752,12 @@ std::string expr2ct::convert_with_precedence(
 
     if(object.id() == ID_label)
       return "&&" + object.get_string(ID_identifier);
-    else if(object.id() == ID_index && to_index_expr(object).index().is_zero())
+    else if(
+      object.id() == ID_index && to_index_expr(object).index().is_constant() &&
+      to_constant_expr(to_index_expr(object).index()).is_zero())
+    {
       return convert(to_index_expr(object).array());
+    }
     else if(to_pointer_type(src.type()).base_type().id() == ID_code)
       return convert_unary(to_unary_expr(src), "", precedence = 15);
     else
diff --git a/src/ansi-c/goto-conversion/builtin_functions.cpp b/src/ansi-c/goto-conversion/builtin_functions.cpp
index bf864fcdb1e..89575f0ee29 100644
--- a/src/ansi-c/goto-conversion/builtin_functions.cpp
+++ b/src/ansi-c/goto-conversion/builtin_functions.cpp
@@ -606,7 +606,8 @@ exprt make_va_list(const exprt &expr)
   }
 
   while(result.type().id() == ID_array &&
-        to_array_type(result.type()).size().is_one())
+        to_array_type(result.type()).size().is_constant() &&
+        to_constant_expr(to_array_type(result.type()).size()).is_one())
   {
     result = index_exprt{result, from_integer(0, c_index_type())};
   }
diff --git a/src/ansi-c/goto-conversion/goto_check_c.cpp b/src/ansi-c/goto-conversion/goto_check_c.cpp
index f829ebeda7e..0fde03f8899 100644
--- a/src/ansi-c/goto-conversion/goto_check_c.cpp
+++ b/src/ansi-c/goto-conversion/goto_check_c.cpp
@@ -1685,7 +1685,8 @@ void goto_check_ct::bounds_check_index(
   }
   else if(
     expr.array().id() == ID_member &&
-    (size.is_zero() || array_type.get_bool(ID_C_flexible_array_member)))
+    ((size.is_constant() && to_constant_expr(size).is_zero()) ||
+     array_type.get_bool(ID_C_flexible_array_member)))
   {
     // a variable sized struct member
     //
@@ -1766,8 +1767,12 @@ void goto_check_ct::add_guarded_property(
     enable_simplify ? simplify_expr(asserted_expr, ns) : asserted_expr;
 
   // throw away trivial properties?
-  if(!retain_trivial && simplified_expr.is_true())
+  if(
+    !retain_trivial && simplified_expr.is_constant() &&
+    to_constant_expr(simplified_expr).is_true())
+  {
     return;
+  }
 
   // add the guard
   exprt guarded_expr = guard(simplified_expr);
@@ -2245,7 +2250,8 @@ void goto_check_ct::goto_check(
       // These are further 'exit points' of the program
       const exprt simplified_guard = simplify_expr(i.condition(), ns);
       if(
-        enable_memory_cleanup_check && simplified_guard.is_false() &&
+        enable_memory_cleanup_check && simplified_guard.is_constant() &&
+        to_constant_expr(simplified_guard).is_false() &&
         (function_identifier == "abort" || function_identifier == "exit" ||
          function_identifier == "_Exit" ||
          (i.labels.size() == 1 && i.labels.front() == "__VERIFIER_abort")))
diff --git a/src/ansi-c/goto-conversion/goto_clean_expr.cpp b/src/ansi-c/goto-conversion/goto_clean_expr.cpp
index c015c1fe414..1193f7eb6c9 100644
--- a/src/ansi-c/goto-conversion/goto_clean_expr.cpp
+++ b/src/ansi-c/goto-conversion/goto_clean_expr.cpp
@@ -114,13 +114,15 @@ void goto_convertt::rewrite_boolean(exprt &expr)
     "' must be Boolean, but got ",
     irep_pretty_diagnosticst{expr});
 
+  const source_locationt source_location = expr.find_source_location();
+
   // re-write "a ==> b" into a?b:1
   if(auto implies = expr_try_dynamic_cast<implies_exprt>(expr))
   {
     expr = if_exprt{
       std::move(implies->lhs()),
       std::move(implies->rhs()),
-      true_exprt{},
+      true_exprt{}.with_source_location(source_location),
       bool_typet{}};
     return;
   }
@@ -135,6 +137,8 @@ void goto_convertt::rewrite_boolean(exprt &expr)
   else // ID_or
     tmp = false_exprt();
 
+  tmp.add_source_location() = source_location;
+
   exprt::operandst &ops = expr.operands();
 
   // start with last one
@@ -146,17 +150,21 @@ void goto_convertt::rewrite_boolean(exprt &expr)
     DATA_INVARIANT_WITH_DIAGNOSTICS(
       op.is_boolean(),
       "boolean operators must have only boolean operands",
-      expr.find_source_location());
+      source_location);
 
     if(expr.id() == ID_and)
     {
-      if_exprt if_e(op, tmp, false_exprt());
+      exprt if_e =
+        if_exprt{op, tmp, false_exprt{}.with_source_location(source_location)}
+          .with_source_location(source_location);
       tmp.swap(if_e);
       continue;
     }
     if(expr.id() == ID_or)
     {
-      if_exprt if_e(op, true_exprt(), tmp);
+      exprt if_e =
+        if_exprt{op, true_exprt{}.with_source_location(source_location), tmp}
+          .with_source_location(source_location);
       tmp.swap(if_e);
       continue;
     }
@@ -220,13 +228,13 @@ goto_convertt::clean_expr_resultt goto_convertt::clean_expr(
     {
       exprt tmp_cond=if_expr.cond();
       simplify(tmp_cond, ns);
-      if(tmp_cond.is_true())
+      if(tmp_cond.is_constant() && to_constant_expr(tmp_cond).is_true())
       {
         clean_expr(if_expr.true_case(), dest, result_is_used);
         expr=if_expr.true_case();
         return;
       }
-      else if(tmp_cond.is_false())
+      else if(tmp_cond.is_constant() && to_constant_expr(tmp_cond).is_false())
       {
         clean_expr(if_expr.false_case(), dest, result_is_used);
         expr=if_expr.false_case();
diff --git a/src/ansi-c/goto-conversion/goto_convert.cpp b/src/ansi-c/goto-conversion/goto_convert.cpp
index f07ed0f424c..45992b93505 100644
--- a/src/ansi-c/goto-conversion/goto_convert.cpp
+++ b/src/ansi-c/goto-conversion/goto_convert.cpp
@@ -419,7 +419,9 @@ void goto_convertt::optimize_guarded_gotos(goto_programt &dest)
 
     if(
       it_goto_y == dest.instructions.end() || !it_goto_y->is_goto() ||
-      !it_goto_y->condition().is_true() || it_goto_y->is_target())
+      !it_goto_y->condition().is_constant() ||
+      !to_constant_expr(it_goto_y->condition()).is_true() ||
+      it_goto_y->is_target())
     {
       continue;
     }
@@ -700,7 +702,7 @@ void goto_convertt::convert(
       typecast_exprt::conditional_cast(code.op0(), bool_typet());
     simplify(assertion, ns);
     INVARIANT_WITH_DIAGNOSTICS(
-      !assertion.is_false(),
+      !assertion.is_constant() || !to_constant_expr(assertion).is_false(),
       "static assertion " + id2string(get_string_constant(code.op1())),
       code.op0().find_source_location());
   }
@@ -743,7 +745,8 @@ void goto_convertt::convert_block(
   // in a prior break/continue/return already, don't create dead code
   if(
     !dest.empty() && dest.instructions.back().is_goto() &&
-    dest.instructions.back().condition().is_true())
+    dest.instructions.back().condition().is_constant() &&
+    to_constant_expr(dest.instructions.back().condition()).is_true())
   {
     // don't do destructors when we are unreachable
   }
@@ -1774,7 +1777,8 @@ void goto_convertt::generate_ifthenelse(
   // do guarded assertions directly
   if(
     is_size_one(true_case) && true_case.instructions.back().is_assert() &&
-    true_case.instructions.back().condition().is_false() &&
+    true_case.instructions.back().condition().is_constant() &&
+    to_constant_expr(true_case.instructions.back().condition()).is_false() &&
     true_case.instructions.back().labels.empty())
   {
     // The above conjunction deliberately excludes the instance
@@ -1792,7 +1796,8 @@ void goto_convertt::generate_ifthenelse(
   // similarly, do guarded assertions directly
   if(
     is_size_one(false_case) && false_case.instructions.back().is_assert() &&
-    false_case.instructions.back().condition().is_false() &&
+    false_case.instructions.back().condition().is_constant() &&
+    to_constant_expr(false_case.instructions.back().condition()).is_false() &&
     false_case.instructions.back().labels.empty())
   {
     // The above conjunction deliberately excludes the instance
@@ -1812,7 +1817,11 @@ void goto_convertt::generate_ifthenelse(
   if(
     is_empty(false_case) && true_case.instructions.size() == 2 &&
     true_case.instructions.front().is_assert() &&
-    simplify_expr(true_case.instructions.front().condition(), ns).is_false() &&
+    simplify_expr(true_case.instructions.front().condition(), ns)
+      .is_constant() &&
+    to_constant_expr(
+      simplify_expr(true_case.instructions.front().condition(), ns))
+      .is_false() &&
     true_case.instructions.front().labels.empty() &&
     true_case.instructions.back().is_other() &&
     true_case.instructions.back().get_other().get_statement() ==
diff --git a/src/ansi-c/goto-conversion/goto_convert_functions.cpp b/src/ansi-c/goto-conversion/goto_convert_functions.cpp
index 07a3c3713e1..8fa454f27ed 100644
--- a/src/ansi-c/goto-conversion/goto_convert_functions.cpp
+++ b/src/ansi-c/goto-conversion/goto_convert_functions.cpp
@@ -96,8 +96,11 @@ void goto_convert_functionst::add_return(
   // see if we have an unconditional goto at the end
   if(!f.body.instructions.empty() &&
      f.body.instructions.back().is_goto() &&
-     f.body.instructions.back().guard.is_true())
+     f.body.instructions.back().guard.is_constant() &&
+     to_constant_expr(f.body.instructions.back().guard).is_true())
+  {
     return;
+  }
 #else
 
   if(!f.body.instructions.empty())
@@ -108,7 +111,10 @@ void goto_convert_functionst::add_return(
     while(true)
     {
       // unconditional goto, say from while(1)?
-      if(last_instruction->is_goto() && last_instruction->condition().is_true())
+      if(
+        last_instruction->is_goto() &&
+        last_instruction->condition().is_constant() &&
+        to_constant_expr(last_instruction->condition()).is_true())
       {
         return;
       }
diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y
index 59e320f7112..79e20d89187 100644
--- a/src/ansi-c/parser.y
+++ b/src/ansi-c/parser.y
@@ -1558,7 +1558,8 @@ pragma_packed:
         {
           init($$);
           if(!PARSER.pragma_pack.empty() &&
-             PARSER.pragma_pack.back().is_one())
+             PARSER.pragma_pack.back().is_constant() &&
+             to_constant_expr(PARSER.pragma_pack.back()).is_one())
             set($$, ID_packed);
         }
         ;
@@ -1762,7 +1763,8 @@ member_declaring_list:
           if(parser_stack($2).id() != ID_struct &&
              parser_stack($2).id() != ID_union &&
              !PARSER.pragma_pack.empty() &&
-             !PARSER.pragma_pack.back().is_zero())
+             (!PARSER.pragma_pack.back().is_constant() ||
+             !to_constant_expr(PARSER.pragma_pack.back()).is_zero()))
           {
             // communicate #pragma pack(n) alignment constraints by
             // by both setting packing AND alignment for individual struct/union
diff --git a/src/ansi-c/printf_formatter.cpp b/src/ansi-c/printf_formatter.cpp
index 7ad8c06667c..d6a4dc741d3 100644
--- a/src/ansi-c/printf_formatter.cpp
+++ b/src/ansi-c/printf_formatter.cpp
@@ -215,7 +215,8 @@ void printf_formattert::process_format(std::ostream &out)
             expr_try_dynamic_cast<index_exprt>(address_of->object()))
         {
           if(
-            index_expr->index().is_zero() &&
+            index_expr->index().is_constant() &&
+            to_constant_expr(index_expr->index()).is_zero() &&
             index_expr->array().id() == ID_string_constant)
           {
             out << format_constant(index_expr->array());
diff --git a/src/cpp/cpp_instantiate_template.cpp b/src/cpp/cpp_instantiate_template.cpp
index 4328428b326..618bb1a09b4 100644
--- a/src/cpp/cpp_instantiate_template.cpp
+++ b/src/cpp/cpp_instantiate_template.cpp
@@ -67,9 +67,9 @@ std::string cpp_typecheckt::template_suffix(
       // this must be a constant, which includes true/false
       mp_integer i;
 
-      if(e.is_true())
+      if(to_constant_expr(e).is_true())
         i=1;
-      else if(e.is_false())
+      else if(to_constant_expr(e).is_false())
         i=0;
       else if(to_integer(to_constant_expr(e), i))
       {
diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp
index 41ec14ef5c2..af842155704 100644
--- a/src/cpp/cpp_typecheck_conversions.cpp
+++ b/src/cpp/cpp_typecheck_conversions.cpp
@@ -465,8 +465,10 @@ bool cpp_typecheckt::standard_conversion_pointer(
     return false;
 
   // integer 0 to NULL pointer conversion?
-  if(simplify_expr(expr, *this).is_zero() &&
-     expr.type().id()!=ID_pointer)
+  auto simp_expr = simplify_expr(expr, *this);
+  if(
+    simp_expr.is_constant() && to_constant_expr(simp_expr).is_zero() &&
+    expr.type().id() != ID_pointer)
   {
     new_expr=expr;
     new_expr.set(ID_value, ID_NULL);
@@ -603,7 +605,7 @@ bool cpp_typecheckt::standard_conversion_pointer_to_member(
   if(expr.get_bool(ID_C_lvalue))
     return false;
 
-  if(expr.is_constant() && is_null_pointer(to_constant_expr(expr)))
+  if(expr.is_constant() && to_constant_expr(expr).is_null_pointer())
   {
     new_expr = typecast_exprt::conditional_cast(expr, type);
     return true;
@@ -1857,7 +1859,8 @@ bool cpp_typecheckt::reinterpret_typecast(
     type.id() == ID_pointer && !is_reference(type))
   {
     // integer to pointer
-    if(simplify_expr(e, *this).is_zero())
+    auto simp_e = simplify_expr(e, *this);
+    if(simp_e.is_constant() && to_constant_expr(simp_e).is_zero())
     {
       // NULL
       new_expr=e;
diff --git a/src/cpp/cpp_typecheck_method_bodies.cpp b/src/cpp/cpp_typecheck_method_bodies.cpp
index e8389d721be..13279619d45 100644
--- a/src/cpp/cpp_typecheck_method_bodies.cpp
+++ b/src/cpp/cpp_typecheck_method_bodies.cpp
@@ -39,10 +39,16 @@ void cpp_typecheckt::typecheck_method_bodies()
 #ifdef DEBUG
     std::cout << "convert_method_body: " << method_symbol.name << '\n';
     std::cout << "  is_not_nil: " << body.is_not_nil() << '\n';
-    std::cout << "  !is_zero: " << (!body.is_zero()) << '\n';
+    std::cout << "  !is_zero: "
+              << (!body.is_constant() || !to_constant_expr(body).is_zero())
+              << '\n';
 #endif
-    if(body.is_not_nil() && !body.is_zero())
+    if(
+      body.is_not_nil() &&
+      (!body.is_constant() || !to_constant_expr(body).is_zero()))
+    {
       convert_function(method_symbol);
+    }
   }
 
   old_instantiation_stack.swap(instantiation_stack);
diff --git a/src/cpp/cpp_typecheck_static_assert.cpp b/src/cpp/cpp_typecheck_static_assert.cpp
index a792c010355..394bd2dbe81 100644
--- a/src/cpp/cpp_typecheck_static_assert.cpp
+++ b/src/cpp/cpp_typecheck_static_assert.cpp
@@ -21,7 +21,7 @@ void cpp_typecheckt::convert(cpp_static_assertt &cpp_static_assert)
   implicit_typecast_bool(cpp_static_assert.op0());
   make_constant(cpp_static_assert.op0());
 
-  if(cpp_static_assert.op0().is_false())
+  if(to_constant_expr(cpp_static_assert.op0()).is_false())
   {
     // failed
     error().source_location=cpp_static_assert.source_location();
diff --git a/src/cprover/bv_pointers_wide.cpp b/src/cprover/bv_pointers_wide.cpp
index 8cb9e7b46a3..9197306f0b1 100644
--- a/src/cprover/bv_pointers_wide.cpp
+++ b/src/cprover/bv_pointers_wide.cpp
@@ -387,7 +387,7 @@ bvt bv_pointers_widet::convert_pointer_type(const exprt &expr)
   {
     const constant_exprt &c = to_constant_expr(expr);
 
-    if(is_null_pointer(c))
+    if(c.is_null_pointer())
       return encode(pointer_logic.get_null_object(), type);
     else
     {
diff --git a/src/cprover/inductiveness.cpp b/src/cprover/inductiveness.cpp
index 6f4484fae12..ee116d8c715 100644
--- a/src/cprover/inductiveness.cpp
+++ b/src/cprover/inductiveness.cpp
@@ -36,7 +36,7 @@ bool is_subsumed(
   bool verbose,
   const namespacet &ns)
 {
-  if(b.is_true())
+  if(b.is_constant() && to_constant_expr(b).is_true())
     return true; // anything subsumes 'true'
 
   if(a1.find(false_exprt()) != a1.end())
@@ -161,7 +161,7 @@ inductiveness_resultt inductiveness_check(
                   << frame_ref.index << consolet::reset << ' ';
 
       // trivially true?
-      if(invariant.is_true())
+      if(invariant.is_constant() && to_constant_expr(invariant).is_true())
       {
         if(solver_options.verbose)
           std::cout << "trivial\n";
diff --git a/src/cprover/instrument_contracts.cpp b/src/cprover/instrument_contracts.cpp
index 88dc0f22ef0..69baa005b5a 100644
--- a/src/cprover/instrument_contracts.cpp
+++ b/src/cprover/instrument_contracts.cpp
@@ -110,12 +110,14 @@ exprt assigns_match(const exprt &assigns, const exprt &lhs)
 
   if(lhs.id() == ID_member)
   {
-    if(assigns_match(assigns, to_member_expr(lhs).struct_op()).is_true())
+    exprt struct_op = assigns_match(assigns, to_member_expr(lhs).struct_op());
+    if(struct_op.is_constant() && to_constant_expr(struct_op).is_true())
       return true_exprt();
   }
   else if(lhs.id() == ID_index)
   {
-    if(assigns_match(assigns, to_index_expr(lhs).array()).is_true())
+    exprt array = assigns_match(assigns, to_index_expr(lhs).array());
+    if(array.is_constant() && to_constant_expr(array).is_true())
       return true_exprt();
   }
 
@@ -169,7 +171,7 @@ static exprt make_assigns_assertion(
       auto match = assigns_match(a, lhs);
 
       // trivial?
-      if(match.is_true())
+      if(match.is_constant() && to_constant_expr(match).is_true())
         return true_exprt();
 
       disjuncts.push_back(std::move(match));
diff --git a/src/cprover/may_alias.cpp b/src/cprover/may_alias.cpp
index 046fbbcd84c..55e1fedfbab 100644
--- a/src/cprover/may_alias.cpp
+++ b/src/cprover/may_alias.cpp
@@ -179,8 +179,12 @@ same_address(const exprt &a, const exprt &b, const namespacet &ns)
 
       CHECK_RETURN(base_same_address.has_value());
 
-      if(base_same_address->is_false())
+      if(
+        base_same_address->is_constant() &&
+        to_constant_expr(*base_same_address).is_false())
+      {
         return false_expr;
+      }
       else
       {
         return and_exprt(
diff --git a/src/cprover/simplify_state_expr.cpp b/src/cprover/simplify_state_expr.cpp
index d11f031a8b5..146d4d8806e 100644
--- a/src/cprover/simplify_state_expr.cpp
+++ b/src/cprover/simplify_state_expr.cpp
@@ -73,7 +73,7 @@ exprt simplify_evaluate_update(
   if(may_alias.has_value())
   {
     // 'simple' case
-    if(may_alias->is_true())
+    if(may_alias->is_constant() && to_constant_expr(*may_alias).is_true())
     {
       // The object is known to be the same.
       // (ς[A:=V])(A) --> V
@@ -83,7 +83,7 @@ exprt simplify_evaluate_update(
         address_taken,
         ns);
     }
-    else if(may_alias->is_false())
+    else if(may_alias->is_constant() && to_constant_expr(*may_alias).is_false())
     {
       // The object is known to be different.
       // (ς[❝x❞:=V])(❝y❞) --> ς(❝y❞)
@@ -444,7 +444,7 @@ exprt simplify_writeable_object_expr(
     else
     {
       const auto &symbol = ns.lookup(identifier);
-      return make_boolean_expr(!symbol.type.get_bool(ID_C_constant));
+      return constant_exprt{!symbol.type.get_bool(ID_C_constant)};
     }
   }
 
@@ -680,7 +680,9 @@ exprt simplify_is_cstring_expr(
     auto may_alias =
       ::may_alias(pointer, update_state_expr.address(), address_taken, ns);
 
-    if(may_alias.has_value() && may_alias->is_false())
+    if(
+      may_alias.has_value() && may_alias->is_constant() &&
+      to_constant_expr(*may_alias).is_false())
     {
       // different objects
       // cstring(s[x:=v], p) --> cstring(s, p)
@@ -690,7 +692,9 @@ exprt simplify_is_cstring_expr(
     // maybe the same
 
     // Are we writing zero?
-    if(update_state_expr.new_value().is_zero())
+    if(
+      update_state_expr.new_value().is_constant() &&
+      to_constant_expr(update_state_expr.new_value()).is_zero())
     {
       // cstring(s[p:=0], q) --> if p alias q then true else cstring(s, q)
       auto same_object = ::same_object(pointer, update_state_expr.address());
@@ -776,7 +780,9 @@ exprt simplify_cstrlen_expr(
     auto may_be_same_object = ::may_be_same_object(
       pointer, update_state_expr.address(), address_taken, ns);
 
-    if(may_be_same_object.is_false())
+    if(
+      may_be_same_object.is_constant() &&
+      to_constant_expr(may_be_same_object).is_false())
     {
       // different objects
       // cstrlen(s[x:=v], p) --> cstrlen(s, p)
diff --git a/src/cprover/state_encoding.cpp b/src/cprover/state_encoding.cpp
index 56ef744c049..3d4e18e87f3 100644
--- a/src/cprover/state_encoding.cpp
+++ b/src/cprover/state_encoding.cpp
@@ -134,7 +134,9 @@ std::vector<symbol_exprt> state_encodingt::incoming_symbols(loct loc) const
 
     // conditional jump from loc_in to loc?
     if(
-      loc_in->is_goto() && !loc_in->condition().is_true() &&
+      loc_in->is_goto() &&
+      (!loc_in->condition().is_constant() ||
+       !to_constant_expr(loc_in->condition()).is_true()) &&
       loc != std::next(loc_in))
     {
       suffix = "T";
@@ -617,7 +619,9 @@ void state_encodingt::setup_incoming(const goto_functiont &goto_function)
   forall_goto_program_instructions(it, goto_function.body)
   {
     auto next = std::next(it);
-    if(it->is_goto() && it->condition().is_true())
+    if(
+      it->is_goto() && it->condition().is_constant() &&
+      to_constant_expr(it->condition()).is_true())
     {
     }
     else if(next != goto_function.body.instructions.end())
@@ -1013,7 +1017,7 @@ void state_encodingt::encode(
       // We produce ∅ when the 'other' branch is taken. Get the condition.
       const auto &condition = loc->condition();
 
-      if(condition.is_true())
+      if(condition.is_constant() && to_constant_expr(condition).is_true())
       {
         dest << equal_exprt(out_state_expr(loc), in_state_expr(loc));
       }
diff --git a/src/goto-analyzer/static_verifier.cpp b/src/goto-analyzer/static_verifier.cpp
index 9e9282f6de7..5d535a6e9a7 100644
--- a/src/goto-analyzer/static_verifier.cpp
+++ b/src/goto-analyzer/static_verifier.cpp
@@ -92,11 +92,11 @@ check_assertion(const ai_domain_baset &domain, exprt e, const namespacet &ns)
   }
 
   domain.ai_simplify(e, ns);
-  if(e.is_true())
+  if(e.is_constant() && to_constant_expr(e).is_true())
   {
     return ai_verifier_statust::TRUE;
   }
-  else if(e.is_false())
+  else if(e.is_constant() && to_constant_expr(e).is_false())
   {
     return ai_verifier_statust::FALSE_IF_REACHABLE;
   }
diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp
index 55726c91e2b..d6960b84e2e 100644
--- a/src/goto-analyzer/taint_analysis.cpp
+++ b/src/goto-analyzer/taint_analysis.cpp
@@ -343,7 +343,8 @@ bool taint_analysist::operator()(
           continue;
 
         exprt result = custom_bitvector_analysis.eval(i_it->condition(), i_it);
-        if(simplify_expr(std::move(result), ns).is_true())
+        exprt simp_result = simplify_expr(std::move(result), ns);
+        if(simp_result.is_constant() && to_constant_expr(simp_result).is_true())
           continue;
 
         if(first)
diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp
index 6e31d312d77..79dd9e58232 100644
--- a/src/goto-checker/bmc_util.cpp
+++ b/src/goto-checker/bmc_util.cpp
@@ -57,7 +57,9 @@ ssa_step_matches_failing_property(const irep_idt &property_id)
            symex_target_equationt::SSA_stepst::const_iterator step,
            const decision_proceduret &decision_procedure) {
     return step->is_assert() && step->property_id == property_id &&
-           decision_procedure.get(step->cond_handle).is_false();
+           decision_procedure.get(step->cond_handle).is_constant() &&
+           to_constant_expr(decision_procedure.get(step->cond_handle))
+             .is_false();
   };
 }
 
@@ -250,8 +252,10 @@ void update_properties_status_from_symex_target_equation(
 
     // Don't update status of properties that are constant 'false';
     // we wouldn't have traces for them.
-    const auto status = step.cond_expr.is_true() ? property_statust::PASS
-                                                 : property_statust::UNKNOWN;
+    const auto status = (step.cond_expr.is_constant() &&
+                         to_constant_expr(step.cond_expr).is_true())
+                          ? property_statust::PASS
+                          : property_statust::UNKNOWN;
     auto emplace_result = properties.emplace(
       property_id, property_infot{step.source.pc, step.comment, status});
 
diff --git a/src/goto-checker/counterexample_beautification.cpp b/src/goto-checker/counterexample_beautification.cpp
index 34bc7b0c191..4a15b2726bc 100644
--- a/src/goto-checker/counterexample_beautification.cpp
+++ b/src/goto-checker/counterexample_beautification.cpp
@@ -37,7 +37,8 @@ void counterexample_beautificationt::get_minimization_list(
       it->is_assignment() &&
       it->assignment_type == symex_targett::assignment_typet::STATE)
     {
-      if(!prop_conv.get(it->guard_handle).is_false())
+      exprt v = prop_conv.get(it->guard_handle);
+      if(!v.is_constant() || !to_constant_expr(v).is_false())
       {
         const typet &type = it->ssa_lhs.type();
 
@@ -75,9 +76,14 @@ counterexample_beautificationt::get_failed_property(
       it != equation.SSA_steps.end();
       it++)
   {
+    if(!it->is_assert())
+      continue;
+
+    exprt g = prop_conv.get(it->guard_handle);
+    exprt c = prop_conv.get(it->cond_handle);
     if(
-      it->is_assert() && prop_conv.get(it->guard_handle).is_true() &&
-      prop_conv.get(it->cond_handle).is_false())
+      g.is_constant() && to_constant_expr(g).is_true() && c.is_constant() &&
+      to_constant_expr(c).is_false())
     {
       return it;
     }
diff --git a/src/goto-checker/goto_symex_fault_localizer.cpp b/src/goto-checker/goto_symex_fault_localizer.cpp
index 7e70100657c..3c4407bd3b1 100644
--- a/src/goto-checker/goto_symex_fault_localizer.cpp
+++ b/src/goto-checker/goto_symex_fault_localizer.cpp
@@ -108,11 +108,12 @@ void goto_symex_fault_localizert::update_scores(
   for(auto &l : localization_points)
   {
     auto &score = l.second->second;
-    if(solver.get(l.first).is_true())
+    exprt v = solver.get(l.first);
+    if(v.is_constant() && to_constant_expr(v).is_true())
     {
       score++;
     }
-    else if(solver.get(l.first).is_false() && score > 0)
+    else if(v.is_constant() && to_constant_expr(v).is_false() && score > 0)
     {
       score--;
     }
diff --git a/src/goto-checker/goto_symex_property_decider.cpp b/src/goto-checker/goto_symex_property_decider.cpp
index 7dcc0fe1c40..1c10d3709c4 100644
--- a/src/goto-checker/goto_symex_property_decider.cpp
+++ b/src/goto-checker/goto_symex_property_decider.cpp
@@ -90,7 +90,8 @@ void goto_symex_property_decidert::add_constraint_from_goals(
   {
     if(
       select_property(goal_pair.first) &&
-      !goal_pair.second.condition.is_false())
+      (!goal_pair.second.condition.is_constant() ||
+       !to_constant_expr(goal_pair.second.condition).is_false()))
     {
       disjuncts.push_back(goal_pair.second.condition);
     }
@@ -142,10 +143,9 @@ void goto_symex_property_decidert::update_properties_status_from_goals(
     for(auto &goal_pair : goal_map)
     {
       auto &status = properties.at(goal_pair.first).status;
+      exprt v = solver->decision_procedure().get(goal_pair.second.condition);
       if(
-        solver->decision_procedure()
-          .get(goal_pair.second.condition)
-          .is_true() &&
+        v.is_constant() && to_constant_expr(v).is_true() &&
         status != property_statust::FAIL)
       {
         status |= property_statust::FAIL;
diff --git a/src/goto-checker/symex_bmc.cpp b/src/goto-checker/symex_bmc.cpp
index 56bd0c198d6..66f5b954161 100644
--- a/src/goto-checker/symex_bmc.cpp
+++ b/src/goto-checker/symex_bmc.cpp
@@ -57,19 +57,21 @@ void symex_bmct::symex_step(
   const goto_programt::const_targett cur_pc = state.source.pc;
   const guardt cur_guard = state.guard;
 
-  if(
-    !state.guard.is_false() && state.source.pc->is_assume() &&
-    simplify_expr(state.source.pc->condition(), ns).is_false())
+  if(!state.guard.is_false() && state.source.pc->is_assume())
   {
-    log.statistics() << "aborting path on assume(false) at "
-                     << state.source.pc->source_location() << " thread "
-                     << state.source.thread_nr;
-
-    const irep_idt &c = state.source.pc->source_location().get_comment();
-    if(!c.empty())
-      log.statistics() << ": " << c;
-
-    log.statistics() << log.eom;
+    exprt simp_cond = simplify_expr(state.source.pc->condition(), ns);
+    if(simp_cond.is_constant() && to_constant_expr(simp_cond).is_false())
+    {
+      log.statistics() << "aborting path on assume(false) at "
+                       << state.source.pc->source_location() << " thread "
+                       << state.source.thread_nr;
+
+      const irep_idt &c = state.source.pc->source_location().get_comment();
+      if(!c.empty())
+        log.statistics() << ": " << c;
+
+      log.statistics() << log.eom;
+    }
   }
 
   goto_symext::symex_step(get_goto_function, state);
@@ -88,7 +90,8 @@ void symex_bmct::symex_step(
     // sure the goto is considered covered
     if(
       cur_pc->is_goto() && cur_pc->get_target() != state.source.pc &&
-      cur_pc->condition().is_true())
+      cur_pc->condition().is_constant() &&
+      to_constant_expr(cur_pc->condition()).is_true())
       symex_coverage.covered(cur_pc, cur_pc->get_target());
     else if(!state.guard.is_false())
       symex_coverage.covered(cur_pc, state.source.pc);
@@ -111,8 +114,11 @@ void symex_bmct::merge_goto(
     // could the branch possibly be taken?
     !prev_guard.is_false() && !state.guard.is_false() &&
     // branches only, no single-successor goto
-    !prev_pc->condition().is_true())
+    (!prev_pc->condition().is_constant() ||
+     !to_constant_expr(prev_pc->condition()).is_true()))
+  {
     symex_coverage.covered(prev_pc, state.source.pc);
+  }
 }
 
 bool symex_bmct::should_stop_unwind(
diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp
index 9fbeaa5875b..aee698f102c 100644
--- a/src/goto-instrument/accelerate/accelerate.cpp
+++ b/src/goto-instrument/accelerate/accelerate.cpp
@@ -44,7 +44,8 @@ goto_programt::targett acceleratet::find_back_jump(
   for(const auto &t : loop)
   {
     if(
-      t->is_goto() && t->condition().is_true() && t->targets.size() == 1 &&
+      t->is_goto() && t->condition().is_constant() &&
+      to_constant_expr(t->condition()).is_true() && t->targets.size() == 1 &&
       t->targets.front() == loop_header &&
       t->location_number > back_jump->location_number)
     {
diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp
index a0a6dcd37ad..8506de77737 100644
--- a/src/goto-instrument/accelerate/acceleration_utils.cpp
+++ b/src/goto-instrument/accelerate/acceleration_utils.cpp
@@ -256,7 +256,10 @@ exprt acceleration_utilst::precondition(patht &path)
       // Ignore.
     }
 
-    if(!r_it->guard.is_true() && !r_it->guard.is_nil())
+    if(
+      (!r_it->guard.is_constant() ||
+       !to_constant_expr(r_it->guard).is_true()) &&
+      !r_it->guard.is_nil())
     {
       // The guard isn't constant true, so we need to accumulate that too.
       ret=implies_exprt(r_it->guard, ret);
diff --git a/src/goto-instrument/accelerate/cone_of_influence.cpp b/src/goto-instrument/accelerate/cone_of_influence.cpp
index 43256e6fc1a..9bc9eac5058 100644
--- a/src/goto-instrument/accelerate/cone_of_influence.cpp
+++ b/src/goto-instrument/accelerate/cone_of_influence.cpp
@@ -89,7 +89,9 @@ void cone_of_influencet::get_succs(
 
   if(rit->is_goto())
   {
-    if(!rit->condition().is_false())
+    if(
+      !rit->condition().is_constant() ||
+      !to_constant_expr(rit->condition()).is_false())
     {
       // Branch can be taken.
       for(goto_programt::targetst::const_iterator t=rit->targets.begin();
@@ -102,14 +104,18 @@ void cone_of_influencet::get_succs(
       }
     }
 
-    if(rit->condition().is_true())
+    if(
+      rit->condition().is_constant() &&
+      to_constant_expr(rit->condition()).is_true())
     {
       return;
     }
   }
   else if(rit->is_assume() || rit->is_assert())
   {
-    if(rit->condition().is_false())
+    if(
+      rit->condition().is_constant() &&
+      to_constant_expr(rit->condition()).is_false())
     {
       return;
     }
diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
index 954be5565e6..93cc2d8fe34 100644
--- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
+++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
@@ -789,7 +789,9 @@ void disjunctive_polynomial_accelerationt::build_path(
     for(const auto &succ : succs)
     {
       exprt &distinguisher=distinguishing_points[succ];
-      bool taken=scratch_program.eval(distinguisher).is_true();
+      exprt distinguisher_eval = scratch_program.eval(distinguisher);
+      bool taken = distinguisher_eval.is_constant() &&
+                   to_constant_expr(distinguisher_eval).is_true();
 
       if(taken)
       {
@@ -992,7 +994,8 @@ void disjunctive_polynomial_accelerationt::record_path(
       it != distinguishers.end();
       ++it)
   {
-    path_val[*it]=program.eval(*it).is_true();
+    exprt eval = program.eval(*it);
+    path_val[*it] = eval.is_constant() && to_constant_expr(eval).is_true();
   }
 
   accelerated_paths.push_back(path_val);
diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
index 41a88788c58..f6801faac96 100644
--- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp
+++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
@@ -785,7 +785,10 @@ exprt polynomial_acceleratort::precondition(patht &path)
       // Ignore.
     }
 
-    if(!r_it->guard.is_true() && !r_it->guard.is_nil())
+    if(
+      (!r_it->guard.is_constant() ||
+       !to_constant_expr(r_it->guard).is_true()) &&
+      !r_it->guard.is_nil())
     {
       // The guard isn't constant true, so we need to accumulate that too.
       ret=implies_exprt(r_it->guard, ret);
diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.cpp b/src/goto-instrument/accelerate/sat_path_enumerator.cpp
index eb645a5a9b1..c63242295d4 100644
--- a/src/goto-instrument/accelerate/sat_path_enumerator.cpp
+++ b/src/goto-instrument/accelerate/sat_path_enumerator.cpp
@@ -136,7 +136,9 @@ void sat_path_enumeratort::build_path(
     for(const auto &succ : succs)
     {
       exprt &distinguisher=distinguishing_points[succ];
-      bool taken=scratch_program.eval(distinguisher).is_true();
+      exprt distinguisher_eval = scratch_program.eval(distinguisher);
+      bool taken = distinguisher_eval.is_constant() &&
+                   to_constant_expr(distinguisher_eval).is_true();
 
       if(taken)
       {
@@ -335,7 +337,10 @@ void sat_path_enumeratort::record_path(scratch_programt &program)
   distinguish_valuest path_val;
 
   for(const auto &expr : distinguishers)
-    path_val[expr]=program.eval(expr).is_true();
+  {
+    exprt eval = program.eval(expr);
+    path_val[expr] = eval.is_constant() && to_constant_expr(eval).is_true();
+  }
 
   accelerated_paths.push_back(path_val);
 }
diff --git a/src/goto-instrument/call_sequences.cpp b/src/goto-instrument/call_sequences.cpp
index ddbc688aa47..a797cdb67ca 100644
--- a/src/goto-instrument/call_sequences.cpp
+++ b/src/goto-instrument/call_sequences.cpp
@@ -231,8 +231,12 @@ void check_call_sequencet::operator()()
     {
       goto_programt::const_targett t=e.pc->get_target();
 
-      if(e.pc->condition().is_true())
+      if(
+        e.pc->condition().is_constant() &&
+        to_constant_expr(e.pc->condition()).is_true())
+      {
         e.pc=t;
+      }
       else
       {
         e.pc++;
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
index f99d87e4477..a2a6000f004 100644
--- a/src/goto-instrument/contracts/contracts.cpp
+++ b/src/goto-instrument/contracts/contracts.cpp
@@ -375,7 +375,9 @@ void code_contractst::check_apply_loop_contracts(
   }
 
   // TODO: Fix loop contract handling for do/while loops.
-  if(loop_end->is_goto() && !loop_end->condition().is_true())
+  if(
+    loop_end->is_goto() && (!loop_end->condition().is_constant() ||
+                            !to_constant_expr(loop_end->condition()).is_true()))
   {
     log.error() << "Loop contracts are unsupported on do/while loops: "
                 << loop_head_location << messaget::eom;
@@ -782,7 +784,7 @@ void code_contractst::apply_function_contract(
   // Generate: assume(ensures)
   for(auto &clause : instantiated_ensures_clauses)
   {
-    if(clause.is_false())
+    if(clause.is_constant() && to_constant_expr(clause).is_false())
     {
       throw invalid_input_exceptiont(
         std::string("Attempt to assume false at ")
@@ -1353,7 +1355,9 @@ void code_contractst::add_contract_check(
   {
     auto instantiated_clause =
       to_lambda_expr(clause).application(instantiation_values);
-    if(instantiated_clause.is_false())
+    if(
+      instantiated_clause.is_constant() &&
+      to_constant_expr(instantiated_clause).is_false())
     {
       throw invalid_input_exceptiont(
         std::string("Attempt to assume false at ")
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_check_loop_normal_form.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_check_loop_normal_form.cpp
index 505ca6c6695..e797707edd6 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_check_loop_normal_form.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_check_loop_normal_form.cpp
@@ -156,7 +156,10 @@ void dfcc_check_loop_normal_form(goto_programt &goto_program, messaget &log)
     //       IF TRUE GOTO HEAD
     // EXIT: SKIP
     // ```
-    if(latch->has_condition() && !latch->condition().is_true())
+    if(
+      latch->has_condition() &&
+      (!latch->condition().is_constant() ||
+       !to_constant_expr(latch->condition()).is_true()))
     {
       const source_locationt &loc = latch->source_location();
       const auto &exit =
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp
index 8a97ef48fd0..41ad34547a4 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp
@@ -110,8 +110,8 @@ void dfcc_contract_clauses_codegent::encode_assignable_target_group(
     new_vars = cleaner.clean(condition, dest, language_mode);
 
   // Jump target if condition is false
-  auto goto_instruction = dest.add(
-    goto_programt::make_incomplete_goto(not_exprt{condition}, source_location));
+  auto goto_instruction = dest.add(goto_programt::make_incomplete_goto(
+    boolean_negate(condition), source_location));
 
   for(const auto &target : group.targets())
     encode_assignable_target(language_mode, target, dest);
@@ -169,7 +169,7 @@ void dfcc_contract_clauses_codegent::encode_assignable_target(
     arguments.emplace_back(size.value());
 
     // is_ptr_to_ptr
-    arguments.emplace_back(make_boolean_expr(target.type().id() == ID_pointer));
+    arguments.emplace_back(constant_exprt{target.type().id() == ID_pointer});
 
     dest.add(
       goto_programt::make_function_call(code_function_call, source_location));
@@ -199,8 +199,8 @@ void dfcc_contract_clauses_codegent::encode_freeable_target_group(
     new_vars = cleaner.clean(condition, dest, language_mode);
 
   // Jump target if condition is false
-  auto goto_instruction = dest.add(
-    goto_programt::make_incomplete_goto(not_exprt{condition}, source_location));
+  auto goto_instruction = dest.add(goto_programt::make_incomplete_goto(
+    boolean_negate(condition), source_location));
 
   for(const auto &target : group.targets())
     encode_freeable_target(language_mode, target, dest);
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp
index 45d83370521..fe4c425ee61 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp
@@ -282,8 +282,8 @@ void dfcc_wrapper_programt::encode_requires_write_set()
     addr_of_requires_write_set,
     from_integer(0, size_type()),
     from_integer(0, size_type()),
-    make_boolean_expr(check_mode),
-    make_boolean_expr(!check_mode),
+    constant_exprt{check_mode},
+    constant_exprt{!check_mode},
     false_exprt(),
     false_exprt(),
     true_exprt(),
@@ -355,8 +355,8 @@ void dfcc_wrapper_programt::encode_ensures_write_set()
     from_integer(0, size_type()),
     false_exprt(),
     false_exprt(),
-    make_boolean_expr(!check_mode),
-    make_boolean_expr(check_mode),
+    constant_exprt{!check_mode},
+    constant_exprt{check_mode},
     true_exprt(),
     true_exprt(),
     wrapper_sl);
diff --git a/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp b/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp
index 346fbe6e78f..b820ce321f1 100644
--- a/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp
+++ b/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp
@@ -68,7 +68,7 @@ void havoc_assigns_clause_targetst::havoc_if_valid(
     skip_program.add(goto_programt::make_skip(source_location_no_checks));
 
   dest.add(goto_programt::make_goto(
-    skip_target, not_exprt{car.valid_var()}, source_location_no_checks));
+    skip_target, boolean_negate(car.valid_var()), source_location_no_checks));
 
   if(car.havoc_method == car_havoc_methodt::HAVOC_OBJECT)
   {
@@ -142,7 +142,7 @@ void havoc_assigns_clause_targetst::havoc_static_local(
     skip_program.add(goto_programt::make_skip(source_location_no_checks));
 
   dest.add(goto_programt::make_goto(
-    skip_target, not_exprt{car.valid_var()}, source_location_no_checks));
+    skip_target, boolean_negate(car.valid_var()), source_location_no_checks));
 
   const auto &target_type = car.target().type();
   side_effect_expr_nondett nondet(target_type, source_location);
diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp
index fc273e46259..e2a4fdb64b8 100644
--- a/src/goto-instrument/contracts/instrument_spec_assigns.cpp
+++ b/src/goto-instrument/contracts/instrument_spec_assigns.cpp
@@ -585,8 +585,10 @@ car_exprt instrument_spec_assignst::create_car_expr(
           valid_var,
           lower_bound_var,
           upper_bound_var,
-          is_ptr_to_ptr.is_true() ? car_havoc_methodt::NONDET_ASSIGN
-                                  : car_havoc_methodt::HAVOC_SLICE};
+          (is_ptr_to_ptr.is_constant() &&
+           to_constant_expr(is_ptr_to_ptr).is_true())
+            ? car_havoc_methodt::NONDET_ASSIGN
+            : car_havoc_methodt::HAVOC_SLICE};
       }
     }
   }
@@ -656,9 +658,9 @@ exprt instrument_spec_assignst::target_validity_expr(
   // (or is NULL if we allow it explicitly).
   // This assertion will be falsified whenever `start_address` is invalid or
   // not of the right size (or is NULL if we do not allow it explicitly).
-  auto result =
-    or_exprt{not_exprt{car.condition()},
-             w_ok_exprt{car.target_start_address(), car.target_size()}};
+  auto result = or_exprt{
+    boolean_negate(car.condition()),
+    w_ok_exprt{car.target_start_address(), car.target_size()}};
 
   if(allow_null_target)
     result.add_to_operands(null_object(car.target_start_address()));
@@ -685,7 +687,9 @@ void instrument_spec_assignst::target_validity_assertion(
   std::string comment = "Check that ";
   comment += from_expr(ns, "", car.target());
   comment += " is valid";
-  if(!car.condition().is_true())
+  if(
+    !car.condition().is_constant() ||
+    !to_constant_expr(car.condition()).is_true())
   {
     comment += " when ";
     comment += from_expr(ns, "", car.condition());
@@ -719,8 +723,12 @@ void instrument_spec_assignst::inclusion_check_assertion(
   std::string comment = "Check that ";
   if(!is_assigns_clause_replacement_tracking_comment(orig_comment))
   {
-    if(!car.condition().is_true())
+    if(
+      !car.condition().is_constant() ||
+      !to_constant_expr(car.condition()).is_true())
+    {
       comment += from_expr(ns, "", car.condition()) + ": ";
+    }
     comment += from_expr(ns, "", car.target());
   }
   else
diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp
index a33319509b2..d64b2ed91d8 100644
--- a/src/goto-instrument/contracts/utils.cpp
+++ b/src/goto-instrument/contracts/utils.cpp
@@ -41,7 +41,9 @@ static void append_safe_havoc_code_for_expr(
   // skip havocing only if all pointer derefs in the expression are valid
   // (to avoid spurious pointer deref errors)
   dest.add(goto_programt::make_goto(
-    skip_target, not_exprt{all_dereferences_are_valid(expr, ns)}, location));
+    skip_target,
+    boolean_negate(all_dereferences_are_valid(expr, ns)),
+    location));
 
   havoc_code_impl();
 
@@ -149,7 +151,9 @@ void havoc_assigns_targetst::append_havoc_code_for_expr(
     {
       const auto &ptr = funcall.arguments().at(0);
       const auto &size = funcall.arguments().at(1);
-      if(funcall.arguments().at(2).is_true())
+      if(
+        funcall.arguments().at(2).is_constant() &&
+        to_constant_expr(funcall.arguments().at(2)).is_true())
       {
         append_havoc_pointer_code(expr.source_location(), ptr, dest);
       }
@@ -259,10 +263,14 @@ void simplify_gotos(goto_programt &goto_program, namespacet &ns)
 {
   for(auto &instruction : goto_program.instructions)
   {
-    if(
-      instruction.is_goto() &&
-      simplify_expr(instruction.condition(), ns).is_false())
+    if(!instruction.is_goto())
+      continue;
+
+    exprt simp_cond = simplify_expr(instruction.condition(), ns);
+    if(simp_cond.is_constant() && to_constant_expr(simp_cond).is_false())
+    {
       instruction.turn_into_skip();
+    }
   }
 }
 
@@ -433,8 +441,8 @@ static void replace_history_parameter_rec(
 
     // 2.2. Skip storing the history if the expression is invalid
     auto goto_instruction = history.add(goto_programt::make_incomplete_goto(
-      not_exprt{
-        all_dereferences_are_valid(parameter, namespacet(symbol_table))},
+      boolean_negate(
+        all_dereferences_are_valid(parameter, namespacet(symbol_table))),
       location));
 
     // 2.3. Add an assignment such that the value pointed to by the new
diff --git a/src/goto-instrument/cover_basic_blocks.cpp b/src/goto-instrument/cover_basic_blocks.cpp
index 36af6b16964..ef1e3f207dc 100644
--- a/src/goto-instrument/cover_basic_blocks.cpp
+++ b/src/goto-instrument/cover_basic_blocks.cpp
@@ -23,8 +23,11 @@ std::optional<std::size_t> cover_basic_blockst::continuation_of_block(
   const goto_programt::targett in_t = *instruction->incoming_edges.cbegin();
   if(
     in_t->is_goto() && !in_t->is_backwards_goto() &&
-    in_t->condition().is_true())
+    in_t->condition().is_constant() &&
+    to_constant_expr(in_t->condition()).is_true())
+  {
     return block_map[in_t];
+  }
 
   return {};
 }
diff --git a/src/goto-instrument/cover_instrument_branch.cpp b/src/goto-instrument/cover_instrument_branch.cpp
index efec9d5409c..0619b96bb38 100644
--- a/src/goto-instrument/cover_instrument_branch.cpp
+++ b/src/goto-instrument/cover_instrument_branch.cpp
@@ -26,7 +26,8 @@ void cover_branch_instrumentert::instrument(
   const bool is_function_entry_point =
     i_it == goto_program.instructions.begin();
   const bool is_conditional_goto =
-    i_it->is_goto() && !i_it->condition().is_true();
+    i_it->is_goto() && (!i_it->condition().is_constant() ||
+                        !to_constant_expr(i_it->condition()).is_true());
   if(!is_function_entry_point && !is_conditional_goto)
     return;
 
diff --git a/src/goto-instrument/dot.cpp b/src/goto-instrument/dot.cpp
index 770a52a5f26..5c50d772d4e 100644
--- a/src/goto-instrument/dot.cpp
+++ b/src/goto-instrument/dot.cpp
@@ -108,8 +108,12 @@ void dott::write_dot_subgraph(
       std::stringstream tmp;
       if(it->is_goto())
       {
-        if(it->condition().is_true())
+        if(
+          it->condition().is_constant() &&
+          to_constant_expr(it->condition()).is_true())
+        {
           tmp.str("Goto");
+        }
         else
         {
           std::string t = from_expr(ns, function_id, it->condition());
@@ -320,14 +324,20 @@ void dott::find_next(
   std::set<goto_programt::const_targett, goto_programt::target_less_than> &tres,
   std::set<goto_programt::const_targett, goto_programt::target_less_than> &fres)
 {
-  if(it->is_goto() && !it->condition().is_false())
+  if(
+    it->is_goto() && (!it->condition().is_constant() ||
+                      !to_constant_expr(it->condition()).is_false()))
   {
     for(const auto &target : it->targets)
       tres.insert(target);
   }
 
-  if(it->is_goto() && it->condition().is_true())
+  if(
+    it->is_goto() && it->condition().is_constant() &&
+    to_constant_expr(it->condition()).is_true())
+  {
     return;
+  }
 
   goto_programt::const_targett next = it; next++;
   if(next!=instructions.end())
diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp
index 8f6800b35b8..dc2ff6115e7 100644
--- a/src/goto-instrument/dump_c.cpp
+++ b/src/goto-instrument/dump_c.cpp
@@ -1399,7 +1399,7 @@ void dump_ct::cleanup_expr(exprt &expr)
     }
     // add a typecast for NULL
     else if(
-      u.op().is_constant() && is_null_pointer(to_constant_expr(u.op())) &&
+      u.op().is_constant() && to_constant_expr(u.op()).is_null_pointer() &&
       to_pointer_type(u.op().type()).base_type().id() == ID_empty)
     {
       const struct_union_typet::componentt &comp=
@@ -1459,7 +1459,7 @@ void dump_ct::cleanup_expr(exprt &expr)
             // add a typecast for NULL or 0
             if(
               argument.is_constant() &&
-              is_null_pointer(to_constant_expr(argument)))
+              to_constant_expr(argument).is_null_pointer())
             {
               const typet &comp_type=
                 to_union_type(type).components().front().type();
@@ -1499,7 +1499,9 @@ void dump_ct::cleanup_expr(exprt &expr)
   {
     const byte_update_exprt &bu = to_byte_update_expr(expr);
 
-    if(bu.op().id() == ID_union && bu.offset().is_zero())
+    if(
+      bu.op().id() == ID_union && bu.offset().is_constant() &&
+      to_constant_expr(bu.offset()).is_zero())
     {
       const union_exprt &union_expr = to_union_expr(bu.op());
       const union_typet &union_type =
@@ -1537,7 +1539,7 @@ void dump_ct::cleanup_expr(exprt &expr)
       to_side_effect_expr(bu.op()).get_statement() == ID_nondet &&
       (bu.op().type().id() == ID_union ||
        bu.op().type().id() == ID_union_tag) &&
-      bu.offset().is_zero())
+      bu.offset().is_constant() && to_constant_expr(bu.offset()).is_zero())
     {
       const union_typet &union_type =
         bu.op().type().id() == ID_union_tag
diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index f8b8c8a6414..5e1d79dd2d7 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -281,9 +281,12 @@ void full_slicert::operator()(
     else if(implicit(instruction))
       add_to_queue(queue, instruction_node_index, instruction);
     else if(
-      (instruction->is_goto() && instruction->condition().is_true()) ||
+      (instruction->is_goto() && instruction->condition().is_constant() &&
+       to_constant_expr(instruction->condition()).is_true()) ||
       instruction->is_throw())
+    {
       jumps.push_back(instruction_node_index);
+    }
     else if(instruction->is_decl())
     {
       const auto &s = instruction->decl_symbol();
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
index 94c3351236d..c733e926e23 100644
--- a/src/goto-instrument/goto_program2code.cpp
+++ b/src/goto-instrument/goto_program2code.cpp
@@ -311,7 +311,7 @@ goto_programt::const_targett goto_program2codet::convert_assign_varargs(
   const exprt this_va_list_expr = target->assign_lhs();
   const exprt &r = skip_typecast(target->assign_rhs());
 
-  if(r.is_constant() && is_null_pointer(to_constant_expr(r)))
+  if(r.is_constant() && to_constant_expr(r).is_null_pointer())
   {
     code_function_callt f(
       symbol_exprt("va_end", code_typet({}, empty_typet())),
@@ -550,8 +550,12 @@ goto_programt::const_targett goto_program2codet::convert_goto(
       (upper_bound==goto_program.instructions.end() ||
        upper_bound->location_number > loop_entry->second->location_number))
     return convert_goto_while(target, loop_entry->second, dest);
-  else if(!target->condition().is_true())
+  else if(
+    !target->condition().is_constant() ||
+    !to_constant_expr(target->condition()).is_true())
+  {
     return convert_goto_switch(target, upper_bound, dest);
+  }
   else if(!loop_last_stack.empty())
     return convert_goto_break_continue(target, upper_bound, dest);
   else
@@ -580,7 +584,9 @@ goto_programt::const_targett goto_program2codet::convert_goto_while(
     w.cond() = not_exprt(target->condition());
     simplify(w.cond(), ns);
   }
-  else if(target->condition().is_true())
+  else if(
+    target->condition().is_constant() &&
+    to_constant_expr(target->condition()).is_true())
   {
     target = convert_goto_goto(target, to_code_block(w.body()));
   }
@@ -597,11 +603,15 @@ goto_programt::const_targett goto_program2codet::convert_goto_while(
   loop_last_stack.pop_back();
 
   convert_labels(loop_end, to_code_block(w.body()));
-  if(loop_end->condition().is_false())
+  if(
+    loop_end->condition().is_constant() &&
+    to_constant_expr(loop_end->condition()).is_false())
   {
     to_code_block(w.body()).add(code_breakt());
   }
-  else if(!loop_end->condition().is_true())
+  else if(
+    !loop_end->condition().is_constant() ||
+    !to_constant_expr(loop_end->condition()).is_true())
   {
     code_ifthenelset i(not_exprt(loop_end->condition()), code_breakt());
     simplify(i.cond(), ns);
@@ -624,15 +634,18 @@ goto_programt::const_targett goto_program2codet::convert_goto_while(
 
     f.swap(w);
   }
-  else if(w.body().has_operands() &&
-          w.cond().is_true())
+  else if(
+    w.body().has_operands() && w.cond().is_constant() &&
+    to_constant_expr(w.cond()).is_true())
   {
     const codet &back=to_code(w.body().operands().back());
 
-    if(back.get_statement()==ID_break ||
-       (back.get_statement()==ID_ifthenelse &&
-        to_code_ifthenelse(back).cond().is_true() &&
-        to_code_ifthenelse(back).then_case().get_statement()==ID_break))
+    if(
+      back.get_statement() == ID_break ||
+      (back.get_statement() == ID_ifthenelse &&
+       to_code_ifthenelse(back).cond().is_constant() &&
+       to_constant_expr(to_code_ifthenelse(back).cond()).is_true() &&
+       to_code_ifthenelse(back).then_case().get_statement() == ID_break))
     {
       w.body().operands().pop_back();
       code_dowhilet d(false_exprt(), w.body());
@@ -667,7 +680,8 @@ goto_programt::const_targett goto_program2codet::get_cases(
   {
     if(
       cases_it->is_goto() && !cases_it->is_backwards_goto() &&
-      cases_it->condition().is_true())
+      cases_it->condition().is_constant() &&
+      to_constant_expr(cases_it->condition()).is_true())
     {
       default_target=cases_it->get_target();
 
@@ -834,7 +848,8 @@ bool goto_program2codet::remove_default(
         next_case != goto_program.instructions.end() &&
         next_case == default_target &&
         (!it->case_last->is_goto() ||
-         (it->case_last->condition().is_true() &&
+         (it->case_last->condition().is_constant() &&
+          to_constant_expr(it->case_last->condition()).is_true() &&
           it->case_last->get_target() == default_target)))
       {
         // if there is no goto here, yet we got here, all others would
@@ -845,9 +860,12 @@ bool goto_program2codet::remove_default(
 
     // jumps to default are ok
     if(
-      it->case_last->is_goto() && it->case_last->condition().is_true() &&
+      it->case_last->is_goto() && it->case_last->condition().is_constant() &&
+      to_constant_expr(it->case_last->condition()).is_true() &&
       it->case_last->get_target() == default_target)
+    {
       continue;
+    }
 
     // fall-through is ok
     if(!it->case_last->is_goto())
@@ -1059,7 +1077,8 @@ goto_programt::const_targett goto_program2codet::convert_goto_if(
     has_else =
       before_else->is_goto() &&
       before_else->get_target()->location_number > end_if->location_number &&
-      before_else->condition().is_true() &&
+      before_else->condition().is_constant() &&
+      to_constant_expr(before_else->condition()).is_true() &&
       (upper_bound == goto_program.instructions.end() ||
        upper_bound->location_number >=
          before_else->get_target()->location_number);
@@ -1145,7 +1164,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_break_continue(
 
     copy_source_location(target, i);
 
-    if(i.cond().is_true())
+    if(i.cond().is_constant() && to_constant_expr(i.cond()).is_true())
       dest.add(std::move(i.then_case()));
     else
       dest.add(std::move(i));
@@ -1169,7 +1188,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_break_continue(
 
     copy_source_location(target, i);
 
-    if(i.cond().is_true())
+    if(i.cond().is_constant() && to_constant_expr(i.cond()).is_true())
       dest.add(std::move(i.then_case()));
     else
       dest.add(std::move(i));
@@ -1227,7 +1246,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_goto(
 
   copy_source_location(target, i);
 
-  if(i.cond().is_true())
+  if(i.cond().is_constant() && to_constant_expr(i.cond()).is_true())
     dest.add(std::move(i.then_case()));
   else
     dest.add(std::move(i));
@@ -1292,7 +1311,9 @@ goto_programt::const_targett goto_program2codet::convert_start_thread(
   // 2: code in existing thread
   /* check the structure and compute the iterators */
   DATA_INVARIANT(
-    next->is_goto() && next->condition().is_true(), "START THREAD pattern");
+    next->is_goto() && next->condition().is_constant() &&
+      to_constant_expr(next->condition()).is_true(),
+    "START THREAD pattern");
   DATA_INVARIANT(!next->is_backwards_goto(), "START THREAD pattern");
   DATA_INVARIANT(
     thread_start->location_number < next->get_target()->location_number,
@@ -1508,9 +1529,13 @@ void goto_program2codet::cleanup_code(
     if(do_while.body().get_statement()==ID_skip)
       do_while.set_statement(ID_while);
     // do stmt while(false) is just stmt
-    else if(do_while.cond().is_false() &&
-            do_while.body().get_statement()!=ID_block)
+    else if(
+      do_while.cond().is_constant() &&
+      to_constant_expr(do_while.cond()).is_false() &&
+      do_while.body().get_statement() != ID_block)
+    {
       code=do_while.body();
+    }
   }
 }
 
@@ -1692,13 +1717,15 @@ void goto_program2codet::cleanup_code_ifthenelse(
   // assert(false) expands to if(true) assert(false), simplify again (and also
   // simplify other cases)
   if(
-    cond.is_true() &&
+    cond.is_constant() && to_constant_expr(cond).is_true() &&
     (i_t_e.else_case().is_nil() || !has_labels(i_t_e.else_case())))
   {
     codet tmp = i_t_e.then_case();
     code.swap(tmp);
   }
-  else if(cond.is_false() && !has_labels(i_t_e.then_case()))
+  else if(
+    cond.is_constant() && to_constant_expr(cond).is_false() &&
+    !has_labels(i_t_e.then_case()))
   {
     if(i_t_e.else_case().is_nil())
       code=code_skipt();
diff --git a/src/goto-instrument/horn_encoding.cpp b/src/goto-instrument/horn_encoding.cpp
index 4d316fe47bd..2b32d454170 100644
--- a/src/goto-instrument/horn_encoding.cpp
+++ b/src/goto-instrument/horn_encoding.cpp
@@ -428,7 +428,9 @@ std::vector<symbol_exprt> state_encodingt::incoming_symbols(loct loc) const
 
     // conditional jump from loc_in to loc?
     if(
-      loc_in->is_goto() && !loc_in->condition().is_true() &&
+      loc_in->is_goto() &&
+      (!loc_in->condition().is_constant() ||
+       !to_constant_expr(loc_in->condition()).is_true()) &&
       loc != std::next(loc_in))
     {
       suffix = "T";
@@ -688,7 +690,9 @@ void state_encodingt::setup_incoming(const goto_functiont &goto_function)
   forall_goto_program_instructions(it, goto_function.body)
   {
     auto next = std::next(it);
-    if(it->is_goto() && it->condition().is_true())
+    if(
+      it->is_goto() && it->condition().is_constant() &&
+      to_constant_expr(it->condition()).is_true())
     {
     }
     else if(next != goto_function.body.instructions.end())
@@ -921,7 +925,7 @@ void state_encodingt::encode(
       // We produce ∅ when the 'other' branch is taken. Get the condition.
       const auto &condition = loc->condition();
 
-      if(condition.is_true())
+      if(condition.is_constant() && to_constant_expr(condition).is_true())
       {
         dest << equal_exprt(out_state_expr(loc), in_state_expr(loc));
       }
diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp
index c52adcdd905..837ef835d54 100644
--- a/src/goto-instrument/unwind.cpp
+++ b/src/goto-instrument/unwind.cpp
@@ -141,7 +141,9 @@ void goto_unwindt::unwind(
 
     exprt exit_cond = false_exprt(); // default is false
 
-    if(!t->condition().is_true()) // cond in backedge
+    if(
+      !t->condition().is_constant() ||
+      !to_constant_expr(t->condition()).is_true()) // cond in backedge
     {
       exit_cond = boolean_negate(t->condition());
     }
@@ -191,7 +193,9 @@ void goto_unwindt::unwind(
     goto_programt::const_targett t_before=loop_exit;
     t_before--;
 
-    if(!t_before->is_goto() || !t_before->condition().is_true())
+    if(
+      !t_before->is_goto() || !t_before->condition().is_constant() ||
+      !to_constant_expr(t_before->condition()).is_true())
     {
       goto_programt::targett t_goto = goto_program.insert_before(
         loop_exit,
diff --git a/src/goto-programs/cfg.h b/src/goto-programs/cfg.h
index e271d761b19..6e152b5905c 100644
--- a/src/goto-programs/cfg.h
+++ b/src/goto-programs/cfg.h
@@ -320,7 +320,8 @@ void cfg_baset<T, P, I>::compute_edges_goto(
 {
   if(
     next_PC != goto_program.instructions.end() &&
-    !instruction.condition().is_true())
+    (!instruction.condition().is_constant() ||
+     !to_constant_expr(instruction.condition()).is_true()))
   {
     this->add_edge(entry, entry_map[next_PC]);
   }
@@ -501,8 +502,12 @@ void cfg_baset<T, P, I>::compute_edges(
 
   case ASSUME:
     // false guard -> no successor
-    if(instruction.condition().is_false())
+    if(
+      instruction.condition().is_constant() &&
+      to_constant_expr(instruction.condition()).is_false())
+    {
       break;
+    }
 
   case ASSIGN:
   case ASSERT:
diff --git a/src/goto-programs/ensure_one_backedge_per_target.cpp b/src/goto-programs/ensure_one_backedge_per_target.cpp
index f9f3c2c6d1e..3bdc63bb9a4 100644
--- a/src/goto-programs/ensure_one_backedge_per_target.cpp
+++ b/src/goto-programs/ensure_one_backedge_per_target.cpp
@@ -57,7 +57,9 @@ bool ensure_one_backedge_per_target(
 
   // If the last backedge is a conditional jump, add an extra unconditional
   // backedge after it:
-  if(!last_backedge->condition().is_true())
+  if(
+    !last_backedge->condition().is_constant() ||
+    !to_constant_expr(last_backedge->condition()).is_true())
   {
     auto new_goto =
       goto_program.insert_after(last_backedge, goto_programt::make_goto(it));
diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp
index db89fd0f4fd..46a418c656c 100644
--- a/src/goto-programs/goto_program.cpp
+++ b/src/goto-programs/goto_program.cpp
@@ -79,7 +79,7 @@ std::ostream &goto_programt::instructiont::output(std::ostream &out) const
 
   case GOTO:
   case INCOMPLETE_GOTO:
-    if(!condition().is_true())
+    if(!condition().is_constant() || !to_constant_expr(condition()).is_true())
     {
       out << "IF " << format(condition()) << " THEN ";
     }
@@ -525,7 +525,9 @@ std::string as_string(
     return "(NO INSTRUCTION TYPE)";
 
   case GOTO:
-    if(!i.condition().is_true())
+    if(
+      !i.condition().is_constant() ||
+      !to_constant_expr(i.condition()).is_true())
     {
       result += "IF " + from_expr(ns, function, i.condition()) + " THEN ";
     }
@@ -742,8 +744,14 @@ void goto_programt::copy_from(const goto_programt &src)
 bool goto_programt::has_assertion() const
 {
   for(const auto &i : instructions)
-    if(i.is_assert() && !i.condition().is_true())
+  {
+    if(
+      i.is_assert() && (!i.condition().is_constant() ||
+                        !to_constant_expr(i.condition()).is_true()))
+    {
       return true;
+    }
+  }
 
   return false;
 }
diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h
index fa8eca15353..6a9a1e9c05b 100644
--- a/src/goto-programs/goto_program.h
+++ b/src/goto-programs/goto_program.h
@@ -1137,8 +1137,13 @@ std::list<Target> goto_programt::get_successors(
   {
     std::list<Target> successors(i.targets.begin(), i.targets.end());
 
-    if(!i.condition().is_true() && next != instructions.end())
+    if(
+      (!i.condition().is_constant() ||
+       !to_constant_expr(i.condition()).is_true()) &&
+      next != instructions.end())
+    {
       successors.push_back(next);
+    }
 
     return successors;
   }
@@ -1167,7 +1172,9 @@ std::list<Target> goto_programt::get_successors(
 
   if(i.is_assume())
   {
-    return !i.condition().is_false() && next != instructions.end()
+    return (!i.condition().is_constant() ||
+            !to_constant_expr(i.condition()).is_false()) &&
+               next != instructions.end()
              ? std::list<Target>{next}
              : std::list<Target>();
   }
diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp
index 0a7797af2d3..af722107ab8 100644
--- a/src/goto-programs/goto_trace.cpp
+++ b/src/goto-programs/goto_trace.cpp
@@ -229,7 +229,7 @@ std::string trace_numeric_value(
     }
     else if(type.id()==ID_bool)
     {
-      return expr.is_true()?"1":"0";
+      return to_constant_expr(expr).is_true() ? "1" : "0";
     }
     else if(type.id()==ID_integer)
     {
diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index e0aef679768..1c9dde5a659 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -238,8 +238,12 @@ static bool filter_out(
     prev_it->pc->source_location() == it->pc->source_location())
     return true;
 
-  if(it->is_goto() && it->pc->condition().is_true())
+  if(
+    it->is_goto() && it->pc->condition().is_constant() &&
+    to_constant_expr(it->pc->condition()).is_true())
+  {
     return true;
+  }
 
   const source_locationt &source_location = it->pc->source_location();
 
@@ -546,7 +550,8 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
     if(
       it->hidden ||
       (!it->is_assignment() && !it->is_goto() && !it->is_assert()) ||
-      (it->is_goto() && it->source.pc->condition().is_true()) ||
+      (it->is_goto() && it->source.pc->condition().is_constant() &&
+       to_constant_expr(it->source.pc->condition()).is_true()) ||
       source_location.is_nil() || source_location.is_built_in() ||
       source_location.get_line().empty())
     {
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
index cdb413e351e..7c1997ce1f8 100644
--- a/src/goto-programs/interpreter_evaluate.cpp
+++ b/src/goto-programs/interpreter_evaluate.cpp
@@ -382,7 +382,7 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr)
     }
     else if(expr.is_boolean())
     {
-      return {expr.is_true()};
+      return {to_constant_expr(expr).is_true()};
     }
     else if(expr.type().id()==ID_string)
     {
diff --git a/src/goto-programs/json_expr.cpp b/src/goto-programs/json_expr.cpp
index 16139131b90..5b534131555 100644
--- a/src/goto-programs/json_expr.cpp
+++ b/src/goto-programs/json_expr.cpp
@@ -53,7 +53,7 @@ static exprt simplify_json_expr(const exprt &src)
     }
     else if(
       object.id() == ID_index && to_index_expr(object).index().is_constant() &&
-      to_constant_expr(to_index_expr(object).index()).value_is_zero_string())
+      to_constant_expr(to_index_expr(object).index()).is_zero())
     {
       // simplify expressions of the form  &array[0]
       return simplify_json_expr(to_index_expr(object).array());
@@ -288,8 +288,9 @@ json_objectt json(const exprt &expr, const namespacet &ns, const irep_idt &mode)
     else if(type.id() == ID_bool)
     {
       result["name"] = json_stringt("boolean");
-      result["binary"] = json_stringt(expr.is_true() ? "1" : "0");
-      result["data"] = jsont::json_boolean(expr.is_true());
+      result["binary"] =
+        json_stringt(to_constant_expr(expr).is_true() ? "1" : "0");
+      result["data"] = jsont::json_boolean(to_constant_expr(expr).is_true());
     }
     else if(type.id() == ID_string)
     {
diff --git a/src/goto-programs/pointer_arithmetic.cpp b/src/goto-programs/pointer_arithmetic.cpp
index 7c52e30fd85..64e0ea04efd 100644
--- a/src/goto-programs/pointer_arithmetic.cpp
+++ b/src/goto-programs/pointer_arithmetic.cpp
@@ -46,7 +46,9 @@ void pointer_arithmetict::read(const exprt &src)
     {
       const index_exprt &index_expr = to_index_expr(address_of_src.op());
 
-      if(index_expr.index().is_zero())
+      if(
+        index_expr.index().is_constant() &&
+        to_constant_expr(index_expr.index()).is_zero())
         make_pointer(address_of_src);
       else
       {
diff --git a/src/goto-programs/remove_const_function_pointers.cpp b/src/goto-programs/remove_const_function_pointers.cpp
index 043a3107184..4eff54dc30d 100644
--- a/src/goto-programs/remove_const_function_pointers.cpp
+++ b/src/goto-programs/remove_const_function_pointers.cpp
@@ -170,7 +170,7 @@ bool remove_const_function_pointerst::try_resolve_function_call(
   }
   else if(simplified_expr.is_constant())
   {
-    if(simplified_expr.is_zero())
+    if(to_constant_expr(simplified_expr).is_zero())
     {
       // We have the null pointer - no need to throw everything away
       // but we don't add any functions either
diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index 7db4f3456b7..1be6140690e 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -236,11 +236,11 @@ static void fix_return_type(
   exprt old_lhs=function_call.lhs();
   function_call.lhs()=tmp_symbol_expr;
 
-  dest.add(goto_programt::make_assignment(code_assignt(
+  dest.add(goto_programt::make_assignment(
     old_lhs,
     make_byte_extract(
       tmp_symbol_expr, from_integer(0, c_index_type()), old_lhs.type()),
-    source_location)));
+    source_location));
 }
 
 void remove_function_pointerst::remove_function_pointer(
diff --git a/src/goto-programs/remove_skip.cpp b/src/goto-programs/remove_skip.cpp
index 8ca1aea3787..f227c547bb0 100644
--- a/src/goto-programs/remove_skip.cpp
+++ b/src/goto-programs/remove_skip.cpp
@@ -37,8 +37,12 @@ bool is_skip(
 
   if(it->is_goto())
   {
-    if(it->condition().is_false())
+    if(
+      it->condition().is_constant() &&
+      to_constant_expr(it->condition()).is_false())
+    {
       return true;
+    }
 
     goto_programt::const_targett next_it = it;
     next_it++;
@@ -48,7 +52,9 @@ bool is_skip(
 
     // A branch to the next instruction is a skip
     // We also require the guard to be 'true'
-    return it->condition().is_true() && it->get_target() == next_it;
+    return it->condition().is_constant() &&
+           to_constant_expr(it->condition()).is_true() &&
+           it->get_target() == next_it;
   }
 
   if(it->is_other())
diff --git a/src/goto-programs/rewrite_union.cpp b/src/goto-programs/rewrite_union.cpp
index 71b37ed0c54..9c35023a013 100644
--- a/src/goto-programs/rewrite_union.cpp
+++ b/src/goto-programs/rewrite_union.cpp
@@ -146,7 +146,9 @@ static bool restore_union_rec(exprt &expr, const namespacet &ns)
 
       for(const auto &comp : union_type.components())
       {
-        if(be.offset().is_zero() && be.type() == comp.type())
+        if(
+          be.offset().is_constant() &&
+          to_constant_expr(be.offset()).is_zero() && be.type() == comp.type())
         {
           expr = member_exprt{be.op(), comp.get_name(), be.type()};
           return false;
diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp
index 5a00c5a7efb..9f86d746f76 100644
--- a/src/goto-programs/string_abstraction.cpp
+++ b/src/goto-programs/string_abstraction.cpp
@@ -910,7 +910,7 @@ bool string_abstractiont::build_array(const array_exprt &object,
 
   exprt::operandst::const_iterator it=object.operands().begin();
   for(mp_integer i = 0; i < *size; ++i, ++it)
-    if(it->is_zero())
+    if(it->is_constant() && to_constant_expr(*it).is_zero())
       return build_symbol_constant(i, *size, dest);
 
   return true;
@@ -1194,7 +1194,7 @@ goto_programt::targett string_abstractiont::abstract_char_assign(
     rhsp = &(to_typecast_expr(*rhsp).op());
 
   // we only care if the constant zero is assigned
-  if(!rhsp->is_zero())
+  if(!rhsp->is_constant() || !to_constant_expr(*rhsp).is_zero())
     return target;
 
   // index into a character array
diff --git a/src/goto-programs/vcd_goto_trace.cpp b/src/goto-programs/vcd_goto_trace.cpp
index fe2e8b94130..54a1aa984f3 100644
--- a/src/goto-programs/vcd_goto_trace.cpp
+++ b/src/goto-programs/vcd_goto_trace.cpp
@@ -131,15 +131,25 @@ void output_vcd(
         // booleans are special in VCD
         if(type.id() == ID_bool)
         {
-          if(step.full_lhs_value.is_true())
+          if(
+            step.full_lhs_value.is_constant() &&
+            to_constant_expr(step.full_lhs_value).is_true())
+          {
             out << "1"
                 << "V" << number << "\n";
-          else if(step.full_lhs_value.is_false())
+          }
+          else if(
+            step.full_lhs_value.is_constant() &&
+            to_constant_expr(step.full_lhs_value).is_false())
+          {
             out << "0"
                 << "V" << number << "\n";
+          }
           else
+          {
             out << "x"
                 << "V" << number << "\n";
+          }
         }
         else
         {
diff --git a/src/goto-programs/xml_expr.cpp b/src/goto-programs/xml_expr.cpp
index da90516dace..99616b91bd3 100644
--- a/src/goto-programs/xml_expr.cpp
+++ b/src/goto-programs/xml_expr.cpp
@@ -221,7 +221,7 @@ xmlt xml(const exprt &expr, const namespacet &ns)
       result.name = "pointer";
       result.set_attribute(
         "binary", integer2binary(bvrep2integer(value, width, false), width));
-      if(is_null_pointer(constant_expr))
+      if(constant_expr.is_null_pointer())
         result.data = "NULL";
     }
     else if(type.id() == ID_bool)
diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
index 7e4013f5b6e..0ef1bf2bb98 100644
--- a/src/goto-symex/build_goto_trace.cpp
+++ b/src/goto-symex/build_goto_trace.cpp
@@ -84,9 +84,9 @@ static exprt build_full_lhs_rec(
 
     exprt tmp = decision_procedure.get(to_if_expr(src_ssa).cond());
 
-    if(tmp.is_true())
+    if(tmp.is_constant() && to_constant_expr(tmp).is_true())
       return tmp2.true_case();
-    else if(tmp.is_false())
+    else if(tmp.is_constant() && to_constant_expr(tmp).is_false())
       return tmp2.false_case();
     else
       return std::move(tmp2);
@@ -241,7 +241,8 @@ void build_goto_trace(
 
     const SSA_stept &SSA_step = *it;
 
-    if(!decision_procedure.get(SSA_step.guard_handle).is_true())
+    exprt v = decision_procedure.get(SSA_step.guard_handle);
+    if(!v.is_constant() || !to_constant_expr(v).is_true())
       continue;
 
     if(it->is_constraint() ||
@@ -409,8 +410,9 @@ void build_goto_trace(
       {
         goto_trace_step.cond_expr = SSA_step.cond_expr;
 
+        exprt v = decision_procedure.get(SSA_step.cond_handle);
         goto_trace_step.cond_value =
-          decision_procedure.get(SSA_step.cond_handle).is_true();
+          v.is_constant() && to_constant_expr(v).is_true();
       }
 
       if(SSA_step.source.pc->is_assert() || SSA_step.source.pc->is_assume())
@@ -445,8 +447,11 @@ static bool is_failed_assertion_step(
   symex_target_equationt::SSA_stepst::const_iterator step,
   const decision_proceduret &decision_procedure)
 {
-  return step->is_assert() &&
-         decision_procedure.get(step->cond_handle).is_false();
+  if(!step->is_assert())
+    return false;
+
+  exprt v = decision_procedure.get(step->cond_handle);
+  return v.is_constant() && to_constant_expr(v).is_false();
 }
 
 void build_goto_trace(
diff --git a/src/goto-symex/goto_state.cpp b/src/goto-symex/goto_state.cpp
index fb8e382f437..8cbe0038a13 100644
--- a/src/goto-symex/goto_state.cpp
+++ b/src/goto-symex/goto_state.cpp
@@ -145,11 +145,7 @@ void goto_statet::apply_condition(
     if(!is_ssa_expr(lhs) || !goto_symex_can_forward_propagatet(ns)(rhs))
       return;
 
-    if(rhs.is_true())
-      apply_condition(equal_exprt{lhs, false_exprt{}}, previous_state, ns);
-    else if(rhs.is_false())
-      apply_condition(equal_exprt{lhs, true_exprt{}}, previous_state, ns);
-    else
-      UNREACHABLE;
+    PRECONDITION(rhs.is_constant());
+    apply_condition(equal_exprt{lhs, boolean_negate(rhs)}, previous_state, ns);
   }
 }
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index 9ac435c89a4..ed295bc5d25 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -353,10 +353,18 @@ exprt goto_symex_statet::l2_rename_rvalues(exprt lvalue, const namespacet &ns)
     // The condition is an rvalue:
     auto &if_lvalue = to_if_expr(lvalue);
     if_lvalue.cond() = rename(if_lvalue.cond(), ns);
-    if(!if_lvalue.cond().is_false())
+    if(
+      !if_lvalue.cond().is_constant() ||
+      !to_constant_expr(if_lvalue.cond()).is_false())
+    {
       if_lvalue.true_case() = l2_rename_rvalues(if_lvalue.true_case(), ns);
-    if(!if_lvalue.cond().is_true())
+    }
+    if(
+      !if_lvalue.cond().is_constant() ||
+      !to_constant_expr(if_lvalue.cond()).is_true())
+    {
       if_lvalue.false_case() = l2_rename_rvalues(if_lvalue.false_case(), ns);
+    }
   }
   else if(lvalue.id() == ID_complex_real)
   {
@@ -450,8 +458,12 @@ bool goto_symex_statet::l2_thread_read_encoding(
     }
 
     guardt cond = read_guard;
-    if(!no_write.op().is_false())
+    if(
+      !no_write.op().is_constant() ||
+      !to_constant_expr(no_write.op()).is_false())
+    {
       cond |= guardt{no_write.op(), guard_manager};
+    }
 
     // It is safe to perform constant propagation in case we have read or
     // written this object within the atomic section. We must actually do this,
@@ -494,8 +506,12 @@ bool goto_symex_statet::l2_thread_read_encoding(
     expr = std::move(ssa_l2);
 
     a_s_read.second.push_back(guard);
-    if(!no_write.op().is_false())
+    if(
+      !no_write.op().is_constant() ||
+      !to_constant_expr(no_write.op()).is_false())
+    {
       a_s_read.second.back().add(no_write);
+    }
 
     return true;
   }
diff --git a/src/goto-symex/memory_model_sc.cpp b/src/goto-symex/memory_model_sc.cpp
index bbf2cab2692..60cd377c9fc 100644
--- a/src/goto-symex/memory_model_sc.cpp
+++ b/src/goto-symex/memory_model_sc.cpp
@@ -302,7 +302,9 @@ void memory_model_sct::from_read(symex_target_equationt &equation)
           exprt cond;
           cond.make_nil();
 
-          if(c_it->first.second==*w_prime && !ws1.is_false())
+          if(
+            c_it->first.second == *w_prime &&
+            (!ws1.is_constant() || !to_constant_expr(ws1).is_false()))
           {
             exprt fr=before(r, *w);
 
@@ -314,7 +316,9 @@ void memory_model_sct::from_read(symex_target_equationt &equation)
                 and_exprt(r->guard, (*w)->guard, ws1, rf),
                 fr);
           }
-          else if(c_it->first.second==*w && !ws2.is_false())
+          else if(
+            c_it->first.second == *w &&
+            (!ws2.is_constant() || !to_constant_expr(ws2).is_false()))
           {
             exprt fr=before(r, *w_prime);
 
diff --git a/src/goto-symex/memory_model_tso.cpp b/src/goto-symex/memory_model_tso.cpp
index 54d6b58b677..68299e840d8 100644
--- a/src/goto-symex/memory_model_tso.cpp
+++ b/src/goto-symex/memory_model_tso.cpp
@@ -148,7 +148,7 @@ void memory_model_tsot::program_order(
           simplify(cond, ns);
         }
 
-        if(!cond.is_false())
+        if(!cond.is_constant() || !to_constant_expr(cond).is_false())
         {
           if(ordering.is_nil())
             ordering=partial_order_concurrencyt::before(
diff --git a/src/goto-symex/partial_order_concurrency.cpp b/src/goto-symex/partial_order_concurrency.cpp
index 9ff92da9824..4073549fbd3 100644
--- a/src/goto-symex/partial_order_concurrency.cpp
+++ b/src/goto-symex/partial_order_concurrency.cpp
@@ -51,9 +51,9 @@ void partial_order_concurrencyt::add_init_writes(
     if(init_done.find(a)!=init_done.end())
       continue;
 
-    if(spawn_seen ||
-       e_it->is_shared_read() ||
-       !e_it->guard.is_true())
+    if(
+      spawn_seen || e_it->is_shared_read() || !e_it->guard.is_constant() ||
+      !to_constant_expr(e_it->guard).is_true())
     {
       init_steps.emplace_back(
         e_it->source, goto_trace_stept::typet::SHARED_WRITE);
diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp
index 8b71f111674..74255afe4ff 100644
--- a/src/goto-symex/postcondition.cpp
+++ b/src/goto-symex/postcondition.cpp
@@ -62,7 +62,7 @@ void postcondition(
   {
     postconditiont postcondition(ns, value_set, *it, s);
     postcondition.compute(dest);
-    if(dest.is_false())
+    if(dest.is_constant() && to_constant_expr(dest).is_false())
       return;
   }
 }
@@ -137,7 +137,7 @@ void postconditiont::strengthen(exprt &dest)
     exprt equality =
       get_original_name(equal_exprt{SSA_step.ssa_lhs, SSA_step.ssa_rhs});
 
-    if(dest.is_true())
+    if(dest.is_constant() && to_constant_expr(dest).is_true())
       dest.swap(equality);
     else
       dest=and_exprt(dest, equality);
diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp
index 76fc7f48a83..5b0739510a9 100644
--- a/src/goto-symex/precondition.cpp
+++ b/src/goto-symex/precondition.cpp
@@ -70,7 +70,7 @@ void precondition(
   {
     preconditiont precondition(ns, value_sets, target, *it, s, message_handler);
     precondition.compute(dest);
-    if(dest.is_false())
+    if(dest.is_constant() && to_constant_expr(dest).is_false())
       return;
   }
 }
diff --git a/src/goto-symex/shadow_memory.cpp b/src/goto-symex/shadow_memory.cpp
index fe7b2005d53..1113bd9cfec 100644
--- a/src/goto-symex/shadow_memory.cpp
+++ b/src/goto-symex/shadow_memory.cpp
@@ -39,7 +39,8 @@ void shadow_memoryt::initialize_shadow_memory(
 
     if(
       field_pair.second.id() == ID_typecast &&
-      to_typecast_expr(field_pair.second).op().is_zero())
+      to_typecast_expr(field_pair.second).op().is_constant() &&
+      to_constant_expr(to_typecast_expr(field_pair.second).op()).is_zero())
     {
       const auto zero_value =
         zero_initializer(type, expr.source_location(), ns);
diff --git a/src/goto-symex/shadow_memory_util.cpp b/src/goto-symex/shadow_memory_util.cpp
index b86a725b067..85a18973e27 100644
--- a/src/goto-symex/shadow_memory_util.cpp
+++ b/src/goto-symex/shadow_memory_util.cpp
@@ -319,9 +319,7 @@ bool contains_null_or_invalid(
   const std::vector<exprt> &value_set,
   const exprt &address)
 {
-  if(
-    address.id() == ID_constant && address.type().id() == ID_pointer &&
-    to_constant_expr(address).is_zero())
+  if(address.is_constant() && to_constant_expr(address).is_null_pointer())
   {
     for(const auto &e : value_set)
     {
@@ -692,7 +690,8 @@ static void clean_string_constant(exprt &expr)
 {
   const auto *index_expr = expr_try_dynamic_cast<index_exprt>(expr);
   if(
-    index_expr && index_expr->index().is_zero() &&
+    index_expr && index_expr->index().is_constant() &&
+    to_constant_expr(index_expr->index()).is_zero() &&
     can_cast_expr<string_constantt>(index_expr->array()))
   {
     expr = index_expr->array();
@@ -930,19 +929,21 @@ std::vector<std::pair<exprt, exprt>> get_shadow_dereference_candidates(
     const exprt base_cond = get_matched_base_cond(
       shadowed_address.address, matched_base_address, ns, log);
     shadow_memory_log_text_and_expr(ns, log, "base_cond", base_cond);
-    if(base_cond.is_false())
+    if(base_cond.is_constant() && to_constant_expr(base_cond).is_false())
     {
       continue;
     }
 
     const exprt expr_cond =
       get_matched_expr_cond(dereference.pointer, expr, ns, log);
-    if(expr_cond.is_false())
+    if(expr_cond.is_constant() && to_constant_expr(expr_cond).is_false())
     {
       continue;
     }
 
-    if(base_cond.is_true() && expr_cond.is_true())
+    if(
+      base_cond.is_constant() && to_constant_expr(base_cond).is_true() &&
+      expr_cond.is_constant() && to_constant_expr(expr_cond).is_true())
     {
 #ifdef DEBUG_SHADOW_MEMORY
       log.debug() << "exact match" << messaget::eom;
@@ -953,7 +954,7 @@ std::vector<std::pair<exprt, exprt>> get_shadow_dereference_candidates(
       break;
     }
 
-    if(base_cond.is_true())
+    if(base_cond.is_constant() && to_constant_expr(base_cond).is_true())
     {
       // No point looking at further shadow addresses
       // as only one of them can match.
@@ -1097,19 +1098,21 @@ get_shadow_memory_for_matched_object(
     const exprt base_cond = get_matched_base_cond(
       shadowed_address.address, matched_base_address, ns, log);
     shadow_memory_log_text_and_expr(ns, log, "base_cond", base_cond);
-    if(base_cond.is_false())
+    if(base_cond.is_constant() && to_constant_expr(base_cond).is_false())
     {
       continue;
     }
 
     const exprt expr_cond =
       get_matched_expr_cond(dereference.pointer, expr, ns, log);
-    if(expr_cond.is_false())
+    if(expr_cond.is_constant() && to_constant_expr(expr_cond).is_false())
     {
       continue;
     }
 
-    if(base_cond.is_true() && expr_cond.is_true())
+    if(
+      base_cond.is_constant() && to_constant_expr(base_cond).is_true() &&
+      expr_cond.is_constant() && to_constant_expr(expr_cond).is_true())
     {
       log_shadow_memory_message(log, "exact match");
 
@@ -1119,7 +1122,7 @@ get_shadow_memory_for_matched_object(
       break;
     }
 
-    if(base_cond.is_true())
+    if(base_cond.is_constant() && to_constant_expr(base_cond).is_true())
     {
       // No point looking at further shadow addresses
       // as only one of them can match.
diff --git a/src/goto-symex/show_program.cpp b/src/goto-symex/show_program.cpp
index 13c409ea197..fc6fc205f9e 100644
--- a/src/goto-symex/show_program.cpp
+++ b/src/goto-symex/show_program.cpp
@@ -47,7 +47,7 @@ static void show_step(
     std::cout << annotation << '(' << string_value << ')';
   std::cout << '\n';
 
-  if(!step.guard.is_true())
+  if(!step.guard.is_constant() || !to_constant_expr(step.guard).is_true())
   {
     const std::string guard_string = from_expr(ns, function_id, step.guard);
     std::cout << std::string(std::to_string(count).size() + 3, ' ');
@@ -76,7 +76,8 @@ void show_program(const namespacet &ns, const symex_target_equationt &equation)
       show_step(ns, step, "ASSUME", count);
     else if(step.is_constraint())
     {
-      PRECONDITION(step.guard.is_true());
+      PRECONDITION(
+        step.guard.is_constant() && to_constant_expr(step.guard).is_true());
       show_step(ns, step, "CONSTRAINT", count);
     }
     else if(step.is_shared_read())
diff --git a/src/goto-symex/solver_hardness.cpp b/src/goto-symex/solver_hardness.cpp
index 95c8ea70033..eeeccffadfc 100644
--- a/src/goto-symex/solver_hardness.cpp
+++ b/src/goto-symex/solver_hardness.cpp
@@ -246,7 +246,9 @@ solver_hardnesst::goto_instruction2string(goto_programt::const_targett pc)
 
   case GOTO:
   case INCOMPLETE_GOTO:
-    if(!instruction.condition().is_true())
+    if(
+      !instruction.condition().is_constant() ||
+      !to_constant_expr(instruction.condition()).is_true())
     {
       out << "IF " << format(instruction.condition()) << " THEN ";
     }
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index c829e4b1d8c..001fffff1a1 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -46,7 +46,10 @@ static bool is_string_constant_initialization(const exprt &rhs)
       const auto &index =
         expr_try_dynamic_cast<index_exprt>(address_of->object()))
     {
-      if(index->array().id() == ID_string_constant && index->index().is_zero())
+      if(
+        index->array().id() == ID_string_constant &&
+        index->index().is_constant() &&
+        to_constant_expr(index->index()).is_zero())
       {
         return true;
       }
@@ -238,7 +241,7 @@ void symex_assignt::assign_non_struct_symbol(
       : assignment_type;
 
   target.assignment(
-    make_and(state.guard.as_expr(), conjunction(guard)),
+    conjunction(state.guard.as_expr(), conjunction(guard)),
     l2_lhs,
     l2_full_lhs,
     get_original_name(l2_full_lhs),
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index 9d3797a7247..0f672aeef32 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -172,7 +172,9 @@ void goto_symext::symex_allocate(
   INVARIANT(
     zero_init.is_constant(), "allocate expects constant as second argument");
 
-  if(!zero_init.is_zero() && !zero_init.is_false())
+  if(
+    !to_constant_expr(zero_init).is_zero() &&
+    !to_constant_expr(zero_init).is_false())
   {
     const auto zero_value =
       zero_initializer(*object_type, code.source_location(), ns);
@@ -317,7 +319,8 @@ static irep_idt get_string_argument_rec(const exprt &src)
 
       if(
         index_expr.array().id() == ID_string_constant &&
-        index_expr.index().is_zero())
+        index_expr.index().is_constant() &&
+        to_constant_expr(index_expr.index()).is_zero())
       {
         const exprt &fmt_str = index_expr.array();
         return to_string_constant(fmt_str).value();
@@ -358,8 +361,12 @@ static std::optional<exprt> get_va_args(const exprt::operandst &operands)
     return {};
 
   const index_exprt &index_expr = to_index_expr(object);
-  if(!index_expr.index().is_zero())
+  if(
+    !index_expr.index().is_constant() ||
+    !to_constant_expr(index_expr.index()).is_zero())
+  {
     return {};
+  }
   else
     return index_expr.array();
 }
@@ -454,14 +461,13 @@ void goto_symext::symex_output(
   PRECONDITION(code.operands().size() >= 2);
   exprt id_arg = state.rename(code.op0(), ns).get();
 
-  std::list<renamedt<exprt, L2>> args;
+  std::list<exprt> args;
 
   for(std::size_t i=1; i<code.operands().size(); i++)
   {
     renamedt<exprt, L2> l2_arg = state.rename(code.operands()[i], ns);
-    if(symex_config.simplify_opt)
-      l2_arg.simplify(ns);
-    args.emplace_back(l2_arg);
+    args.emplace_back(l2_arg.get());
+    do_simplify(args.back());
   }
 
   const irep_idt output_id=get_string_argument(id_arg, ns);
diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp
index 5c1ff7134a9..3389c04e037 100644
--- a/src/goto-symex/symex_clean_expr.cpp
+++ b/src/goto-symex/symex_clean_expr.cpp
@@ -82,7 +82,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
     if(expr.type().id() == ID_empty)
       return;
 
-    if(!ode.offset().is_zero())
+    if(!ode.offset().is_constant() || !to_constant_expr(ode.offset()).is_zero())
     {
       if(expr.type().id() != ID_array)
       {
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index 25a61e2f74e..76e1159cb74 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -362,7 +362,9 @@ void goto_symext::dereference_rec(
   }
   else if(
     expr.id() == ID_index && to_index_expr(expr).array().id() == ID_member &&
-    to_array_type(to_index_expr(expr).array().type()).size().is_zero())
+    to_array_type(to_index_expr(expr).array().type()).size().is_constant() &&
+    to_constant_expr(to_array_type(to_index_expr(expr).array().type()).size())
+      .is_zero())
   {
     // This is an expression of the form x.a[i],
     // where a is a zero-sized array. This gets
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index 6fdf9f4ff5e..bc316977499 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -273,9 +273,11 @@ void goto_symext::symex_function_call_post_clean(
   }
 
   // read the arguments -- before the locality renaming
-  const std::vector<renamedt<exprt, L2>> renamed_arguments =
+  const std::vector<exprt> renamed_arguments =
     make_range(cleaned_arguments).map([&](const exprt &a) {
-      return state.rename(a, ns);
+      exprt arg = state.rename(a, ns).get();
+      do_simplify(arg);
+      return arg;
     });
 
   // we hide the call if the caller and callee are both hidden
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index 404f04fec72..7c1f76beaa6 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -91,7 +91,7 @@ static std::optional<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
 
   if(
     skip_typecast(other_operand).id() != ID_address_of &&
-    (!constant_expr || !is_null_pointer(*constant_expr)))
+    (!constant_expr || !constant_expr->is_null_pointer()))
   {
     return {};
   }
@@ -139,13 +139,14 @@ static std::optional<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
           typecast_exprt::conditional_cast(value.pointer, other_operand.type()),
           other_operand},
         ns);
-      if(test_equal.is_true())
+      auto constant_expr = expr_try_dynamic_cast<constant_exprt>(test_equal);
+      if(constant_expr && constant_expr->is_true())
       {
         constant_found = true;
         // We can't break because we have to make sure we find any instances of
         // ID_unknown or ID_invalid
       }
-      else if(!test_equal.is_false())
+      else if(!constant_expr)
       {
         // We can't conclude anything about the value-set
         return {};
@@ -238,11 +239,10 @@ void goto_symext::symex_goto(statet &state)
   renamedt<exprt, L2> renamed_guard = state.rename(std::move(new_guard), ns);
   renamed_guard = try_evaluate_pointer_comparisons(
     std::move(renamed_guard), state.value_set, language_mode, ns);
-  if(symex_config.simplify_opt)
-    renamed_guard.simplify(ns);
   new_guard = renamed_guard.get();
+  do_simplify(new_guard);
 
-  if(new_guard.is_false())
+  if(new_guard.is_constant() && to_constant_expr(new_guard).is_false())
   {
     target.location(state.guard.as_expr(), state.source);
 
@@ -251,7 +251,7 @@ void goto_symext::symex_goto(statet &state)
     return; // nothing to do
   }
 
-  target.goto_instruction(state.guard.as_expr(), renamed_guard, state.source);
+  target.goto_instruction(state.guard.as_expr(), new_guard, state.source);
 
   DATA_INVARIANT(
     !instruction.targets.empty(), "goto should have at least one target");
@@ -275,11 +275,12 @@ void goto_symext::symex_goto(statet &state)
        // while(cond);
        (instruction.incoming_edges.size() == 1 &&
         *instruction.incoming_edges.begin() == goto_target &&
-        goto_target->is_goto() && new_guard.is_true())))
+        goto_target->is_goto() && new_guard.is_constant() &&
+        to_constant_expr(new_guard).is_true())))
     {
       // generate assume(false) or a suitable negation if this
       // instruction is a conditional goto
-      exprt negated_guard = not_exprt{new_guard};
+      exprt negated_guard = boolean_negate(new_guard);
       do_simplify(negated_guard);
       log.statistics() << "replacing self-loop at "
                        << state.source.pc->source_location() << " by assume("
@@ -314,7 +315,7 @@ void goto_symext::symex_goto(statet &state)
       return;
     }
 
-    if(new_guard.is_true())
+    if(new_guard.is_constant() && to_constant_expr(new_guard).is_true())
     {
       // we continue executing the loop
       if(check_break(loop_id, unwind))
@@ -328,7 +329,8 @@ void goto_symext::symex_goto(statet &state)
 
   // No point executing both branches of an unconditional goto.
   if(
-    new_guard.is_true() && // We have an unconditional goto, AND
+    new_guard.is_constant() && to_constant_expr(new_guard).is_true() &&
+    // We have an unconditional goto, AND
     // either there are no reachable blocks between us and the target in the
     // surrounding scope (because state.guard == true implies there is no path
     // around this GOTO instruction)
@@ -355,7 +357,7 @@ void goto_symext::symex_goto(statet &state)
     state_pc++;
 
     // skip dead instructions
-    if(new_guard.is_true())
+    if(new_guard.is_constant() && to_constant_expr(new_guard).is_true())
       while(state_pc!=goto_target && !state_pc->is_target())
         ++state_pc;
 
@@ -442,7 +444,7 @@ void goto_symext::symex_goto(statet &state)
   // On an unconditional GOTO we don't need our state, as it will be overwritten
   // by merge_goto. Therefore we move it onto goto_state_list instead of copying
   // as usual.
-  if(new_guard.is_true())
+  if(new_guard.is_constant() && to_constant_expr(new_guard).is_true())
   {
     // The move here only moves goto_statet, the base class of goto_symex_statet
     // and not the entire thing.
@@ -572,7 +574,9 @@ void goto_symext::symex_unreachable_goto(statet &state)
     goto_state_list.emplace_back(state.source, std::move(new_state));
   };
 
-  if(instruction.condition().is_true())
+  if(
+    instruction.condition().is_constant() &&
+    to_constant_expr(instruction.condition()).is_true())
   {
     if(instruction.is_backwards_goto())
     {
@@ -929,12 +933,7 @@ void goto_symext::loop_bound_exceeded(
 {
   const std::string loop_number = std::to_string(state.source.pc->loop_number);
 
-  exprt negated_cond;
-
-  if(guard.is_true())
-    negated_cond=false_exprt();
-  else
-    negated_cond=not_exprt(guard);
+  exprt negated_cond = boolean_negate(guard);
 
   if(symex_config.unwinding_assertions)
   {
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index de1e7f1f388..9e19cbc99f7 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -186,7 +186,7 @@ void goto_symext::vcc(
   state.total_vccs++;
   path_segment_vccs++;
 
-  if(condition.is_true())
+  if(condition.is_constant() && to_constant_expr(condition).is_true())
     return;
 
   const exprt guarded_condition = state.guard.guard_expr(condition);
@@ -218,10 +218,10 @@ void goto_symext::symex_assume(statet &state, const exprt &cond)
 
 void goto_symext::symex_assume_l2(statet &state, const exprt &cond)
 {
-  if(cond.is_true())
+  if(cond.is_constant() && to_constant_expr(cond).is_true())
     return;
 
-  if(cond.is_false())
+  if(cond.is_constant() && to_constant_expr(cond).is_false())
     state.reachable = false;
 
   // we are willing to re-write some quantified expressions
@@ -855,11 +855,15 @@ void goto_symext::try_filter_value_sets(
 
     do_simplify(modified_condition);
 
-    if(jump_taken_value_set && modified_condition.is_false())
+    if(
+      jump_taken_value_set && modified_condition.is_constant() &&
+      to_constant_expr(modified_condition).is_false())
     {
       erase_from_jump_taken_value_set.insert(value_set_element);
     }
-    else if(jump_not_taken_value_set && modified_condition.is_true())
+    else if(
+      jump_not_taken_value_set && modified_condition.is_constant() &&
+      to_constant_expr(modified_condition).is_true())
     {
       erase_from_jump_not_taken_value_set.insert(value_set_element);
     }
diff --git a/src/goto-symex/symex_target.h b/src/goto-symex/symex_target.h
index 209bc6de49e..fc6bad23f66 100644
--- a/src/goto-symex/symex_target.h
+++ b/src/goto-symex/symex_target.h
@@ -158,7 +158,7 @@ class symex_targett
   virtual void function_call(
     const exprt &guard,
     const irep_idt &function_id,
-    const std::vector<renamedt<exprt, L2>> &ssa_function_arguments,
+    const std::vector<exprt> &ssa_function_arguments,
     const sourcet &source,
     bool hidden) = 0;
 
@@ -192,7 +192,7 @@ class symex_targett
     const exprt &guard,
     const sourcet &source,
     const irep_idt &output_id,
-    const std::list<renamedt<exprt, L2>> &args) = 0;
+    const std::list<exprt> &args) = 0;
 
   /// Record formatted output.
   /// \param guard: Precondition for writing to the output
@@ -251,7 +251,7 @@ class symex_targett
   ///  goto instruction
   virtual void goto_instruction(
     const exprt &guard,
-    const renamedt<exprt, L2> &cond,
+    const exprt &cond,
     const sourcet &source) = 0;
 
   /// Record a _global_ constraint: there is no guard limiting its scope.
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index 0bb35155e01..5e469e730d4 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -181,7 +181,7 @@ void symex_target_equationt::location(
 void symex_target_equationt::function_call(
   const exprt &guard,
   const irep_idt &function_id,
-  const std::vector<renamedt<exprt, L2>> &function_arguments,
+  const std::vector<exprt> &function_arguments,
   const sourcet &source,
   const bool hidden)
 {
@@ -190,8 +190,7 @@ void symex_target_equationt::function_call(
 
   SSA_step.guard = guard;
   SSA_step.called_function = function_id;
-  for(const auto &arg : function_arguments)
-    SSA_step.ssa_function_arguments.emplace_back(arg.get());
+  SSA_step.ssa_function_arguments = function_arguments;
   SSA_step.hidden = hidden;
 
   merge_ireps(SSA_step);
@@ -217,14 +216,13 @@ void symex_target_equationt::output(
   const exprt &guard,
   const sourcet &source,
   const irep_idt &output_id,
-  const std::list<renamedt<exprt, L2>> &args)
+  const std::list<exprt> &args)
 {
   SSA_steps.emplace_back(source, goto_trace_stept::typet::OUTPUT);
   SSA_stept &SSA_step=SSA_steps.back();
 
   SSA_step.guard=guard;
-  for(const auto &arg : args)
-    SSA_step.io_args.emplace_back(arg.get());
+  SSA_step.io_args = args;
   SSA_step.io_id=output_id;
 
   merge_ireps(SSA_step);
@@ -299,14 +297,14 @@ void symex_target_equationt::assertion(
 
 void symex_target_equationt::goto_instruction(
   const exprt &guard,
-  const renamedt<exprt, L2> &cond,
+  const exprt &cond,
   const sourcet &source)
 {
   SSA_steps.emplace_back(source, goto_trace_stept::typet::GOTO);
   SSA_stept &SSA_step=SSA_steps.back();
 
   SSA_step.guard=guard;
-  SSA_step.cond_expr = cond.get();
+  SSA_step.cond_expr = cond;
 
   merge_ireps(SSA_step);
 }
diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h
index b10a922b113..ef2f1056a3c 100644
--- a/src/goto-symex/symex_target_equation.h
+++ b/src/goto-symex/symex_target_equation.h
@@ -82,7 +82,7 @@ class symex_target_equationt:public symex_targett
   virtual void function_call(
     const exprt &guard,
     const irep_idt &function_id,
-    const std::vector<renamedt<exprt, L2>> &ssa_function_arguments,
+    const std::vector<exprt> &ssa_function_arguments,
     const sourcet &source,
     bool hidden);
 
@@ -103,7 +103,7 @@ class symex_target_equationt:public symex_targett
     const exprt &guard,
     const sourcet &source,
     const irep_idt &output_id,
-    const std::list<renamedt<exprt, L2>> &args);
+    const std::list<exprt> &args);
 
   /// \copydoc symex_targett::output_fmt()
   virtual void output_fmt(
@@ -137,7 +137,7 @@ class symex_target_equationt:public symex_targett
   /// \copydoc symex_targett::goto_instruction()
   virtual void goto_instruction(
     const exprt &guard,
-    const renamedt<exprt, L2> &cond,
+    const exprt &cond,
     const sourcet &source);
 
   /// \copydoc symex_targett::constraint()
diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp
index dd32b5eec57..5c4e91ebfc9 100644
--- a/src/goto-synthesizer/cegis_verifier.cpp
+++ b/src/goto-synthesizer/cegis_verifier.cpp
@@ -71,7 +71,7 @@ get_checked_pointer_from_null_pointer_check(const exprt &violation)
   // NULL == ptr
   if(
     can_cast_expr<constant_exprt>(lhs_pointer) &&
-    is_null_pointer(*expr_try_dynamic_cast<constant_exprt>(lhs_pointer)))
+    expr_try_dynamic_cast<constant_exprt>(lhs_pointer)->is_null_pointer())
   {
     return rhs_pointer;
   }
diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp
index 65fc1a8f4d4..b8f04a6838f 100644
--- a/src/linking/linking.cpp
+++ b/src/linking/linking.cpp
@@ -523,15 +523,18 @@ bool linkingt::adjust_object_type_rec(
     const exprt &old_size=to_array_type(t1).size();
     const exprt &new_size=to_array_type(t2).size();
 
-    if((old_size.is_nil() && new_size.is_not_nil()) ||
-       (old_size.is_zero() && new_size.is_not_nil()) ||
-       info.old_symbol.is_weak)
+    if(
+      (old_size.is_nil() && new_size.is_not_nil()) ||
+      (old_size.is_constant() && to_constant_expr(old_size).is_zero() &&
+       new_size.is_not_nil()) ||
+      info.old_symbol.is_weak)
     {
       info.set_to_new=true; // store new type
     }
-    else if(new_size.is_nil() ||
-            new_size.is_zero() ||
-            info.new_symbol.is_weak)
+    else if(
+      new_size.is_nil() ||
+      (new_size.is_constant() && to_constant_expr(new_size).is_zero()) ||
+      info.new_symbol.is_weak)
     {
       // ok, we will use the old type
     }
@@ -549,9 +552,8 @@ bool linkingt::adjust_object_type_rec(
         return true;
       }
 
-      equal_exprt eq(old_size, new_size);
-
-      if(!simplify_expr(eq, ns).is_true())
+      exprt maybe_eq = simplify_expr(equal_exprt{old_size, new_size}, ns);
+      if(!maybe_eq.is_constant() || !to_constant_expr(maybe_eq).is_true())
       {
         linking_diagnosticst diag{message_handler, ns};
         diag.error(
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index fca7edf08d0..0a83b83700b 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -621,7 +621,7 @@ void value_sett::get_value_set_rec(
   else if(expr.is_constant())
   {
     // check if NULL
-    if(is_null_pointer(to_constant_expr(expr)))
+    if(to_constant_expr(expr).is_null_pointer())
     {
       insert(
         dest,
@@ -656,7 +656,7 @@ void value_sett::get_value_set_rec(
     {
       // integer-to-something
 
-      if(op.is_zero())
+      if(op.is_constant() && to_constant_expr(op).is_zero())
       {
         insert(dest, exprt(ID_null_object, empty_typet{}), mp_integer{0});
       }
@@ -1398,7 +1398,7 @@ void value_sett::get_reference_set_rec(
         offsett o = a_it->second;
         const auto i = numeric_cast<mp_integer>(offset);
 
-        if(offset.is_zero())
+        if(i.has_value() && i == 0)
         {
         }
         else if(i.has_value() && o)
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index 3af8d4b72b1..4499dd31450 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -486,7 +486,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
 
   if(root_object.id() == ID_null_object)
   {
-    if(!o.offset().is_zero())
+    if(!o.offset().is_constant() || !to_constant_expr(o.offset()).is_zero())
       return {};
 
     valuet result;
@@ -572,7 +572,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
     // something generic -- really has to be a symbol
     address_of_exprt object_pointer(object);
 
-    if(o.offset().is_zero())
+    if(o.offset().is_constant() && to_constant_expr(o.offset()).is_zero())
     {
       result.pointer_guard = equal_exprt(
         typecast_exprt::conditional_cast(pointer_expr, object_pointer.type()),
@@ -588,7 +588,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
 
     if(
       dereference_type_compare(object_type, dereference_type, ns) &&
-      o.offset().is_zero())
+      o.offset().is_constant() && to_constant_expr(o.offset()).is_zero())
     {
       // The simplest case: types match, and offset is zero!
       // This is great, we are almost done.
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index 5d595cccb4b..6fc272f6289 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -532,7 +532,7 @@ void value_set_fit::get_value_set_rec(
   else if(expr.is_constant())
   {
     // check if NULL
-    if(is_null_pointer(to_constant_expr(expr)))
+    if(to_constant_expr(expr).is_null_pointer())
     {
       insert(
         dest,
@@ -924,7 +924,7 @@ void value_set_fit::get_reference_set_sharing_rec(
         offsett o = object_entry.second;
         const auto i = numeric_cast<mp_integer>(offset);
 
-        if(offset.is_zero())
+        if(i.has_value() && i == 0)
         {
         }
         else if(i.has_value() && offset_is_zero(o))
diff --git a/src/solvers/flattening/boolbv_quantifier.cpp b/src/solvers/flattening/boolbv_quantifier.cpp
index 5ca7c77b243..4d27c497b88 100644
--- a/src/solvers/flattening/boolbv_quantifier.cpp
+++ b/src/solvers/flattening/boolbv_quantifier.cpp
@@ -174,7 +174,10 @@ static std::optional<exprt> eager_quantifier_instantiation(
 
   const exprt where_simplified = simplify_expr(expr.where(), ns);
 
-  if(where_simplified.is_true() || where_simplified.is_false())
+  if(
+    where_simplified.is_constant() &&
+    (to_constant_expr(where_simplified).is_true() ||
+     to_constant_expr(where_simplified).is_false()))
   {
     return where_simplified;
   }
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index a022801df4b..f14954c253a 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -443,7 +443,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
   {
     const constant_exprt &c = to_constant_expr(expr);
 
-    if(is_null_pointer(c))
+    if(c.is_null_pointer())
       return encode(pointer_logic.get_null_object(), type);
     else
     {
diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp
index c5b866d6104..2de32c82abb 100644
--- a/src/solvers/flattening/pointer_logic.cpp
+++ b/src/solvers/flattening/pointer_logic.cpp
@@ -129,7 +129,7 @@ exprt pointer_logict::pointer_expr(
 
   const byte_extract_exprt &be = to_byte_extract_expr(deep_object);
   const address_of_exprt base(be.op());
-  if(be.offset().is_zero())
+  if(be.offset().is_constant() && to_constant_expr(be.offset()).is_zero())
     return typecast_exprt::conditional_cast(base, type);
 
   const auto object_size = pointer_offset_size(be.op().type(), ns);
diff --git a/src/solvers/prop/bdd_expr.cpp b/src/solvers/prop/bdd_expr.cpp
index f900c90f765..112d162911f 100644
--- a/src/solvers/prop/bdd_expr.cpp
+++ b/src/solvers/prop/bdd_expr.cpp
@@ -21,7 +21,10 @@ bddt bdd_exprt::from_expr_rec(const exprt &expr)
   PRECONDITION(expr.is_boolean());
 
   if(expr.is_constant())
-    return expr.is_false() ? bdd_mgr.bdd_false() : bdd_mgr.bdd_true();
+  {
+    return to_constant_expr(expr).is_false() ? bdd_mgr.bdd_false()
+                                             : bdd_mgr.bdd_true();
+  }
   else if(expr.id()==ID_not)
     return from_expr_rec(to_not_expr(expr).op()).bdd_not();
   else if(expr.id()==ID_and ||
@@ -138,7 +141,7 @@ exprt bdd_exprt::as_expr(
           if(r.else_branch().is_complement()) // else is false
           {
             exprt then_case = as_expr(r.then_branch(), cache);
-            return make_and(n_expr, then_case);
+            return conjunction(n_expr, then_case);
           }
           exprt then_case = as_expr(r.then_branch(), cache);
           return make_or(not_exprt(n_expr), then_case);
@@ -149,7 +152,7 @@ exprt bdd_exprt::as_expr(
         if(r.then_branch().is_complement()) // then is false
         {
           exprt else_case = as_expr(r.else_branch(), cache);
-          return make_and(not_exprt(n_expr), else_case);
+          return conjunction(not_exprt(n_expr), else_case);
         }
         exprt else_case = as_expr(r.else_branch(), cache);
         return make_or(n_expr, else_case);
diff --git a/src/solvers/prop/cover_goals.cpp b/src/solvers/prop/cover_goals.cpp
index b2782f7c5fe..76ff73dcab5 100644
--- a/src/solvers/prop/cover_goals.cpp
+++ b/src/solvers/prop/cover_goals.cpp
@@ -26,9 +26,12 @@ void cover_goalst::mark()
     o->satisfying_assignment();
 
   for(auto &g : goals)
-    if(
-      g.status == goalt::statust::UNKNOWN &&
-      decision_procedure.get(g.condition).is_true())
+  {
+    if(g.status != goalt::statust::UNKNOWN)
+      continue;
+
+    exprt v = decision_procedure.get(g.condition);
+    if(v.is_constant() && to_constant_expr(v).is_true())
     {
       g.status=goalt::statust::COVERED;
       _number_covered++;
@@ -37,6 +40,7 @@ void cover_goalst::mark()
       for(const auto &o : observers)
         o->goal_covered(g);
     }
+  }
 }
 
 /// Build clause
@@ -47,8 +51,14 @@ void cover_goalst::constraint()
   // cover at least one unknown goal
 
   for(const auto &g : goals)
-    if(g.status == goalt::statust::UNKNOWN && !g.condition.is_false())
+  {
+    if(
+      g.status == goalt::statust::UNKNOWN &&
+      (!g.condition.is_constant() || !to_constant_expr(g.condition).is_false()))
+    {
       disjuncts.push_back(g.condition);
+    }
+  }
 
   // this is 'false' if there are no disjuncts
   decision_procedure.set_to_true(disjunction(disjuncts));
diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp
index 597f95c7067..36a65e1c10c 100644
--- a/src/solvers/prop/prop_conv_solver.cpp
+++ b/src/solvers/prop/prop_conv_solver.cpp
@@ -78,11 +78,11 @@ std::optional<bool> prop_conv_solvert::get_bool(const exprt &expr) const
 {
   // trivial cases
 
-  if(expr.is_true())
+  if(expr.is_constant() && to_constant_expr(expr).is_true())
   {
     return true;
   }
-  else if(expr.is_false())
+  else if(expr.is_constant() && to_constant_expr(expr).is_false())
   {
     return false;
   }
@@ -195,12 +195,12 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr)
 
   if(expr.is_constant())
   {
-    if(expr.is_true())
+    if(to_constant_expr(expr).is_true())
       return const_literal(true);
     else
     {
       INVARIANT(
-        expr.is_false(),
+        to_constant_expr(expr).is_false(),
         "constant expression of type bool should be either true or false");
       return const_literal(false);
     }
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index b5c5366658c..d0945e247f9 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -273,7 +273,7 @@ static bool is_zero_width(const typet &type, const namespacet &ns)
   }
   else if(auto array_type = type_try_dynamic_cast<array_typet>(type))
   {
-    // we ignore array_type->size().is_zero() for now as there may be
+    // we ignore array_type->size() being zero for now as there may be
     // out-of-bounds accesses that we need to model
     return is_zero_width(array_type->element_type(), ns);
   }
@@ -364,9 +364,9 @@ exprt smt2_convt::get(const exprt &expr) const
   else if(expr.id() == ID_not)
   {
     auto op = get(to_not_expr(expr).op());
-    if(op.is_true())
+    if(op.is_constant() && to_constant_expr(op).is_true())
       return false_exprt();
-    else if(op.is_false())
+    else if(op.is_constant() && to_constant_expr(op).is_false())
       return true_exprt();
   }
   else if(
@@ -811,7 +811,7 @@ void smt2_convt::convert_address_of_rec(
     const exprt &array = index_expr.array();
     const exprt &index = index_expr.index();
 
-    if(index.is_zero())
+    if(index.is_constant() && to_constant_expr(index).is_zero())
     {
       if(array.type().id()==ID_pointer)
         convert_expr(array);
@@ -899,9 +899,9 @@ literalt smt2_convt::convert(const exprt &expr)
 
   // Three cases where no new handle is needed.
 
-  if(expr.is_true())
+  if(expr.is_constant() && to_constant_expr(expr).is_true())
     return const_literal(true);
-  else if(expr.is_false())
+  else if(expr.is_constant() && to_constant_expr(expr).is_false())
     return const_literal(false);
   else if(expr.id()==ID_literal)
     return to_literal_expr(expr).get_literal();
@@ -3379,7 +3379,7 @@ void smt2_convt::convert_constant(const constant_exprt &expr)
   }
   else if(expr_type.id()==ID_pointer)
   {
-    if(is_null_pointer(expr))
+    if(expr.is_null_pointer())
     {
       out << "(_ bv0 " << boolbv_width(expr_type)
           << ")";
diff --git a/src/solvers/smt2/smt2_format.cpp b/src/solvers/smt2/smt2_format.cpp
index 551f58f073c..80dd9751ca5 100644
--- a/src/solvers/smt2/smt2_format.cpp
+++ b/src/solvers/smt2/smt2_format.cpp
@@ -60,9 +60,9 @@ std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr)
     }
     else if(expr_type.id() == ID_bool)
     {
-      if(expr.is_true())
+      if(to_constant_expr(expr).is_true())
         out << "true";
-      else if(expr.is_false())
+      else if(to_constant_expr(expr).is_false())
         out << "false";
       else
         DATA_INVARIANT(false, "unknown Boolean constant");
diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
index dc4efc6fb3d..919212ec8a8 100644
--- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
+++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
@@ -329,7 +329,7 @@ struct sort_based_literal_convertert : public smt_sort_const_downcast_visitort
 
 static smt_termt convert_expr_to_smt(const constant_exprt &constant_literal)
 {
-  if(is_null_pointer(constant_literal))
+  if(constant_literal.is_null_pointer())
   {
     const size_t bit_width =
       type_checked_cast<pointer_typet>(constant_literal.type()).get_width();
diff --git a/src/solvers/strings/string_builtin_function.cpp b/src/solvers/strings/string_builtin_function.cpp
index 689818c4aaf..2d7b0e62b0a 100644
--- a/src/solvers/strings/string_builtin_function.cpp
+++ b/src/solvers/strings/string_builtin_function.cpp
@@ -31,7 +31,7 @@ std::optional<std::vector<mp_integer>> eval_string(
     const exprt cond = get_value(ite.cond());
     if(!cond.is_constant())
       return {};
-    return cond.is_true()
+    return to_constant_expr(cond).is_true()
              ? eval_string(to_array_string_expr(ite.true_case()), get_value)
              : eval_string(to_array_string_expr(ite.false_case()), get_value);
   }
diff --git a/src/solvers/strings/string_format_builtin_function.cpp b/src/solvers/strings/string_format_builtin_function.cpp
index 20ce1f8ab2a..8608a589461 100644
--- a/src/solvers/strings/string_format_builtin_function.cpp
+++ b/src/solvers/strings/string_format_builtin_function.cpp
@@ -596,8 +596,9 @@ string_constraintst string_format_builtin_functiont::constraints(
 
   auto result_constraint_pair = add_axioms_for_format(
     generator, result, format_string.value(), inputs, message_handler);
+  auto simp_expr = simplify_expr(result_constraint_pair.first, generator.ns);
   INVARIANT(
-    simplify_expr(result_constraint_pair.first, generator.ns).is_zero(),
+    simp_expr.is_constant() && to_constant_expr(simp_expr).is_zero(),
     "add_axioms_for_format should return 0, meaning that formatting was"
     "successful");
   result_constraint_pair.second.existential.push_back(
diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp
index e1980bed5f4..56624a4ca76 100644
--- a/src/solvers/strings/string_refinement.cpp
+++ b/src/solvers/strings/string_refinement.cpp
@@ -920,7 +920,7 @@ void string_refinementt::add_lemma(
     simplify(simple_lemma, ns);
   }
 
-  if(simple_lemma.is_true())
+  if(simple_lemma.is_constant() && to_constant_expr(simple_lemma).is_true())
   {
 #if 0
     log.debug() << "string_refinementt::add_lemma : tautology" << messaget::eom;
@@ -1843,9 +1843,9 @@ exprt string_refinementt::get(const exprt &expr) const
     {
       const auto &if_expr = expr_dynamic_cast<if_exprt>(current.get());
       const exprt cond = get(if_expr.cond());
-      if(cond.is_true())
+      if(cond.is_constant() && to_constant_expr(cond).is_true())
         current = std::cref(if_expr.true_case());
-      else if(cond.is_false())
+      else if(cond.is_constant() && to_constant_expr(cond).is_false())
         current = std::cref(if_expr.false_case());
       else
         UNREACHABLE;
@@ -2021,7 +2021,7 @@ static bool is_valid_string_constraint(
       const exprt i = pair.second[j];
       const equal_exprt equals(rep, i);
       const exprt result = simplify_expr(equals, ns);
-      if(result.is_false())
+      if(result.is_constant() && to_constant_expr(result).is_false())
       {
         stream << "Indices not equal: " << to_string(constraint)
                << ", str: " << format(pair.first) << messaget::eom;
diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp
index 4b14ec6ec7f..87babfb8b68 100644
--- a/src/util/arith_tools.cpp
+++ b/src/util/arith_tools.cpp
@@ -25,7 +25,7 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
 
   if(type_id==ID_pointer)
   {
-    if(is_null_pointer(expr))
+    if(expr.is_null_pointer())
     {
       int_value=0;
       return false;
diff --git a/src/util/expr.cpp b/src/util/expr.cpp
index bb9c814a496..88f269f90a8 100644
--- a/src/util/expr.cpp
+++ b/src/util/expr.cpp
@@ -26,14 +26,14 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \return True if is a Boolean constant representing `true`, false otherwise.
 bool exprt::is_true() const
 {
-  return is_constant() && is_boolean() && get(ID_value) != ID_false;
+  return is_constant() && to_constant_expr(*this).is_true();
 }
 
 /// Return whether the expression is a constant representing `false`.
 /// \return True if is a Boolean constant representing `false`, false otherwise.
 bool exprt::is_false() const
 {
-  return is_constant() && is_boolean() && get(ID_value) == ID_false;
+  return is_constant() && to_constant_expr(*this).is_false();
 }
 
 /// Return whether the expression is a constant representing 0.
@@ -47,44 +47,9 @@ bool exprt::is_false() const
 bool exprt::is_zero() const
 {
   if(is_constant())
-  {
-    const constant_exprt &constant=to_constant_expr(*this);
-    const irep_idt &type_id=type().id_string();
-
-    if(type_id==ID_integer || type_id==ID_natural)
-    {
-      return constant.value_is_zero_string();
-    }
-    else if(type_id==ID_rational)
-    {
-      rationalt rat_value;
-      if(to_rational(*this, rat_value))
-        CHECK_RETURN(false);
-      return rat_value.is_zero();
-    }
-    else if(
-      type_id == ID_unsignedbv || type_id == ID_signedbv ||
-      type_id == ID_c_bool || type_id == ID_c_bit_field)
-    {
-      return constant.value_is_zero_string();
-    }
-    else if(type_id==ID_fixedbv)
-    {
-      if(fixedbvt(constant)==0)
-        return true;
-    }
-    else if(type_id==ID_floatbv)
-    {
-      if(ieee_floatt(constant)==0)
-        return true;
-    }
-    else if(type_id==ID_pointer)
-    {
-      return is_null_pointer(constant);
-    }
-  }
-
-  return false;
+    return to_constant_expr(*this).is_zero();
+  else
+    return false;
 }
 
 /// Return whether the expression is a constant representing 1.
@@ -96,47 +61,9 @@ bool exprt::is_zero() const
 bool exprt::is_one() const
 {
   if(is_constant())
-  {
-    const auto &constant_expr = to_constant_expr(*this);
-    const irep_idt &type_id = type().id();
-
-    if(type_id==ID_integer || type_id==ID_natural)
-    {
-      mp_integer int_value =
-        string2integer(id2string(constant_expr.get_value()));
-      if(int_value==1)
-        return true;
-    }
-    else if(type_id==ID_rational)
-    {
-      rationalt rat_value;
-      if(to_rational(*this, rat_value))
-        CHECK_RETURN(false);
-      return rat_value.is_one();
-    }
-    else if(
-      type_id == ID_unsignedbv || type_id == ID_signedbv ||
-      type_id == ID_c_bool || type_id == ID_c_bit_field)
-    {
-      const auto width = to_bitvector_type(type()).get_width();
-      mp_integer int_value =
-        bvrep2integer(id2string(constant_expr.get_value()), width, false);
-      if(int_value==1)
-        return true;
-    }
-    else if(type_id==ID_fixedbv)
-    {
-      if(fixedbvt(constant_expr) == 1)
-        return true;
-    }
-    else if(type_id==ID_floatbv)
-    {
-      if(ieee_floatt(constant_expr) == 1)
-        return true;
-    }
-  }
-
-  return false;
+    return to_constant_expr(*this).is_one();
+  else
+    return false;
 }
 
 /// Get a \ref source_locationt from the expression or from its operands
diff --git a/src/util/expr.h b/src/util/expr.h
index 08e1d57a7e0..8327843c852 100644
--- a/src/util/expr.h
+++ b/src/util/expr.h
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_UTIL_EXPR_H
 
 #include "as_const.h"
+#include "deprecate.h"
 #include "type.h"
 #include "validate_expressions.h"
 #include "validate_types.h"
@@ -214,9 +215,13 @@ class exprt:public irept
     return id() == ID_constant;
   }
 
+  DEPRECATED(SINCE(2024, 9, 10, "use constant_exprt::is_true() instead"))
   bool is_true() const;
+  DEPRECATED(SINCE(2024, 9, 10, "use constant_exprt::is_false() instead"))
   bool is_false() const;
+  DEPRECATED(SINCE(2024, 9, 10, "use constant_exprt::is_zero() instead"))
   bool is_zero() const;
+  DEPRECATED(SINCE(2024, 9, 10, "use constant_exprt::is_one() instead"))
   bool is_one() const;
 
   /// Return whether the expression represents a Boolean.
diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp
index 3525b2804e1..e78ef7970b0 100644
--- a/src/util/expr_initializer.cpp
+++ b/src/util/expr_initializer.cpp
@@ -66,7 +66,7 @@ std::optional<exprt> expr_initializert::expr_initializer_rec(
     exprt result;
     if(init_expr.id() == ID_nondet)
       result = side_effect_expr_nondett(type, source_location);
-    else if(init_expr.is_zero())
+    else if(init_expr.is_constant() && to_constant_expr(init_expr).is_zero())
       result = from_integer(0, type);
     else
       result = duplicate_per_byte(init_expr, type, ns);
@@ -80,7 +80,7 @@ std::optional<exprt> expr_initializert::expr_initializer_rec(
     exprt result;
     if(init_expr.id() == ID_nondet)
       result = side_effect_expr_nondett(type, source_location);
-    else if(init_expr.is_zero())
+    else if(init_expr.is_constant() && to_constant_expr(init_expr).is_zero())
       result = constant_exprt(ID_0, type);
     else
       result = duplicate_per_byte(init_expr, type, ns);
@@ -94,7 +94,7 @@ std::optional<exprt> expr_initializert::expr_initializer_rec(
     exprt result;
     if(init_expr.id() == ID_nondet)
       result = side_effect_expr_nondett(type, source_location);
-    else if(init_expr.is_zero())
+    else if(init_expr.is_constant() && to_constant_expr(init_expr).is_zero())
     {
       const std::size_t width = to_bitvector_type(type).get_width();
       std::string value(width, '0');
@@ -112,7 +112,7 @@ std::optional<exprt> expr_initializert::expr_initializer_rec(
     exprt result;
     if(init_expr.id() == ID_nondet)
       result = side_effect_expr_nondett(type, source_location);
-    else if(init_expr.is_zero())
+    else if(init_expr.is_constant() && to_constant_expr(init_expr).is_zero())
     {
       auto sub_zero = expr_initializer_rec(
         to_complex_type(type).subtype(), source_location, init_expr);
@@ -287,7 +287,7 @@ std::optional<exprt> expr_initializert::expr_initializer_rec(
     exprt result;
     if(init_expr.id() == ID_nondet)
       result = side_effect_expr_nondett(type, source_location);
-    else if(init_expr.is_zero())
+    else if(init_expr.is_constant() && to_constant_expr(init_expr).is_zero())
       result = constant_exprt(irep_idt(), type);
     else
       result = duplicate_per_byte(init_expr, type, ns);
diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp
index 7e4739a7372..6727edaf0d0 100644
--- a/src/util/expr_util.cpp
+++ b/src/util/expr_util.cpp
@@ -68,33 +68,7 @@ exprt make_binary(const exprt &expr)
 
 with_exprt make_with_expr(const update_exprt &src)
 {
-  const exprt::operandst &designator=src.designator();
-  PRECONDITION(!designator.empty());
-
-  with_exprt result{exprt{}, exprt{}, exprt{}};
-  exprt *dest=&result;
-
-  for(const auto &expr : designator)
-  {
-    with_exprt tmp{exprt{}, exprt{}, exprt{}};
-
-    if(expr.id() == ID_index_designator)
-    {
-      tmp.where() = to_index_designator(expr).index();
-    }
-    else if(expr.id() == ID_member_designator)
-    {
-      // irep_idt component_name=
-      //  to_member_designator(*it).get_component_name();
-    }
-    else
-      UNREACHABLE;
-
-    *dest=tmp;
-    dest=&to_with_expr(*dest).new_value();
-  }
-
-  return result;
+  return src.make_with_expr();
 }
 
 exprt is_not_zero(
@@ -128,12 +102,17 @@ exprt is_not_zero(
 
 exprt boolean_negate(const exprt &src)
 {
+  PRECONDITION(src.is_boolean());
+
   if(src.id() == ID_not)
     return to_not_expr(src).op();
-  else if(src.is_true())
-    return false_exprt();
-  else if(src.is_false())
-    return true_exprt();
+  else if(auto constant_expr = expr_try_dynamic_cast<constant_exprt>(src))
+  {
+    if(constant_expr->is_true())
+      return false_exprt{};
+    else
+      return true_exprt{};
+  }
   else
     return not_exprt(src);
 }
@@ -338,51 +317,15 @@ bool can_forward_propagatet::is_constant_address_of(const exprt &expr) const
 
 constant_exprt make_boolean_expr(bool value)
 {
-  if(value)
-    return true_exprt();
-  else
-    return false_exprt();
+  return constant_exprt{value};
 }
 
 exprt make_and(exprt a, exprt b)
 {
-  PRECONDITION(a.is_boolean() && b.is_boolean());
-  if(b.is_constant())
-  {
-    if(b.get(ID_value) == ID_false)
-      return false_exprt{};
-    return a;
-  }
-  if(a.is_constant())
-  {
-    if(a.get(ID_value) == ID_false)
-      return false_exprt{};
-    return b;
-  }
-  if(b.id() == ID_and)
-  {
-    b.add_to_operands(std::move(a));
-    return b;
-  }
-  return and_exprt{std::move(a), std::move(b)};
+  return conjunction(a, b);
 }
 
 bool is_null_pointer(const constant_exprt &expr)
 {
-  if(expr.type().id() != ID_pointer)
-    return false;
-
-  if(expr.get_value() == ID_NULL)
-    return true;
-
-    // We used to support "0" (when NULL_is_zero), but really front-ends should
-    // resolve this and generate ID_NULL instead.
-#if 0
-  return config.ansi_c.NULL_is_zero && expr.value_is_zero_string();
-#else
-  INVARIANT(
-    !expr.value_is_zero_string() || !config.ansi_c.NULL_is_zero,
-    "front-end should use ID_NULL");
-  return false;
-#endif
+  return expr.is_null_pointer();
 }
diff --git a/src/util/expr_util.h b/src/util/expr_util.h
index b423dcdd9fb..558c0bd9ac9 100644
--- a/src/util/expr_util.h
+++ b/src/util/expr_util.h
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
  * \date   Sun Jul 31 21:54:44 BST 2011
 */
 
+#include "deprecate.h"
 #include "irep.h"
 
 #include <functional>
@@ -40,6 +41,7 @@ bool is_assignable(const exprt &);
 exprt make_binary(const exprt &);
 
 /// converts an update expr into a (possibly nested) with expression
+DEPRECATED(SINCE(2024, 9, 10, "use update_exprt::make_with_expr() instead"))
 with_exprt make_with_expr(const update_exprt &);
 
 /// converts a scalar/float expression to C/C++ Booleans
@@ -106,16 +108,19 @@ class can_forward_propagatet
 };
 
 /// returns true_exprt if given true and false_exprt otherwise
+DEPRECATED(SINCE(2024, 9, 10, "use constant_exprt::constant_exprt(bool)"))
 constant_exprt make_boolean_expr(bool);
 
 /// Conjunction of two expressions. If the second is already an `and_exprt`
 /// add to its operands instead of creating a new expression. If one is `true`,
 /// return the other expression. If one is `false` returns `false`.
+DEPRECATED(SINCE(2024, 9, 10, "use conjunction(exprt, exprt) instead"))
 exprt make_and(exprt a, exprt b);
 
 /// Returns true if \p expr has a pointer type and a value NULL; it also returns
 /// true when \p expr has value zero and NULL_is_zero is true; returns false in
 /// all other cases.
+DEPRECATED(SINCE(2024, 9, 10, "use constant_exprt::is_null_pointer() instead"))
 bool is_null_pointer(const constant_exprt &expr);
 
 #endif // CPROVER_UTIL_EXPR_UTIL_H
diff --git a/src/util/fixedbv.cpp b/src/util/fixedbv.cpp
index 822dff02a35..f41a666d595 100644
--- a/src/util/fixedbv.cpp
+++ b/src/util/fixedbv.cpp
@@ -126,11 +126,6 @@ fixedbvt &fixedbvt::operator/=(const fixedbvt &o)
   return *this;
 }
 
-bool fixedbvt::operator==(int i) const
-{
-  return v==power(2, spec.get_fraction_bits())*i;
-}
-
 std::string fixedbvt::format(
   const format_spect &format_spec) const
 {
diff --git a/src/util/fixedbv.h b/src/util/fixedbv.h
index bf37be62b7f..57e2a2b6263 100644
--- a/src/util/fixedbv.h
+++ b/src/util/fixedbv.h
@@ -66,8 +66,6 @@ class fixedbvt
 
   std::string format(const format_spect &format_spec) const;
 
-  bool operator==(int i) const;
-
   bool is_zero() const
   {
     return v==0;
diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp
index 582edeaa093..bd9b2f70e3c 100644
--- a/src/util/format_expr.cpp
+++ b/src/util/format_expr.cpp
@@ -194,7 +194,7 @@ static std::ostream &format_rec(std::ostream &os, const constant_exprt &src)
     return os << ieee_floatt(src);
   else if(type == ID_pointer)
   {
-    if(is_null_pointer(src))
+    if(src.is_null_pointer())
       return os << ID_NULL;
     else if(
       src.get_value() == "INVALID" || src.get_value().starts_with("INVALID-"))
diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp
index 1fee65294a2..29c1771a4b0 100644
--- a/src/util/ieee_float.cpp
+++ b/src/util/ieee_float.cpp
@@ -1024,13 +1024,6 @@ bool ieee_floatt::ieee_equal(const ieee_floatt &other) const
   return *this==other;
 }
 
-bool ieee_floatt::operator==(int i) const
-{
-  ieee_floatt other(spec);
-  other.from_integer(i);
-  return *this==other;
-}
-
 bool ieee_floatt::operator!=(const ieee_floatt &other) const
 {
   return !(*this==other);
diff --git a/src/util/ieee_float.h b/src/util/ieee_float.h
index 788975ba040..74bb2a8316a 100644
--- a/src/util/ieee_float.h
+++ b/src/util/ieee_float.h
@@ -133,13 +133,6 @@ class ieee_floatt
 
   ieee_float_spect spec;
 
-  explicit ieee_floatt(const ieee_float_spect &_spec):
-    rounding_mode(ROUND_TO_EVEN),
-    spec(_spec), sign_flag(false), exponent(0), fraction(0),
-    NaN_flag(false), infinity_flag(false)
-  {
-  }
-
   explicit ieee_floatt(ieee_float_spect __spec, rounding_modet __rounding_mode)
     : rounding_mode(__rounding_mode),
       spec(std::move(__spec)),
@@ -151,21 +144,17 @@ class ieee_floatt
   {
   }
 
-  explicit ieee_floatt(const floatbv_typet &type):
-    rounding_mode(ROUND_TO_EVEN),
-    spec(ieee_float_spect(type)),
-    sign_flag(false),
-    exponent(0),
-    fraction(0),
-    NaN_flag(false),
-    infinity_flag(false)
+  explicit ieee_floatt(const ieee_float_spect &_spec)
+    : ieee_floatt(_spec, ROUND_TO_EVEN)
+  {
+  }
+
+  explicit ieee_floatt(const floatbv_typet &type)
+    : ieee_floatt(ieee_float_spect(type))
   {
   }
 
-  ieee_floatt():
-    rounding_mode(ROUND_TO_EVEN),
-    sign_flag(false), exponent(0), fraction(0),
-    NaN_flag(false), infinity_flag(false)
+  ieee_floatt() : ieee_floatt(ieee_float_spect{}, ROUND_TO_EVEN)
   {
   }
 
@@ -305,7 +294,6 @@ class ieee_floatt
   // e.g., NAN==NAN
   bool operator==(const ieee_floatt &other) const;
   bool operator!=(const ieee_floatt &other) const;
-  bool operator==(int i) const;
 
   // these do IEEE equality, i.e., NAN!=NAN
   bool ieee_equal(const ieee_floatt &other) const;
diff --git a/src/util/interval.cpp b/src/util/interval.cpp
index 48c6d49c609..b7ee86d0453 100644
--- a/src/util/interval.cpp
+++ b/src/util/interval.cpp
@@ -689,7 +689,7 @@ exprt constant_interval_exprt::generate_division_expression(
 
   PRECONDITION(!is_zero(rhs));
 
-  if(rhs.is_one())
+  if(rhs.is_constant() && to_constant_expr(rhs).is_one())
   {
     return lhs;
   }
@@ -744,7 +744,7 @@ exprt constant_interval_exprt::generate_modulo_expression(
 
   PRECONDITION(!is_zero(rhs));
 
-  if(rhs.is_one())
+  if(rhs.is_constant() && to_constant_expr(rhs).is_one())
   {
     return lhs;
   }
@@ -1269,7 +1269,7 @@ bool constant_interval_exprt::is_zero(const exprt &expr)
 
   INVARIANT(!is_max(expr) && !is_min(expr), "We excluded those cases");
 
-  if(expr.is_zero())
+  if(expr.is_constant() && to_constant_expr(expr).is_zero())
   {
     return true;
   }
@@ -1351,7 +1351,8 @@ bool constant_interval_exprt::equal(const exprt &a, const exprt &b)
 
   INVARIANT(!is_extreme(l, r), "We've excluded this before");
 
-  return simplified_expr(equal_exprt(l, r)).is_true();
+  exprt simp_eq = simplified_expr(equal_exprt(l, r));
+  return simp_eq.is_constant() && to_constant_expr(simp_eq).is_true();
 }
 
 // TODO: Signed/unsigned comparisons.
@@ -1399,7 +1400,8 @@ bool constant_interval_exprt::less_than(const exprt &a, const exprt &b)
     !is_extreme(l) && !is_extreme(r),
     "We have excluded all of these cases in the code above");
 
-  return simplified_expr(binary_relation_exprt(l, ID_lt, r)).is_true();
+  exprt simp_lt = simplified_expr(binary_relation_exprt(l, ID_lt, r));
+  return simp_lt.is_constant() && to_constant_expr(simp_lt).is_true();
 }
 
 bool constant_interval_exprt::greater_than(const exprt &a, const exprt &b)
@@ -1628,8 +1630,11 @@ constant_interval_exprt::typecast(const typet &type) const
 {
   if(is_boolean() && is_int(type))
   {
-    bool lower = !has_no_lower_bound() && get_lower().is_true();
-    bool upper = has_no_upper_bound() || get_upper().is_true();
+    bool lower = !has_no_lower_bound() && get_lower().is_constant() &&
+                 to_constant_expr(get_lower()).is_true();
+    bool upper =
+      has_no_upper_bound() ||
+      (get_upper().is_constant() && to_constant_expr(get_upper()).is_true());
 
     INVARIANT(!lower || upper, "");
 
@@ -1875,7 +1880,9 @@ bool constant_interval_exprt::contains_zero() const
     return false;
   }
 
-  if(get_lower().is_zero() || get_upper().is_zero())
+  if(
+    (get_lower().is_constant() && to_constant_expr(get_lower()).is_zero()) ||
+    (get_upper().is_constant() && to_constant_expr(get_upper()).is_zero()))
   {
     return true;
   }
diff --git a/src/util/pointer_offset_sum.cpp b/src/util/pointer_offset_sum.cpp
index dc34d0eb0ce..238cd7d203e 100644
--- a/src/util/pointer_offset_sum.cpp
+++ b/src/util/pointer_offset_sum.cpp
@@ -19,9 +19,9 @@ exprt pointer_offset_sum(const exprt &a, const exprt &b)
     return a;
   else if(b.id() == ID_unknown)
     return b;
-  else if(a.is_zero())
+  else if(a.is_constant() && to_constant_expr(a).is_zero())
     return b;
-  else if(b.is_zero())
+  else if(b.is_constant() && to_constant_expr(b).is_zero())
     return a;
 
   return plus_exprt(a, typecast_exprt::conditional_cast(b, a.type()));
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 266de986ac4..26a036d0a25 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -105,7 +105,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_sign(const sign_exprt &expr)
     if(type.id()==ID_floatbv)
     {
       ieee_floatt value(to_constant_expr(expr.op()));
-      return make_boolean_expr(value.get_sign());
+      return constant_exprt{value.get_sign()};
     }
     else if(type.id()==ID_signedbv ||
             type.id()==ID_unsignedbv)
@@ -113,7 +113,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_sign(const sign_exprt &expr)
       const auto value = numeric_cast<mp_integer>(expr.op());
       if(value.has_value())
       {
-        return make_boolean_expr(*value >= 0);
+        return constant_exprt{*value >= 0};
       }
     }
   }
@@ -858,7 +858,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
   if(
     expr_type.id() == ID_pointer && expr.op().is_constant() &&
     (to_constant_expr(expr.op()).get_value() == ID_NULL ||
-     (expr.op().is_zero() && config.ansi_c.NULL_is_zero)))
+     (to_constant_expr(expr.op()).is_zero() && config.ansi_c.NULL_is_zero)))
   {
     exprt tmp = expr.op();
     tmp.type()=expr.type();
@@ -904,9 +904,10 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
 
     if(
       (op_plus_expr.op0().id() == ID_typecast &&
-       to_typecast_expr(op_plus_expr.op0()).op().is_zero()) ||
+       to_typecast_expr(op_plus_expr.op0()).op().is_constant() &&
+       to_constant_expr(to_typecast_expr(op_plus_expr.op0()).op()).is_zero()) ||
       (op_plus_expr.op0().is_constant() &&
-       is_null_pointer(to_constant_expr(op_plus_expr.op0()))))
+       to_constant_expr(op_plus_expr.op0()).is_null_pointer()))
     {
       auto sub_size =
         pointer_offset_size(to_pointer_type(op_type).base_type(), ns);
@@ -1032,7 +1033,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
 
       if(expr_type_id==ID_bool)
       {
-        return make_boolean_expr(int_value != 0);
+        return constant_exprt{int_value != 0};
       }
 
       if(expr_type_id==ID_unsignedbv ||
@@ -1071,11 +1072,11 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
          expr_type_id==ID_c_enum ||
          expr_type_id==ID_c_bit_field)
       {
-        if(operand.is_true())
+        if(to_constant_expr(operand).is_true())
         {
           return from_integer(1, expr_type);
         }
-        else if(operand.is_false())
+        else if(to_constant_expr(operand).is_false())
         {
           return from_integer(0, expr_type);
         }
@@ -1085,15 +1086,15 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
         const auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(expr_type));
         if(!c_enum_type.is_incomplete()) // possibly incomplete
         {
-          unsigned int_value = operand.is_true() ? 1u : 0u;
+          unsigned int_value = to_constant_expr(operand).is_true() ? 1u : 0u;
           exprt tmp=from_integer(int_value, c_enum_type);
           tmp.type()=expr_type; // we maintain the tag type
           return std::move(tmp);
         }
       }
-      else if(expr_type_id==ID_pointer &&
-              operand.is_false() &&
-              config.ansi_c.NULL_is_zero)
+      else if(
+        expr_type_id == ID_pointer && to_constant_expr(operand).is_false() &&
+        config.ansi_c.NULL_is_zero)
       {
         return null_pointer_exprt(to_pointer_type(expr_type));
       }
@@ -1110,7 +1111,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
 
       if(expr_type_id==ID_bool)
       {
-        return make_boolean_expr(int_value != 0);
+        return constant_exprt{int_value != 0};
       }
 
       if(expr_type_id==ID_c_bool)
@@ -2094,8 +2095,9 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
 
   // byte update of full object is byte_extract(new value)
   if(
-    offset.is_zero() && val_size.has_value() && *val_size > 0 &&
-    root_size.has_value() && *root_size > 0 && *val_size >= *root_size)
+    offset.is_constant() && to_constant_expr(offset).is_zero() &&
+    val_size.has_value() && *val_size > 0 && root_size.has_value() &&
+    *root_size > 0 && *val_size >= *root_size)
   {
     byte_extract_exprt be(
       matching_byte_extract_id,
@@ -2419,8 +2421,9 @@ simplify_exprt::simplify_overflow_binary(const binary_overflow_exprt &expr)
   // When one operand is zero, an overflow can only occur for a subtraction from
   // zero.
   if(
-    expr.op1().is_zero() ||
-    (expr.op0().is_zero() && !can_cast_expr<minus_overflow_exprt>(expr)))
+    (expr.op1().is_constant() && to_constant_expr(expr.op1()).is_zero()) ||
+    (expr.op0().is_constant() && to_constant_expr(expr.op0()).is_zero() &&
+     !can_cast_expr<minus_overflow_exprt>(expr)))
   {
     return false_exprt{};
   }
@@ -2428,7 +2431,8 @@ simplify_exprt::simplify_overflow_binary(const binary_overflow_exprt &expr)
   // One is neutral element for multiplication
   if(
     can_cast_expr<mult_overflow_exprt>(expr) &&
-    (expr.op0().is_one() || expr.op1().is_one()))
+    ((expr.op0().is_constant() && to_constant_expr(expr.op0()).is_one()) ||
+     (expr.op1().is_constant() && to_constant_expr(expr.op1()).is_one())))
   {
     return false_exprt{};
   }
@@ -2489,7 +2493,7 @@ simplify_exprt::resultt<>
 simplify_exprt::simplify_overflow_unary(const unary_overflow_exprt &expr)
 {
   // zero is a neutral element for all operations supported here
-  if(expr.op().is_zero())
+  if(expr.op().is_constant() && to_constant_expr(expr.op()).is_zero())
     return false_exprt{};
 
   // catch some cases over mathematical types
@@ -2539,7 +2543,7 @@ simplify_exprt::simplify_overflow_result(const overflow_result_exprt &expr)
   if(expr.id() == ID_overflow_result_unary_minus)
   {
     // zero is a neutral element
-    if(expr.op0().is_zero())
+    if(expr.op0().is_constant() && to_constant_expr(expr.op0()).is_zero())
       return struct_exprt{{expr.op0(), false_exprt{}}, expr.type()};
 
     // catch some cases over mathematical types
@@ -2590,7 +2594,7 @@ simplify_exprt::simplify_overflow_result(const overflow_result_exprt &expr)
   {
     // When one operand is zero, an overflow can only occur for a subtraction
     // from zero.
-    if(expr.op0().is_zero())
+    if(expr.op0().is_constant() && to_constant_expr(expr.op0()).is_zero())
     {
       if(
         expr.id() == ID_overflow_result_plus ||
@@ -2604,7 +2608,7 @@ simplify_exprt::simplify_overflow_result(const overflow_result_exprt &expr)
           {from_integer(0, expr.op0().type()), false_exprt{}}, expr.type()};
       }
     }
-    else if(expr.op1().is_zero())
+    else if(expr.op1().is_constant() && to_constant_expr(expr.op1()).is_zero())
     {
       if(
         expr.id() == ID_overflow_result_plus ||
@@ -2623,10 +2627,14 @@ simplify_exprt::simplify_overflow_result(const overflow_result_exprt &expr)
     // One is neutral element for multiplication
     if(
       expr.id() == ID_overflow_result_mult &&
-      (expr.op0().is_one() || expr.op1().is_one()))
+      ((expr.op0().is_constant() && to_constant_expr(expr.op0()).is_one()) ||
+       (expr.op1().is_constant() && to_constant_expr(expr.op1()).is_one())))
     {
       return struct_exprt{
-        {expr.op0().is_one() ? expr.op1() : expr.op0(), false_exprt{}},
+        {(expr.op0().is_constant() && to_constant_expr(expr.op0()).is_one())
+           ? expr.op1()
+           : expr.op0(),
+         false_exprt{}},
         expr.type()};
     }
 
diff --git a/src/util/simplify_expr_array.cpp b/src/util/simplify_expr_array.cpp
index 1a520182176..702819d6225 100644
--- a/src/util/simplify_expr_array.cpp
+++ b/src/util/simplify_expr_array.cpp
@@ -93,11 +93,15 @@ simplify_exprt::simplify_index(const index_exprt &expr)
       exprt new_index_expr = simplify_index(
         index_exprt(with_expr.old(), index, new_expr.type())); // recursive call
 
-      if(equality_expr.is_true())
+      if(
+        equality_expr.is_constant() &&
+        to_constant_expr(equality_expr).is_true())
       {
         return with_expr.new_value();
       }
-      else if(equality_expr.is_false())
+      else if(
+        equality_expr.is_constant() &&
+        to_constant_expr(equality_expr).is_false())
       {
         return new_index_expr;
       }
diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp
index 569c91ef837..6cf7d82e265 100644
--- a/src/util/simplify_expr_boolean.cpp
+++ b/src/util/simplify_expr_boolean.cpp
@@ -56,13 +56,13 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
 
       bool erase;
 
-      if(it->is_true())
+      if(it->is_constant() && to_constant_expr(*it).is_true())
       {
         erase=true;
         negate=!negate;
       }
       else
-        erase=it->is_false();
+        erase = it->is_constant() && to_constant_expr(*it).is_false();
 
       if(erase)
       {
@@ -75,7 +75,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
 
     if(new_operands.empty())
     {
-      return make_boolean_expr(negate);
+      return constant_exprt{negate};
     }
     else if(new_operands.size() == 1)
     {
@@ -110,8 +110,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
       if(!it->is_boolean())
         return unchanged(expr);
 
-      bool is_true=it->is_true();
-      bool is_false=it->is_false();
+      bool is_true = it->is_constant() && to_constant_expr(*it).is_true();
+      bool is_false = it->is_constant() && to_constant_expr(*it).is_false();
 
       if(expr.id()==ID_and && is_false)
       {
@@ -298,12 +298,12 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
         op.id() == ID_not && op.is_boolean() &&
         expr_set.find(to_not_expr(op).op()) != expr_set.end())
       {
-        return make_boolean_expr(expr.id() == ID_or);
+        return constant_exprt{expr.id() == ID_or};
       }
 
     if(new_operands.empty())
     {
-      return make_boolean_expr(expr.id() == ID_and);
+      return constant_exprt{expr.id() == ID_and};
     }
     else if(new_operands.size() == 1)
     {
@@ -334,11 +334,11 @@ simplify_exprt::resultt<> simplify_exprt::simplify_not(const not_exprt &expr)
   {
     return to_not_expr(op).op();
   }
-  else if(op.is_false())
+  else if(op.is_constant() && to_constant_expr(op).is_false())
   {
     return true_exprt();
   }
-  else if(op.is_true())
+  else if(op.is_constant() && to_constant_expr(op).is_true())
   {
     return false_exprt();
   }
diff --git a/src/util/simplify_expr_floatbv.cpp b/src/util/simplify_expr_floatbv.cpp
index f7fdd2952b3..8f69dbaba88 100644
--- a/src/util/simplify_expr_floatbv.cpp
+++ b/src/util/simplify_expr_floatbv.cpp
@@ -27,7 +27,7 @@ simplify_exprt::simplify_isinf(const unary_exprt &expr)
   if(expr.op().is_constant())
   {
     ieee_floatt value(to_constant_expr(expr.op()));
-    return make_boolean_expr(value.is_infinity());
+    return constant_exprt{value.is_infinity()};
   }
 
   return unchanged(expr);
@@ -41,7 +41,7 @@ simplify_exprt::simplify_isnan(const unary_exprt &expr)
   if(expr.op().is_constant())
   {
     ieee_floatt value(to_constant_expr(expr.op()));
-    return make_boolean_expr(value.is_NaN());
+    return constant_exprt{value.is_NaN()};
   }
 
   return unchanged(expr);
@@ -55,7 +55,7 @@ simplify_exprt::simplify_isnormal(const unary_exprt &expr)
   if(expr.op().is_constant())
   {
     ieee_floatt value(to_constant_expr(expr.op()));
-    return make_boolean_expr(value.is_normal());
+    return constant_exprt{value.is_normal()};
   }
 
   return unchanged(expr);
@@ -116,7 +116,7 @@ bool simplify_exprt::simplify_sign(exprt &expr)
     if(type.id()==ID_floatbv)
     {
       ieee_floatt value(to_constant_expr(expr.op0()));
-      expr = make_boolean_expr(value.get_sign());
+      expr = constant_exprt{value.get_sign()};
       return false;
     }
     else if(type.id()==ID_signedbv ||
@@ -125,7 +125,7 @@ bool simplify_exprt::simplify_sign(exprt &expr)
       mp_integer value;
       if(!to_integer(expr.op0(), value))
       {
-        expr = make_boolean_expr(value>=0);
+        expr = constant_exprt{value>=0};
         return false;
       }
     }
@@ -325,8 +325,9 @@ simplify_exprt::simplify_floatbv_op(const ieee_float_op_exprt &expr)
   }
 
   // division by one? Exact for all rounding modes.
-  if(expr.id()==ID_floatbv_div &&
-     op1.is_constant() && op1.is_one())
+  if(
+    expr.id() == ID_floatbv_div && op1.is_constant() &&
+    to_constant_expr(op1).is_one())
   {
     return op0;
   }
@@ -355,9 +356,9 @@ simplify_exprt::simplify_ieee_float_relation(const binary_relation_exprt &expr)
     ieee_floatt f_rhs(to_constant_expr(expr.rhs()));
 
     if(expr.id()==ID_ieee_float_notequal)
-      return make_boolean_expr(f_lhs.ieee_not_equal(f_rhs));
+      return constant_exprt{f_lhs.ieee_not_equal(f_rhs)};
     else if(expr.id()==ID_ieee_float_equal)
-      return make_boolean_expr(f_lhs.ieee_equal(f_rhs));
+      return constant_exprt{f_lhs.ieee_equal(f_rhs)};
     else
       UNREACHABLE;
   }
diff --git a/src/util/simplify_expr_if.cpp b/src/util/simplify_expr_if.cpp
index c951603af48..31188f7df39 100644
--- a/src/util/simplify_expr_if.cpp
+++ b/src/util/simplify_expr_if.cpp
@@ -250,8 +250,8 @@ simplify_exprt::simplify_if_preorder(const if_exprt &expr)
   // 1 ? a : b -> a  and  0 ? a : b -> b
   if(r_cond.expr.is_constant())
   {
-    return changed(
-      simplify_rec(r_cond.expr.is_true() ? truevalue : falsevalue));
+    return changed(simplify_rec(
+      to_constant_expr(r_cond.expr).is_true() ? truevalue : falsevalue));
   }
 
   if(do_simplify_if)
@@ -350,33 +350,39 @@ simplify_exprt::resultt<> simplify_exprt::simplify_if(const if_exprt &expr)
     {
       // a?b:c <-> (a && b) || (!a && c)
 
-      if(truevalue.is_true() && falsevalue.is_false())
+      if(
+        truevalue.is_constant() && to_constant_expr(truevalue).is_true() &&
+        falsevalue.is_constant() && to_constant_expr(falsevalue).is_false())
       {
         // a?1:0 <-> a
         return cond;
       }
-      else if(truevalue.is_false() && falsevalue.is_true())
+      else if(
+        truevalue.is_constant() && to_constant_expr(truevalue).is_false() &&
+        falsevalue.is_constant() && to_constant_expr(falsevalue).is_true())
       {
         // a?0:1 <-> !a
         return changed(simplify_not(not_exprt(cond)));
       }
-      else if(falsevalue.is_false())
+      else if(
+        falsevalue.is_constant() && to_constant_expr(falsevalue).is_false())
       {
         // a?b:0 <-> a AND b
         return changed(simplify_boolean(and_exprt(cond, truevalue)));
       }
-      else if(falsevalue.is_true())
+      else if(
+        falsevalue.is_constant() && to_constant_expr(falsevalue).is_true())
       {
         // a?b:1 <-> !a OR b
         return changed(
           simplify_boolean(or_exprt(simplify_not(not_exprt(cond)), truevalue)));
       }
-      else if(truevalue.is_true())
+      else if(truevalue.is_constant() && to_constant_expr(truevalue).is_true())
       {
         // a?1:b <-> a||(!a && b) <-> a OR b
         return changed(simplify_boolean(or_exprt(cond, falsevalue)));
       }
-      else if(truevalue.is_false())
+      else if(truevalue.is_constant() && to_constant_expr(truevalue).is_false())
       {
         // a?0:b <-> !a && b
         return changed(simplify_boolean(
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index 473f75bb450..5cbce879efa 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -189,8 +189,9 @@ simplify_exprt::resultt<> simplify_exprt::simplify_mult(const mult_exprt &expr)
 
     // if one of the operands is zero the result is zero
     // note: not true on IEEE floating point arithmetic
-    if(it->is_zero() &&
-       it->type().id()!=ID_floatbv)
+    if(
+      it->is_constant() && to_constant_expr(*it).is_zero() &&
+      it->type().id() != ID_floatbv)
     {
       return from_integer(0, expr.type());
     }
@@ -250,7 +251,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_mult(const mult_exprt &expr)
   else
   {
     // if the constant is a one and there are other factors
-    if(constant_found && constant->is_one())
+    if(constant_found && to_constant_expr(*constant).is_one())
     {
       // just delete it
       new_operands.erase(constant);
@@ -343,8 +344,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_div(const div_exprt &expr)
   else if(expr_type.id()==ID_fixedbv)
   {
     // division by one?
-    if(expr.op1().is_constant() &&
-       expr.op1().is_one())
+    if(expr.op1().is_constant() && to_constant_expr(expr.op1()).is_one())
     {
       return expr.op0();
     }
@@ -538,7 +538,9 @@ simplify_exprt::resultt<> simplify_exprt::simplify_plus(const plus_exprt &expr)
         it != new_operands.end();
         /* no it++ */)
     {
-      if(is_number(it->type()) && it->is_zero())
+      if(
+        is_number(it->type()) && it->is_constant() &&
+        to_constant_expr(*it).is_zero())
       {
         it = new_operands.erase(it);
         no_change = false;
@@ -619,7 +621,8 @@ simplify_exprt::simplify_minus(const minus_exprt &expr)
       if(
         offset_op0.is_constant() && offset_op1.is_constant() &&
         object_size.has_value() && element_size.has_value() &&
-        element_size->is_constant() && !element_size->is_zero() &&
+        element_size->is_constant() &&
+        !to_constant_expr(*element_size).is_zero() &&
         numeric_cast_v<mp_integer>(to_constant_expr(offset_op0)) <=
           *object_size &&
         numeric_cast_v<mp_integer>(to_constant_expr(offset_op1)) <=
@@ -647,7 +650,7 @@ simplify_exprt::simplify_minus(const minus_exprt &expr)
 
       if(
         element_size.has_value() && element_size->is_constant() &&
-        !element_size->is_zero())
+        !to_constant_expr(*element_size).is_zero())
       {
         return changed(simplify_rec(div_exprt{
           minus_exprt{offset_op0, offset_op1},
@@ -675,7 +678,9 @@ simplify_exprt::simplify_bitwise(const multi_ary_exprt &expr)
       if(op.id() == ID_typecast && to_typecast_expr(op).op().is_boolean())
       {
       }
-      else if(op.is_zero() || op.is_one())
+      else if(
+        op.is_constant() &&
+        (to_constant_expr(op).is_zero() || to_constant_expr(op).is_one()))
       {
       }
       else
@@ -700,9 +705,9 @@ simplify_exprt::simplify_bitwise(const multi_ary_exprt &expr)
       {
         if(it->id()==ID_typecast)
           *it = to_typecast_expr(*it).op();
-        else if(it->is_zero())
+        else if(it->is_constant() && to_constant_expr(*it).is_zero())
           *it=false_exprt();
-        else if(it->is_one())
+        else if(it->is_constant() && to_constant_expr(*it).is_one())
           *it=true_exprt();
       }
 
@@ -770,14 +775,16 @@ simplify_exprt::simplify_bitwise(const multi_ary_exprt &expr)
     for(exprt::operandst::iterator it = new_expr.operands().begin();
         it != new_expr.operands().end();) // no it++
     {
-      if(it->is_zero() && new_expr.operands().size() > 1)
+      if(
+        it->is_constant() && to_constant_expr(*it).is_zero() &&
+        new_expr.operands().size() > 1)
       {
         it = new_expr.operands().erase(it);
         no_change = false;
       }
       else if(
         it->is_constant() && it->type().id() == ID_bv &&
-        to_constant_expr(*it).value_is_zero_string() &&
+        *it == to_bv_type(it->type()).all_zeros_expr() &&
         new_expr.operands().size() > 1)
       {
         it = new_expr.operands().erase(it);
@@ -859,7 +866,7 @@ simplify_exprt::simplify_extractbit(const extractbit_exprt &expr)
     src_bit_width,
     numeric_cast_v<std::size_t>(*index_converted_to_int));
 
-  return make_boolean_expr(bit);
+  return constant_exprt{bit};
 }
 
 simplify_exprt::resultt<>
@@ -875,9 +882,11 @@ simplify_exprt::simplify_concatenation(const concatenation_exprt &expr)
     Forall_operands(it, new_expr)
     {
       exprt &op=*it;
-      if(op.is_true() || op.is_false())
+      if(
+        op.is_constant() &&
+        (to_constant_expr(op).is_true() || to_constant_expr(op).is_false()))
       {
-        const bool value = op.is_true();
+        const bool value = to_constant_expr(op).is_true();
         op = from_integer(value, unsignedbv_typet(1));
         no_change = false;
       }
@@ -1452,7 +1461,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_both_constant(
       }
       equal = tmp0_const.is_zero() && tmp1_const.is_zero();
     }
-    return make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
+    return constant_exprt{expr.id() == ID_equal ? equal : !equal};
   }
 
   if(tmp0.type().id() == ID_fixedbv)
@@ -1461,13 +1470,13 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_both_constant(
     fixedbvt f1(tmp1_const);
 
     if(expr.id() == ID_ge)
-      return make_boolean_expr(f0 >= f1);
+      return constant_exprt{f0 >= f1};
     else if(expr.id() == ID_le)
-      return make_boolean_expr(f0 <= f1);
+      return constant_exprt{f0 <= f1};
     else if(expr.id() == ID_gt)
-      return make_boolean_expr(f0 > f1);
+      return constant_exprt{f0 > f1};
     else if(expr.id() == ID_lt)
-      return make_boolean_expr(f0 < f1);
+      return constant_exprt{f0 < f1};
     else
       UNREACHABLE;
   }
@@ -1477,13 +1486,13 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_both_constant(
     ieee_floatt f1(tmp1_const);
 
     if(expr.id() == ID_ge)
-      return make_boolean_expr(f0 >= f1);
+      return constant_exprt{f0 >= f1};
     else if(expr.id() == ID_le)
-      return make_boolean_expr(f0 <= f1);
+      return constant_exprt{f0 <= f1};
     else if(expr.id() == ID_gt)
-      return make_boolean_expr(f0 > f1);
+      return constant_exprt{f0 > f1};
     else if(expr.id() == ID_lt)
-      return make_boolean_expr(f0 < f1);
+      return constant_exprt{f0 < f1};
     else
       UNREACHABLE;
   }
@@ -1498,13 +1507,13 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_both_constant(
       return unchanged(expr);
 
     if(expr.id() == ID_ge)
-      return make_boolean_expr(r0 >= r1);
+      return constant_exprt{r0 >= r1};
     else if(expr.id() == ID_le)
-      return make_boolean_expr(r0 <= r1);
+      return constant_exprt{r0 <= r1};
     else if(expr.id() == ID_gt)
-      return make_boolean_expr(r0 > r1);
+      return constant_exprt{r0 > r1};
     else if(expr.id() == ID_lt)
-      return make_boolean_expr(r0 < r1);
+      return constant_exprt{r0 < r1};
     else
       UNREACHABLE;
   }
@@ -1521,13 +1530,13 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_both_constant(
       return unchanged(expr);
 
     if(expr.id() == ID_ge)
-      return make_boolean_expr(*v0 >= *v1);
+      return constant_exprt{*v0 >= *v1};
     else if(expr.id() == ID_le)
-      return make_boolean_expr(*v0 <= *v1);
+      return constant_exprt{*v0 <= *v1};
     else if(expr.id() == ID_gt)
-      return make_boolean_expr(*v0 > *v1);
+      return constant_exprt{*v0 > *v1};
     else if(expr.id() == ID_lt)
-      return make_boolean_expr(*v0 < *v1);
+      return constant_exprt{*v0 < *v1};
     else
       UNREACHABLE;
   }
@@ -1537,9 +1546,10 @@ static bool eliminate_common_addends(exprt &op0, exprt &op1)
 {
   // we can't eliminate zeros
   if(
-    op0.is_zero() || op1.is_zero() ||
-    (op0.is_constant() && is_null_pointer(to_constant_expr(op0))) ||
-    (op1.is_constant() && is_null_pointer(to_constant_expr(op1))))
+    (op0.is_constant() && to_constant_expr(op0).is_zero()) ||
+    (op1.is_constant() && to_constant_expr(op1).is_zero()) ||
+    (op0.is_constant() && to_constant_expr(op0).is_null_pointer()) ||
+    (op1.is_constant() && to_constant_expr(op1).is_null_pointer()))
   {
     return true;
   }
@@ -1566,8 +1576,9 @@ static bool eliminate_common_addends(exprt &op0, exprt &op1)
   }
   else if(op0==op1)
   {
-    if(!op0.is_zero() &&
-       op0.type().id()!=ID_complex)
+    if(
+      (!op0.is_constant() || !to_constant_expr(op0).is_zero()) &&
+      op0.type().id() != ID_complex)
     {
       // elimination!
       op0=from_integer(0, op0.type());
@@ -1625,7 +1636,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_no_constant(
                            std::move(offset), ID_lt, std::move(*object_size)})
               .expr;
           if(in_object_bounds.is_constant())
-            return tvt{in_object_bounds.is_true()};
+            return tvt{to_constant_expr(in_object_bounds).is_true()};
         }
 
         return tvt::unknown();
@@ -1736,7 +1747,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant(
 
     const constant_exprt &op1_constant = to_constant_expr(expr.op1());
 
-    if(is_null_pointer(op1_constant))
+    if(op1_constant.is_null_pointer())
     {
       // the address of an object is never NULL
 
@@ -1799,8 +1810,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant(
 
         exprt ptr = simplify_object(expr.op0()).expr;
         // NULL + N == NULL is N == 0
-        if(ptr.is_constant() && is_null_pointer(to_constant_expr(ptr)))
-          return make_boolean_expr(offset.is_zero());
+        if(ptr.is_constant() && to_constant_expr(ptr).is_null_pointer())
+          return constant_exprt{to_constant_expr(offset).is_zero()};
         // &x + N == NULL is false when the offset is in bounds
         else if(auto address_of = expr_try_dynamic_cast<address_of_exprt>(ptr))
         {
@@ -1887,7 +1898,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant(
 
   // is the constant zero?
 
-  if(expr.op1().is_zero())
+  if(expr.op1().is_constant() && to_constant_expr(expr.op1()).is_zero())
   {
     if(expr.id()==ID_ge &&
        expr.op0().type().id()==ID_unsignedbv)
@@ -1976,13 +1987,17 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant(
     const auto &lhs_typecast_op = to_typecast_expr(expr.op0()).op();
 
     // we re-write (TYPE)boolean == 0 -> !boolean
-    if(expr.op1().is_zero() && expr.id()==ID_equal)
+    if(
+      expr.op1().is_constant() && to_constant_expr(expr.op1()).is_zero() &&
+      expr.id() == ID_equal)
     {
       return changed(simplify_not(not_exprt(lhs_typecast_op)));
     }
 
     // we re-write (TYPE)boolean != 0 -> boolean
-    if(expr.op1().is_zero() && expr.id()==ID_notequal)
+    if(
+      expr.op1().is_constant() && to_constant_expr(expr.op1()).is_zero() &&
+      expr.id() == ID_notequal)
     {
       return lhs_typecast_op;
     }
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
index 1511717dd94..92e1b3e8d7f 100644
--- a/src/util/simplify_expr_pointer.cpp
+++ b/src/util/simplify_expr_pointer.cpp
@@ -38,7 +38,7 @@ static bool is_dereference_integer_object(
     {
       const constant_exprt &constant = to_constant_expr(pointer);
 
-      if(is_null_pointer(constant))
+      if(constant.is_null_pointer())
       {
         address=0;
         return true;
@@ -218,11 +218,15 @@ simplify_exprt::simplify_address_of_arg(const exprt &expr)
     }
 
     // condition is a constant?
-    if(new_if_expr.cond().is_true())
+    if(
+      new_if_expr.cond().is_constant() &&
+      to_constant_expr(new_if_expr.cond()).is_true())
     {
       return new_if_expr.true_case();
     }
-    else if(new_if_expr.cond().is_false())
+    else if(
+      new_if_expr.cond().is_constant() &&
+      to_constant_expr(new_if_expr.cond()).is_false())
     {
       return new_if_expr.false_case();
     }
@@ -246,7 +250,9 @@ simplify_exprt::simplify_address_of(const address_of_exprt &expr)
   {
     auto index_expr = to_index_expr(new_object.expr);
 
-    if(!index_expr.index().is_zero())
+    if(
+      !index_expr.index().is_constant() ||
+      !to_constant_expr(index_expr.index()).is_zero())
     {
       // we normalize &a[i] to (&a[0])+i
       exprt offset = index_expr.op1();
@@ -353,7 +359,7 @@ simplify_exprt::simplify_pointer_offset(const pointer_offset_exprt &expr)
     {
       if(op.type().id()==ID_pointer)
         ptr_expr.push_back(op);
-      else if(!op.is_zero())
+      else if(!op.is_constant() || !to_constant_expr(op).is_zero())
       {
         exprt tmp=op;
         if(tmp.type()!=expr.type())
@@ -398,7 +404,7 @@ simplify_exprt::simplify_pointer_offset(const pointer_offset_exprt &expr)
   {
     const constant_exprt &c_ptr = to_constant_expr(ptr);
 
-    if(is_null_pointer(c_ptr))
+    if(c_ptr.is_null_pointer())
     {
       return from_integer(0, expr.type());
     }
@@ -424,7 +430,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_address_of(
 
   if(
     tmp0_address_of.object().id() == ID_index &&
-    to_index_expr(tmp0_address_of.object()).index().is_zero())
+    to_index_expr(tmp0_address_of.object()).index().is_constant() &&
+    to_constant_expr(to_index_expr(tmp0_address_of.object()).index()).is_zero())
   {
     tmp0_address_of =
       address_of_exprt(to_index_expr(tmp0_address_of.object()).array());
@@ -438,7 +445,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_address_of(
 
   if(
     tmp1_address_of.object().id() == ID_index &&
-    to_index_expr(tmp1_address_of.object()).index().is_zero())
+    to_index_expr(tmp1_address_of.object()).index().is_constant() &&
+    to_constant_expr(to_index_expr(tmp1_address_of.object()).index()).is_zero())
   {
     tmp1 = address_of_exprt(to_index_expr(tmp1_address_of.object()).array());
   }
@@ -451,7 +459,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_address_of(
     bool equal = to_symbol_expr(tmp0_object).get_identifier() ==
                  to_symbol_expr(tmp1_object).get_identifier();
 
-    return make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
+    return constant_exprt{expr.id() == ID_equal ? equal : !equal};
   }
   else if(
     tmp0_object.id() == ID_dynamic_object &&
@@ -460,19 +468,19 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_address_of(
     bool equal = to_dynamic_object_expr(tmp0_object).get_instance() ==
                  to_dynamic_object_expr(tmp1_object).get_instance();
 
-    return make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
+    return constant_exprt{expr.id() == ID_equal ? equal : !equal};
   }
   else if(
     (tmp0_object.id() == ID_symbol && tmp1_object.id() == ID_dynamic_object) ||
     (tmp0_object.id() == ID_dynamic_object && tmp1_object.id() == ID_symbol))
   {
-    return make_boolean_expr(expr.id() != ID_equal);
+    return constant_exprt{expr.id() != ID_equal};
   }
   else if(
     tmp0_object.id() == ID_string_constant &&
     tmp1_object.id() == ID_string_constant && tmp0_object == tmp1_object)
   {
-    return make_boolean_expr(expr.id() == ID_equal);
+    return constant_exprt{expr.id() == ID_equal};
   }
 
   return unchanged(expr);
@@ -500,7 +508,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_pointer_object(
         return unchanged(expr);
       }
     }
-    else if(!op.is_constant() || !op.is_zero())
+    else if(!op.is_constant() || !to_constant_expr(op).is_zero())
     {
       return unchanged(expr);
     }
@@ -571,7 +579,7 @@ simplify_exprt::simplify_is_dynamic_object(const unary_exprt &expr)
   }
 
   // NULL is not dynamic
-  if(op.is_constant() && is_null_pointer(to_constant_expr(op)))
+  if(op.is_constant() && to_constant_expr(op).is_null_pointer())
     return false_exprt();
 
   // &something depends on the something
@@ -584,8 +592,7 @@ simplify_exprt::simplify_is_dynamic_object(const unary_exprt &expr)
       const irep_idt identifier = to_symbol_expr(op_object).get_identifier();
 
       // this is for the benefit of symex
-      return make_boolean_expr(
-        identifier.starts_with(SYMEX_DYNAMIC_PREFIX "::"));
+      return constant_exprt{identifier.starts_with(SYMEX_DYNAMIC_PREFIX "::")};
     }
     else if(op_object.id() == ID_string_constant)
     {
@@ -619,7 +626,7 @@ simplify_exprt::simplify_is_invalid_pointer(const unary_exprt &expr)
   }
 
   // NULL is not invalid
-  if(op.is_constant() && is_null_pointer(to_constant_expr(op)))
+  if(op.is_constant() && to_constant_expr(op).is_null_pointer())
   {
     return false_exprt();
   }
diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp
index 80b1961508c..9ad47c77688 100644
--- a/src/util/simplify_expr_struct.cpp
+++ b/src/util/simplify_expr_struct.cpp
@@ -172,7 +172,9 @@ simplify_exprt::simplify_member(const member_exprt &expr)
     {
       // rewrite byte_extract(X, 0).member to X
       // if the type of X is that of the member
-      if(byte_extract_expr.offset().is_zero())
+      if(
+        byte_extract_expr.offset().is_constant() &&
+        to_constant_expr(byte_extract_expr.offset()).is_zero())
       {
         const union_typet &union_type =
           op.type().id() == ID_union_tag
diff --git a/src/util/simplify_utils.cpp b/src/util/simplify_utils.cpp
index 3b61acd4d08..624d43e3f22 100644
--- a/src/util/simplify_utils.cpp
+++ b/src/util/simplify_utils.cpp
@@ -439,7 +439,7 @@ expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
     }
     else if(type.id() == ID_pointer)
     {
-      if(config.ansi_c.NULL_is_zero && is_null_pointer(to_constant_expr(expr)))
+      if(config.ansi_c.NULL_is_zero && to_constant_expr(expr).is_null_pointer())
         return std::string(to_bitvector_type(type).get_width(), '0');
       else
         return {};
diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp
index 50cb5684220..d1f57046ca6 100644
--- a/src/util/std_expr.cpp
+++ b/src/util/std_expr.cpp
@@ -8,19 +8,155 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "std_expr.h"
 
+#include "arith_tools.h"
+#include "config.h"
+#include "expr_util.h"
+#include "fixedbv.h"
+#include "ieee_float.h"
+#include "mathematical_types.h"
 #include "namespace.h"
 #include "pointer_expr.h"
 #include "range.h"
+#include "rational.h"
+#include "rational_tools.h"
 #include "substitute_symbols.h"
 
 #include <map>
 
+constant_exprt::constant_exprt(bool value)
+  : constant_exprt(value ? ID_true : ID_false, bool_typet{})
+{
+}
+
 bool constant_exprt::value_is_zero_string() const
 {
   const std::string val=id2string(get_value());
   return val.find_first_not_of('0')==std::string::npos;
 }
 
+bool constant_exprt::is_true() const
+{
+  return is_boolean() && get_value() != ID_false;
+}
+
+bool constant_exprt::is_false() const
+{
+  return is_boolean() && get_value() == ID_false;
+}
+
+bool constant_exprt::is_zero() const
+{
+  const irep_idt &type_id = type().id();
+
+  if(type_id == ID_integer)
+  {
+    return integer_typet{}.zero_expr() == *this;
+  }
+  else if(type_id == ID_natural)
+  {
+    return natural_typet{}.zero_expr() == *this;
+  }
+  else if(type_id == ID_real)
+  {
+    return real_typet{}.zero_expr() == *this;
+  }
+  else if(type_id == ID_rational)
+  {
+    rationalt rat_value;
+    if(to_rational(*this, rat_value))
+      CHECK_RETURN(false);
+    return rat_value.is_zero();
+  }
+  else if(
+    type_id == ID_unsignedbv || type_id == ID_signedbv ||
+    type_id == ID_c_bool || type_id == ID_c_bit_field)
+  {
+    return value_is_zero_string();
+  }
+  else if(type_id == ID_fixedbv)
+  {
+    return fixedbvt(*this).is_zero();
+  }
+  else if(type_id == ID_floatbv)
+  {
+    return ieee_floatt(*this).is_zero();
+  }
+  else if(type_id == ID_pointer)
+  {
+    return is_null_pointer();
+  }
+  else
+    return false;
+}
+
+bool constant_exprt::is_one() const
+{
+  const irep_idt &type_id = type().id();
+
+  if(type_id == ID_integer)
+  {
+    return integer_typet{}.one_expr() == *this;
+  }
+  else if(type_id == ID_natural)
+  {
+    return natural_typet{}.one_expr() == *this;
+  }
+  else if(type_id == ID_real)
+  {
+    return real_typet{}.one_expr() == *this;
+  }
+  else if(type_id == ID_rational)
+  {
+    rationalt rat_value;
+    if(to_rational(*this, rat_value))
+      CHECK_RETURN(false);
+    return rat_value.is_one();
+  }
+  else if(
+    type_id == ID_unsignedbv || type_id == ID_signedbv ||
+    type_id == ID_c_bool || type_id == ID_c_bit_field)
+  {
+    const auto width = to_bitvector_type(type()).get_width();
+    mp_integer int_value = bvrep2integer(id2string(get_value()), width, false);
+    return int_value == 1;
+  }
+  else if(type_id == ID_fixedbv)
+  {
+    fixedbv_spect spec{to_fixedbv_type(type())};
+    fixedbvt one{spec};
+    one.from_integer(1);
+    return one == fixedbvt{*this};
+  }
+  else if(type_id == ID_floatbv)
+  {
+    ieee_floatt one{to_floatbv_type(type())};
+    one.from_integer(1);
+    return one == ieee_floatt{*this};
+  }
+  else
+    return false;
+}
+
+bool constant_exprt::is_null_pointer() const
+{
+  if(type().id() != ID_pointer)
+    return false;
+
+  if(get_value() == ID_NULL)
+    return true;
+
+    // We used to support "0" (when NULL_is_zero), but really front-ends should
+    // resolve this and generate ID_NULL instead.
+#if 0
+  return config.ansi_c.NULL_is_zero && value_is_zero_string();
+#else
+  INVARIANT(
+    !value_is_zero_string() || !config.ansi_c.NULL_is_zero,
+    "front-end should use ID_NULL");
+  return false;
+#endif
+}
+
 void constant_exprt::check(const exprt &expr, const validation_modet vm)
 {
   nullary_exprt::check(expr, vm);
@@ -63,12 +199,37 @@ exprt disjunction(const exprt::operandst &op)
   }
 }
 
+exprt conjunction(exprt a, exprt b)
+{
+  PRECONDITION(a.is_boolean() && b.is_boolean());
+  if(b.is_constant())
+  {
+    if(to_constant_expr(b).is_false())
+      return false_exprt{};
+    return a;
+  }
+  if(a.is_constant())
+  {
+    if(to_constant_expr(a).is_false())
+      return false_exprt{};
+    return b;
+  }
+  if(b.id() == ID_and)
+  {
+    b.add_to_operands(std::move(a));
+    return b;
+  }
+  return and_exprt{std::move(a), std::move(b)};
+}
+
 exprt conjunction(const exprt::operandst &op)
 {
   if(op.empty())
     return true_exprt();
   else if(op.size()==1)
     return op.front();
+  else if(op.size() == 2)
+    return conjunction(op[0], op[1]);
   else
   {
     return and_exprt(exprt::operandst(op));
@@ -174,6 +335,37 @@ void let_exprt::validate(const exprt &expr, const validation_modet vm)
   }
 }
 
+with_exprt update_exprt::make_with_expr() const
+{
+  const exprt::operandst &designators = designator();
+  PRECONDITION(!designators.empty());
+
+  with_exprt result{exprt{}, exprt{}, exprt{}};
+  exprt *dest = &result;
+
+  for(const auto &expr : designators)
+  {
+    with_exprt tmp{exprt{}, exprt{}, exprt{}};
+
+    if(expr.id() == ID_index_designator)
+    {
+      tmp.where() = to_index_designator(expr).index();
+    }
+    else if(expr.id() == ID_member_designator)
+    {
+      // irep_idt component_name=
+      //  to_member_designator(*it).get_component_name();
+    }
+    else
+      UNREACHABLE;
+
+    *dest = tmp;
+    dest = &to_with_expr(*dest).new_value();
+  }
+
+  return result;
+}
+
 exprt binding_exprt::instantiate(const operandst &values) const
 {
   // number of values must match the number of bound variables
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index 431de0bfa00..71006ee4050 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -2152,6 +2152,11 @@ class and_exprt:public multi_ary_exprt
 
 exprt conjunction(const exprt::operandst &);
 
+/// Conjunction of two expressions. If the second is already an `and_exprt`
+/// add to its operands instead of creating a new expression. If one is `true`,
+/// return the other expression. If one is `false` returns `false`.
+exprt conjunction(exprt a, exprt b);
+
 template <>
 inline bool can_cast_expr<and_exprt>(const exprt &base)
 {
@@ -2698,6 +2703,9 @@ class update_exprt : public ternary_exprt
     return op2();
   }
 
+  /// converts an update expr into a (possibly nested) with expression
+  with_exprt make_with_expr() const;
+
   static void check(
     const exprt &expr,
     const validation_modet vm = validation_modet::INVARIANT)
@@ -2992,6 +3000,9 @@ class constant_exprt : public nullary_exprt
     set_value(_value);
   }
 
+  /// returns true_exprt if given true and false_exprt otherwise
+  explicit constant_exprt(bool);
+
   const irep_idt &get_value() const
   {
     return get(ID_value);
@@ -3002,7 +3013,36 @@ class constant_exprt : public nullary_exprt
     set(ID_value, value);
   }
 
-  bool value_is_zero_string() const;
+  /// Return whether the expression is a constant representing `true`.
+  /// \return True if is a Boolean value representing `true`, false otherwise.
+  bool is_true() const;
+
+  /// Return whether the expression is a constant representing `false`.
+  /// \return True if is a Boolean constant representing `false`, false otherwise.
+  bool is_false() const;
+
+  /// Return whether the expression is a constant representing 0.
+  /// Will consider the following types: ID_integer, ID_natural, ID_rational,
+  /// ID_unsignedbv, ID_signedbv, ID_c_bool, ID_c_bit_field, ID_fixedbv,
+  /// ID_floatbv, ID_pointer.<br>
+  /// For ID_pointer, returns true iff the value is a zero string or a null
+  /// pointer.
+  /// For everything not in the above list, return false.
+  /// \return True if has value 0, false otherwise.
+  bool is_zero() const;
+
+  /// Return whether the expression is a constant representing 1.
+  /// Will consider the following types: ID_integer, ID_natural, ID_rational,
+  /// ID_unsignedbv, ID_signedbv, ID_c_bool, ID_c_bit_field, ID_fixedbv,
+  /// ID_floatbv.<br>
+  /// For all other types, return false.
+  /// \return True if has value 1, false otherwise.
+  bool is_one() const;
+
+  /// Returns true if \p expr has a pointer type and a value NULL; it also
+  /// returns true when \p expr has value zero and NULL_is_zero is true; returns
+  /// false in all other cases.
+  bool is_null_pointer() const;
 
   static void check(
     const exprt &expr,
@@ -3015,6 +3055,9 @@ class constant_exprt : public nullary_exprt
   {
     check(expr, vm);
   }
+
+protected:
+  bool value_is_zero_string() const;
 };
 
 template <>
diff --git a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp
index dc21adae69e..de56f91a7a6 100644
--- a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp
+++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp
@@ -803,7 +803,8 @@ void ASSUME_TRUE(
     auto assumption = env.do_assume(expr, ns);
     REQUIRE(assumption.id() != ID_nil);
     REQUIRE(assumption.is_boolean());
-    REQUIRE(assumption.is_true());
+    REQUIRE(assumption.is_constant());
+    REQUIRE(to_constant_expr(assumption).is_true());
   }
 }
 
@@ -817,7 +818,8 @@ void ASSUME_FALSE(
     auto assumption = env.do_assume(expr, ns);
     REQUIRE(assumption.id() != ID_nil);
     REQUIRE(assumption.is_boolean());
-    REQUIRE(assumption.is_false());
+    REQUIRE(assumption.is_constant());
+    REQUIRE(to_constant_expr(assumption).is_false());
   }
 }
 
diff --git a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp
index afd79a0e43c..7762afdc748 100644
--- a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp
+++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp
@@ -34,7 +34,8 @@ static void ASSUME_TRUE(
 
   REQUIRE(assumption.id() != ID_nil);
   REQUIRE(assumption.is_boolean());
-  REQUIRE(assumption.is_true());
+  REQUIRE(assumption.is_constant());
+  REQUIRE(to_constant_expr(assumption).is_true());
 }
 
 static void EXPECT_RESULT(
diff --git a/unit/goto-symex/goto_symex_state.cpp b/unit/goto-symex/goto_symex_state.cpp
index 8e5d02395e6..7d76dd61fab 100644
--- a/unit/goto-symex/goto_symex_state.cpp
+++ b/unit/goto-symex/goto_symex_state.cpp
@@ -172,8 +172,7 @@ SCENARIO(
           const symbol_exprt object_symbol =
             to_symbol_expr(object_descriptor->object());
           REQUIRE(object_symbol.get_identifier() == "int_value!0");
-          REQUIRE(to_constant_expr(object_descriptor->offset())
-                    .value_is_zero_string());
+          REQUIRE(to_constant_expr(object_descriptor->offset()).is_zero());
         }
         THEN("The target equations are unchanged")
         {
diff --git a/unit/goto-symex/shadow_memory_util.cpp b/unit/goto-symex/shadow_memory_util.cpp
index 3fec5ef0c4c..e6700c46545 100644
--- a/unit/goto-symex/shadow_memory_util.cpp
+++ b/unit/goto-symex/shadow_memory_util.cpp
@@ -263,7 +263,7 @@ exprt simplify_bit_or_exprt(const exprt &expr)
     for(const auto &operand : or_expr->operands())
     {
       const exprt reduced = simplify_bit_or_exprt(operand);
-      res |= reduced.is_true();
+      res |= reduced.is_constant() && to_constant_expr(reduced).is_true();
     }
     return from_integer(res, bool_typet{});
   }
diff --git a/unit/util/expr.cpp b/unit/util/expr.cpp
index 462708fb3b0..dccae7f5d16 100644
--- a/unit/util/expr.cpp
+++ b/unit/util/expr.cpp
@@ -20,7 +20,7 @@ SCENARIO("bitfield-expr-is-zero", "[core][util][expr]")
 
     THEN("is_zero() should be false")
     {
-      REQUIRE_FALSE(bitfield3.is_zero());
+      REQUIRE_FALSE(to_constant_expr(bitfield3).is_zero());
     }
   }
   GIVEN("An exprt representing a bitfield constant of 0")
@@ -30,7 +30,7 @@ SCENARIO("bitfield-expr-is-zero", "[core][util][expr]")
 
     THEN("is_zero() should be true")
     {
-      REQUIRE(bitfield0.is_zero());
+      REQUIRE(to_constant_expr(bitfield0).is_zero());
     }
   }
 }
diff --git a/unit/util/interval/get_extreme.cpp b/unit/util/interval/get_extreme.cpp
index 63c15d3f5d0..0c79efd58d9 100644
--- a/unit/util/interval/get_extreme.cpp
+++ b/unit/util/interval/get_extreme.cpp
@@ -41,7 +41,8 @@ SCENARIO("get extreme exprt value", "[core][analyses][interval][get_extreme]")
 
       THEN("Require it is TRUE")
       {
-        REQUIRE(op1.is_true());
+        REQUIRE(op1.is_constant());
+        REQUIRE(to_constant_expr(op1).is_true());
         REQUIRE(interval_eval);
       }
     }
@@ -55,7 +56,8 @@ SCENARIO("get extreme exprt value", "[core][analyses][interval][get_extreme]")
 
       THEN("Require it is FALSE")
       {
-        REQUIRE(op1.is_false());
+        REQUIRE(op1.is_constant());
+        REQUIRE(to_constant_expr(op1).is_false());
         REQUIRE_FALSE(interval_eval);
       }
     }
@@ -70,7 +72,8 @@ SCENARIO("get extreme exprt value", "[core][analyses][interval][get_extreme]")
 
       THEN("Require it is TRUE")
       {
-        REQUIRE(op1.is_true());
+        REQUIRE(op1.is_constant());
+        REQUIRE(to_constant_expr(op1).is_true());
         REQUIRE(interval_eval);
         REQUIRE(constant_interval_exprt::equal(CEV(1), CEV(1)));
       }
diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp
index 18a4f4b88c5..6aee7d9128f 100644
--- a/unit/util/simplify_expr.cpp
+++ b/unit/util/simplify_expr.cpp
@@ -246,7 +246,8 @@ TEST_CASE("Simplify pointer_object equality", "[core][util]")
 
   exprt simp = simplify_expr(equal_exprt{p_o_void, p_o_int}, ns);
 
-  REQUIRE(simp.is_true());
+  REQUIRE(simp.is_constant());
+  REQUIRE(to_constant_expr(simp).is_true());
 }
 
 TEST_CASE("Simplify cast from bool", "[core][util]")