diff --git a/jbmc/regression/jbmc/exception-cleanup/test.desc b/jbmc/regression/jbmc/exception-cleanup/test.desc
index a3787221ff2..a3a271c9941 100644
--- a/jbmc/regression/jbmc/exception-cleanup/test.desc
+++ b/jbmc/regression/jbmc/exception-cleanup/test.desc
@@ -4,8 +4,11 @@ Test.class
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-0 remaining after simplification$
+1 remaining after simplification$
 --
 ^warning: ignoring
 --
-The function "unreachable" should be successfully noted as unreachable by symex.
+The function "unreachable" should be successfully noted as unreachable by symex,
+but the final uncaught-exception test in __CPROVER__start is not yet decidable
+in symex, as it requires symex to note that within a catch block
+@inflight_exception is definitely *not* null, which it can't just yet.
diff --git a/jbmc/regression/jbmc/exception-cleanup/vccs.desc b/jbmc/regression/jbmc/exception-cleanup/vccs.desc
index 83b698bdd53..4dd86b143ae 100644
--- a/jbmc/regression/jbmc/exception-cleanup/vccs.desc
+++ b/jbmc/regression/jbmc/exception-cleanup/vccs.desc
@@ -3,6 +3,8 @@ Test.class
 --function Test.main --show-vcc
 ^EXIT=0$
 ^SIGNAL=0$
+file Test\.java line 6 function java::Test.main:\(I\)V
+no uncaught exception
 --
 file Test\.java line 42 function java::Test\.unreachable:\(\)V bytecode-index 5
 assertion at file Test\.java line 42 function java::Test\.unreachable:\(\)V bytecode-index 5
