diff --git a/src/goto-symex/Makefile b/src/goto-symex/Makefile
index 7876b206a28..f9f2fea35d1 100644
--- a/src/goto-symex/Makefile
+++ b/src/goto-symex/Makefile
@@ -12,6 +12,7 @@ SRC = auto_objects.cpp \
       path_storage.cpp \
       postcondition.cpp \
       precondition.cpp \
+      renamed.cpp \
       renaming_level.cpp \
       show_program.cpp \
       show_vcc.cpp \
diff --git a/src/goto-symex/goto_state.cpp b/src/goto-symex/goto_state.cpp
index 4fe5b7ab7ed..b0752ab01f7 100644
--- a/src/goto-symex/goto_state.cpp
+++ b/src/goto-symex/goto_state.cpp
@@ -104,7 +104,11 @@ void goto_statet::apply_condition(
         else if(propagation_entry->get() != rhs)
           propagation.replace(l1_identifier, rhs);
 
-        value_set.assign(l1_lhs, rhs, ns, true, false);
+        auto l1_lhs_checked = check_l1_renaming(l1_lhs);
+        CHECK_RETURN(l1_lhs_checked);
+        auto l1_rhs_checked = check_l1_renaming(rhs);
+        CHECK_RETURN(l1_rhs_checked);
+        value_set.assign(*l1_lhs_checked, *l1_rhs_checked, ns, true, false);
       }
     }
   }
diff --git a/src/goto-symex/goto_state.h b/src/goto-symex/goto_state.h
index b9fea0528cc..f87e64616f0 100644
--- a/src/goto-symex/goto_state.h
+++ b/src/goto-symex/goto_state.h
@@ -16,9 +16,9 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 
 #include <analyses/guard.h>
 #include <analyses/local_safe_pointers.h>
-#include <pointer-analysis/value_set.h>
 
 #include "renaming_level.h"
+#include "symex_value_set.h"
 
 /// Container for data that varies per program point, e.g. the constant
 /// propagator state, when state needs to branch. This is copied out of
@@ -40,7 +40,7 @@ class goto_statet
   }
 
   /// Uses level 1 names, and is used to do dereferencing
