diff --git a/src/goto-instrument/rw_set.cpp b/src/goto-instrument/rw_set.cpp
index 0278ce04a7b..c678b672c1f 100644
--- a/src/goto-instrument/rw_set.cpp
+++ b/src/goto-instrument/rw_set.cpp
@@ -79,14 +79,15 @@ void _rw_set_loct::compute()
 void _rw_set_loct::assign(const exprt &lhs, const exprt &rhs)
 {
   read(rhs);
-  read_write_rec(lhs, false, true, "", guardt(true_exprt()));
+  read_write_rec(lhs, false, true, "", exprt::operandst());
 }
 
 void _rw_set_loct::read_write_rec(
   const exprt &expr,
-  bool r, bool w,
+  bool r,
+  bool w,
   const std::string &suffix,
-  const guardt &guard)
+  const exprt::operandst &guard_conjuncts)
 {
   if(expr.id()==ID_symbol)
   {
@@ -96,16 +97,16 @@ void _rw_set_loct::read_write_rec(
 
     if(r)
     {
-      const auto &entry =
-        r_entries.emplace(object, entryt(symbol_expr, object, guard.as_expr()));
+      const auto &entry = r_entries.emplace(
+        object, entryt(symbol_expr, object, conjunction(guard_conjuncts)));
 
       track_deref(entry.first->second, true);
     }
 
     if(w)
     {
-      const auto &entry =
-        w_entries.emplace(object, entryt(symbol_expr, object, guard.as_expr()));
+      const auto &entry = w_entries.emplace(
+        object, entryt(symbol_expr, object, conjunction(guard_conjuncts)));
 
       track_deref(entry.first->second, false);
     }
@@ -114,20 +115,21 @@ void _rw_set_loct::read_write_rec(
   {
     assert(expr.operands().size()==1);
     const std::string &component_name=expr.get_string(ID_component_name);
-    read_write_rec(expr.op0(), r, w, "."+component_name+suffix, guard);
+    read_write_rec(
+      expr.op0(), r, w, "." + component_name + suffix, guard_conjuncts);
   }
   else if(expr.id()==ID_index)
   {
     // we don't distinguish the array elements for now
     assert(expr.operands().size()==2);
-    read_write_rec(expr.op0(), r, w, "[]"+suffix, guard);
-    read(expr.op1(), guard);
+    read_write_rec(expr.op0(), r, w, "[]" + suffix, guard_conjuncts);
+    read(expr.op1(), guard_conjuncts);
   }
   else if(expr.id()==ID_dereference)
   {
     assert(expr.operands().size()==1);
     set_track_deref();
-    read(expr.op0(), guard);
+    read(expr.op0(), guard_conjuncts);
 
     exprt tmp=expr;
     #ifdef LOCAL_MAY
@@ -147,25 +149,25 @@ void _rw_set_loct::read_write_rec(
         entryt &entry=r_entries[object];
         entry.object=object;
         entry.symbol_expr=symbol_exprt(ID_unknown);
-        entry.guard=guard.as_expr(); // should 'OR'
+        entry.guard = conjunction(guard_conjuncts); // should 'OR'
 
         continue;
       }
       #endif
-      read_write_rec(*it, r, w, suffix, guard);
+      read_write_rec(*it, r, w, suffix, guard_conjuncts);
     }
     #else
     dereference(function_id, target, tmp, ns, value_sets);
 
-    read_write_rec(tmp, r, w, suffix, guard);
-    #endif
+    read_write_rec(tmp, r, w, suffix, guard_conjuncts);
+#endif
 
     reset_track_deref();
   }
   else if(expr.id()==ID_typecast)
   {
     assert(expr.operands().size()==1);
-    read_write_rec(expr.op0(), r, w, suffix, guard);
+    read_write_rec(expr.op0(), r, w, suffix, guard_conjuncts);
   }
   else if(expr.id()==ID_address_of)
   {
@@ -174,20 +176,20 @@ void _rw_set_loct::read_write_rec(
   else if(expr.id()==ID_if)
   {
     assert(expr.operands().size()==3);
-    read(expr.op0(), guard);
+    read(expr.op0(), guard_conjuncts);
 
-    guardt true_guard(guard);
-    true_guard.add(expr.op0());
+    exprt::operandst true_guard = guard_conjuncts;
+    true_guard.push_back(expr.op0());
     read_write_rec(expr.op1(), r, w, suffix, true_guard);
 
-    guardt false_guard(guard);
-    false_guard.add(not_exprt(expr.op0()));
+    exprt::operandst false_guard = guard_conjuncts;
+    false_guard.push_back(not_exprt(expr.op0()));
     read_write_rec(expr.op2(), r, w, suffix, false_guard);
   }
   else
   {
     forall_operands(it, expr)
-      read_write_rec(*it, r, w, suffix, guard);
+      read_write_rec(*it, r, w, suffix, guard_conjuncts);
   }
 }
 
diff --git a/src/goto-instrument/rw_set.h b/src/goto-instrument/rw_set.h
index b53478bdd45..d878b4e0d72 100644
--- a/src/goto-instrument/rw_set.h
+++ b/src/goto-instrument/rw_set.h
@@ -18,7 +18,6 @@ Date: February 2006
 #include <vector>
 #include <set>
 
-#include <util/guard.h>
 #include <util/std_expr.h>
 
 #include <goto-programs/goto_model.h>
@@ -158,17 +157,17 @@ class _rw_set_loct:public rw_set_baset
 
   void read(const exprt &expr)
   {
-    read_write_rec(expr, true, false, "", guardt(true_exprt()));
+    read_write_rec(expr, true, false, "", exprt::operandst());
   }
 
-  void read(const exprt &expr, const guardt &guard)
+  void read(const exprt &expr, const exprt::operandst &guard_conjuncts)
   {
-    read_write_rec(expr, true, false, "", guard);
+    read_write_rec(expr, true, false, "", guard_conjuncts);
   }
 
   void write(const exprt &expr)
   {
-    read_write_rec(expr, false, true, "", guardt(true_exprt()));
+    read_write_rec(expr, false, true, "", exprt::operandst());
   }
 
   void compute();
@@ -177,9 +176,10 @@ class _rw_set_loct:public rw_set_baset
 
   void read_write_rec(
     const exprt &expr,
-    bool r, bool w,
+    bool r,
+    bool w,
     const std::string &suffix,
-    const guardt &guard);
+    const exprt::operandst &guard_conjuncts);
 };
 
 class rw_set_loct:public _rw_set_loct
diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h
index c070e688c35..a0b4e5e0c46 100644
--- a/src/goto-programs/goto_convert_class.h
+++ b/src/goto-programs/goto_convert_class.h
@@ -17,7 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <unordered_set>
 
 #include <util/allocate_objects.h>
-#include <util/guard.h>
 #include <util/message.h>
 #include <util/namespace.h>
 #include <util/replace_expr.h>
diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp
index 6584b7dd3cc..d21086d9a5f 100644
--- a/src/goto-symex/symex_clean_expr.cpp
+++ b/src/goto-symex/symex_clean_expr.cpp
@@ -125,7 +125,7 @@ void goto_symext::process_array_expr(statet &state, exprt &expr)
   value_set_dereferencet dereference(
     ns, state.symbol_table, symex_dereference_state, language_mode, false);
 
-  expr = dereference.dereference(expr, guardt{true_exprt()});
+  expr = dereference.dereference(expr);
 
   ::process_array_expr(expr, symex_config.simplify_opt, ns);
 }
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index a8e30ada387..3c18d106d90 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -234,7 +234,7 @@ void goto_symext::dereference_rec(exprt &expr, statet &state)
       expr_is_not_null);
 
     // std::cout << "**** " << format(tmp1) << '\n';