diff --git a/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.c b/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.c
deleted file mode 100644
index 40219aa82f8..00000000000
--- a/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.c
+++ /dev/null
@@ -1,181 +0,0 @@
-#include <assert.h>
-
-static void noop()
-{
-}
-
-int test(int nondet_int_array[])
-{
-  int a = 1, b = 2, c = 3;
-  int *ptr_to_a = &a, *ptr_to_b = &b, *ptr_to_c = &c, *ptr_to_null = 0;
-
-  // Symex knows the value of ptr_to_a, ptr_to_b, ptr_to_c and ptr_to_null, so
-  // it should be able to evaluate simple conditions involving them.
-
-  // Equality "=="
-
-  // A non-null pointer and a matching value
-  int unconditionally_reachable_1;
-  if(ptr_to_a == &a)
-    unconditionally_reachable_1 = 7;
-
-  // A non-null pointer and a non-matching value (not a null pointer)
-  int unreachable_1;
-  if(ptr_to_a == &c)
-    unreachable_1 = 7;
-
-  // A non-null pointer and a non-matching value (a null pointer)
-  int unreachable_2;
-  if(ptr_to_a == 0)
-    unreachable_2 = 7;
-
-  // A null pointer and a matching value
-  int unconditionally_reachable_2;
-  if(ptr_to_null == 0)
-    unconditionally_reachable_2 = 7;
-
-  // A null pointer and a non-matching value
-  int unreachable_3;
-  if(ptr_to_null == &a)
-    unreachable_3 = 7;
-
-  // Disequality "!="
-
-  // A non-null pointer and a matching value
-  int unreachable_4;
-  if(ptr_to_a != &a)
-    unreachable_4 = 7;
-
-  // A non-null pointer and a non-matching value (not a null pointer)
-  int unconditionally_reachable_3;
-  if(ptr_to_a != &c)
-    unconditionally_reachable_3 = 7;
-
-  // A non-null pointer and a non-matching value (a null pointer)
-  int unconditionally_reachable_4;
-  if(ptr_to_a != 0)
-    unconditionally_reachable_4 = 7;
-
-  // A null pointer and a matching value
-  int unreachable_5;
-  if(ptr_to_null != 0)
-    unreachable_5 = 7;
-
-  // A null pointer and a non-matching value
-  int unconditionally_reachable_5;
-  if(ptr_to_null != &a)
-    unconditionally_reachable_5 = 7;
-
-  // Symex can't tell what ptr_to_a_or_b points to, but we can tell that it
-  // doesn't point to some things
-  int *ptr_to_a_or_b = nondet_int_array[0] == 0 ? &a : &b;
-  int *ptr_to_a_or_b_or_null =
-    nondet_int_array[1] == 0 ? &a : nondet_int_array[1] == 1 ? &b : 0;
-
-  // Equality "=="
-
-  // A non-null pointer and a matching value
-  int possibly_reachable_1;
-  if(ptr_to_a_or_b == &a)
-    possibly_reachable_1 = 7;
-
-  // A non-null pointer and a non-matching value (not a null pointer)
-  int unreachable_6;
-  if(ptr_to_a_or_b == &c)
-    unreachable_6 = 7;
-
-  // A non-null pointer and a non-matching value (a null pointer)
-  int unreachable_7;
-  if(ptr_to_a_or_b == 0)
-    unreachable_7 = 7;
-
-  // A possibly-null pointer and a matching value (not a null pointer)
-  int possibly_reachable_2;
-  if(ptr_to_a_or_b_or_null == &a)
-    possibly_reachable_2 = 7;
-
-  // A possibly-null pointer and a matching value (a null pointer)
-  int possibly_reachable_3;
-  if(ptr_to_a_or_b_or_null == 0)
-    possibly_reachable_3 = 7;
-
-  // A possibly-null pointer and a non-matching value
-  int unreachable_8;
-  if(ptr_to_a_or_b_or_null == &c)
-    unreachable_8 = 7;
-
-  // Disequality "!="
-
-  // A non-null pointer and a matching value
-  int possibly_reachable_4;
-  if(ptr_to_a_or_b != &a)
-    possibly_reachable_4 = 7;
-
-  // A non-null pointer and a non-matching value (not a null pointer)
-  int unconditionally_reachable_6;
-  if(ptr_to_a_or_b != &c)
-    unconditionally_reachable_6 = 7;
-
-  // A non-null pointer and a non-matching value (a null pointer)
-  int unconditionally_reachable_7;
-  if(ptr_to_a_or_b != 0)
-    unconditionally_reachable_7 = 7;
-
-  // A possibly-null pointer and a matching value (not a null pointer)
-  int possibly_reachable_5;
-  if(ptr_to_a_or_b_or_null != &a)
-    possibly_reachable_5 = 7;
-
-  // A possibly-null pointer and a matching value (a null pointer)
-  int possibly_reachable_6;
-  if(ptr_to_a_or_b_or_null != 0)
-    possibly_reachable_6 = 7;
-
-  // A possibly-null pointer and a non-matching value
-  int unconditionally_reachable_8;
-  if(ptr_to_a_or_b_or_null != &c)
-    unconditionally_reachable_8 = 7;
-
-  // We should also be able to do all of the above in compound expressions which
-  // use logical operators like AND, OR and NOT, or even ternary expressions.
-
-  int unconditionally_reachable_9;
-  if(!(ptr_to_a == &c) && ptr_to_a_or_b != 0)
-    unconditionally_reachable_9 = 7;
-
-  int unreachable_9;
-  if(!(ptr_to_null == 0) || ptr_to_a_or_b == 0)
-    unreachable_9 = 7;
-
-  int unconditionally_reachable_10;
-  if((ptr_to_a == &a && !(ptr_to_a_or_b == 0)) || ptr_to_a_or_b_or_null == &c)
-    unconditionally_reachable_10 = 7;
-
-  int unreachable_10;
-  if(ptr_to_a_or_b_or_null != 0 ? ptr_to_null != 0 : ptr_to_a_or_b == &c)
-    unreachable_10 = 7;
-
-  // And everything should work with the symbol on the left or the right
-
-  int unconditionally_reachable_11;
-  if(!(&c == ptr_to_a) && 0 != ptr_to_a_or_b)
-    unconditionally_reachable_11 = 7;
-
-  int unreachable_11;
-  if(!(0 == ptr_to_null) || 0 == ptr_to_a_or_b)
-    unreachable_11 = 7;
-
-  int unconditionally_reachable_12;
-  if((&a == ptr_to_a && !(0 == ptr_to_a_or_b)) || &c == ptr_to_a_or_b_or_null)
-    unconditionally_reachable_12 = 7;
-
-  int unreachable_12;
-  if(0 != ptr_to_a_or_b_or_null ? 0 != ptr_to_null : &c == ptr_to_a_or_b)
-    unreachable_12 = 7;
-
-  int possibly_reachable_7;
-  if(0 != ptr_to_a_or_b_or_null)
-    possibly_reachable_7 = 7;
-
-  assert(0);
-}
diff --git a/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc b/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc
deleted file mode 100644
index d8f0a0e31c7..00000000000
--- a/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc
+++ /dev/null
@@ -1,60 +0,0 @@
-CORE paths-lifo-expected-failure
-test.c
---function test --show-vcc
-^EXIT=0$
-^SIGNAL=0$
-test::1::unconditionally_reachable_1[^\s]+ = 7$
-test::1::unconditionally_reachable_2[^\s]+ = 7$
-test::1::unconditionally_reachable_3[^\s]+ = 7$
-test::1::unconditionally_reachable_4[^\s]+ = 7$
-test::1::unconditionally_reachable_5[^\s]+ = 7$
-test::1::unconditionally_reachable_6[^\s]+ = 7$
-test::1::unconditionally_reachable_7[^\s]+ = 7$
-test::1::unconditionally_reachable_8[^\s]+ = 7$
-test::1::unconditionally_reachable_9[^\s]+ = 7$
-test::1::unconditionally_reachable_10[^\s]+ = 7$
-test::1::possibly_reachable_1[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_1[^\s]+\)$
-test::1::possibly_reachable_2[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_2[^\s]+\)$
-test::1::possibly_reachable_3[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_3[^\s]+\)$
-test::1::possibly_reachable_4[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_4[^\s]+\)$
-test::1::possibly_reachable_5[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_5[^\s]+\)$
-test::1::possibly_reachable_6[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_6[^\s]+\)$
-test::1::possibly_reachable_7[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_7[^\s]+\)$
---
-test::1::unconditionally_reachable_1[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_1[^\s]+\)$
-test::1::unconditionally_reachable_2[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_2[^\s]+\)$
-test::1::unconditionally_reachable_3[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_3[^\s]+\)$
-test::1::unconditionally_reachable_4[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_4[^\s]+\)$
-test::1::unconditionally_reachable_5[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_5[^\s]+\)$
-test::1::unconditionally_reachable_6[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_6[^\s]+\)$
-test::1::unconditionally_reachable_7[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_7[^\s]+\)$
-test::1::unconditionally_reachable_8[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_8[^\s]+\)$
-test::1::unconditionally_reachable_9[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_9[^\s]+\)$
-test::1::unconditionally_reachable_10[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_10[^\s]+\)$
-test::1::unconditionally_reachable_11[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_11[^\s]+\)$
-test::1::unconditionally_reachable_12[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_12[^\s]+\)$
-test::1::unreachable_1[^\s]+ = 7$
-test::1::unreachable_2[^\s]+ = 7$
-test::1::unreachable_3[^\s]+ = 7$
-test::1::unreachable_4[^\s]+ = 7$
-test::1::unreachable_5[^\s]+ = 7$
-test::1::unreachable_6[^\s]+ = 7$
-test::1::unreachable_7[^\s]+ = 7$
-test::1::unreachable_8[^\s]+ = 7$
-test::1::unreachable_9[^\s]+ = 7$
-test::1::unreachable_10[^\s]+ = 7$
-test::1::unreachable_11[^\s]+ = 7$
-test::1::unreachable_12[^\s]+ = 7$
-^warning: ignoring
-unreachable_1[3-9]
-unreachable[2-9][0-9]
-unconditionally_reachable_1[3-9]
-unconditionally_reachable[2-9][0-9]
-possibly_reachable_[8-9]
-possibly_reachable_[1-9][0-9]
---
-Pointer comparisons will be resolved in symex by a mixture of constant
-propagation and value-set filtering in try_evaluate_pointer_comparisons.
-
-The expected failure for path-symex is because the lines we check for
-possibly_reachable_* would only appear when there is convergence behaviour.
diff --git a/src/goto-symex/renaming_level.h b/src/goto-symex/renaming_level.h
index 5c9af1c513c..8096ca37cf0 100644
--- a/src/goto-symex/renaming_level.h
+++ b/src/goto-symex/renaming_level.h
@@ -15,9 +15,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #include <map>
 #include <unordered_set>
 
