diff --git a/src/solvers/prop/decision_procedure.h b/src/solvers/prop/decision_procedure.h
index 818b9cd1952..73609bfecbc 100644
--- a/src/solvers/prop/decision_procedure.h
+++ b/src/solvers/prop/decision_procedure.h
@@ -34,8 +34,14 @@ class decision_proceduret
   void set_to_false(const exprt &expr);
 
   /// Convert a Boolean expression and return the corresponding literal
+  /// This will go away, use handle(expr) instead
   virtual literalt convert(const exprt &expr) = 0;
 
+  /// Generate a handle for an expression; this offers an efficient way
+  /// to refer to the expression in subsequent calls to \ref get or
+  /// \ref set_to
+  virtual exprt handle(const exprt &expr) = 0;
+
   /// Result of running the decision procedure
   enum class resultt
   {
@@ -54,6 +60,7 @@ class decision_proceduret
 
   /// Return value of literal \p l from satisfying assignment.
   /// Return tvt::UNKNOWN if not available
+  /// This will go away, use get instead.
   virtual tvt l_get(literalt l) const = 0;
 
   /// Print satisfying assignment to \p out
diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp
index b371aa37e21..38792212e5c 100644
--- a/src/solvers/prop/prop_conv.cpp
+++ b/src/solvers/prop/prop_conv.cpp
@@ -7,8 +7,16 @@ Author: Daniel Kroening, kroening@kroening.com
 \*******************************************************************/
 
 #include "prop_conv.h"
+
+#include "literal_expr.h"
+
 #include <algorithm>
 
+exprt prop_convt::handle(const exprt &expr)
+{
+  return literal_exprt(convert(expr));
+}
+
 /// determine whether a variable is in the final conflict
 bool prop_convt::is_in_conflict(literalt) const
 {
diff --git a/src/solvers/prop/prop_conv.h b/src/solvers/prop/prop_conv.h
index c026e87cb49..db1981f55c5 100644
--- a/src/solvers/prop/prop_conv.h
+++ b/src/solvers/prop/prop_conv.h
@@ -22,6 +22,13 @@ class prop_convt:public decision_proceduret
 
   using decision_proceduret::operator();
 
+  /// returns a 'handle', which is an expression that
+  /// has the same value as the argument in any model
+  /// that is generated.
+  /// This may be the expression itself or a more compact
+  /// but solver-specific representation.
+  exprt handle(const exprt &expr) override;
+
   // incremental solving
   virtual void set_frozen(literalt a);
   virtual void set_frozen(const bvt &);