-    exprt tmp2 = dereference.dereference(tmp1, guardt(true_exprt()));
+    exprt tmp2 = dereference.dereference(tmp1);
     // std::cout << "**** " << format(tmp2) << '\n';
 
     expr.swap(tmp2);
diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/src/pointer-analysis/goto_program_dereference.cpp
index 84873392291..6b8cc639843 100644
--- a/src/pointer-analysis/goto_program_dereference.cpp
+++ b/src/pointer-analysis/goto_program_dereference.cpp
@@ -44,61 +44,10 @@ goto_program_dereferencet::get_or_create_failed_symbol(const exprt &expr)
   return nullptr;
 }
 
-/// \deprecated
-bool goto_program_dereferencet::is_valid_object(
-  const irep_idt &identifier)
-{
-  const symbolt &symbol=ns.lookup(identifier);
-
-  if(symbol.type.id()==ID_code)
-    return true;
-
-  if(symbol.is_static_lifetime)
-    return true; // global/static
-
-  #if 0
-  return valid_local_variables->find(symbol.name)!=
-     valid_local_variables->end(); // valid local
-  #else
-  return true;
-  #endif
-}
-
-/// \deprecated
-void goto_program_dereferencet::dereference_failure(
-  const std::string &property,
-  const std::string &msg,
-  const guardt &guard)
-{
-  exprt guard_expr=guard.as_expr();
-
-  if(assertions.insert(guard_expr).second)
-  {
-    guard_expr = boolean_negate(guard_expr);
-
-    // first try simplifier on it
-    if(options.get_bool_option("simplify"))
-      simplify(guard_expr, ns);
-
-    if(!guard_expr.is_true())
-    {
-      goto_program_instruction_typet type=
-        options.get_bool_option("assert-to-assume")?ASSUME:ASSERT;
-
-      goto_programt::targett t=new_code.add_instruction(type);
-      t->guard.swap(guard_expr);
-      t->source_location=dereference_location;
-      t->source_location.set_property_class(property);
-      t->source_location.set_comment("dereference failure: "+msg);
-    }
-  }
-}
-
 /// Turn subexpression of `expr` of the form `&*p` into p
 /// and use `dereference` on subexpressions of the form `*p`
 /// \param expr: expression in which to remove dereferences
