diff --git a/regression/cbmc/pointer-offset-02/main.c b/regression/cbmc/pointer-offset-02/main.c
new file mode 100644
index 00000000000..b0499278b79
--- /dev/null
+++ b/regression/cbmc/pointer-offset-02/main.c
@@ -0,0 +1,7 @@
+#include <stdlib.h>
+
+int main()
+{
+  int *p = malloc(sizeof(int));
+  __CPROVER_assert(__CPROVER_POINTER_OFFSET(p) == 0, "");
+}
diff --git a/regression/cbmc/pointer-offset-02/test.desc b/regression/cbmc/pointer-offset-02/test.desc
new file mode 100644
index 00000000000..1a951f0fee5
--- /dev/null
+++ b/regression/cbmc/pointer-offset-02/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--verbosity 8
+^Generated \d+ VCC\(s\), 0 remaining after simplification$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/goto-symex/Makefile b/src/goto-symex/Makefile
index c1d8e5b04ce..ec56bb5e12c 100644
--- a/src/goto-symex/Makefile
+++ b/src/goto-symex/Makefile
@@ -18,6 +18,7 @@ SRC = auto_objects.cpp \
       shadow_memory_util.cpp \
       show_program.cpp \
       show_vcc.cpp \
+      simplify_expr_with_value_set.cpp \
       slice.cpp \
       solver_hardness.cpp \
       ssa_step.cpp \
diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp
index 1b3cd036f5c..46427c0fd50 100644
--- a/src/goto-symex/field_sensitivity.cpp
+++ b/src/goto-symex/field_sensitivity.cpp
@@ -12,9 +12,9 @@ Author: Michael Tautschnig
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/pointer_offset_size.h>
-#include <util/simplify_expr.h>
 
 #include "goto_symex_state.h"
+#include "simplify_expr_with_value_set.h"
 #include "symex_target.h"
 
 #define ENABLE_ARRAY_FIELD_SENSITIVITY
@@ -51,14 +51,14 @@ exprt field_sensitivityt::apply(
     !write && expr.id() == ID_member &&
     to_member_expr(expr).struct_op().id() == ID_struct)
   {
-    return simplify_opt(std::move(expr), ns);
+    return simplify_opt(std::move(expr), state.value_set, ns);
   }
 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
   else if(
     !write && expr.id() == ID_index &&
     to_index_expr(expr).array().id() == ID_array)
   {
-    return simplify_opt(std::move(expr), ns);
+    return simplify_opt(std::move(expr), state.value_set, ns);
   }
 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
   else if(expr.id() == ID_member)
