diff --git a/jbmc/regression/jbmc/exception-cleanup/test.desc b/jbmc/regression/jbmc/exception-cleanup/test.desc
index a3a271c9941..a3787221ff2 100644
--- a/jbmc/regression/jbmc/exception-cleanup/test.desc
+++ b/jbmc/regression/jbmc/exception-cleanup/test.desc
@@ -4,11 +4,8 @@ Test.class
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-1 remaining after simplification$
+0 remaining after simplification$
 --
 ^warning: ignoring
 --
-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.
+The function "unreachable" should be successfully noted as unreachable by symex.
diff --git a/jbmc/regression/jbmc/exception-cleanup/vccs.desc b/jbmc/regression/jbmc/exception-cleanup/vccs.desc
index 4dd86b143ae..83b698bdd53 100644
--- a/jbmc/regression/jbmc/exception-cleanup/vccs.desc
+++ b/jbmc/regression/jbmc/exception-cleanup/vccs.desc
@@ -3,8 +3,6 @@ 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
new file mode 100644
index 00000000000..40219aa82f8
--- /dev/null
+++ b/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.c
@@ -0,0 +1,181 @@
+#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
new file mode 100644
index 00000000000..d8f0a0e31c7
--- /dev/null
+++ b/regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc
@@ -0,0 +1,60 @@
+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 8096ca37cf0..5c9af1c513c 100644
--- a/src/goto-symex/renaming_level.h
+++ b/src/goto-symex/renaming_level.h
@@ -15,7 +15,9 @@ 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>
@@ -87,6 +89,9 @@ class renamedt : private underlyingt
     (void)::simplify(value(), ns);
   }
 
+  using mutator_functiont =
+    std::function<optionalt<renamedt>(const renamedt &)>;
+
 private:
   underlyingt &value()
   {
@@ -98,12 +103,51 @@ 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 0fdfcbbe938..30f19f0adf0 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 /// Symbolic Execution
 
 #include "goto_symex.h"
+#include "goto_symex_is_constant.h"
 
 #include <algorithm>
 
@@ -19,6 +20,7 @@ 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(
@@ -65,6 +67,161 @@ 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;
@@ -73,6 +230,8 @@ 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 b9bf3b4d32e..ac4270a6634 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -721,9 +721,11 @@ 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 auto &value_set_element : value_set_elements)
+  for(const exprt &value_set_element : value_set_elements)
   {
-    if(value_set_element.id() == ID_unknown)
+    if(
+      value_set_element.id() == ID_unknown ||
+      value_set_element.id() == ID_invalid)
     {
       continue;
     }
@@ -735,19 +737,17 @@ void goto_symext::try_filter_value_sets(
       continue;
     }
 
-    value_set_dereferencet::valuet possible_value =
+    value_set_dereferencet::valuet value =
       value_set_dereferencet::build_reference_to(
         value_set_element, *symbol_expr, ns);
 
-    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});
+    if(value.pointer.is_nil())
+      continue;
 
     exprt modified_condition(condition);
 
     address_of_aware_replace_symbolt replace_symbol{};
-    replace_symbol.insert(*symbol_expr, replacement_expr);
+    replace_symbol.insert(*symbol_expr, value.pointer);
     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 66186c8d134..9d9c7d5efe4 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -23,6 +23,7 @@ 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>
@@ -361,7 +362,9 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
   const exprt &pointer_expr,
   const namespacet &ns)
 {
-  const typet &dereference_type = pointer_expr.type().subtype();
+  const pointer_typet &pointer_type =
+    type_checked_cast<pointer_typet>(pointer_expr.type());
+  const typet &dereference_type = pointer_type.subtype();
 
   if(what.id()==ID_unknown ||
      what.id()==ID_invalid)
@@ -385,6 +388,7 @@ 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)
   {
@@ -394,6 +398,7 @@ 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)
   {
@@ -414,6 +419,7 @@ 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(
@@ -424,6 +430,8 @@ 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
     {
@@ -440,6 +448,7 @@ 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};
       }
     }
   }
@@ -472,6 +481,8 @@ 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 &&
@@ -515,9 +526,12 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
         // TODO: need to assert well-alignedness
       }
 
-      result.value = typecast_exprt::conditional_cast(
-        index_exprt(root_object, adjusted_offset, root_object_type.subtype()),
-        dereference_type);
+      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);
     }
     else
     {
@@ -531,11 +545,15 @@ 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 d1488be443b..4889a7cb362 100644
--- a/src/pointer-analysis/value_set_dereference.h
+++ b/src/pointer-analysis/value_set_dereference.h
@@ -59,9 +59,11 @@ class value_set_dereferencet final
   {
   public:
     exprt value;
+    exprt pointer;
     exprt pointer_guard;
 
-    valuet() : value(nil_exprt()), pointer_guard(false_exprt())
+    valuet()
+      : value{nil_exprt{}}, pointer{nil_exprt{}}, pointer_guard{false_exprt{}}
     {
     }
   };