-#include <util/expr_iterator.h>
 #include <util/irep.h>
-#include <util/range.h>
 #include <util/sharing_map.h>
 #include <util/simplify_expr.h>
 #include <util/ssa_expr.h>
@@ -89,9 +87,6 @@ class renamedt : private underlyingt
     (void)::simplify(value(), ns);
   }
 
-  using mutator_functiont =
-    std::function<optionalt<renamedt>(const renamedt &)>;
-
 private:
   underlyingt &value()
   {
@@ -103,51 +98,12 @@ 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)
-  {
-    optionalt<renamedt<exprt, level>> replacement =
-      get_mutated_expr(static_cast<const renamedt<exprt, level> &>(*it));
-
-    if(replacement)
-      it.mutate() = std::move(replacement->value());
-  }
-}
-
 /// Functor to set the level 0 renaming of SSA expressions.
 /// Level 0 corresponds to threads.
 /// The renaming is built for one particular interleaving.
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index 30f19f0adf0..0fdfcbbe938 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com
 /// Symbolic Execution
 
 #include "goto_symex.h"
-#include "goto_symex_is_constant.h"
 
 #include <algorithm>
 
@@ -20,7 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/pointer_offset_size.h>
 #include <util/std_expr.h>
 
-#include <pointer-analysis/value_set_dereference.h>
 #include <util/simplify_expr.h>
 
 void goto_symext::apply_goto_condition(
@@ -67,161 +65,6 @@ void goto_symext::apply_goto_condition(
   }
 }
 