@@ -151,7 +151,10 @@ exprt field_sensitivityt::apply(
     // than only the full array
     index_exprt &index = to_index_expr(expr);
     if(should_simplify)
-      simplify(index.index(), ns);
+    {
+      simplify_expr_with_value_sett{state.value_set, language_mode, ns}
+        .simplify(index.index());
+    }
 
     if(
       is_ssa_expr(index.array()) && index.array().type().id() == ID_array &&
@@ -160,9 +163,12 @@ exprt field_sensitivityt::apply(
       // place the entire index expression, not just the array operand, in an
       // SSA expression
       ssa_exprt tmp = to_ssa_expr(index.array());
-      auto l2_index = state.rename(index.index(), ns);
+      auto l2_index = state.rename(index.index(), ns).get();
       if(should_simplify)
-        l2_index.simplify(ns);
+      {
+        simplify_expr_with_value_sett{state.value_set, language_mode, ns}
+          .simplify(l2_index);
+      }
       bool was_l2 = !tmp.get_level_2().empty();
       exprt l2_size =
         state.rename(to_array_type(index.array().type()).size(), ns).get();
@@ -181,14 +187,14 @@ exprt field_sensitivityt::apply(
         numeric_cast_v<mp_integer>(to_constant_expr(l2_size)) <=
           max_field_sensitivity_array_size)
       {
-        if(l2_index.get().is_constant())
+        if(l2_index.is_constant())
         {
           // place the entire index expression, not just the array operand,
           // in an SSA expression
           ssa_exprt ssa_array = to_ssa_expr(index.array());
           ssa_array.remove_level_2();
           index.array() = ssa_array.get_original_expr();
-          index.index() = l2_index.get();
+          index.index() = l2_index;
           tmp.set_expression(index);
           if(was_l2)
           {
@@ -393,7 +399,10 @@ void field_sensitivityt::field_assignments_rec(
       const exprt member_rhs = apply(
         ns,
         state,
-        simplify_opt(member_exprt{ssa_rhs, comp.get_name(), comp.type()}, ns),
+        simplify_opt(
+          member_exprt{ssa_rhs, comp.get_name(), comp.type()},
+          state.value_set,
+          ns),
         false);
 
       const exprt &member_lhs = *fs_it;
@@ -437,6 +446,7 @@ void field_sensitivityt::field_assignments_rec(
         simplify_opt(
           make_byte_extract(
             ssa_rhs, from_integer(0, c_index_type()), comp.type()),
+          state.value_set,
           ns),
         false);
 
@@ -476,7 +486,9 @@ void field_sensitivityt::field_assignments_rec(
         ns,
         state,
         simplify_opt(
-          index_exprt{ssa_rhs, from_integer(i, type->index_type())}, ns),
+          index_exprt{ssa_rhs, from_integer(i, type->index_type())},
+          state.value_set,
+          ns),
         false);
 
       const exprt &index_lhs = *fs_it;
@@ -558,10 +570,14 @@ bool field_sensitivityt::is_divisible(
   return false;
 }
 
-exprt field_sensitivityt::simplify_opt(exprt e, const namespacet &ns) const
+exprt field_sensitivityt::simplify_opt(
+  exprt e,
+  const value_sett &value_set,
+  const namespacet &ns) const
 {
   if(!should_simplify)
     return e;
 
-  return simplify_expr(std::move(e), ns);
+  simplify_expr_with_value_sett{value_set, language_mode, ns}.simplify(e);
+  return e;
 }
diff --git a/src/goto-symex/field_sensitivity.h b/src/goto-symex/field_sensitivity.h
index 5fa0fe79b8d..7ab159638a2 100644
--- a/src/goto-symex/field_sensitivity.h
+++ b/src/goto-symex/field_sensitivity.h
@@ -14,6 +14,7 @@ Author: Michael Tautschnig
 class namespacet;
 class goto_symex_statet;
 class symex_targett;
+class value_sett;
 
 class field_sensitive_ssa_exprt : public exprt
 {
@@ -119,9 +120,14 @@ class field_sensitivityt
   /// \param max_array_size: maximum size for which field sensitivity will be
   ///   applied to array cells
   /// \param should_simplify: simplify expressions
-  field_sensitivityt(std::size_t max_array_size, bool should_simplify)
+  /// \param language_mode: mode of the language that expressions belong to.
+  field_sensitivityt(
+    std::size_t max_array_size,
+    bool should_simplify,
+    const irep_idt &language_mode)
     : max_field_sensitivity_array_size(max_array_size),
-      should_simplify(should_simplify)
+      should_simplify(should_simplify),
+      language_mode(language_mode)
   {
   }
 
@@ -201,6 +207,7 @@ class field_sensitivityt
   const std::size_t max_field_sensitivity_array_size;
 
   const bool should_simplify;
+  const irep_idt &language_mode;
 
   void field_assignments_rec(
     const namespacet &ns,
@@ -210,7 +217,10 @@ class field_sensitivityt
     symex_targett &target,
     bool allow_pointer_unsoundness) const;
 
-  [[nodiscard]] exprt simplify_opt(exprt e, const namespacet &ns) const;
+  [[nodiscard]] exprt simplify_opt(
+    exprt e,
+    const value_sett &value_set,
+    const namespacet &ns) const;
 };
 
 #endif // CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp
index 375a681b83c..24d9e4dc33b 100644
--- a/src/goto-symex/goto_symex.cpp
+++ b/src/goto-symex/goto_symex.cpp
@@ -11,9 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_symex.h"
 
-#include "expr_skeleton.h"
-#include "symex_assign.h"
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/format_expr.h>
@@ -21,18 +18,23 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/mathematical_expr.h>
 #include <util/mathematical_types.h>
 #include <util/pointer_offset_size.h>
-#include <util/simplify_expr.h>
 #include <util/simplify_utils.h>
 #include <util/std_code.h>
 #include <util/string_expr.h>
 #include <util/string_utils.h>
 
+#include "expr_skeleton.h"
+#include "simplify_expr_with_value_set.h"
+#include "symex_assign.h"
+
 #include <climits>
 
-void goto_symext::do_simplify(exprt &expr)
+void goto_symext::do_simplify(exprt &expr, const value_sett &value_set)
 {
   if(symex_config.simplify_opt)
-    simplify(expr, ns);
+  {
+    simplify_expr_with_value_sett{value_set, language_mode, ns}.simplify(expr);
+  }
 }
 
 void goto_symext::symex_assign(
@@ -61,7 +63,7 @@ void goto_symext::symex_assign(
   // "byte_extract <type> from an_lvalue offset this_rvalue") can affect whether
   // we use field-sensitive symbols or not, so L2-rename them up front:
   lhs = state.l2_rename_rvalues(lhs, ns);
-  do_simplify(lhs);
+  do_simplify(lhs, state.value_set);
   lhs = state.field_sensitivity.apply(ns, state, std::move(lhs), true);
 
   if(rhs.id() == ID_side_effect)
@@ -104,7 +106,13 @@ void goto_symext::symex_assign(
       assignment_type = symex_targett::assignment_typet::HIDDEN;
 
     symex_assignt symex_assign{
-      shadow_memory, state, assignment_type, ns, symex_config, target};
+      shadow_memory,
+      state,
+      assignment_type,
+      ns,
+      symex_config,
+      language_mode,
+      target};
 
     // Try to constant propagate potential side effects of the assignment, when
     // simplification is turned on and there is one thread only. Constant
@@ -134,7 +142,13 @@ void goto_symext::symex_assign(
 
     exprt::operandst lhs_if_then_else_conditions;
     symex_assignt{
-      shadow_memory, state, assignment_type, ns, symex_config, target}
+      shadow_memory,
+      state,
+      assignment_type,
+      ns,
+      symex_config,
+      language_mode,
+      target}
       .assign_rec(lhs, expr_skeletont{}, rhs, lhs_if_then_else_conditions);
 
     if(need_atomic_section)
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index ae06ad54072..28518580aec 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -27,6 +27,7 @@ class shadow_memory_field_definitionst;
 class side_effect_exprt;
 class symex_assignt;
 class typet;
+class value_sett;
 
 /// \brief The main class for the forward symbolic simulator
 /// \remarks
@@ -528,7 +529,7 @@ class goto_symext
   /// \param state: Symbolic execution state for current instruction
   void symex_catch(statet &state);
 
-  virtual void do_simplify(exprt &expr);
+  virtual void do_simplify(exprt &expr, const value_sett &value_set);
 
   /// Symbolically execute an ASSIGN instruction or simulate such an execution
   /// for a synthetic assignment
@@ -876,20 +877,4 @@ void symex_transition(
   goto_programt::const_targett to,
   bool is_backwards_goto);
 
-/// Try to evaluate pointer comparisons where they can be trivially determined
-/// using the value-set. This is optional as all it does is allow symex to
-/// resolve some comparisons itself and therefore create a simpler formula for
-/// the SAT solver.
-/// \param [in,out] condition: An L2-renamed expression with boolean type
-/// \param value_set: The value-set for determining what pointer-typed symbols
-///   might possibly point to
-/// \param language_mode: The language mode
-/// \param ns: A namespace
-/// \return The possibly modified condition
-renamedt<exprt, L2> try_evaluate_pointer_comparisons(
-  renamedt<exprt, L2> condition,
-  const value_sett &value_set,
-  const irep_idt &language_mode,
-  const namespacet &ns);
-
 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index 9ac435c89a4..253b4be198e 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -24,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <pointer-analysis/add_failed_symbols.h>
 
 #include "goto_symex_can_forward_propagate.h"
+#include "simplify_expr_with_value_set.h"
 #include "symex_target_equation.h"
 
 static void get_l1_name(exprt &expr);
@@ -32,14 +33,19 @@ goto_symex_statet::goto_symex_statet(
   const symex_targett::sourcet &_source,
   std::size_t max_field_sensitive_array_size,
   bool should_simplify,
+  const irep_idt &language_mode,
   guard_managert &manager,
   std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider)
   : goto_statet(manager),
     source(_source),
     guard_manager(manager),
     symex_target(nullptr),
-    field_sensitivity(max_field_sensitive_array_size, should_simplify),
+    field_sensitivity(
+      max_field_sensitive_array_size,
+      should_simplify,
+      language_mode),
     record_events({true}),
+    language_mode(language_mode),
     fresh_l2_name_provider(fresh_l2_name_provider)
 {
   threads.emplace_back(guard_manager);
@@ -85,7 +91,7 @@ renamedt<ssa_exprt, L2> goto_symex_statet::assignment(
   // the type might need renaming
   rename<L2>(lhs.type(), l1_identifier, ns);
   if(rhs_is_simplified)
-    simplify(lhs, ns);
+    simplify_expr_with_value_sett{value_set, language_mode, ns}.simplify(lhs);
   lhs.update_type();
   if(run_validation_checks)
   {
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
index 939279b8ef2..96020d5970e 100644
--- a/src/goto-symex/goto_symex_state.h
+++ b/src/goto-symex/goto_symex_state.h
@@ -45,6 +45,7 @@ class goto_symex_statet final : public goto_statet
     const symex_targett::sourcet &,
     std::size_t max_field_sensitive_array_size,
     bool should_simplify,
+    const irep_idt &language_mode,
     guard_managert &manager,
     std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider);
   ~goto_symex_statet();
@@ -258,6 +259,7 @@ class goto_symex_statet final : public goto_statet
   }
 
 private:
+  const irep_idt &language_mode;
   std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider;
 
   /// \brief Dangerous, do not use
diff --git a/src/goto-symex/renamed.h b/src/goto-symex/renamed.h
index 71bf60403e9..651f134623b 100644
--- a/src/goto-symex/renamed.h
+++ b/src/goto-symex/renamed.h
@@ -11,8 +11,8 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #ifndef CPROVER_GOTO_SYMEX_RENAMED_H
 #define CPROVER_GOTO_SYMEX_RENAMED_H
 
-#include <util/expr_iterator.h>
-#include <util/simplify_expr.h>
+#include <util/simplify_expr_class.h>
+
 #include <util/std_expr.h>
 
 class ssa_exprt;
@@ -42,14 +42,11 @@ class renamedt : private underlyingt
     return static_cast<const underlyingt &>(*this);
   }
 
-  void simplify(const namespacet &ns)
+  void simplify(simplify_exprt &simplifier)
   {
-    (void)::simplify(value(), ns);
+    simplifier.simplify(value());
   }
 
-  using mutator_functiont =
-    std::function<std::optional<renamedt>(const renamedt &)>;
-
 private:
   underlyingt &value()
   {
@@ -62,49 +59,10 @@ class renamedt : private underlyingt
   friend struct symex_level2t;
   friend class goto_symex_statet;
 
-  template <levelt make_renamed_level>
-  friend renamedt<exprt, make_renamed_level>
-  make_renamed(constant_exprt constant);
-
-  template <levelt selectively_mutate_level>
-  friend void selectively_mutate(
-    renamedt<exprt, selectively_mutate_level> &renamed,
-    typename renamedt<exprt, selectively_mutate_level>::mutator_functiont
-      get_mutated_expr);
-
   /// Only the friend classes can create renamedt objects
   explicit renamedt(underlyingt value) : underlyingt(std::move(value))
   {
   }
 };
 
-template <levelt level>
-renamedt<exprt, level> make_renamed(constant_exprt constant)
-{
-  return renamedt<exprt, level>(std::move(constant));
-}
-
-/// This permits replacing subexpressions of the renamed value, so long as
-/// each replacement is consistent with our current renaming level (for
-/// example, replacing subexpressions of L2 expressions with ones which are
-/// themselves L2 renamed).
-/// The passed function will be called with each expression node in preorder
-/// (i.e. parent expressions before children), and should return an empty
-/// optional to make no change or a renamed expression to make a change.
-template <levelt level>
-void selectively_mutate(
-  renamedt<exprt, level> &renamed,
-  typename renamedt<exprt, level>::mutator_functiont get_mutated_expr)
-{
-  for(auto it = renamed.depth_begin(), itend = renamed.depth_end(); it != itend;
-      ++it)
-  {
-    std::optional<renamedt<exprt, level>> replacement =
-      get_mutated_expr(static_cast<const renamedt<exprt, level> &>(*it));
-
-    if(replacement)
-      it.mutate() = std::move(replacement->value());
-  }
-}
-
 #endif // CPROVER_GOTO_SYMEX_RENAMED_H
diff --git a/src/goto-symex/shadow_memory_util.cpp b/src/goto-symex/shadow_memory_util.cpp
index ebc6dde0867..f807a057116 100644
--- a/src/goto-symex/shadow_memory_util.cpp
+++ b/src/goto-symex/shadow_memory_util.cpp
@@ -20,6 +20,7 @@ Author: Peter Schrammel
 #include <util/invariant.h>
 #include <util/namespace.h>
 #include <util/pointer_offset_size.h>
+#include <util/simplify_expr.h>
 #include <util/ssa_expr.h>
 #include <util/std_expr.h>
 #include <util/string_constant.h>
diff --git a/src/goto-symex/simplify_expr_with_value_set.cpp b/src/goto-symex/simplify_expr_with_value_set.cpp
new file mode 100644
index 00000000000..c28ab650150
--- /dev/null
+++ b/src/goto-symex/simplify_expr_with_value_set.cpp
@@ -0,0 +1,283 @@
+/*******************************************************************\
+
+Module: Variant of simplify_exprt that uses a value_sett
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#include "simplify_expr_with_value_set.h"
+
+#include <util/expr_util.h>
+#include <util/pointer_expr.h>
+#include <util/simplify_expr.h>
+#include <util/ssa_expr.h>
+
+#include <pointer-analysis/add_failed_symbols.h>
+#include <pointer-analysis/value_set.h>
+#include <pointer-analysis/value_set_dereference.h>
+
+#include "goto_symex_can_forward_propagate.h"
+
+/// Try to evaluate a simple pointer comparison.
+/// \param operation: ID_equal or ID_not_equal
+/// \param symbol_expr: The symbol expression in the condition
+/// \param other_operand: The other expression in the condition; we only support
+///   an address of expression, a typecast of an address of expression or a
+///   null pointer, and return an empty std::optional in all other cases
+/// \param value_set: The value-set for looking up what the symbol can point to
+/// \param language_mode: The language mode
+/// \param ns: A namespace
+/// \return If we were able to evaluate the condition as true or false then we
+///   return that, otherwise we return an empty std::optional
+static std::optional<exprt> try_evaluate_pointer_comparison(
+  const irep_idt &operation,
+  const symbol_exprt &symbol_expr,
+  const exprt &other_operand,
+  const value_sett &value_set,
+  const irep_idt language_mode,
+  const namespacet &ns)
+{
+  const constant_exprt *constant_expr =
+    expr_try_dynamic_cast<constant_exprt>(other_operand);
+
+  if(
+    skip_typecast(other_operand).id() != ID_address_of &&
+    (!constant_expr || !constant_expr->is_null_pointer()))
+  {
+    return {};
+  }
+
+  const ssa_exprt *ssa_symbol_expr =
+    expr_try_dynamic_cast<ssa_exprt>(symbol_expr);
+
+  ssa_exprt l1_expr{*ssa_symbol_expr};
+  l1_expr.remove_level_2();
+  const std::vector<exprt> value_set_elements =
+    value_set.get_value_set(l1_expr, ns);
+
+  bool constant_found = false;
+
+  for(const auto &value_set_element : value_set_elements)
+  {
+    if(
+      value_set_element.id() == ID_unknown ||
+      value_set_element.id() == ID_invalid ||
+      is_failed_symbol(
+        to_object_descriptor_expr(value_set_element).root_object()) ||
+      to_object_descriptor_expr(value_set_element).offset().id() == ID_unknown)
+    {
+      // We can't conclude anything about the value-set
+      return {};
+    }
+
+    if(!constant_found)
+    {
+      if(value_set_dereferencet::should_ignore_value(
+           value_set_element, false, language_mode))
+      {
+        continue;
+      }
+
+      value_set_dereferencet::valuet value =
+        value_set_dereferencet::build_reference_to(
+          value_set_element, symbol_expr, ns);
+
+      // use the simplifier to test equality as we need to skip over typecasts
+      // and cannot rely on canonical representations, which would permit a
+      // simple syntactic equality test
+      exprt test_equal = simplify_expr(
+        equal_exprt{
+          typecast_exprt::conditional_cast(value.pointer, other_operand.type()),
+          other_operand},
+        ns);
+      if(test_equal.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())
+      {
+        // We can't conclude anything about the value-set
+        return {};
+      }
+    }
+  }
+
+  if(!constant_found)
+  {
+    // The symbol cannot possibly have the value \p other_operand because it
+    // isn't in the symbol's value-set
+    return operation == ID_equal ? static_cast<exprt>(false_exprt{})
+                                 : static_cast<exprt>(true_exprt{});
+  }
+  else if(value_set_elements.size() == 1)
+  {
+    // The symbol must have the value \p other_operand because it is the only
+    // thing in the symbol's value-set
+    return operation == ID_equal ? static_cast<exprt>(true_exprt{})
+                                 : static_cast<exprt>(false_exprt{});
+  }
+  else
+  {
+    return {};
+  }
+}
+
+simplify_exprt::resultt<> simplify_expr_with_value_sett::simplify_inequality(
+  const binary_relation_exprt &expr)
+{
+  if(expr.id() != ID_equal && expr.id() != ID_notequal)
+    return simplify_exprt::simplify_inequality(expr);
+
+  if(!can_cast_type<pointer_typet>(to_binary_expr(expr).op0().type()))
+    return simplify_exprt::simplify_inequality(expr);
+
+  exprt lhs = to_binary_expr(expr).op0(), rhs = to_binary_expr(expr).op1();
+  if(can_cast_expr<symbol_exprt>(rhs))
+    std::swap(lhs, rhs);
+
+  const symbol_exprt *symbol_expr_lhs =
+    expr_try_dynamic_cast<symbol_exprt>(lhs);
+
+  if(!symbol_expr_lhs)
+    return simplify_exprt::simplify_inequality(expr);
+
+  if(!goto_symex_can_forward_propagatet(ns)(rhs))
+    return simplify_exprt::simplify_inequality(expr);
+
+  auto maybe_constant = try_evaluate_pointer_comparison(
+    expr.id(), *symbol_expr_lhs, rhs, value_set, language_mode, ns);
+  if(maybe_constant.has_value())
+    return changed(*maybe_constant);
+  else
+    return unchanged(expr);
+}
+
+simplify_exprt::resultt<>
+simplify_expr_with_value_sett::simplify_inequality_pointer_object(
+  const binary_relation_exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
+  PRECONDITION(expr.is_boolean());
+
+  auto collect_objects = [this](const exprt &pointer)
+  {
+    std::set<exprt> objects;
+    if(auto address_of = expr_try_dynamic_cast<address_of_exprt>(pointer))
+    {
+      objects.insert(
+        object_descriptor_exprt::root_object(address_of->object()));
+    }
+    else if(auto ssa_expr = expr_try_dynamic_cast<ssa_exprt>(pointer))
+    {
+      ssa_exprt l1_expr{*ssa_expr};
+      l1_expr.remove_level_2();
+      const std::vector<exprt> value_set_elements =
+        value_set.get_value_set(l1_expr, ns);
+
+      for(const auto &value_set_element : value_set_elements)
+      {
+        if(
+          value_set_element.id() == ID_unknown ||
+          value_set_element.id() == ID_invalid ||
+          is_failed_symbol(
+            to_object_descriptor_expr(value_set_element).root_object()))
+        {
+          objects.clear();
+          break;
+        }
+
+        objects.insert(
+          to_object_descriptor_expr(value_set_element).root_object());
+      }
+    }
+    return objects;
+  };
+
+  auto lhs_objects =
+    collect_objects(to_pointer_object_expr(expr.lhs()).pointer());
+  auto rhs_objects =
+    collect_objects(to_pointer_object_expr(expr.rhs()).pointer());
+
+  if(lhs_objects.size() == 1 && lhs_objects == rhs_objects)
+  {
+    // there is exactly one pointed-to object on both left-hand and right-hand
+    // side, and that object is the same
+    return expr.id() == ID_equal ? changed(static_cast<exprt>(true_exprt{}))
+                                 : changed(static_cast<exprt>(false_exprt{}));
+  }
+
+  std::list<exprt> intersection;
+  std::set_intersection(
+    lhs_objects.begin(),
+    lhs_objects.end(),
+    rhs_objects.begin(),
+    rhs_objects.end(),
+    std::back_inserter(intersection));
+  if(!lhs_objects.empty() && !rhs_objects.empty() && intersection.empty())
+  {
+    // all pointed-to objects on the left-hand side are different from any of
+    // the pointed-to objects on the right-hand side
+    return expr.id() == ID_equal ? changed(static_cast<exprt>(false_exprt{}))
+                                 : changed(static_cast<exprt>(true_exprt{}));
+  }
+
+  return simplify_exprt::simplify_inequality_pointer_object(expr);
+}
+
+simplify_exprt::resultt<>
+simplify_expr_with_value_sett::simplify_pointer_offset(
+  const pointer_offset_exprt &expr)
+{
+  const exprt &ptr = expr.pointer();
+
+  if(ptr.type().id() != ID_pointer)
+    return unchanged(expr);
+
+  const ssa_exprt *ssa_symbol_expr = expr_try_dynamic_cast<ssa_exprt>(ptr);
+
+  if(!ssa_symbol_expr)
+    return simplify_exprt::simplify_pointer_offset(expr);
+
+  ssa_exprt l1_expr{*ssa_symbol_expr};
+  l1_expr.remove_level_2();
+  const std::vector<exprt> value_set_elements =
+    value_set.get_value_set(l1_expr, ns);
+
+  std::optional<exprt> offset;
+
+  for(const auto &value_set_element : value_set_elements)
+  {
+    if(
+      value_set_element.id() == ID_unknown ||
+      value_set_element.id() == ID_invalid ||
+      is_failed_symbol(
+        to_object_descriptor_expr(value_set_element).root_object()) ||
+      to_object_descriptor_expr(value_set_element).offset().id() == ID_unknown)
+    {
+      offset.reset();
+      break;
+    }
+
+    exprt this_offset = to_object_descriptor_expr(value_set_element).offset();
+    if(
+      this_offset.id() == ID_unknown ||
+      (offset.has_value() && this_offset != *offset))
+    {
+      offset.reset();
+      break;
+    }
+    else if(!offset.has_value())
+    {
+      offset = this_offset;
+    }
+  }
+
+  if(!offset.has_value())
+    return simplify_exprt::simplify_pointer_offset(expr);
+
+  return changed(
+    simplify_rec(typecast_exprt::conditional_cast(*offset, expr.type())));
+}
diff --git a/src/goto-symex/simplify_expr_with_value_set.h b/src/goto-symex/simplify_expr_with_value_set.h
new file mode 100644
index 00000000000..c610ea01bef
--- /dev/null
+++ b/src/goto-symex/simplify_expr_with_value_set.h
@@ -0,0 +1,39 @@
+/*******************************************************************\
+
+Module: Variant of simplify_exprt that uses a value_sett
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_SYMEX_SIMPLIFY_EXPR_WITH_VALUE_SET_H
+#define CPROVER_GOTO_SYMEX_SIMPLIFY_EXPR_WITH_VALUE_SET_H
+
+#include <util/simplify_expr_class.h>
+
+class value_sett;
+
+class simplify_expr_with_value_sett : public simplify_exprt
+{
+public:
+  simplify_expr_with_value_sett(
+    const value_sett &_vs,
+    const irep_idt &_mode,
+    const namespacet &_ns)
+    : simplify_exprt(_ns), value_set(_vs), language_mode(_mode)
+  {
+  }
+
+  [[nodiscard]] resultt<>
+  simplify_inequality(const binary_relation_exprt &) override;
+  [[nodiscard]] resultt<>
+  simplify_inequality_pointer_object(const binary_relation_exprt &) override;
+  [[nodiscard]] resultt<>
+  simplify_pointer_offset(const pointer_offset_exprt &) override;
+
+protected:
+  const value_sett &value_set;
+  const irep_idt language_mode;
+};
+
+#endif // CPROVER_GOTO_SYMEX_SIMPLIFY_EXPR_WITH_VALUE_SET_H
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index c829e4b1d8c..8846ae84b14 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "expr_skeleton.h"
 #include "goto_symex_state.h"
+#include "simplify_expr_with_value_set.h"
 #include "symex_config.h"
 
 // We can either use with_exprt or update_exprt when building expressions that
@@ -206,7 +207,10 @@ void symex_assignt::assign_non_struct_symbol(
   assignmentt assignment{lhs, full_lhs, l2_rhs};
 
   if(symex_config.simplify_opt)
-    assignment.rhs = simplify_expr(std::move(assignment.rhs), ns);
+  {
+    simplify_expr_with_value_sett{state.value_set, language_mode, ns}.simplify(
+      assignment.rhs);
+  }
 
   const ssa_exprt l2_lhs = state
                              .assignment(
diff --git a/src/goto-symex/symex_assign.h b/src/goto-symex/symex_assign.h
index 2d8fa1611a7..e6a282637d7 100644
--- a/src/goto-symex/symex_assign.h
+++ b/src/goto-symex/symex_assign.h
@@ -33,12 +33,14 @@ class symex_assignt
     symex_targett::assignment_typet assignment_type,
     const namespacet &ns,
     const symex_configt &symex_config,
+    const irep_idt &language_mode,
     symex_targett &target)
     : shadow_memory(shadow_memory),
       state(state),
       assignment_type(assignment_type),
       ns(ns),
       symex_config(symex_config),
+      language_mode(language_mode),
       target(target)
   {
   }
@@ -65,6 +67,7 @@ class symex_assignt
   symex_targett::assignment_typet assignment_type;
   const namespacet &ns;
   const symex_configt &symex_config;
+  const irep_idt &language_mode;
   symex_targett &target;
 
   void assign_from_struct(
diff --git a/src/goto-symex/symex_atomic_section.cpp b/src/goto-symex/symex_atomic_section.cpp
index c96807e463f..231c40303e7 100644
--- a/src/goto-symex/symex_atomic_section.cpp
+++ b/src/goto-symex/symex_atomic_section.cpp
@@ -58,7 +58,7 @@ void goto_symext::symex_atomic_end(statet &state)
         ++it)
       read_guard|=*it;
     exprt read_guard_expr=read_guard.as_expr();
-    do_simplify(read_guard_expr);
+    do_simplify(read_guard_expr, state.value_set);
 
     target.shared_read(
       read_guard_expr,
@@ -80,7 +80,7 @@ void goto_symext::symex_atomic_end(statet &state)
         ++it)
       write_guard|=*it;
     exprt write_guard_expr=write_guard.as_expr();
-    do_simplify(write_guard_expr);
+    do_simplify(write_guard_expr, state.value_set);
 
     target.shared_write(
       write_guard_expr,
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index 9d3797a7247..8b85640bb4d 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -9,8 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file
 /// Symbolic Execution of ANSI-C
 
-#include "goto_symex.h"
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/expr_initializer.h>
@@ -19,11 +17,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/invariant_utils.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
-#include <util/simplify_expr.h>
 #include <util/std_code.h>
 #include <util/string_constant.h>
 
+#include "goto_symex.h"
 #include "path_storage.h"
+#include "simplify_expr_with_value_set.h"
 
 inline static std::optional<typet> c_sizeof_type_rec(const exprt &expr)
 {
@@ -73,7 +72,8 @@ void goto_symext::symex_allocate(
   {
     // to allow constant propagation
     exprt tmp_size = state.rename(size, ns).get();
-    simplify(tmp_size, ns);
+    simplify_expr_with_value_sett{state.value_set, language_mode, ns}.simplify(
+      tmp_size);
 
     // special treatment for sizeof(T)*x
     {
@@ -167,7 +167,8 @@ void goto_symext::symex_allocate(
 
   // to allow constant propagation
   exprt zero_init = state.rename(to_binary_expr(code).op1(), ns).get();
-  simplify(zero_init, ns);
+  simplify_expr_with_value_sett{state.value_set, language_mode, ns}.simplify(
+    zero_init);
 
   INVARIANT(
     zero_init.is_constant(), "allocate expects constant as second argument");
@@ -292,7 +293,7 @@ void goto_symext::symex_va_start(
 
   array = clean_expr(std::move(array), state, false);
   array = state.rename(std::move(array), ns).get();
-  do_simplify(array);
+  do_simplify(array, state.value_set);
   symex_assign(state, va_array.symbol_expr(), std::move(array));
 
   exprt rhs = address_of_exprt{index_exprt{
@@ -332,10 +333,14 @@ static irep_idt get_string_argument_rec(const exprt &src)
   return irep_idt();
 }
 
-static irep_idt get_string_argument(const exprt &src, const namespacet &ns)
+static irep_idt get_string_argument(
+  const exprt &src,
+  const value_sett &value_set,
+  const irep_idt &language_mode,
+  const namespacet &ns)
 {
   exprt tmp=src;
-  simplify(tmp, ns);
+  simplify_expr_with_value_sett{value_set, language_mode, ns}.simplify(tmp);
   return get_string_argument_rec(tmp);
 }
 
@@ -373,7 +378,7 @@ void goto_symext::symex_printf(
   exprt tmp_rhs = rhs;
   clean_expr(tmp_rhs, state, false);
   tmp_rhs = state.rename(std::move(tmp_rhs), ns).get();
-  do_simplify(tmp_rhs);
+  do_simplify(tmp_rhs, state.value_set);
 
   const exprt::operandst &operands=tmp_rhs.operands();
   std::list<exprt> args;
@@ -410,14 +415,14 @@ void goto_symext::symex_printf(
         parameter = to_address_of_expr(parameter).object();
       clean_expr(parameter, state, false);
       parameter = state.rename(std::move(parameter), ns).get();
-      do_simplify(parameter);
+      do_simplify(parameter, state.value_set);
 
       args.push_back(std::move(parameter));
     }
   }
 
-  const irep_idt format_string=
-    get_string_argument(operands[0], ns);
+  const irep_idt format_string =
+    get_string_argument(operands[0], state.value_set, language_mode, ns);
 
   if(!format_string.empty())
     target.output_fmt(
@@ -438,11 +443,12 @@ void goto_symext::symex_input(
   for(std::size_t i=1; i<code.operands().size(); i++)
   {
     exprt l2_arg = state.rename(code.operands()[i], ns).get();
-    do_simplify(l2_arg);
+    do_simplify(l2_arg, state.value_set);
     args.emplace_back(std::move(l2_arg));
   }
 
-  const irep_idt input_id=get_string_argument(id_arg, ns);
+  const irep_idt input_id =
+    get_string_argument(id_arg, state.value_set, language_mode, ns);
 
   target.input(state.guard.as_expr(), state.source, input_id, args);
 }
@@ -460,11 +466,15 @@ void goto_symext::symex_output(
   {
     renamedt<exprt, L2> l2_arg = state.rename(code.operands()[i], ns);
     if(symex_config.simplify_opt)
-      l2_arg.simplify(ns);
+    {
+      simplify_expr_with_value_sett simp{state.value_set, language_mode, ns};
+      l2_arg.simplify(simp);
+    }
     args.emplace_back(l2_arg);
   }
 
-  const irep_idt output_id=get_string_argument(id_arg, ns);
+  const irep_idt output_id =
+    get_string_argument(id_arg, state.value_set, language_mode, ns);
 
   target.output(state.guard.as_expr(), state.source, output_id, args);
 }
diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp
index 5c1ff7134a9..7926a8a86be 100644
--- a/src/goto-symex/symex_clean_expr.cpp
+++ b/src/goto-symex/symex_clean_expr.cpp
@@ -9,36 +9,33 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file
 /// Symbolic Execution of ANSI-C
 
-#include "goto_symex.h"
-
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/expr_iterator.h>
 #include <util/pointer_offset_size.h>
-#include <util/simplify_expr.h>
+
+#include <pointer-analysis/value_set_dereference.h>
 
 #include "expr_skeleton.h"
+#include "goto_symex.h"
 #include "path_storage.h"
 #include "symex_assign.h"
 #include "symex_dereference_state.h"
 
-#include <pointer-analysis/value_set_dereference.h>
-
 /// Given an expression, find the root object and the offset into it.
 ///
 /// The extra complication to be considered here is that the expression may
 /// have any number of ternary expressions mixed with type casts.
-static void
-process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
+static void process_array_expr(exprt &expr, const namespacet &ns)
 {
   // This may change the type of the expression!
 
   if(expr.id()==ID_if)
   {
     if_exprt &if_expr=to_if_expr(expr);
-    process_array_expr(if_expr.true_case(), do_simplify, ns);
-    process_array_expr(if_expr.false_case(), do_simplify, ns);
+    process_array_expr(if_expr.true_case(), ns);
+    process_array_expr(if_expr.false_case(), ns);
 
     if(if_expr.true_case() != if_expr.false_case())
     {
@@ -57,7 +54,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
     // strip
     exprt tmp = to_address_of_expr(expr).object();
     expr.swap(tmp);
-    process_array_expr(expr, do_simplify, ns);
+    process_array_expr(expr, ns);
   }
   else if(
     is_ssa_expr(expr) && to_ssa_expr(expr).get_original_expr().id() == ID_index)
@@ -67,7 +64,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
     exprt tmp=index_expr.array();
     expr.swap(tmp);
 
-    process_array_expr(expr, do_simplify, ns);
+    process_array_expr(expr, ns);
   }
   else if(expr.id() != ID_symbol)
   {
@@ -88,8 +85,6 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
       {
         auto array_size = size_of_expr(expr.type(), ns);
         CHECK_RETURN(array_size.has_value());
-        if(do_simplify)
-          simplify(array_size.value(), ns);
         expr = make_byte_extract(
           expr,
           from_integer(0, c_index_type()),
@@ -116,8 +111,6 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
           subtraction, ID_ge, from_integer(0, subtraction.type())},
         subtraction,
         from_integer(0, subtraction.type())};
-      if(do_simplify)
-        simplify(new_size, ns);
 
       array_typet new_array_type(subtype, new_size);
 
@@ -141,7 +134,8 @@ void goto_symext::process_array_expr(statet &state, exprt &expr)
   expr = dereference.dereference(expr, symex_config.show_points_to_sets);
   lift_lets(state, expr);
 
-  ::process_array_expr(expr, symex_config.simplify_opt, ns);
+  ::process_array_expr(expr, ns);
+  do_simplify(expr, state.value_set);
 }
 
 /// Rewrite index/member expressions in byte_extract to offset
@@ -184,7 +178,7 @@ void goto_symext::lift_let(statet &state, const let_exprt &let_expr)
 {
   exprt let_value = clean_expr(let_expr.value(), state, false);
   let_value = state.rename(std::move(let_value), ns).get();
-  do_simplify(let_value);
+  do_simplify(let_value, state.value_set);
 
   exprt::operandst value_assignment_guard;
   symex_assignt{
@@ -193,6 +187,7 @@ void goto_symext::lift_let(statet &state, const let_exprt &let_expr)
     symex_targett::assignment_typet::HIDDEN,
     ns,
     symex_config,
+    language_mode,
     target}
     .assign_symbol(
       to_ssa_expr(state.rename<L1>(let_expr.symbol(), ns).get()),
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index 25a61e2f74e..835cb2e763e 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -101,7 +101,7 @@ exprt goto_symext::address_arithmetic(
     // recursive call
     result = address_arithmetic(be, state, keep_array);
 
-    do_simplify(result);
+    do_simplify(result, state.value_set);
   }
   else if(expr.id()==ID_dereference)
   {
@@ -158,7 +158,7 @@ exprt goto_symext::address_arithmetic(
 
       result = address_arithmetic(be, state, keep_array);
 
-      do_simplify(result);
+      do_simplify(result, state.value_set);
     }
     else
       result=address_of_exprt(result);
@@ -236,6 +236,7 @@ goto_symext::cache_dereference(exprt &dereference_result, statet &state)
     symex_targett::assignment_typet::STATE,
     ns,
     symex_config,
+    language_mode,
     target};
 
   assign.assign_symbol(
@@ -307,7 +308,7 @@ void goto_symext::dereference_rec(
 
     tmp1 = state.rename<L1_WITH_CONSTANT_PROPAGATION>(tmp1, ns).get();
 
-    do_simplify(tmp1);
+    do_simplify(tmp1, state.value_set);
 
     if(symex_config.run_validation_checks)
     {
@@ -514,7 +515,7 @@ void goto_symext::dereference(exprt &expr, statet &state, bool write)
   // when all we need is
   // s1 := s1 with (member := X) [and guard b]
   // s2 := s2 with (member := X) [and guard !b]
-  do_simplify(expr);
+  do_simplify(expr, state.value_set);
 
   if(symex_config.run_validation_checks)
   {
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index 6fdf9f4ff5e..db4bfa133bc 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -131,7 +131,13 @@ void goto_symext::parameter_assignments(
 
       exprt::operandst lhs_conditions;
       symex_assignt{
-        shadow_memory, state, assignment_type, ns, symex_config, target}
+        shadow_memory,
+        state,
+        assignment_type,
+        ns,
+        symex_config,
+        language_mode,
+        target}
         .assign_rec(lhs, expr_skeletont{}, rhs, lhs_conditions);
     }
 
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index b1a27b4b6ce..1745a8e445e 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -12,18 +12,15 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/exception_utils.h>
 #include <util/expr_util.h>
 #include <util/invariant.h>
-#include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 
 #include <langapi/language_util.h>
-#include <pointer-analysis/add_failed_symbols.h>
-#include <pointer-analysis/value_set_dereference.h>
 
 #include "goto_symex.h"
-#include "goto_symex_can_forward_propagate.h"
 #include "path_storage.h"
+#include "simplify_expr_with_value_set.h"
 
 #include <algorithm>
 
@@ -67,166 +64,6 @@ void goto_symext::apply_goto_condition(
   jump_not_taken_state.apply_condition(negated_new_guard, current_state, ns);
 }
 
-/// Try to evaluate a simple pointer comparison.
-/// \param operation: ID_equal or ID_not_equal
-/// \param symbol_expr: The symbol expression in the condition
-/// \param other_operand: The other expression in the condition; we only support
-///   an address of expression, a typecast of an address of expression or a
-///   null pointer, and return an empty std::optional in all other cases
-/// \param value_set: The value-set for looking up what the symbol can point to
-/// \param language_mode: The language mode
-/// \param ns: A namespace
-/// \return If we were able to evaluate the condition as true or false then we
-///   return that, otherwise we return an empty std::optional
-static std::optional<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
-  const irep_idt &operation,
-  const symbol_exprt &symbol_expr,
-  const exprt &other_operand,
-  const value_sett &value_set,
-  const irep_idt language_mode,
-  const namespacet &ns)
-{
-  const constant_exprt *constant_expr =
-    expr_try_dynamic_cast<constant_exprt>(other_operand);
-
-  if(
-    skip_typecast(other_operand).id() != ID_address_of &&
-    (!constant_expr || !constant_expr->is_null_pointer()))
-  {
-    return {};
-  }
-
-  const ssa_exprt *ssa_symbol_expr =
-    expr_try_dynamic_cast<ssa_exprt>(symbol_expr);
-
-  ssa_exprt l1_expr{*ssa_symbol_expr};
-  l1_expr.remove_level_2();
-  const std::vector<exprt> value_set_elements =
-    value_set.get_value_set(l1_expr, ns);
-
-  bool constant_found = false;
-
-  for(const auto &value_set_element : value_set_elements)
-  {
-    if(
-      value_set_element.id() == ID_unknown ||
-      value_set_element.id() == ID_invalid ||
-      is_failed_symbol(
-        to_object_descriptor_expr(value_set_element).root_object()) ||
-      to_object_descriptor_expr(value_set_element).offset().id() == ID_unknown)
-    {
-      // We can't conclude anything about the value-set
-      return {};
-    }
-
-    if(!constant_found)
-    {
-      if(value_set_dereferencet::should_ignore_value(
-           value_set_element, false, language_mode))
-      {
-        continue;
-      }
-
-      value_set_dereferencet::valuet value =
-        value_set_dereferencet::build_reference_to(
-          value_set_element, symbol_expr, ns);
-
-      // use the simplifier to test equality as we need to skip over typecasts
-      // and cannot rely on canonical representations, which would permit a
-      // simple syntactic equality test
-      exprt test_equal = simplify_expr(
-        equal_exprt{
-          typecast_exprt::conditional_cast(value.pointer, other_operand.type()),
-          other_operand},
-        ns);
-      if(test_equal.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())
-      {
-        // We can't conclude anything about the value-set
-        return {};
-      }
-    }
-  }
-
-  if(!constant_found)
-  {
-    // The symbol cannot possibly have the value \p other_operand because it
-    // isn't in the symbol's value-set
-    return operation == ID_equal ? make_renamed<L2>(false_exprt{})
-                                 : make_renamed<L2>(true_exprt{});
-  }
-  else if(value_set_elements.size() == 1)
-  {
-    // The symbol must have the value \p other_operand because it is the only
-    // thing in the symbol's value-set
-    return operation == ID_equal ? make_renamed<L2>(true_exprt{})
-                                 : make_renamed<L2>(false_exprt{});
-  }
-  else
-  {
-    return {};
-  }
-}
-
-/// Check if we have a simple pointer comparison, and if so try to evaluate it.
-/// \param renamed_expr: The L2-renamed expression to check
-/// \param value_set: The value-set for looking up what the symbol can point to
-/// \param language_mode: The language mode
-/// \param ns: A namespace
-/// \return If we were able to evaluate the condition as true or false then we
-///   return that, otherwise we return an empty std::optional
-static std::optional<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
-  const renamedt<exprt, L2> &renamed_expr,
-  const value_sett &value_set,
-  const irep_idt &language_mode,
-  const namespacet &ns)
-{
-  const exprt &expr = renamed_expr.get();
-
-  if(expr.id() != ID_equal && expr.id() != ID_notequal)
-    return {};
-
-  if(!can_cast_type<pointer_typet>(to_binary_expr(expr).op0().type()))
-    return {};
-
-  exprt lhs = to_binary_expr(expr).op0(), rhs = to_binary_expr(expr).op1();
-  if(can_cast_expr<symbol_exprt>(rhs))
-    std::swap(lhs, rhs);
-
-  const symbol_exprt *symbol_expr_lhs =
-    expr_try_dynamic_cast<symbol_exprt>(lhs);
-
-  if(!symbol_expr_lhs)
-    return {};
-
-  if(!goto_symex_can_forward_propagatet(ns)(rhs))
-    return {};
-
-  return try_evaluate_pointer_comparison(
-    expr.id(), *symbol_expr_lhs, rhs, value_set, language_mode, ns);
-}
-
-renamedt<exprt, L2> try_evaluate_pointer_comparisons(
-  renamedt<exprt, L2> condition,
-  const value_sett &value_set,
-  const irep_idt &language_mode,
-  const namespacet &ns)
-{
-  selectively_mutate(
-    condition,
-    [&value_set, &language_mode, &ns](const renamedt<exprt, L2> &expr) {
-      return try_evaluate_pointer_comparison(
-        expr, value_set, language_mode, ns);
-    });
-
-  return condition;
-}
-
 void goto_symext::symex_goto(statet &state)
 {
   PRECONDITION(state.reachable);
@@ -236,10 +73,11 @@ void goto_symext::symex_goto(statet &state)
   exprt new_guard = clean_expr(instruction.condition(), state, false);
 
   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);
+  {
+    simplify_expr_with_value_sett simp{state.value_set, language_mode, ns};
+    renamed_guard.simplify(simp);
+  }
   new_guard = renamed_guard.get();
 
   if(new_guard.is_false())
@@ -280,7 +118,7 @@ void goto_symext::symex_goto(statet &state)
       // generate assume(false) or a suitable negation if this
       // instruction is a conditional goto
       exprt negated_guard = boolean_negate(new_guard);
-      do_simplify(negated_guard);
+      do_simplify(negated_guard, state.value_set);
       log.statistics() << "replacing self-loop at "
                        << state.source.pc->source_location() << " by assume("
                        << from_expr(ns, state.source.function_id, negated_guard)
@@ -831,7 +669,11 @@ static void merge_names(
   {
     rhs = if_exprt(diff_guard.as_expr(), goto_state_rhs, dest_state_rhs);
     if(do_simplify)
+    {
+      // Do not value-set supported filtering here as neither dest_state nor
+      // goto_state necessarily have a comprehensive value set.
       simplify(rhs, ns);
+    }
   }
 
   dest_state.record_events.push(false);
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index de1e7f1f388..77e8884158c 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -157,7 +157,7 @@ void goto_symext::symex_assert(
   // First, push negations in and perhaps convert existential quantifiers into
   // universals:
   if(has_subexpr(condition, ID_exists) || has_subexpr(condition, ID_forall))
-    do_simplify(condition);
+    do_simplify(condition, state.value_set);
 
   // Second, L2-rename universal quantifiers:
   if(has_subexpr(condition, ID_forall))
@@ -167,7 +167,7 @@ void goto_symext::symex_assert(
   exprt l2_condition = state.rename(std::move(condition), ns).get();
 
   // now try simplifier on it
-  do_simplify(l2_condition);
+  do_simplify(l2_condition, state.value_set);
 
   std::string msg = id2string(instruction.source_location().get_comment());
   if(msg.empty())
@@ -200,7 +200,7 @@ void goto_symext::symex_assume(statet &state, const exprt &cond)
 {
   exprt simplified_cond = clean_expr(cond, state, false);
   simplified_cond = state.rename(std::move(simplified_cond), ns).get();
-  do_simplify(simplified_cond);
+  do_simplify(simplified_cond, state.value_set);
 
   // It would be better to call try_filter_value_sets after apply_condition,
   // but it is not currently possible. See the comment at the beginning of
@@ -418,6 +418,7 @@ std::unique_ptr<goto_symext::statet> goto_symext::initialize_entry_point_state(
     symex_targett::sourcet(entry_point_id, start_function->body),
     symex_config.max_field_sensitivity_array_size,
     symex_config.simplify_opt,
+    language_mode,
     guard_manager,
     [storage](const irep_idt &id) { return storage->get_unique_l2_index(id); });
 
@@ -847,13 +848,13 @@ void goto_symext::try_filter_value_sets(
     // without another round of constant propagation.
     // It would be sufficient to replace this call to do_simplify() with
     // something that just replaces `*&x` with `x` whenever it finds it.
-    do_simplify(modified_condition);
+    do_simplify(modified_condition, state.value_set);
 
     state.record_events.push(false);
     modified_condition = state.rename(std::move(modified_condition), ns).get();
     state.record_events.pop();
 
-    do_simplify(modified_condition);
+    do_simplify(modified_condition, state.value_set);
 
     if(jump_taken_value_set && modified_condition.is_false())
     {
diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp
index 188cb44b21f..c5e046356bf 100644
--- a/src/goto-symex/symex_other.cpp
+++ b/src/goto-symex/symex_other.cpp
@@ -151,14 +151,14 @@ void goto_symext::symex_other(
       {
         src_array = make_byte_extract(
           src_array, from_integer(0, c_index_type()), dest_array.type());
-        do_simplify(src_array);
+        do_simplify(src_array, state.value_set);
       }
       else
       {
         // ID_array_replace
         dest_array = make_byte_extract(
           dest_array, from_integer(0, c_index_type()), src_array.type());
-        do_simplify(dest_array);
+        do_simplify(dest_array, state.value_set);
       }
     }
 
@@ -197,7 +197,7 @@ void goto_symext::symex_other(
     {
       auto array_size = size_of_expr(array_expr.type(), ns);
       CHECK_RETURN(array_size.has_value());
-      do_simplify(array_size.value());
+      do_simplify(array_size.value(), state.value_set);
       array_expr = make_byte_extract(
         array_expr,
         from_integer(0, c_index_type()),
diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp
index 0681eb60413..a394209c413 100644
--- a/src/goto-symex/symex_start_thread.cpp
+++ b/src/goto-symex/symex_start_thread.cpp
@@ -99,6 +99,7 @@ void goto_symext::symex_start_thread(statet &state)
       symex_targett::assignment_typet::HIDDEN,
       ns,
       symex_config,
+      language_mode,
       target}
       .assign_symbol(lhs_l1, expr_skeletont{}, rhs, lhs_conditions);
     const exprt l2_lhs = state.rename(lhs_l1, ns).get();
@@ -150,6 +151,7 @@ void goto_symext::symex_start_thread(statet &state)
       symex_targett::assignment_typet::HIDDEN,
       ns,
       symex_config,
+      language_mode,
       target}
       .assign_symbol(lhs, expr_skeletont{}, rhs, lhs_conditions);
   }
diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp
index 5c4e91ebfc9..9214c70608e 100644
--- a/src/goto-synthesizer/cegis_verifier.cpp
+++ b/src/goto-synthesizer/cegis_verifier.cpp
@@ -13,9 +13,11 @@ Author: Qinheping Hu
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/expr_iterator.h>
 #include <util/options.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
+#include <util/simplify_expr.h>
 
 #include <goto-programs/pointer_arithmetic.h>
 #include <goto-programs/process_goto_program.h>
diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h
index 1a9a1fe2998..cef6fa22b09 100644
--- a/src/util/simplify_expr_class.h
+++ b/src/util/simplify_expr_class.h
@@ -174,7 +174,8 @@ class simplify_exprt
   [[nodiscard]] resultt<> simplify_bitnot(const bitnot_exprt &);
   [[nodiscard]] resultt<> simplify_not(const not_exprt &);
   [[nodiscard]] resultt<> simplify_boolean(const exprt &);
-  [[nodiscard]] resultt<> simplify_inequality(const binary_relation_exprt &);
+  [[nodiscard]] virtual resultt<>
+  simplify_inequality(const binary_relation_exprt &);
   [[nodiscard]] resultt<>
   simplify_ieee_float_relation(const binary_relation_exprt &);
   [[nodiscard]] resultt<> simplify_lambda(const lambda_exprt &);
@@ -201,7 +202,8 @@ class simplify_exprt
   [[nodiscard]] resultt<>
   simplify_dereference_preorder(const dereference_exprt &);
   [[nodiscard]] resultt<> simplify_address_of(const address_of_exprt &);
-  [[nodiscard]] resultt<> simplify_pointer_offset(const pointer_offset_exprt &);
+  [[nodiscard]] virtual resultt<>
+  simplify_pointer_offset(const pointer_offset_exprt &);
   [[nodiscard]] resultt<> simplify_bswap(const bswap_exprt &);
   [[nodiscard]] resultt<> simplify_isinf(const unary_exprt &);
   [[nodiscard]] resultt<> simplify_isnan(const unary_exprt &);
@@ -271,7 +273,7 @@ class simplify_exprt
   simplify_inequality_rhs_is_constant(const binary_relation_exprt &);
   [[nodiscard]] resultt<>
   simplify_inequality_address_of(const binary_relation_exprt &);
-  [[nodiscard]] resultt<>
+  [[nodiscard]] virtual resultt<>
   simplify_inequality_pointer_object(const binary_relation_exprt &);
 
   // main recursion
diff --git a/unit/goto-symex/apply_condition.cpp b/unit/goto-symex/apply_condition.cpp
index 9c22a88a024..d207762c0a4 100644
--- a/unit/goto-symex/apply_condition.cpp
+++ b/unit/goto-symex/apply_condition.cpp
@@ -46,6 +46,7 @@ SCENARIO(
     source,
     DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE,
     true,
+    irep_idt{},
     guard_manager,
     fresh_name};
 
diff --git a/unit/goto-symex/goto_symex_state.cpp b/unit/goto-symex/goto_symex_state.cpp
index 8e5d02395e6..999fadf374c 100644
--- a/unit/goto-symex/goto_symex_state.cpp
+++ b/unit/goto-symex/goto_symex_state.cpp
@@ -42,6 +42,7 @@ SCENARIO(
     source,
     DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE,
     true,
+    irep_idt{},
     manager,
     fresh_name};
 
diff --git a/unit/goto-symex/module_dependencies.txt b/unit/goto-symex/module_dependencies.txt
index c17c6602282..972d4e9fd5c 100644
--- a/unit/goto-symex/module_dependencies.txt
+++ b/unit/goto-symex/module_dependencies.txt
@@ -1,4 +1,6 @@
 analyses
+goto-programs
 goto-symex
+pointer-analysis
 testing-utils
 util
diff --git a/unit/goto-symex/shadow_memory_util.cpp b/unit/goto-symex/shadow_memory_util.cpp
index 3fec5ef0c4c..8e9a8208967 100644
--- a/unit/goto-symex/shadow_memory_util.cpp
+++ b/unit/goto-symex/shadow_memory_util.cpp
@@ -6,6 +6,7 @@
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/pointer_expr.h>
+#include <util/simplify_expr.h>
 #include <util/string_constant.h>
 
 #include <goto-symex/shadow_memory_util.h>
diff --git a/unit/goto-symex/symex_assign.cpp b/unit/goto-symex/symex_assign.cpp
index 2338921f1c9..3464c3ba7c2 100644
--- a/unit/goto-symex/symex_assign.cpp
+++ b/unit/goto-symex/symex_assign.cpp
@@ -52,6 +52,7 @@ SCENARIO(
     source,
     DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE,
     true,
+    irep_idt{},
     manager,
     fresh_name};
 
@@ -89,6 +90,7 @@ SCENARIO(
         symex_targett::assignment_typet::STATE,
         ns,
         symex_config,
+        irep_idt{},
         target_equation}
         .assign_symbol(ssa_foo, expr_skeletont{}, rhs1, guard);
       THEN("An equation is added to the target")
@@ -145,6 +147,7 @@ SCENARIO(
         symex_targett::assignment_typet::STATE,
         ns,
         symex_config,
+        irep_idt{},
         target_equation};
       symex_assign.assign_symbol(ssa_foo, expr_skeletont{}, rhs1, guard);
       THEN("An equation with an empty guard is added to the target")
@@ -231,6 +234,7 @@ SCENARIO(
         symex_targett::assignment_typet::STATE,
         ns,
         symex_config,
+        irep_idt{},
         target_equation}
         .assign_symbol(struct1_ssa, skeleton, rhs, guard);
       THEN("Two equations are added to the target")
diff --git a/unit/goto-symex/try_evaluate_pointer_comparisons.cpp b/unit/goto-symex/try_evaluate_pointer_comparisons.cpp
index 1581e99e9de..b3ae467deba 100644
--- a/unit/goto-symex/try_evaluate_pointer_comparisons.cpp
+++ b/unit/goto-symex/try_evaluate_pointer_comparisons.cpp
@@ -8,8 +8,14 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 
 #include <util/c_types.h>
 #include <util/magic.h>
+#include <util/namespace.h>
+#include <util/symbol_table.h>
 
-#include <goto-symex/goto_symex.h>
+#include <goto-programs/goto_program.h>
+
+#include <goto-symex/goto_symex_state.h>
+#include <goto-symex/simplify_expr_with_value_set.h>
+#include <pointer-analysis/value_set.h>
 #include <testing-utils/use_catch.h>
 
 static void add_to_symbol_table(
@@ -56,6 +62,7 @@ SCENARIO(
     source,
     DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE,
     true,
+    ID_java,
     guard_manager,
     fresh_name};
 
@@ -70,13 +77,12 @@ SCENARIO(
     WHEN("Evaluating ptr1 == &value1")
     {
       const equal_exprt comparison{ptr1, address1};
-      const renamedt<exprt, L2> renamed_comparison =
-        state.rename(comparison, ns);
-      auto result = try_evaluate_pointer_comparisons(
-        renamed_comparison, value_set, ID_java, ns);
+      renamedt<exprt, L2> renamed_comparison = state.rename(comparison, ns);
+      simplify_expr_with_value_sett simp{value_set, ID_java, ns};
+      renamed_comparison.simplify(simp);
       THEN("Evaluation succeeds")
       {
-        REQUIRE(result.get() == true_exprt{});
+        REQUIRE(renamed_comparison.get() == true_exprt{});
       }
     }
 
@@ -88,39 +94,36 @@ SCENARIO(
       const equal_exprt comparison{
         ptr1,
         typecast_exprt{typecast_exprt{address1, ptr_short_type}, ptr_type}};
-      const renamedt<exprt, L2> renamed_comparison =
-        state.rename(comparison, ns);
-      auto result = try_evaluate_pointer_comparisons(
-        renamed_comparison, value_set, ID_java, ns);
+      renamedt<exprt, L2> renamed_comparison = state.rename(comparison, ns);
+      simplify_expr_with_value_sett simp{value_set, ID_java, ns};
+      renamed_comparison.simplify(simp);
       THEN("Evaluation succeeds")
       {
-        REQUIRE(result.get() == true_exprt{});
+        REQUIRE(renamed_comparison.get() == true_exprt{});
       }
     }
 
     WHEN("Evaluating ptr1 != &value1")
     {
       const notequal_exprt comparison{ptr1, address1};
-      const renamedt<exprt, L2> renamed_comparison =
-        state.rename(comparison, ns);
-      auto result = try_evaluate_pointer_comparisons(
-        renamed_comparison, value_set, ID_java, ns);
+      renamedt<exprt, L2> renamed_comparison = state.rename(comparison, ns);
+      simplify_expr_with_value_sett simp{value_set, ID_java, ns};
+      renamed_comparison.simplify(simp);
       THEN("Evaluation succeeds")
       {
-        REQUIRE(result.get() == false_exprt{});
+        REQUIRE(renamed_comparison.get() == false_exprt{});
       }
     }
 
     WHEN("Evaluating ptr1 == ptr2")
     {
       const equal_exprt comparison{ptr1, ptr2};
-      const renamedt<exprt, L2> renamed_comparison =
-        state.rename(comparison, ns);
-      auto result = try_evaluate_pointer_comparisons(
-        renamed_comparison, value_set, ID_java, ns);
+      renamedt<exprt, L2> renamed_comparison = state.rename(comparison, ns);
+      simplify_expr_with_value_sett simp{value_set, ID_java, ns};
+      renamed_comparison.simplify(simp);
       THEN("Evaluation leaves the expression unchanged")
       {
-        REQUIRE(result.get() == renamed_comparison.get());
+        REQUIRE(renamed_comparison.get() == renamed_comparison.get());
       }
     }
   }
@@ -139,39 +142,36 @@ SCENARIO(
     WHEN("Evaluating ptr1 == &value1")
     {
       const equal_exprt comparison{ptr1, address1};
-      const renamedt<exprt, L2> renamed_comparison =
-        state.rename(comparison, ns);
-      auto result = try_evaluate_pointer_comparisons(
-        renamed_comparison, value_set, ID_java, ns);
+      renamedt<exprt, L2> renamed_comparison = state.rename(comparison, ns);
+      simplify_expr_with_value_sett simp{value_set, ID_java, ns};
+      renamed_comparison.simplify(simp);
       THEN("Evaluation leaves the expression unchanged")
       {
-        REQUIRE(result.get() == renamed_comparison.get());
+        REQUIRE(renamed_comparison.get() == renamed_comparison.get());
       }
     }
 
     WHEN("Evaluating ptr1 != &value1")
     {
       const notequal_exprt comparison{ptr1, address1};
-      const renamedt<exprt, L2> renamed_comparison =
-        state.rename(comparison, ns);
-      auto result = try_evaluate_pointer_comparisons(
-        renamed_comparison, value_set, ID_java, ns);
+      renamedt<exprt, L2> renamed_comparison = state.rename(comparison, ns);
+      simplify_expr_with_value_sett simp{value_set, ID_java, ns};
+      renamed_comparison.simplify(simp);
       THEN("Evaluation leaves the expression unchanged")
       {
-        REQUIRE(result.get() == renamed_comparison.get());
+        REQUIRE(renamed_comparison.get() == renamed_comparison.get());
       }
     }
 
     WHEN("Evaluating ptr1 != nullptr")
     {
       const notequal_exprt comparison{ptr1, null_ptr};
-      const renamedt<exprt, L2> renamed_comparison =
-        state.rename(comparison, ns);
-      auto result = try_evaluate_pointer_comparisons(
-        renamed_comparison, value_set, ID_java, ns);
+      renamedt<exprt, L2> renamed_comparison = state.rename(comparison, ns);
+      simplify_expr_with_value_sett simp{value_set, ID_java, ns};
+      renamed_comparison.simplify(simp);
       THEN("Evaluation succeeds")
       {
-        REQUIRE(result.get() == true_exprt{});
+        REQUIRE(renamed_comparison.get() == true_exprt{});
       }
     }
   }
@@ -191,39 +191,36 @@ SCENARIO(
     WHEN("Evaluating ptr1 == &value1")
     {
       const equal_exprt comparison{ptr1, address1};
-      const renamedt<exprt, L2> renamed_comparison =
-        state.rename(comparison, ns);
-      auto result = try_evaluate_pointer_comparisons(
-        renamed_comparison, value_set, ID_java, ns);
+      renamedt<exprt, L2> renamed_comparison = state.rename(comparison, ns);
+      simplify_expr_with_value_sett simp{value_set, ID_java, ns};
+      renamed_comparison.simplify(simp);
       THEN("Evaluation leaves the expression unchanged")
       {
-        REQUIRE(result.get() == renamed_comparison.get());
+        REQUIRE(renamed_comparison.get() == renamed_comparison.get());
       }
     }
 
     WHEN("Evaluating ptr1 != &value1")
     {
       const notequal_exprt comparison{ptr1, address1};
-      const renamedt<exprt, L2> renamed_comparison =
-        state.rename(comparison, ns);
-      auto result = try_evaluate_pointer_comparisons(
-        renamed_comparison, value_set, ID_java, ns);
+      renamedt<exprt, L2> renamed_comparison = state.rename(comparison, ns);
+      simplify_expr_with_value_sett simp{value_set, ID_java, ns};
+      renamed_comparison.simplify(simp);
       THEN("Evaluation leaves the expression unchanged")
       {
-        REQUIRE(result.get() == renamed_comparison.get());
+        REQUIRE(renamed_comparison.get() == renamed_comparison.get());
       }
     }
 
     WHEN("Evaluating ptr1 != nullptr")
     {
       const notequal_exprt comparison{ptr1, null_ptr};
-      const renamedt<exprt, L2> renamed_comparison =
-        state.rename(comparison, ns);
-      auto result = try_evaluate_pointer_comparisons(
-        renamed_comparison, value_set, ID_java, ns);
+      renamedt<exprt, L2> renamed_comparison = state.rename(comparison, ns);
+      simplify_expr_with_value_sett simp{value_set, ID_java, ns};
+      renamed_comparison.simplify(simp);
       THEN("Evaluation leaves the expression unchanged")
       {
-        REQUIRE(result.get() == renamed_comparison.get());
+        REQUIRE(renamed_comparison.get() == renamed_comparison.get());
       }
     }
   }
@@ -247,7 +244,7 @@ SCENARIO(
     // struct_symbol..pointer_field <- &value1
     {
       field_sensitivityt field_sensitivity{
-        DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE, true};
+        DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE, true, ID_java};
       const exprt index_fs =
         field_sensitivity.apply(ns, state, member_l1.get(), true);
       value_set.assign(index_fs, address1_l1.get(), ns, false, false);
@@ -256,26 +253,24 @@ SCENARIO(
     WHEN("Evaluating struct_symbol.pointer_field == &value1")
     {
       const equal_exprt comparison{member, address1};
-      const renamedt<exprt, L2> renamed_comparison =
-        state.rename(comparison, ns);
-      auto result = try_evaluate_pointer_comparisons(
-        renamed_comparison, value_set, ID_java, ns);
+      renamedt<exprt, L2> renamed_comparison = state.rename(comparison, ns);
+      simplify_expr_with_value_sett simp{value_set, ID_java, ns};
+      renamed_comparison.simplify(simp);
       THEN("Evaluation succeeds")
       {
-        REQUIRE(result.get() == true_exprt{});
+        REQUIRE(renamed_comparison.get() == true_exprt{});
       }
     }
 
     WHEN("Evaluating struct_symbol.pointer_field == &value2")
     {
       const equal_exprt comparison{member, address2};
-      const renamedt<exprt, L2> renamed_comparison =
-        state.rename(comparison, ns);
-      auto result = try_evaluate_pointer_comparisons(
-        renamed_comparison, value_set, ID_java, ns);
+      renamedt<exprt, L2> renamed_comparison = state.rename(comparison, ns);
+      simplify_expr_with_value_sett simp{value_set, ID_java, ns};
+      renamed_comparison.simplify(simp);
       THEN("Evaluation succeeds")
       {
-        REQUIRE(result.get() == false_exprt{});
+        REQUIRE(renamed_comparison.get() == false_exprt{});
       }
     }
   }