diff --git a/src/doxyfile b/src/doxyfile
index c0da7ae247d..13b1e6e672c 100644
--- a/src/doxyfile
+++ b/src/doxyfile
@@ -2041,7 +2041,7 @@ INCLUDE_FILE_PATTERNS  =
 # recursively expanded use the := operator instead of the = operator.
 # This tag requires that the tag ENABLE_PREPROCESSING is set to YES.
 
-PREDEFINED             =
+PREDEFINED             = "DEPRECATED(msg)= /// \deprecated msg"
 
 # If the MACRO_EXPANSION and EXPAND_ONLY_PREDEF tags are set to YES then this
 # tag can be used to specify a list of macro names that should be expanded. The
diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp
index 317297c6c7e..f565f84cf9e 100644
--- a/src/goto-symex/postcondition.cpp
+++ b/src/goto-symex/postcondition.cpp
@@ -160,16 +160,13 @@ bool postconditiont::is_used(
   else if(expr.id()==ID_dereference)
   {
     // aliasing may happen here
-    value_setst::valuest expr_set;
-    value_set.get_value_set(to_dereference_expr(expr).pointer(), expr_set, ns);
+    std::vector<exprt> expr_set =
+      value_set.get_value_set(to_dereference_expr(expr).pointer(), ns);
     std::unordered_set<irep_idt> symbols;
 
-    for(value_setst::valuest::const_iterator
-        it=expr_set.begin();
-        it!=expr_set.end();
-        it++)
+    for(const exprt &e : expr_set)
     {
-      const exprt tmp = get_original_name(*it);
+      const exprt tmp = get_original_name(e);
       find_symbols(tmp, symbols);
     }
 
diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp
index dd0ccb50296..8c367c5bc2c 100644
--- a/src/goto-symex/precondition.cpp
+++ b/src/goto-symex/precondition.cpp
@@ -112,16 +112,12 @@ void preconditiont::compute_rec(exprt &dest)
 
     // aliasing may happen here
 
-    value_setst::valuest expr_set;
-    value_sets.get_values(
-      SSA_step.source.function_id, target, deref_expr.pointer(), expr_set);
+    const std::vector<exprt> expr_set = value_sets.get_values(
+      SSA_step.source.function_id, target, deref_expr.pointer());
     std::unordered_set<irep_idt> symbols;
 
-    for(value_setst::valuest::const_iterator
-        it=expr_set.begin();
-        it!=expr_set.end();
-        it++)
-      find_symbols(*it, symbols);
+    for(const exprt &e : expr_set)
+      find_symbols(e, symbols);
 
     if(symbols.find(lhs_identifier)!=symbols.end())
     {
diff --git a/src/goto-symex/symex_dereference_state.cpp b/src/goto-symex/symex_dereference_state.cpp
index 28dc90b916f..5828566db4f 100644
--- a/src/goto-symex/symex_dereference_state.cpp
+++ b/src/goto-symex/symex_dereference_state.cpp
@@ -107,3 +107,10 @@ void symex_dereference_statet::get_value_set(
   std::cout << "**************************\n";
 #endif
 }
+
+/// Just forwards a value-set query to `state.value_set`
+std::vector<exprt>
+symex_dereference_statet::get_value_set(const exprt &expr) const
+{
+  return state.value_set.get_value_set(expr, ns);
+}
diff --git a/src/goto-symex/symex_dereference_state.h b/src/goto-symex/symex_dereference_state.h
index b0c0e15682a..174fb0a9ee5 100644
--- a/src/goto-symex/symex_dereference_state.h
+++ b/src/goto-symex/symex_dereference_state.h
@@ -34,9 +34,12 @@ class symex_dereference_statet:
   goto_symext::statet &state;
   const namespacet &ns;
 
+  DEPRECATED(SINCE(2019, 05, 22, "use vector returning version instead"))
   void get_value_set(const exprt &expr, value_setst::valuest &value_set)
     const override;
 
+  std::vector<exprt> get_value_set(const exprt &expr) const override;
+
   const symbolt *get_or_create_failed_symbol(const exprt &expr) override;
 };
 
diff --git a/src/pointer-analysis/dereference_callback.h b/src/pointer-analysis/dereference_callback.h
index f39da7f75b4..7a245fcd409 100644
--- a/src/pointer-analysis/dereference_callback.h
+++ b/src/pointer-analysis/dereference_callback.h
@@ -29,9 +29,12 @@ class dereference_callbackt
 public:
   virtual ~dereference_callbackt() = default;
 
+  DEPRECATED(SINCE(2019, 05, 22, "use vector returning version instead"))
   virtual void
   get_value_set(const exprt &expr, value_setst::valuest &value_set) const = 0;
 
+  virtual std::vector<exprt> get_value_set(const exprt &expr) const = 0;
+
   virtual const symbolt *get_or_create_failed_symbol(const exprt &expr) = 0;
 };
 
diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/src/pointer-analysis/goto_program_dereference.cpp
index 7b75c1bbfe6..600463bc6bf 100644
--- a/src/pointer-analysis/goto_program_dereference.cpp
+++ b/src/pointer-analysis/goto_program_dereference.cpp
@@ -147,6 +147,16 @@ void goto_program_dereferencet::get_value_set(
   value_sets.get_values(current_function, current_target, expr, dest);
 }
 
+/// Gets the value set corresponding to the current target and
+/// expression \p expr.
+/// \param expr: an expression
+/// \return the value set
+std::vector<exprt>
+goto_program_dereferencet::get_value_set(const exprt &expr) const
+{
+  return value_sets.get_values(current_function, current_target, expr);
+}
+
 /// Remove dereference expressions contained in `expr`.
 /// \param expr: an expression
 /// \param checks_only: when true, execute the substitution on a copy of expr
diff --git a/src/pointer-analysis/goto_program_dereference.h b/src/pointer-analysis/goto_program_dereference.h
index 2bce9d45380..eee508c2bae 100644
--- a/src/pointer-analysis/goto_program_dereference.h
+++ b/src/pointer-analysis/goto_program_dereference.h
@@ -65,9 +65,12 @@ class goto_program_dereferencet:protected dereference_callbackt
 
   const symbolt *get_or_create_failed_symbol(const exprt &expr) override;
 
+  DEPRECATED(SINCE(2019, 05, 22, "use vector returning version instead"))
   void
   get_value_set(const exprt &expr, value_setst::valuest &dest) const override;
 
+  std::vector<exprt> get_value_set(const exprt &expr) const override;
+
   void dereference_instruction(
     goto_programt::targett target,
     bool checks_only=false);
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index b7a40dc36bf..ff16df24ae7 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/simplify_expr.h>
 
 #include <langapi/language_util.h>
+#include <util/range.h>
 
 #ifdef DEBUG
 #include <iostream>
@@ -308,8 +309,7 @@ bool value_sett::eval_pointer_offset(
   {
     assert(expr.operands().size()==1);
 
-    object_mapt reference_set;
-    get_value_set(expr.op0(), reference_set, ns, true);
+    const object_mapt reference_set = get_value_set(expr.op0(), ns, true);
 
     exprt new_expr;
     mp_integer previous_offset=0;
@@ -352,12 +352,11 @@ bool value_sett::eval_pointer_offset(
 }
 
 void value_sett::get_value_set(
-  const exprt &expr,
+  exprt expr,
   value_setst::valuest &dest,
   const namespacet &ns) const
 {
-  object_mapt object_map;
-  get_value_set(expr, object_map, ns, false);
+  object_mapt object_map = get_value_set(std::move(expr), ns, false);
 
   for(object_map_dt::const_iterator
       it=object_map.read().begin();
@@ -372,17 +371,37 @@ void value_sett::get_value_set(
   #endif
 }
 
+std::vector<exprt>
+value_sett::get_value_set(exprt expr, const namespacet &ns) const
+{
+  const object_mapt object_map = get_value_set(std::move(expr), ns, false);
+  return make_range(object_map.read())
+    .map([&](const object_map_dt::value_type &pair) { return to_expr(pair); });
+}
+
 void value_sett::get_value_set(
-  const exprt &expr,
+  exprt expr,
   object_mapt &dest,
   const namespacet &ns,
   bool is_simplified) const
 {
-  exprt tmp(expr);
   if(!is_simplified)
-    simplify(tmp, ns);
+    simplify(expr, ns);
+
+  get_value_set_rec(expr, dest, "", expr.type(), ns);
+}
+
+value_sett::object_mapt value_sett::get_value_set(
+  exprt expr,
+  const namespacet &ns,
+  bool is_simplified) const
+{
+  if(!is_simplified)
+    simplify(expr, ns);
 
-  get_value_set_rec(tmp, dest, "", tmp.type(), ns);
+  object_mapt dest;
+  get_value_set_rec(expr, dest, "", expr.type(), ns);
+  return dest;
 }
 
 /// Check if 'suffix' starts with 'field'.
@@ -1304,8 +1323,7 @@ void value_sett::assign(
   else
   {
     // basic type
-    object_mapt values_rhs;
-    get_value_set(rhs, values_rhs, ns, is_simplified);
+    object_mapt values_rhs = get_value_set(rhs, ns, is_simplified);
 
     // Permit custom subclass to alter the read values prior to write:
     adjust_assign_rhs_values(rhs, ns, values_rhs);
diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h
index 6ff79285d1c..3fd5440a26a 100644
--- a/src/pointer-analysis/value_set.h
+++ b/src/pointer-analysis/value_set.h
@@ -80,6 +80,7 @@ class value_sett
   /// Represents the offset into an object: either a unique integer offset,
   /// or an unknown value, represented by `!offset`.
   typedef optionalt<mp_integer> offsett;
+  DEPRECATED(SINCE(2019, 05, 22, "Unused"))
   bool offset_is_zero(const offsett &offset) const
   {
     return offset && offset->is_zero();
@@ -236,11 +237,13 @@ class value_sett
 
   /// Set of expressions; only used for the `get` API, not for internal
   /// data representation.
+  DEPRECATED(SINCE(2019, 05, 22, "Only used in deprecated function"))
   typedef std::set<exprt> expr_sett;
 
   /// Set of dynamic object numbers, equivalent to a set of
   /// `dynamic_object_exprt`s with corresponding IDs. Used only in internal
   /// implementation details.
+  DEPRECATED(SINCE(2019, 05, 22, "Unused"))
   typedef std::set<unsigned int> dynamic_object_id_sett;
 
   /// Map representing the entire value set, mapping from string LHS IDs
@@ -258,17 +261,24 @@ class value_sett
   /// `entryt` fields.
   typedef sharing_mapt<irep_idt, entryt> valuest;
 
-  /// Gets values pointed to by `expr`, including following dereference
+  /// Gets values pointed to by \p expr, including following dereference
   /// operators (i.e. this is not a simple lookup in `valuest`).
-  /// \param expr: query expression
-  /// \param [out] dest: assigned a set of expressions that `expr` may point to
-  /// \param ns: global namespace
+  DEPRECATED(
+    SINCE(2019, 05, 22, "Use get_value_set(exprt, const namespacet &) instead"))
   void get_value_set(
-    const exprt &expr,
+    exprt expr,
     value_setst::valuest &dest,
     const namespacet &ns) const;
 
+  /// Gets values pointed to by `expr`, including following dereference
+  /// operators (i.e. this is not a simple lookup in `valuest`).
+  /// \param expr: query expression
+  /// \param ns: global namespace
+  /// \return list of expressions that `expr` may point to
+  std::vector<exprt> get_value_set(exprt expr, const namespacet &ns) const;
+
   /// Appears to be unimplemented.
+  DEPRECATED(SINCE(2019, 05, 22, "Unimplemented"))
   expr_sett &get(const irep_idt &identifier, const std::string &suffix);
 
   void clear()
@@ -454,18 +464,25 @@ class value_sett
   void erase_symbol(const symbol_exprt &symbol_expr, const namespacet &ns);
 
 protected:
-  /// Reads the set of objects pointed to by `expr`, including making
+  /// Reads the set of objects pointed to by \p expr, including making
   /// recursive lookups for dereference operations etc.
-  /// \param expr: query expression
-  /// \param [out] dest: overwritten by the set of object numbers pointed to
-  /// \param ns: global namespace
-  /// \param is_simplified: if false, simplify `expr` before reading.
+  DEPRECATED(
+    SINCE(2019, 05, 22, "Use the version returning object_mapt instead"))
   void get_value_set(
-    const exprt &expr,
+    exprt expr,
     object_mapt &dest,
     const namespacet &ns,
     bool is_simplified) const;
 
+  /// Reads the set of objects pointed to by `expr`, including making
+  /// recursive lookups for dereference operations etc.
+  /// \param expr: query expression
+  /// \param ns: global namespace
+  /// \param is_simplified: if false, simplify `expr` before reading.
+  /// \return the set of object numbers pointed to
+  object_mapt
+  get_value_set(exprt expr, const namespacet &ns, bool is_simplified) const;
+
   /// See the other overload of `get_reference_set`. This one returns object
   /// numbers and offsets instead of expressions.
   void get_reference_set(
diff --git a/src/pointer-analysis/value_set_analysis.h b/src/pointer-analysis/value_set_analysis.h
index 4f391c7b8bb..12606dee785 100644
--- a/src/pointer-analysis/value_set_analysis.h
+++ b/src/pointer-analysis/value_set_analysis.h
@@ -65,6 +65,7 @@ class value_set_analysis_templatet:
 
 public:
   // interface value_sets
+  DEPRECATED(SINCE(2019, 05, 22, "use list returning version instead"))
   void get_values(
     const irep_idt &,
     locationt l,
@@ -73,6 +74,13 @@ class value_set_analysis_templatet:
   {
     (*this)[l].value_set.get_value_set(expr, dest, baset::ns);
   }
+
+  // interface value_sets
+  std::vector<exprt>
+  get_values(const irep_idt &, locationt l, const exprt &expr) override
+  {
+    return (*this)[l].value_set.get_value_set(expr, baset::ns);
+  }
 };
 
 typedef
diff --git a/src/pointer-analysis/value_set_analysis_fi.cpp b/src/pointer-analysis/value_set_analysis_fi.cpp
index c6b59e41986..4ea1df6235a 100644
--- a/src/pointer-analysis/value_set_analysis_fi.cpp
+++ b/src/pointer-analysis/value_set_analysis_fi.cpp
@@ -195,3 +195,17 @@ bool value_set_analysis_fit::check_type(const typet &type)
 
   return false;
 }
+
+std::vector<exprt> value_set_analysis_fit::get_values(
+  const irep_idt &function_id,
+  flow_insensitive_analysis_baset::locationt l,
+  const exprt &expr)
+{
+  state.value_set.from_function =
+    state.value_set.function_numbering.number(function_id);
+  state.value_set.to_function =
+    state.value_set.function_numbering.number(function_id);
+  state.value_set.from_target_index = l->location_number;
+  state.value_set.to_target_index = l->location_number;
+  return state.value_set.get_value_set(expr, ns);
+}
diff --git a/src/pointer-analysis/value_set_analysis_fi.h b/src/pointer-analysis/value_set_analysis_fi.h
index ec6b9d99a81..d04724d6587 100644
--- a/src/pointer-analysis/value_set_analysis_fi.h
+++ b/src/pointer-analysis/value_set_analysis_fi.h
@@ -58,6 +58,7 @@ class value_set_analysis_fit:
 
 public:
   // interface value_sets
+  DEPRECATED(SINCE(2019, 05, 22, "Use the version returning list instead"))
   void get_values(
     const irep_idt &function_id,
     locationt l,
@@ -72,6 +73,11 @@ class value_set_analysis_fit:
     state.value_set.to_target_index = l->location_number;
     state.value_set.get_value_set(expr, dest, ns);
   }
+
+  std::vector<exprt> get_values(
+    const irep_idt &function_id,
+    locationt l,
+    const exprt &expr) override;
 };
 
 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FI_H
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index 224059c779f..9037eb147e5 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "value_set_fi.h"
 
 #include <cassert>
+#include <iterator>
 #include <ostream>
 
 #include <util/symbol_table.h>
@@ -296,6 +297,16 @@ void value_set_fit::get_value_set(
   const exprt &expr,
   std::list<exprt> &value_set,
   const namespacet &ns) const
+{
+  std::vector<exprt> result_as_vector = get_value_set(expr, ns);
+  std::move(
+    result_as_vector.begin(),
+    result_as_vector.end(),
+    std::back_inserter(value_set));
+}
+
+std::vector<exprt>
+value_set_fit::get_value_set(const exprt &expr, const namespacet &ns) const
 {
   object_mapt object_map;
   get_value_set(expr, object_map, ns);
@@ -336,21 +347,24 @@ void value_set_fit::get_value_set(
       flat_map.write()[it->first]=it->second;
   }
 
+  std::vector<exprt> result;
   forall_objects(fit, flat_map.read())
-    value_set.push_back(to_expr(*fit));
+    result.push_back(to_expr(*fit));
 
-  #if 0
+#if 0
   // Sanity check!
   for(std::list<exprt>::const_iterator it=value_set.begin();
       it!=value_set.end();
       it++)
     assert(it->type().id()!="#REF");
-  #endif
+#endif
 
-  #if 0
+#if 0
   for(expr_sett::const_iterator it=value_set.begin(); it!=value_set.end(); it++)
     std::cout << "GET_VALUE_SET: " << format(*it) << '\n';
-  #endif
+#endif
+
+  return result;
 }
 
 void value_set_fit::get_value_set(
diff --git a/src/pointer-analysis/value_set_fi.h b/src/pointer-analysis/value_set_fi.h
index d919c554ad1..d96f4c0a80a 100644
--- a/src/pointer-analysis/value_set_fi.h
+++ b/src/pointer-analysis/value_set_fi.h
@@ -205,11 +205,15 @@ class value_set_fit
   typedef std::unordered_set<idt, string_hash> assign_recursion_sett;
   #endif
 
+  DEPRECATED(SINCE(2019, 05, 22, "Use the version returning vector instead"))
   void get_value_set(
     const exprt &expr,
     std::list<exprt> &dest,
     const namespacet &ns) const;
 
+  std::vector<exprt>
+  get_value_set(const exprt &expr, const namespacet &ns) const;
+
   expr_sett &get(
     const idt &identifier,
     const std::string &suffix);
diff --git a/src/pointer-analysis/value_sets.h b/src/pointer-analysis/value_sets.h
index 24153a71781..2001b7ac763 100644
--- a/src/pointer-analysis/value_sets.h
+++ b/src/pointer-analysis/value_sets.h
@@ -28,12 +28,19 @@ class value_setst
   typedef std::list<exprt> valuest;
 
   // this is not const to allow a lazy evaluation
+  DEPRECATED(SINCE(2019, 05, 22, "use vector returning version instead"))
   virtual void get_values(
     const irep_idt &function_id,
     goto_programt::const_targett l,
     const exprt &expr,
     valuest &dest) = 0;
 
+  // this is not const to allow a lazy evaluation
+  virtual std::vector<exprt> get_values(
+    const irep_idt &function_id,
+    goto_programt::const_targett l,
+    const exprt &expr) = 0;
+
   virtual ~value_setst()
   {
   }