-/// \param guard: boolean expression assumed to hold when dereferencing
-void goto_program_dereferencet::dereference_rec(exprt &expr, guardt &guard)
+void goto_program_dereferencet::dereference_rec(exprt &expr)
 {
   if(!has_subexpr(expr, ID_dereference))
     return;
@@ -109,8 +58,6 @@ void goto_program_dereferencet::dereference_rec(exprt &expr, guardt &guard)
       throw expr.id_string()+" must be Boolean, but got "+
             expr.pretty();
 
-    guardt old_guard=guard;
-
     for(auto &op : expr.operands())
     {
       if(!op.is_boolean())
@@ -118,15 +65,8 @@ void goto_program_dereferencet::dereference_rec(exprt &expr, guardt &guard)
               op.pretty();
 
       if(has_subexpr(op, ID_dereference))
-        dereference_rec(op, guard);
-
-      if(expr.id()==ID_or)
-        guard.add(boolean_negate(op));
-      else
-        guard.add(op);
+        dereference_rec(op);
     }
-
-    guard = std::move(old_guard);
     return;
   }
   else if(expr.id()==ID_if)
@@ -142,26 +82,16 @@ void goto_program_dereferencet::dereference_rec(exprt &expr, guardt &guard)
       throw msg;
     }
 
-    dereference_rec(expr.op0(), guard);
+    dereference_rec(expr.op0());
 
     bool o1 = has_subexpr(expr.op1(), ID_dereference);
     bool o2 = has_subexpr(expr.op2(), ID_dereference);
 
     if(o1)
-    {
-      guardt old_guard=guard;
-      guard.add(expr.op0());
-      dereference_rec(expr.op1(), guard);
-      guard = std::move(old_guard);
-    }
+      dereference_rec(expr.op1());
 
     if(o2)
-    {
-      guardt old_guard=guard;
-      guard.add(boolean_negate(expr.op0()));
-      dereference_rec(expr.op2(), guard);
-      guard = std::move(old_guard);
-    }
+      dereference_rec(expr.op2());
 
     return;
   }
@@ -179,16 +109,14 @@ void goto_program_dereferencet::dereference_rec(exprt &expr, guardt &guard)
   }
 
   Forall_operands(it, expr)
-    dereference_rec(*it, guard);
+    dereference_rec(*it);
 
   if(expr.id()==ID_dereference)
   {
     if(expr.operands().size()!=1)
       throw "dereference expects one operand";
 
-    dereference_location=expr.find_source_location();
-
-    exprt tmp = dereference.dereference(expr.op0(), guard);
+    exprt tmp = dereference.dereference(expr.op0());
 
     expr.swap(tmp);
   }
@@ -201,12 +129,10 @@ void goto_program_dereferencet::dereference_rec(exprt &expr, guardt &guard)
 
     if(expr.op0().type().id()==ID_pointer)
     {
-      dereference_location=expr.find_source_location();
-
       exprt tmp1(ID_plus, expr.op0().type());
       tmp1.operands().swap(expr.operands());
 
-      exprt tmp2 = dereference.dereference(tmp1, guard);
+      exprt tmp2 = dereference.dereference(tmp1);
       tmp2.swap(expr);
     }
   }