-  value_sett value_set;
+  symex_value_sett value_set;
 
   // A guard is a particular condition that has to pass for an instruction
   // to be executed. The easiest example is an if/else: each instruction along
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 12be632efb2..08df4afcd34 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -392,9 +392,9 @@ class goto_symext
   void try_filter_value_sets(
     goto_symex_statet &state,
     exprt condition,
-    const value_sett &original_value_set,
-    value_sett *jump_taken_value_set,
-    value_sett *jump_not_taken_value_set,
+    const symex_value_sett &original_value_set,
+    symex_value_sett *jump_taken_value_set,
+    symex_value_sett *jump_not_taken_value_set,
     const namespacet &ns);
 
   virtual void vcc(
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index 47c59dbc90e..622fd94830b 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -47,90 +47,6 @@ goto_symex_statet::goto_symex_statet(
 
 goto_symex_statet::~goto_symex_statet()=default;
 
-/// Check that \p expr is correctly renamed to level 2 and return true in case
-/// an error is detected.
-static bool check_renaming(const exprt &expr);
-
-static bool check_renaming(const typet &type)
-{
-  if(type.id()==ID_array)
-    return check_renaming(to_array_type(type).size());
-  else if(type.id() == ID_struct || type.id() == ID_union)
-  {
-    for(const auto &c : to_struct_union_type(type).components())
-      if(check_renaming(c.type()))
-        return true;
-  }
-  else if(type.has_subtype())
-    return check_renaming(to_type_with_subtype(type).subtype());
-
-  return false;
-}
-
-static bool check_renaming_l1(const exprt &expr)
-{
-  if(check_renaming(expr.type()))
-    return true;
-
-  if(expr.id()==ID_symbol)
-  {
-    const auto &type = expr.type();
-    if(!expr.get_bool(ID_C_SSA_symbol))
-      return type.id() != ID_code && type.id() != ID_mathematical_function;
-    if(!to_ssa_expr(expr).get_level_2().empty())
-      return true;
-    if(to_ssa_expr(expr).get_original_expr().type() != type)
-      return true;
-  }
-  else
-  {
-    forall_operands(it, expr)
-      if(check_renaming_l1(*it))
-        return true;
-  }
-
-  return false;
-}
-
-static bool check_renaming(const exprt &expr)
-{
-  if(check_renaming(expr.type()))
-    return true;
-
-  if(
-    expr.id() == ID_address_of &&
-    to_address_of_expr(expr).object().id() == ID_symbol)
-  {
-    return check_renaming_l1(to_address_of_expr(expr).object());
-  }
-  else if(
-    expr.id() == ID_address_of &&
-    to_address_of_expr(expr).object().id() == ID_index)
-  {
-    const auto index_expr = to_index_expr(to_address_of_expr(expr).object());
-    return check_renaming_l1(index_expr.array()) ||
-           check_renaming(index_expr.index());
-  }
-  else if(expr.id()==ID_symbol)
-  {
-    const auto &type = expr.type();
-    if(!expr.get_bool(ID_C_SSA_symbol))
-      return type.id() != ID_code && type.id() != ID_mathematical_function;
-    if(to_ssa_expr(expr).get_level_2().empty())
-      return true;
-    if(to_ssa_expr(expr).get_original_expr().type() != type)
-      return true;
-  }
-  else
-  {
-    forall_operands(it, expr)
-      if(check_renaming(*it))
-        return true;
-  }
-
-  return false;
-}
-
 template <>
 renamedt<ssa_exprt, L0>
 goto_symex_statet::set_indices<L0>(ssa_exprt ssa_expr, const namespacet &ns)
@@ -170,7 +86,7 @@ renamedt<ssa_exprt, L2> goto_symex_statet::assignment(
   lhs.update_type();
   if(run_validation_checks)
   {
-    DATA_INVARIANT(!check_renaming_l1(lhs), "lhs renaming failed on l1");
+    DATA_INVARIANT(is_l1_renamed(lhs), "lhs renaming failed on l1");
   }
   const ssa_exprt l1_lhs = lhs;
 
@@ -192,8 +108,8 @@ renamedt<ssa_exprt, L2> goto_symex_statet::assignment(
 
   if(run_validation_checks)
   {
-    DATA_INVARIANT(!check_renaming(lhs), "lhs renaming failed on l2");
-    DATA_INVARIANT(!check_renaming(rhs), "rhs renaming failed on l2");
+    DATA_INVARIANT(is_l2_renamed(lhs), "lhs renaming failed on l2");
+    DATA_INVARIANT(is_l2_renamed(rhs), "rhs renaming failed on l2");
   }
 
   // see #305 on GitHub for a simple example and possible discussion
@@ -222,13 +138,13 @@ renamedt<ssa_exprt, L2> goto_symex_statet::assignment(
     ssa_exprt l1_lhs(lhs);
     l1_lhs.remove_level_2();
 
-    if(run_validation_checks)
-    {
-      DATA_INVARIANT(!check_renaming_l1(l1_lhs), "lhs renaming failed on l1");
-      DATA_INVARIANT(!check_renaming_l1(l1_rhs), "rhs renaming failed on l1");
-    }
+    auto l1_lhs_checked = check_l1_renaming(l1_lhs);
+    DATA_INVARIANT(l1_lhs_checked, "lhs renaming failed on l1");
+    auto l1_rhs_checked = check_l1_renaming(l1_rhs);
+    DATA_INVARIANT(l1_rhs_checked, "rhs renaming failed on l1");
 
-    value_set.assign(l1_lhs, l1_rhs, ns, rhs_is_simplified, is_shared);
+    value_set.assign(
+      *l1_lhs_checked, *l1_rhs_checked, ns, rhs_is_simplified, is_shared);
   }
 
 #if 0
@@ -461,7 +377,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
       source,
       symex_targett::assignment_typet::PHI);
 
-    INVARIANT(!check_renaming(ssa_l2), "expr should be renamed to L2");
+    INVARIANT(is_l2_renamed(ssa_l2), "expr should be renamed to L2");
     expr = std::move(ssa_l2);
 
     a_s_read.second.push_back(guard);
diff --git a/src/goto-symex/renamed.cpp b/src/goto-symex/renamed.cpp
new file mode 100644
index 00000000000..80a5b67f59c
--- /dev/null
+++ b/src/goto-symex/renamed.cpp
@@ -0,0 +1,134 @@
+/*******************************************************************\
+
+Module: Symbolic Execution
+
+Author: Romain Brenguier, romain.brenguier@diffblue.com
+
+\*******************************************************************/
+
+/// \file
+/// Class for expressions or types renamed up to a given level
+
+#include "renamed.h"
+#include <util/ssa_expr.h>
+#include <util/std_expr.h>
+
+template <levelt level>
+renamedt<exprt, level> make_renamed(constant_exprt constant)
+{
+  return renamedt<exprt, level>(std::move(constant));
+}
+
+// Force template instantiations for the three levels
+template renamedt<exprt, L0> make_renamed(constant_exprt constant);
+template renamedt<exprt, L1> make_renamed(constant_exprt constant);
+template renamedt<exprt, L2> make_renamed(constant_exprt constant);
+
+bool is_l1_renamed(const exprt &expr)
+{
+  if(expr.id() == ID_symbol)
+  {
+    const auto &type = expr.type();
+    if(!expr.get_bool(ID_C_SSA_symbol))
+      return type.id() == ID_code || type.id() == ID_mathematical_function;
+    if(!to_ssa_expr(expr).get_level_2().empty())
+      return false;
+    if(to_ssa_expr(expr).get_original_expr().type() != type)
+      return false;
+  }
+  else
+  {
+    forall_operands(it, expr)
+      if(!is_l1_renamed(*it))
+        return false;
+  }
+
+  return true;
+}
+
+bool is_l2_renamed(const typet &type)
+{
+  if(type.id() == ID_array)
+  {
+    if(!is_l2_renamed(to_array_type(type).size()))
+      return false;
+  }
+  else if(type.id() == ID_struct || type.id() == ID_union)
+  {
+    for(const auto &c : to_struct_union_type(type).components())
+      if(!is_l2_renamed(c.type()))
+        return false;
+  }
+  else if(
+    type.has_subtype() && !is_l2_renamed(to_type_with_subtype(type).subtype()))
+  {
+    return false;
+  }
+  return true;
+}
+
+bool is_l2_renamed(const exprt &expr)
+{
+  if(!is_l2_renamed(expr.type()))
+    return false;
+
+  if(
+    expr.id() == ID_address_of &&
+    to_address_of_expr(expr).object().id() == ID_symbol)
+  {
+    return is_l1_renamed(to_address_of_expr(expr).object());
+  }
+  else if(
+    expr.id() == ID_address_of &&
+    to_address_of_expr(expr).object().id() == ID_index)
+  {
+    const auto index_expr = to_index_expr(to_address_of_expr(expr).object());
+    return is_l1_renamed(index_expr.array()) &&
+           is_l2_renamed(index_expr.index());
+  }
+  else if(expr.id() == ID_symbol)
+  {
+    const auto &type = expr.type();
+    if(!expr.get_bool(ID_C_SSA_symbol))
+      return (type.id() == ID_code || type.id() == ID_mathematical_function);
+    if(to_ssa_expr(expr).get_level_2().empty())
+      return false;
+    if(to_ssa_expr(expr).get_original_expr().type() != type)
+      return false;
+  }
+  else
+  {
+    forall_operands(it, expr)
+      if(!is_l2_renamed(*it))
+        return false;
+  }
+  return true;
+}
+
+optionalt<renamedt<exprt, L1>> check_l1_renaming(exprt expr)
+{
+  if(is_l1_renamed(expr))
+    return renamedt<exprt, L1>(std::move(expr));
+  return {};
+}
+
+optionalt<renamedt<ssa_exprt, L1>> check_l1_renaming(ssa_exprt expr)
+{
+  if(is_l1_renamed(expr))
+    return renamedt<ssa_exprt, L1>(std::move(expr));
+  return {};
+}
+
+optionalt<renamedt<exprt, L2>> check_l2_renaming(exprt expr)
+{
+  if(is_l2_renamed(expr))
+    return renamedt<exprt, L2>(std::move(expr));
+  return {};
+}
+
+optionalt<renamedt<typet, L2>> check_l2_renaming(typet type)
+{
+  if(is_l2_renamed(type))
+    return renamedt<typet, L2>(std::move(type));
+  return {};
+}
diff --git a/src/goto-symex/renamed.h b/src/goto-symex/renamed.h
index 4781271da15..4ec04eeaeaa 100644
--- a/src/goto-symex/renamed.h
+++ b/src/goto-symex/renamed.h
@@ -11,6 +11,17 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #ifndef CPROVER_GOTO_SYMEX_RENAMED_H
 #define CPROVER_GOTO_SYMEX_RENAMED_H
 
+#include <functional>
+#include <type_traits>
+#include <util/nodiscard.h>
+#include <util/optional.h>
+#include <util/simplify_expr.h>
+
+class constant_exprt;
+class exprt;
+class ssa_exprt;
+class typet;
+
 /// Symex renaming level names.
 enum levelt
 {
@@ -65,6 +76,11 @@ class renamedt : private underlyingt
     typename renamedt<exprt, selectively_mutate_level>::mutator_functiont
       get_mutated_expr);
 
+  friend optionalt<renamedt<exprt, L1>> check_l1_renaming(exprt expr);
+  friend optionalt<renamedt<ssa_exprt, L1>> check_l1_renaming(ssa_exprt expr);
+  friend optionalt<renamedt<exprt, L2>> check_l2_renaming(exprt expr);
+  friend optionalt<renamedt<typet, L2>> check_l2_renaming(typet type);
+
   /// Only the friend classes can create renamedt objects
   explicit renamedt(underlyingt value) : underlyingt(std::move(value))
   {
@@ -72,10 +88,7 @@ class renamedt : private underlyingt
 };
 
 template <levelt level>
-renamedt<exprt, level> make_renamed(constant_exprt constant)
-{
-  return renamedt<exprt, level>(std::move(constant));
-}
+renamedt<exprt, level> make_renamed(constant_exprt constant);
 
 /// This permits replacing subexpressions of the renamed value, so long as
 /// each replacement is consistent with our current renaming level (for
@@ -100,4 +113,24 @@ void selectively_mutate(
   }
 }
 
+/// \return true if \p expr has been renamed to level 2
+bool is_l2_renamed(const exprt &expr);
+
+/// \return true if \p type has been renamed to level 2
+bool is_l2_renamed(const typet &type);
+
+/// \return true if \p expr has been renamed to level 1
+bool is_l1_renamed(const exprt &expr);
+
+/// \return a renamed object if \p expr has been renamed to level 1
+NODISCARD optionalt<renamedt<exprt, L1>> check_l1_renaming(exprt expr);
+
+NODISCARD optionalt<renamedt<ssa_exprt, L1>> check_l1_renaming(ssa_exprt expr);
+
+/// \return a renamed object if \p expr has been renamed to level 2
+NODISCARD optionalt<renamedt<exprt, L2>> check_l2_renaming(exprt expr);
+
+/// \return a renamed object if \p type has been renamed to level 2
+NODISCARD optionalt<renamedt<typet, L2>> check_l2_renaming(typet type);
+
 #endif // CPROVER_GOTO_SYMEX_RENAMED_H
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 2be9a9262cf..d0244dc0fe1 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -508,7 +508,9 @@ void goto_symext::symex_assign_symbol(
     // have it in the propagation table and the value set while doing the field
     // assignments, thus we cannot skip putting it in there above.
     state.propagation.erase_if_exists(l1_lhs.get_identifier());
-    state.value_set.erase_symbol(l1_lhs, ns);
+    auto l1_lhs_checked = check_l1_renaming(l1_lhs);
+    CHECK_RETURN(l1_lhs_checked);
+    state.value_set.erase_symbol(*l1_lhs_checked, ns);
   }
 }
 
diff --git a/src/goto-symex/symex_dead.cpp b/src/goto-symex/symex_dead.cpp
index ecd2ee78499..b38db6620d1 100644
--- a/src/goto-symex/symex_dead.cpp
+++ b/src/goto-symex/symex_dead.cpp
@@ -40,7 +40,7 @@ void goto_symext::symex_dead(statet &state, const symbol_exprt &symbol_expr)
     // information is not local to a path, but removing it from the propagation
     // map and value-set is safe as 1) it is local to a path and 2) this
     // instance can no longer appear.
-    state.value_set.values.erase_if_exists(l1_identifier);
+    state.value_set.erase_if_exists(l1_identifier);
     state.propagation.erase_if_exists(l1_identifier);
     // Remove from the local L2 renaming map; this means any reads from the dead
     // identifier will use generation 0 (e.g. x!N@M#0, where N and M are
diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp
index 55f3e7cc1d8..44160340d4e 100644
--- a/src/goto-symex/symex_decl.cpp
+++ b/src/goto-symex/symex_decl.cpp
@@ -59,8 +59,10 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
     else
       rhs=exprt(ID_invalid);
 
-    exprt l1_rhs = state.rename<L1>(std::move(rhs), ns).get();
-    state.value_set.assign(ssa, l1_rhs, ns, true, false);
+    renamedt<exprt, L1> l1_rhs = state.rename<L1>(std::move(rhs), ns);
+    auto l1_ssa = check_l1_renaming(ssa);
+    CHECK_RETURN(l1_ssa.has_value());
+    state.value_set.assign(*l1_ssa, l1_rhs, ns, true, false);
   }
 
   // L2 renaming