-/// 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 - must pass
-///   goto_symex_is_constant, and since it is pointer-typed it must therefore
-///   be an address of expression, a typecast of an address of expression or a
-///   null pointer
-/// \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 optionalt
-static optionalt<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);
-
-  INVARIANT(
-    skip_typecast(other_operand).id() == ID_address_of ||
-      (constant_expr && constant_expr->get_value() == ID_NULL),
-    "An expression that passes goto_symex_is_constant and has "
-    "pointer-type must be an address of expression (possibly with some "
-    "typecasts) or a null pointer");
-
-  const ssa_exprt *ssa_symbol_expr =
-    expr_try_dynamic_cast<ssa_exprt>(symbol_expr);
-
-  value_setst::valuest value_set_elements;
-  value_set.get_value_set(
-    ssa_symbol_expr->get_l1_object(), value_set_elements, 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)
-    {
-      // If ID_unknown or ID_invalid are in the value-set then we can't
-      // conclude anything about it
-      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);
-
-      if(value.pointer == other_operand)
-      {
-        constant_found = true;
-        // We can't break because we have to make sure we find any instances of
-        // ID_unknown or ID_invalid
-      }
-    }
-  }
-
-  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 optionalt
-static optionalt<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>(expr.op0().type()))
-    return {};
-
-  exprt lhs = expr.op0(), rhs = 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_is_constantt()(rhs))
-    return {};
-
-  return try_evaluate_pointer_comparison(
-    expr.id(), *symbol_expr_lhs, rhs, value_set, language_mode, ns);
-}
-
-/// 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
-static 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)
 {
   const goto_programt::instructiont &instruction=*state.source.pc;
@@ -230,8 +73,6 @@ void goto_symext::symex_goto(statet &state)
   clean_expr(new_guard, 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);
   new_guard = renamed_guard.get();
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index ac4270a6634..b9bf3b4d32e 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -721,11 +721,9 @@ void goto_symext::try_filter_value_sets(
   // one of its possible values in turn. If that leads to a true for some
   // value_set_element then we can delete it from the value set that will be
   // used if the condition is false, and vice versa.
-  for(const exprt &value_set_element : value_set_elements)
+  for(const auto &value_set_element : value_set_elements)
   {
-    if(
-      value_set_element.id() == ID_unknown ||
-      value_set_element.id() == ID_invalid)
+    if(value_set_element.id() == ID_unknown)
     {
       continue;
     }
@@ -737,17 +735,19 @@ void goto_symext::try_filter_value_sets(
       continue;
     }
 
-    value_set_dereferencet::valuet value =
+    value_set_dereferencet::valuet possible_value =
       value_set_dereferencet::build_reference_to(
         value_set_element, *symbol_expr, ns);
 
-    if(value.pointer.is_nil())
-      continue;
+    exprt replacement_expr =
+      possible_value.value.is_nil()
+        ? static_cast<exprt>(null_pointer_exprt{symbol_type})
+        : static_cast<exprt>(address_of_exprt{possible_value.value});
 
     exprt modified_condition(condition);
 
     address_of_aware_replace_symbolt replace_symbol{};
-    replace_symbol.insert(*symbol_expr, value.pointer);
+    replace_symbol.insert(*symbol_expr, replacement_expr);
     replace_symbol(modified_condition);
 
     // This do_simplify() is needed for the following reason: if `condition` is
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index 9d9c7d5efe4..66186c8d134 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -23,7 +23,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/config.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_iterator.h>
-#include <util/expr_util.h>
 #include <util/format_type.h>
 #include <util/fresh_symbol.h>
 #include <util/options.h>
@@ -362,9 +361,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
   const exprt &pointer_expr,
   const namespacet &ns)
 {
-  const pointer_typet &pointer_type =
-    type_checked_cast<pointer_typet>(pointer_expr.type());
-  const typet &dereference_type = pointer_type.subtype();
+  const typet &dereference_type = pointer_expr.type().subtype();
 
   if(what.id()==ID_unknown ||
      what.id()==ID_invalid)
@@ -388,7 +385,6 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
 
   if(root_object.id() == ID_null_object)
   {
-    result.pointer = null_pointer_exprt{pointer_type};
   }
   else if(root_object.id()==ID_dynamic_object)
   {
@@ -398,7 +394,6 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
 
     // can't remove here, turn into *p
     result.value = dereference_exprt{pointer_expr};
-    result.pointer = pointer_expr;
   }
   else if(root_object.id()==ID_integer_address)
   {
@@ -419,7 +414,6 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
         memory_symbol.type.subtype());
 
       result.value=index_expr;
-      result.pointer = address_of_exprt{index_expr};
     }
     else if(
       dereference_type_compare(
@@ -430,8 +424,6 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
         pointer_offset(pointer_expr),
         memory_symbol.type.subtype());
       result.value=typecast_exprt(index_expr, dereference_type);
-      result.pointer =
-        typecast_exprt{address_of_exprt{index_expr}, pointer_type};
     }
     else
     {
@@ -448,7 +440,6 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
           symbol_expr,
           pointer_offset(pointer_expr),
           dereference_type);
-        result.pointer = address_of_exprt{result.value};
       }
     }
   }