@@ -232,15 +158,13 @@ void goto_program_dereferencet::dereference_expr(
   exprt &expr,
   const bool checks_only)
 {
-  guardt guard{true_exprt{}};
-
   if(checks_only)
   {
     exprt tmp(expr);
-    dereference_rec(tmp, guard);
+    dereference_rec(tmp);
   }
   else
-    dereference_rec(expr, guard);
+    dereference_rec(expr);
 }
 
 void goto_program_dereferencet::dereference_program(
@@ -253,8 +177,6 @@ void goto_program_dereferencet::dereference_program(
       it++)
   {
     new_code.clear();
-    assertions.clear();
-
     dereference_instruction(it, checks_only);
 
     // insert new instructions
@@ -287,9 +209,6 @@ void goto_program_dereferencet::dereference_instruction(
   bool checks_only)
 {
   current_target=target;
-  #if 0
-  valid_local_variables=&target->local_variables;
-  #endif
   goto_programt::instructiont &i=*target;
 
   if(i.has_condition())
@@ -351,45 +270,9 @@ void goto_program_dereferencet::dereference_expression(
 {
   current_function = function_id;
   current_target=target;
-  #if 0
-  valid_local_variables=&target->local_variables;
-  #endif
-
   dereference_expr(expr, false);
 }
 
-/// Throw an exception in case removing dereferences from the program would
-/// throw an exception.
-void goto_program_dereferencet::pointer_checks(
-  goto_programt &goto_program)
-{
-  dereference_program(goto_program, true);
-}
-
-/// Throw an exception in case removing dereferences from the program would
-/// throw an exception.
-void goto_program_dereferencet::pointer_checks(
-  goto_functionst &goto_functions)
-{
-  dereference_program(goto_functions, true);
-}
-
-/// \deprecated
-void remove_pointers(
-  goto_programt &goto_program,
-  symbol_tablet &symbol_table,
-  value_setst &value_sets)
-{
-  namespacet ns(symbol_table);
-
-  optionst options;
-
-  goto_program_dereferencet
-    goto_program_dereference(ns, symbol_table, options, value_sets);
-
-  goto_program_dereference.dereference_program(goto_program);
-}
-
 /// Remove dereferences in all expressions contained in the program
 /// `goto_model`. `value_sets` is used to determine to what objects the pointers
 /// may be pointing to.
@@ -409,32 +292,6 @@ void remove_pointers(
     goto_program_dereference.dereference_program(it->second.body);
 }
 
-/// \deprecated
-void pointer_checks(
-  goto_programt &goto_program,
-  symbol_tablet &symbol_table,
-  const optionst &options,
-  value_setst &value_sets)
-{
-  namespacet ns(symbol_table);
-  goto_program_dereferencet
-    goto_program_dereference(ns, symbol_table, options, value_sets);
-  goto_program_dereference.pointer_checks(goto_program);
-}
-
-/// \deprecated
-void pointer_checks(
-  goto_functionst &goto_functions,
-  symbol_tablet &symbol_table,
-  const optionst &options,
-  value_setst &value_sets)
-{
-  namespacet ns(symbol_table);
-  goto_program_dereferencet
-    goto_program_dereference(ns, symbol_table, options, value_sets);
-  goto_program_dereference.pointer_checks(goto_functions);
-}
-
 /// Remove dereferences in `expr` using `value_sets` to determine to what
 /// objects the pointers may be pointing to.
 void dereference(
diff --git a/src/pointer-analysis/goto_program_dereference.h b/src/pointer-analysis/goto_program_dereference.h
index cadcd089ce2..2bce9d45380 100644
--- a/src/pointer-analysis/goto_program_dereference.h
+++ b/src/pointer-analysis/goto_program_dereference.h
@@ -48,9 +48,6 @@ class goto_program_dereferencet:protected dereference_callbackt
     goto_functionst &goto_functions,
     bool checks_only=false);
 
-  void pointer_checks(goto_programt &goto_program);
-  void pointer_checks(goto_functionst &goto_functions);
-
   void dereference_expression(
     const irep_idt &function_id,
     goto_programt::const_targett target,
@@ -66,17 +63,8 @@ class goto_program_dereferencet:protected dereference_callbackt
   value_setst &value_sets;
   value_set_dereferencet dereference;
 
-  DEPRECATED("Unused")
-  virtual bool is_valid_object(const irep_idt &identifier);
-
   const symbolt *get_or_create_failed_symbol(const exprt &expr) override;
 
-  DEPRECATED("Unused")
-  virtual void dereference_failure(
-    const std::string &property,
-    const std::string &msg,
-    const guardt &guard);
-
   void
   get_value_set(const exprt &expr, value_setst::valuest &dest) const override;
 
@@ -85,22 +73,11 @@ class goto_program_dereferencet:protected dereference_callbackt
     bool checks_only=false);
 
 protected:
-  void dereference_rec(exprt &expr, guardt &guard);
+  void dereference_rec(exprt &expr);
   void dereference_expr(exprt &expr, const bool checks_only);
 
-#if 0
-  const std::set<irep_idt> *valid_local_variables;
-#endif
   irep_idt current_function;
   goto_programt::const_targett current_target;
-
-  /// Unused
-  source_locationt dereference_location;
-
-  /// Unused
-  std::set<exprt> assertions;
-
-  /// Unused
   goto_programt new_code;
 };
 
@@ -115,24 +92,4 @@ void remove_pointers(
   goto_modelt &,
   value_setst &);
 
-DEPRECATED("Unused")
-void remove_pointers(
-  goto_functionst &,
-  symbol_tablet &,
-  value_setst &);
-
-DEPRECATED("Unused")
-void pointer_checks(
-  goto_programt &,
-  symbol_tablet &,
-  const optionst &,
-  value_setst &);
-
-DEPRECATED("Unused")
-void pointer_checks(
-  goto_functionst &,
-  symbol_tablet &,
-  const optionst &,
-  value_setst &);
-
 #endif // CPROVER_POINTER_ANALYSIS_GOTO_PROGRAM_DEREFERENCE_H
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index 2d0f4e92782..4aeb0da1aae 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -32,9 +32,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/simplify_expr.h>
 #include <util/ssa_expr.h>
 
-exprt value_set_dereferencet::dereference(
-  const exprt &pointer,
-  const guardt &guard)
+exprt value_set_dereferencet::dereference(const exprt &pointer)
 {
   if(pointer.type().id()!=ID_pointer)
     throw "dereference expected pointer type, but got "+
@@ -44,16 +42,8 @@ exprt value_set_dereferencet::dereference(
   if(pointer.id()==ID_if)
   {
     const if_exprt &if_expr=to_if_expr(pointer);
-    // push down the if
-    guardt true_guard=guard;
-    guardt false_guard=guard;
-
-    true_guard.add(if_expr.cond());
-    false_guard.add(not_exprt(if_expr.cond()));
-
-    exprt true_case = dereference(if_expr.true_case(), true_guard);
-    exprt false_case = dereference(if_expr.false_case(), false_guard);
-
+    exprt true_case = dereference(if_expr.true_case());
+    exprt false_case = dereference(if_expr.false_case());
     return if_exprt(if_expr.cond(), true_case, false_case);
   }
 
diff --git a/src/pointer-analysis/value_set_dereference.h b/src/pointer-analysis/value_set_dereference.h
index a6206719951..531030cf1ef 100644
--- a/src/pointer-analysis/value_set_dereference.h
+++ b/src/pointer-analysis/value_set_dereference.h
@@ -19,12 +19,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "dereference_callback.h"
 
 class symbol_tablet;
-class guardt;
 class optionst;
 class symbolt;
 
 /// Wrapper for a function dereferencing pointer expressions using a value set.
-class value_set_dereferencet
+class value_set_dereferencet final
 {
 public:
   /// \param _ns: Namespace
@@ -52,10 +51,8 @@ class value_set_dereferencet
 
   /// Dereference the given pointer-expression. Any errors are
   /// reported to the callback method given in the constructor.
-  /// \param pointer: A pointer-typed expression, to
-  ///        be dereferenced.
-  /// \param guard: A guard, which is assumed to hold when dereferencing.
-  virtual exprt dereference(const exprt &pointer, const guardt &guard);
+  /// \param pointer: A pointer-typed expression, to be dereferenced.
+  exprt dereference(const exprt &pointer);
 
 private:
   const namespacet &ns;