diff --git a/src/goto-symex/symex_dereference_state.cpp b/src/goto-symex/symex_dereference_state.cpp
index 5828566db4f..4fc1cfaa39c 100644
--- a/src/goto-symex/symex_dereference_state.cpp
+++ b/src/goto-symex/symex_dereference_state.cpp
@@ -86,7 +86,10 @@ void symex_dereference_statet::get_value_set(
   const exprt &expr,
   value_setst::valuest &value_set) const
 {
-  state.value_set.get_value_set(expr, value_set, ns);
+  auto l1_expr = check_l1_renaming(expr);
+  CHECK_RETURN(l1_expr);
+  for(const auto e : state.value_set.get_value_set(*l1_expr, ns))
+    value_set.push_back(e);
 
 #ifdef DEBUG
   std::cout << "symex_dereference_statet state.value_set={\n";
@@ -112,5 +115,7 @@ void symex_dereference_statet::get_value_set(
 std::vector<exprt>
 symex_dereference_statet::get_value_set(const exprt &expr) const
 {
-  return state.value_set.get_value_set(expr, ns);
+  auto l1_expr = check_l1_renaming(expr);
+  CHECK_RETURN(l1_expr);
+  return state.value_set.get_value_set(*l1_expr, ns);
 }
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index de4640cc563..98386c17c8c 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -83,7 +83,7 @@ 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 symex_value_sett &value_set,
   const irep_idt language_mode,
   const namespacet &ns)
 {
@@ -100,8 +100,12 @@ static optionalt<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
   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 auto checked_l1_expr = check_l1_renaming((exprt)l1_expr);
+  CHECK_RETURN(checked_l1_expr);
   const std::vector<exprt> value_set_elements =
-    value_set.get_value_set(ssa_symbol_expr->get_l1_object(), ns);
+    value_set.get_value_set(*checked_l1_expr, ns);
 
   bool constant_found = false;
 
@@ -167,7 +171,7 @@ static optionalt<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
 ///   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 symex_value_sett &value_set,
   const irep_idt &language_mode,
   const namespacet &ns)
 {
@@ -208,7 +212,7 @@ static optionalt<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
 /// \return The possibly modified condition
 static renamedt<exprt, L2> try_evaluate_pointer_comparisons(
   renamedt<exprt, L2> condition,
-  const value_sett &value_set,
+  const symex_value_sett &value_set,
   const irep_idt &language_mode,
   const namespacet &ns)
 {
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index 6922ddab194..5651836fa04 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -689,9 +689,9 @@ find_unique_pointer_typed_symbol(const exprt &expr)
 void goto_symext::try_filter_value_sets(
   goto_symex_statet &state,
   exprt condition,
-  const value_sett &original_value_set,
-  value_sett *jump_taken_value_set,
-  value_sett *jump_not_taken_value_set,
+  const symex_value_sett &original_value_set,
+  symex_value_sett *jump_taken_value_set,
+  symex_value_sett *jump_not_taken_value_set,
   const namespacet &ns)
 {
   condition = state.rename<L1>(std::move(condition), ns).get();
@@ -704,10 +704,10 @@ void goto_symext::try_filter_value_sets(
     return;
   }
 
-  const pointer_typet &symbol_type = to_pointer_type(symbol_expr->type());
-
+  const auto l1_symbol_expr = check_l1_renaming(*symbol_expr);
+  CHECK_RETURN(l1_symbol_expr);
   const std::vector<exprt> value_set_elements =
-    original_value_set.get_value_set(*symbol_expr, ns);
+    original_value_set.get_value_set(*l1_symbol_expr, ns);
 
   std::unordered_set<exprt, irep_hash> erase_from_jump_taken_value_set;
   std::unordered_set<exprt, irep_hash> erase_from_jump_not_taken_value_set;
@@ -775,16 +775,12 @@ void goto_symext::try_filter_value_sets(
   }
   if(jump_taken_value_set && !erase_from_jump_taken_value_set.empty())
   {
-    auto entry_index = jump_taken_value_set->get_index_of_symbol(
-      symbol_expr->get_identifier(), symbol_type, "", ns);
-    jump_taken_value_set->erase_values_from_entry(
-      *entry_index, erase_from_jump_taken_value_set);
+    jump_taken_value_set->erase(
+      *symbol_expr, ns, erase_from_jump_taken_value_set);
   }
   if(jump_not_taken_value_set && !erase_from_jump_not_taken_value_set.empty())
   {
-    auto entry_index = jump_not_taken_value_set->get_index_of_symbol(
-      symbol_expr->get_identifier(), symbol_type, "", ns);
-    jump_not_taken_value_set->erase_values_from_entry(
-      *entry_index, erase_from_jump_not_taken_value_set);
+    jump_not_taken_value_set->erase(
+      *symbol_expr, ns, erase_from_jump_not_taken_value_set);
   }
 }
diff --git a/src/goto-symex/symex_value_set.h b/src/goto-symex/symex_value_set.h
new file mode 100644
index 00000000000..f5de2dc2f4a
--- /dev/null
+++ b/src/goto-symex/symex_value_set.h
@@ -0,0 +1,77 @@
+/*******************************************************************\
+
+Module: Symbolic Execution
+
+Author: Romain Brenguier, romain.brenguier@diffblue.com
+
+\*******************************************************************/
+
+/// \file
+/// symex_value_sett class definition
+
+#ifndef CPROVER_GOTO_SYMEX_SYMEX_VALUE_SET_H
+#define CPROVER_GOTO_SYMEX_SYMEX_VALUE_SET_H
+
+#include <pointer-analysis/value_set.h>
+#include "renamed.h"
+
+/// Wrapper for value_sett which ensures we access it in a consistent way.
+/// In particular level 1 names should be used.
+class symex_value_sett final
+{
+public:
+  /// \copydoc value_sett::assign
+  void assign(
+    const renamedt<ssa_exprt, L1> &lhs,
+    const renamedt<exprt, L1> &rhs,
+    const namespacet &ns,
+    bool is_simplified,
+    bool add_to_sets)
+  {
+    value_set.assign(lhs.get(), rhs.get(), ns, is_simplified, add_to_sets);
+  }
+
+  /// Remove the entry corresponding to \p lhs
+  void erase_symbol(const renamedt<ssa_exprt, L1> &lhs, const namespacet &ns)
+  {
+    value_set.erase_symbol(lhs.get(), ns);
+  }
+
+  /// Remove the entry corresponding to \p l1_identifier.
+  /// Warning: which identifier is used to represent an expression is an
+  /// implementation detail, it is thus preferred to use \ref erase_symbol.
+  void erase_if_exists(const irep_idt &l1_identifier)
+  {
+    value_set.values.erase_if_exists(l1_identifier);
+  }
+
+  /// Update the entry for \p symbol_expr by erasing any values listed in
+  /// \p to_erase.
+  void erase(
+    const symbol_exprt &symbol_expr,
+    const namespacet &ns,
+    const std::unordered_set<exprt, irep_hash> &to_erase)
+  {
+    const auto entry_index = value_set.get_index_of_symbol(
+      symbol_expr.get_identifier(), symbol_expr.type(), "", ns);
+    value_set.erase_values_from_entry(*entry_index, to_erase);
+  }
+
+  /// \copydoc value_sett::get_value_set(exprt, const namespacet &)
+  std::vector<exprt>
+  get_value_set(const renamedt<exprt, L1> &expr, const namespacet &ns) const
+  {
+    return value_set.get_value_set(expr.get(), ns);
+  }
+
+  /// \copydoc value_sett::make_union(const value_sett &)
+  bool make_union(const symex_value_sett &new_values)
+  {
+    return value_set.make_union(new_values.value_set);
+  }
+
+private:
+  value_sett value_set;
+};
+
+#endif // CPROVER_GOTO_SYMEX_SYMEX_VALUE_SET_H
diff --git a/src/pointer-analysis/module_dependencies.txt b/src/pointer-analysis/module_dependencies.txt
index 25dc8fec88e..d9207afaf19 100644
--- a/src/pointer-analysis/module_dependencies.txt
+++ b/src/pointer-analysis/module_dependencies.txt
@@ -1,5 +1,4 @@
 analyses
 goto-programs
-langapi # should go away
 pointer-analysis
 util
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index ff16df24ae7..4d606733665 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -20,7 +20,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/prefix.h>
 #include <util/simplify_expr.h>
 
-#include <langapi/language_util.h>
+#include <goto-symex/renamed.h>
+#include <util/format_expr.h>
+#include <util/format_type.h>
 #include <util/range.h>
 
 #ifdef DEBUG
@@ -133,9 +135,14 @@ bool value_sett::insert(
 }
 
 void value_sett::output(
-  const namespacet &ns,
+  const namespacet &,
   std::ostream &out,
   const std::string &indent) const
+{
+  output(out, indent);
+}
+
+void value_sett::output(std::ostream &out, const std::string &indent) const
 {
   values.iterate([&](const irep_idt &, const entryt &e) {
     irep_idt identifier, display_name;
@@ -174,29 +181,29 @@ void value_sett::output(
     {
       const exprt &o = object_numbering[o_it->first];
 
-      std::string result;
+      std::ostringstream stream;
 
       if(o.id() == ID_invalid || o.id() == ID_unknown)
-        result = from_expr(ns, identifier, o);
+        stream << format(o);
       else
       {
-        result = "<" + from_expr(ns, identifier, o) + ", ";
+        stream << "<" << format(o) << ", ";
 
         if(o_it->second)
-          result += integer2string(*o_it->second);
+          stream << *o_it->second;
         else
-          result += '*';
+          stream << '*';
 
         if(o.type().is_nil())
-          result += ", ?";
+          stream << ", ?";
         else
-          result += ", " + from_type(ns, identifier, o.type());
+          stream << ", " << format(o.type());
 
-        result += '>';
+        stream << '>';
       }
 
+      const std::string result = stream.str();
       out << result;
-
       width += result.size();
 
       object_map_dt::const_iterator next(o_it);
diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h
index 3fd5440a26a..0c837593fa3 100644
--- a/src/pointer-analysis/value_set.h
+++ b/src/pointer-analysis/value_set.h
@@ -25,7 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 class namespacet;
 
-/// State type in value_set_domaint, used in value-set analysis and goto-symex.
+/// Used in value-set analysis and goto-symex.
 /// Represents a mapping from expressions to the addresses that may be stored
 /// there; for example, a global that is either null or points to a
 /// heap-allocated object, which itself has two fields, one pointing to another
@@ -313,9 +313,11 @@ class value_sett
     bool add_to_sets);
 
   /// Pretty-print this value-set
-  /// \param ns: global namespace
   /// \param [out] out: stream to write to
   /// \param indent: string to use for indentation of the output
+  void output(std::ostream &out, const std::string &indent = "") const;
+
+  DEPRECATED(SINCE(2019, 06, 11, "Use the version without ns argument"))
   void output(
     const namespacet &ns,
     std::ostream &out,