@@ -481,8 +472,6 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
       // This is great, we are almost done.
 
       result.value = typecast_exprt::conditional_cast(object, dereference_type);
-      result.pointer =
-        typecast_exprt::conditional_cast(object_pointer, pointer_type);
     }
     else if(
       root_object_type.id() == ID_array &&
@@ -526,12 +515,9 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
         // TODO: need to assert well-alignedness
       }
 
-      const index_exprt &index_expr =
-        index_exprt(root_object, adjusted_offset, root_object_type.subtype());
-      result.value =
-        typecast_exprt::conditional_cast(index_expr, dereference_type);
-      result.pointer = typecast_exprt::conditional_cast(
-        address_of_exprt{index_expr}, pointer_type);
+      result.value = typecast_exprt::conditional_cast(
+        index_exprt(root_object, adjusted_offset, root_object_type.subtype()),
+        dereference_type);
     }
     else
     {
@@ -545,15 +531,11 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
         // Successfully found a member, array index, or combination thereof
         // that matches the desired type and offset:
         result.value = subexpr.value();
-        result.pointer = typecast_exprt::conditional_cast(
-          address_of_exprt{skip_typecast(subexpr.value())}, pointer_type);
         return result;
       }
 
       // we extract something from the root object
       result.value=o.root_object();
-      result.pointer = typecast_exprt::conditional_cast(
-        address_of_exprt{skip_typecast(o.root_object())}, pointer_type);
 
       // this is relative to the root object
       exprt offset;
diff --git a/src/pointer-analysis/value_set_dereference.h b/src/pointer-analysis/value_set_dereference.h
index 4889a7cb362..d1488be443b 100644
--- a/src/pointer-analysis/value_set_dereference.h
+++ b/src/pointer-analysis/value_set_dereference.h
@@ -59,11 +59,9 @@ class value_set_dereferencet final
   {
   public:
     exprt value;
-    exprt pointer;
     exprt pointer_guard;
 
-    valuet()
-      : value{nil_exprt{}}, pointer{nil_exprt{}}, pointer_guard{false_exprt{}}
+    valuet() : value(nil_exprt()), pointer_guard(false_exprt())
     {
     }
   };