diff --git a/src/goto-checker/goto_symex_fault_localizer.cpp b/src/goto-checker/goto_symex_fault_localizer.cpp
index 77fc01e7e2c..c6c75dd67d4 100644
--- a/src/goto-checker/goto_symex_fault_localizer.cpp
+++ b/src/goto-checker/goto_symex_fault_localizer.cpp
@@ -11,13 +11,11 @@ Author: Peter Schrammel
 
 #include "goto_symex_fault_localizer.h"
 
-#include <solvers/prop/prop_conv.h>
-
 goto_symex_fault_localizert::goto_symex_fault_localizert(
   const optionst &options,
   ui_message_handlert &ui_message_handler,
   const symex_target_equationt &equation,
-  prop_convt &solver)
+  stack_decision_proceduret &solver)
   : options(options),
     ui_message_handler(ui_message_handler),
     equation(equation),
@@ -58,7 +56,7 @@ const SSA_stept &goto_symex_fault_localizert::collect_guards(
       step.assignment_type == symex_targett::assignment_typet::STATE &&
       !step.ignore)
     {
-      literalt l = solver.convert(step.guard_handle);
+      exprt l = solver.handle(step.guard_handle);
       if(!l.is_constant())
       {
         auto emplace_result = fault_location.scores.emplace(step.source.pc, 0);
@@ -79,21 +77,21 @@ bool goto_symex_fault_localizert::check(
   const localization_points_valuet &value)
 {
   PRECONDITION(value.size() == localization_points.size());
-  bvt assumptions;
+  std::vector<exprt> assumptions;
   localization_points_valuet::const_iterator v_it = value.begin();
   for(const auto &l : localization_points)
   {
     if(v_it->is_true())
       assumptions.push_back(l.first);
     else if(v_it->is_false())
-      assumptions.push_back(!l.first);
+      assumptions.push_back(solver.handle(not_exprt(l.first)));
     ++v_it;
   }
 
   // lock the failed assertion
-  assumptions.push_back(!solver.convert(failed_step.cond_handle));
+  assumptions.push_back(solver.handle(not_exprt(failed_step.cond_handle)));
 
-  solver.set_assumptions(assumptions);
+  solver.push(assumptions);
 
   return solver() != decision_proceduret::resultt::D_SATISFIABLE;
 }
@@ -104,11 +102,11 @@ void goto_symex_fault_localizert::update_scores(
   for(auto &l : localization_points)
   {
     auto &score = l.second->second;
-    if(solver.l_get(l.first).is_true())
+    if(solver.get(l.first).is_true())
     {
       score++;
     }
-    else if(solver.l_get(l.first).is_false() && score > 0)
+    else if(solver.get(l.first).is_false() && score > 0)
     {
       score--;
     }
@@ -135,6 +133,5 @@ void goto_symex_fault_localizert::localize_linear(
   }
 
   // clear assumptions
-  bvt assumptions;
-  solver.set_assumptions(assumptions);
+  solver.pop();
 }
diff --git a/src/goto-checker/goto_symex_fault_localizer.h b/src/goto-checker/goto_symex_fault_localizer.h
index 9f5e6ebd64c..7e09f6753d5 100644
--- a/src/goto-checker/goto_symex_fault_localizer.h
+++ b/src/goto-checker/goto_symex_fault_localizer.h
@@ -18,7 +18,7 @@ Author: Peter Schrammel
 
 #include <goto-symex/symex_target_equation.h>
 
-#include <solvers/prop/prop_conv.h>
+#include <solvers/stack_decision_procedure.h>
 
 #include "fault_localization_provider.h"
 
@@ -29,7 +29,7 @@ class goto_symex_fault_localizert
     const optionst &options,
     ui_message_handlert &ui_message_handler,
     const symex_target_equationt &equation,
-    prop_convt &solver);
+    stack_decision_proceduret &solver);
 
   fault_location_infot operator()(const irep_idt &failed_property_id);
 
@@ -37,10 +37,10 @@ class goto_symex_fault_localizert
   const optionst &options;
   ui_message_handlert &ui_message_handler;
   const symex_target_equationt &equation;
-  prop_convt &solver;
+  stack_decision_proceduret &solver;
 
   /// A localization point is a goto instruction that is potentially at fault
-  typedef std::map<literalt, fault_location_infot::score_mapt::iterator>
+  typedef std::map<exprt, fault_location_infot::score_mapt::iterator>
     localization_pointst;
 
   /// Collects the guards as \p localization_points up to \p failed_property_id
diff --git a/src/goto-checker/goto_symex_property_decider.h b/src/goto-checker/goto_symex_property_decider.h
index abc475be897..0e8cd1f54c9 100644
--- a/src/goto-checker/goto_symex_property_decider.h
+++ b/src/goto-checker/goto_symex_property_decider.h
@@ -37,10 +37,6 @@ class goto_symex_property_decidert
   /// Convert the instances of a property into a goal variable
   void convert_goals();
 
-  /// Prevent the solver to optimize-away the goal variables
-  /// (necessary for incremental solving)
-  void freeze_goal_variables();
-
   /// Add disjunction of negated selected properties to the equation
   void add_constraint_from_goals(
     std::function<bool(const irep_idt &property_id)> select_property);
diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp
index f30bc40cc63..7c7acedd20b 100644
--- a/src/solvers/prop/prop_conv.cpp
+++ b/src/solvers/prop/prop_conv.cpp
@@ -7,14 +7,3 @@ Author: Daniel Kroening, kroening@kroening.com
 \*******************************************************************/
 
 #include "prop_conv.h"
-
-#include "literal_expr.h"
-
-#include <util/std_expr.h>
-
-#include <algorithm>
-
-void prop_convt::set_assumptions(const bvt &)
-{
-  UNREACHABLE;
-}
diff --git a/src/solvers/prop/prop_conv.h b/src/solvers/prop/prop_conv.h
index 93ef7f65747..ecf8f57c425 100644
--- a/src/solvers/prop/prop_conv.h
+++ b/src/solvers/prop/prop_conv.h
@@ -10,32 +10,25 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_SOLVERS_PROP_PROP_CONV_H
 #define CPROVER_SOLVERS_PROP_PROP_CONV_H
 
-#include <solvers/decision_procedure.h>
-
-#include "literal.h"
+#include <solvers/stack_decision_procedure.h>
 
+class literalt;
 class tvt;
 
 // API that provides a "handle" in the form of a literalt
 // for expressions.
 
-class prop_convt:public decision_proceduret
+class prop_convt : public stack_decision_proceduret
 {
 public:
   virtual ~prop_convt() { }
 
-  using decision_proceduret::operator();
-
   /// Convert a Boolean expression and return the corresponding literal
   virtual literalt convert(const exprt &expr) = 0;
 
   /// Return value of literal \p l from satisfying assignment.
   /// Return tvt::UNKNOWN if not available
   virtual tvt l_get(literalt l) const = 0;
-
-  // incremental solving
-  virtual void set_assumptions(const bvt &_assumptions);
-  virtual bool has_set_assumptions() const { return false; }
 };
 
 #endif // CPROVER_SOLVERS_PROP_PROP_CONV_H
diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp
index 0b39a41b20f..09d038a0f88 100644
--- a/src/solvers/prop/prop_conv_solver.cpp
+++ b/src/solvers/prop/prop_conv_solver.cpp
@@ -365,7 +365,7 @@ bool prop_conv_solvert::set_equality_to_true(const equal_exprt &expr)
   return true;
 }
 
-void prop_conv_solvert::set_to(const exprt &expr, bool value)
+void prop_conv_solvert::add_constraints_to_prop(const exprt &expr, bool value)
 {
   PRECONDITION(expr.type().id() == ID_bool);
 
@@ -380,7 +380,7 @@ void prop_conv_solvert::set_to(const exprt &expr, bool value)
     {
       if(expr.operands().size() == 1)
       {
-        set_to(expr.op0(), !value);
+        add_constraints_to_prop(expr.op0(), !value);
         return;
       }
     }
@@ -393,7 +393,7 @@ void prop_conv_solvert::set_to(const exprt &expr, bool value)
         if(expr.id() == ID_and)
         {
           forall_operands(it, expr)
-            set_to_true(*it);
+            add_constraints_to_prop(*it, true);
 
           return;
         }
@@ -437,14 +437,14 @@ void prop_conv_solvert::set_to(const exprt &expr, bool value)
         {
           const implies_exprt &implies_expr = to_implies_expr(expr);
 
-          set_to_true(implies_expr.op0());
-          set_to_false(implies_expr.op1());
+          add_constraints_to_prop(implies_expr.op0(), true);
+          add_constraints_to_prop(implies_expr.op1(), false);
           return;
         }
         else if(expr.id() == ID_or) // !(a || b)  ==  (!a && !b)
         {
           forall_operands(it, expr)
-            set_to_false(*it);
+            add_constraints_to_prop(*it, false);
           return;
         }
       }
@@ -525,3 +525,52 @@ std::size_t prop_conv_solvert::get_number_of_solver_calls() const
 {
   return prop.get_number_of_solver_calls();
 }
+
+const char *prop_conv_solvert::context_prefix = "prop_conv::context$";
+
+void prop_conv_solvert::set_to(const exprt &expr, bool value)
+{
+  if(assumption_stack.empty())
+  {
+    // We are in the root context.
+    add_constraints_to_prop(expr, value);
+  }
+  else
+  {
+    // We have a child context. We add context_literal ==> expr to the formula.
+    add_constraints_to_prop(
+      or_exprt(literal_exprt(!assumption_stack.back()), expr), value);
+  }
+}
+
+void prop_conv_solvert::push(const std::vector<exprt> &assumptions)
+{
+  // We push the given assumptions as a single context onto the stack.
+  assumption_stack.reserve(assumption_stack.size() + assumptions.size());
+  for(const auto &assumption : assumptions)
+    assumption_stack.push_back(to_literal_expr(assumption).get_literal());
+  context_size_stack.push_back(assumptions.size());
+
+  prop.set_assumptions(assumption_stack);
+}
+
+void prop_conv_solvert::push()
+{
+  // We create a new context literal.
+  literalt context_literal = convert(symbol_exprt(
+    context_prefix + std::to_string(context_literal_counter++), bool_typet()));
+
+  assumption_stack.push_back(context_literal);
+  context_size_stack.push_back(1);
+
+  prop.set_assumptions(assumption_stack);
+}
+
+void prop_conv_solvert::pop()
+{
+  // We remove the context from the stack.
+  assumption_stack.resize(assumption_stack.size() - context_size_stack.back());
+  context_size_stack.pop_back();
+
+  prop.set_assumptions(assumption_stack);
+}
diff --git a/src/solvers/prop/prop_conv_solver.h b/src/solvers/prop/prop_conv_solver.h
index 13a320a1381..0bb5dfe6adf 100644
--- a/src/solvers/prop/prop_conv_solver.h
+++ b/src/solvers/prop/prop_conv_solver.h
@@ -37,7 +37,6 @@ class prop_conv_solvert : public conflict_providert,
   virtual ~prop_conv_solvert() = default;
 
   // overloading from decision_proceduret
-  void set_to(const exprt &expr, bool value) override;
   decision_proceduret::resultt dec_solve() override;
   void print_assignment(std::ostream &out) const override;
   std::string decision_procedure_text() const override
@@ -50,14 +49,6 @@ class prop_conv_solvert : public conflict_providert,
   {
     return prop.l_get(a);
   }
-  void set_assumptions(const bvt &_assumptions) override
-  {
-    prop.set_assumptions(_assumptions);
-  }
-  bool has_set_assumptions() const override
-  {
-    return prop.has_set_assumptions();
-  }
 
   exprt handle(const exprt &expr) override;
 
@@ -68,6 +59,18 @@ class prop_conv_solvert : public conflict_providert,
   literalt convert(const exprt &expr) override;
   bool is_in_conflict(const exprt &expr) const override;
 
+  /// For a Boolean expression \p expr, add the constraint
+  /// 'current_context => expr' if \p value is `true`,
+  /// otherwise add 'current_context => not expr'
+  void set_to(const exprt &expr, bool value) override;
+
+  void push() override;
+
+  /// Push \p assumptions in form of `literal_exprt`
+  void push(const std::vector<exprt> &assumptions) override;
+
+  void pop() override;
+
   // get literal for expression, if available
   bool literal(const symbol_exprt &expr, literalt &literal) const;
 
@@ -124,10 +127,26 @@ class prop_conv_solvert : public conflict_providert,
 
   virtual void ignoring(const exprt &expr);
 
-  // deliberately protected now to protect lower-level API
   propt &prop;
 
   messaget log;
+
+  static const char *context_prefix;
+
+  /// Assumptions on the stack
+  bvt assumption_stack;
+
+  /// To generate unique literal names for contexts
+  std::size_t context_literal_counter = 0;
+
+  /// `assumption_stack` is segmented in contexts;
+  /// Number of assumptions in each context on the stack
+  std::vector<size_t> context_size_stack;
+
+private:
+  /// Helper method used by `set_to` for adding the constraints to `prop`.
+  /// This method is private because it must not be used by derived classes.
+  void add_constraints_to_prop(const exprt &expr, bool value);
 };
 
 #endif // CPROVER_SOLVERS_PROP_PROP_CONV_SOLVER_H
diff --git a/src/solvers/prop/prop_minimize.cpp b/src/solvers/prop/prop_minimize.cpp
index eb3bf9e6f9c..93a1d521861 100644
--- a/src/solvers/prop/prop_minimize.cpp
+++ b/src/solvers/prop/prop_minimize.cpp
@@ -95,9 +95,6 @@ literalt prop_minimizet::constraint()
 /// Try to cover all objectives
 void prop_minimizet::operator()()
 {
-  // we need to use assumptions
-  PRECONDITION(prop_conv.has_set_assumptions());
-
   _iterations = 0;
   _number_satisfied = 0;
   _value = 0;
@@ -120,9 +117,7 @@ void prop_minimizet::operator()()
       {
         _iterations++;
 
-        bvt assumptions;
-        assumptions.push_back(c);
-        prop_conv.set_assumptions(assumptions);
+        prop_conv.push({literal_exprt{c}});
         dec_result = prop_conv();
 
         switch(dec_result)
@@ -150,8 +145,7 @@ void prop_minimizet::operator()()
     // We don't have a satisfying assignment to work with.
     // Run solver again to get one.
 
-    bvt assumptions; // no assumptions
-    prop_conv.set_assumptions(assumptions);
+    prop_conv.pop();
     (void)prop_conv();
   }
 }
diff --git a/src/solvers/prop/prop_minimize.h b/src/solvers/prop/prop_minimize.h
index de3d730398f..f9f3d682cd9 100644
--- a/src/solvers/prop/prop_minimize.h
+++ b/src/solvers/prop/prop_minimize.h
@@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/message.h>
 
+#include "literal.h"
 #include "prop_conv.h"
 
 /// Computes a satisfying assignment of minimal cost according to a const
diff --git a/src/solvers/refinement/bv_refinement.h b/src/solvers/refinement/bv_refinement.h
index 5761b1b9133..aef407a0ed9 100644
--- a/src/solvers/refinement/bv_refinement.h
+++ b/src/solvers/refinement/bv_refinement.h
@@ -57,8 +57,6 @@ class bv_refinementt:public bv_pointerst
   bvt convert_mod(const mod_exprt &expr) override;
   bvt convert_floatbv_op(const exprt &expr) override;
 
-  void set_assumptions(const bvt &_assumptions) override;
-
 private:
   // the list of operator approximations
   struct approximationt final
@@ -78,8 +76,8 @@ class bv_refinementt:public bv_pointerst
     bvt op0_bv, op1_bv, op2_bv, result_bv;
     mp_integer op0_value, op1_value, op2_value, result_value;
 
-    bvt under_assumptions;
-    bvt over_assumptions;
+    std::vector<exprt> under_assumptions;
+    std::vector<exprt> over_assumptions;
 
     // the kind of under- or over-approximation
     unsigned under_state, over_state;
@@ -108,7 +106,7 @@ class bv_refinementt:public bv_pointerst
 
   bool progress;
   std::list<approximationt> approximations;
-  bvt parent_assumptions;
+
 protected:
   // use gui format
   configt config_;
diff --git a/src/solvers/refinement/bv_refinement_loop.cpp b/src/solvers/refinement/bv_refinement_loop.cpp
index 474b56b0f86..c1ce82b9a82 100644
--- a/src/solvers/refinement/bv_refinement_loop.cpp
+++ b/src/solvers/refinement/bv_refinement_loop.cpp
@@ -87,7 +87,7 @@ decision_proceduret::resultt bv_refinementt::dec_solve()
 decision_proceduret::resultt bv_refinementt::prop_solve()
 {
   // this puts the underapproximations into effect
-  bvt assumptions=parent_assumptions;
+  std::vector<exprt> assumptions;
 
   for(const approximationt &approximation : approximations)
   {
@@ -101,9 +101,9 @@ decision_proceduret::resultt bv_refinementt::prop_solve()
       approximation.under_assumptions.end());
   }
 
-  prop.set_assumptions(assumptions);
+  push(assumptions);
   propt::resultt result=prop.prop_solve();
-  prop.set_assumptions(parent_assumptions);
+  pop();
 
   switch(result)
   {
@@ -132,9 +132,3 @@ void bv_refinementt::check_UNSAT()
   for(approximationt &approximation : this->approximations)
     check_UNSAT(approximation);
 }
-
-void bv_refinementt::set_assumptions(const bvt &_assumptions)
-{
-  parent_assumptions=_assumptions;
-  prop.set_assumptions(_assumptions);
-}
diff --git a/src/solvers/refinement/refine_arithmetic.cpp b/src/solvers/refinement/refine_arithmetic.cpp
index 05875f30da7..eae03360156 100644
--- a/src/solvers/refinement/refine_arithmetic.cpp
+++ b/src/solvers/refinement/refine_arithmetic.cpp
@@ -23,14 +23,14 @@ void bv_refinementt::approximationt::add_over_assumption(literalt l)
 {
   // if it's a constant already, give up
   if(!l.is_constant())
-    over_assumptions.push_back(l);
+    over_assumptions.push_back(literal_exprt(l));
 }
 
 void bv_refinementt::approximationt::add_under_assumption(literalt l)
 {
   // if it's a constant already, give up
   if(!l.is_constant())
-    under_assumptions.push_back(l);
+    under_assumptions.push_back(literal_exprt(l));
 }
 
 bvt bv_refinementt::convert_floatbv_op(const exprt &expr)
@@ -454,8 +454,13 @@ void bv_refinementt::check_UNSAT(approximationt &a)
 bool bv_refinementt::conflicts_with(approximationt &a)
 {
   for(std::size_t i=0; i<a.under_assumptions.size(); i++)
-    if(prop.is_in_conflict(a.under_assumptions[i]))
+  {
+    if(prop.is_in_conflict(
+         to_literal_expr(a.under_assumptions[i]).get_literal()))
+    {
       return true;
+    }
+  }
 
   return false;
 }
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 9d5bd0a8f0b..40b002f9d0c 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -104,10 +104,10 @@ void smt2_convt::write_footer(std::ostream &os)
   {
     os << "; assumptions\n";
 
-    forall_literals(it, assumptions)
+    for(const auto &assumption : assumptions)
     {
       os << "(assert ";
-      convert_literal(*it);
+      convert_literal(to_literal_expr(assumption).get_literal());
       os << ")"
          << "\n";
     }
@@ -690,6 +690,23 @@ void smt2_convt::convert_literal(const literalt l)
   }
 }
 
+void smt2_convt::push()
+{
+  UNIMPLEMENTED;
+}
+
+void smt2_convt::push(const std::vector<exprt> &_assumptions)
+{
+  INVARIANT(assumptions.empty(), "nested contexts are not supported");
+
+  assumptions = _assumptions;
+}
+
+void smt2_convt::pop()
+{
+  assumptions.clear();
+}
+
 std::string smt2_convt::convert_identifier(const irep_idt &identifier)
 {
   // Backslashes are disallowed in quoted symbols just for simplicity.
diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h
index 651ea66a83f..26f02603f12 100644
--- a/src/solvers/smt2/smt2_conv.h
+++ b/src/solvers/smt2/smt2_conv.h
@@ -123,10 +123,15 @@ class smt2_convt:public prop_convt
   }
   void print_assignment(std::ostream &out) const override;
   tvt l_get(literalt l) const override;
-  void set_assumptions(const bvt &bv) override
-  {
-    assumptions = bv;
-  }
+
+  /// Unimplemented
+  void push() override;
+
+  /// Currently, only implements a single stack element (no nested contexts)
+  void push(const std::vector<exprt> &_assumptions) override;
+
+  /// Currently, only implements a single stack element (no nested contexts)
+  void pop() override;
 
   void convert_expr(const exprt &);
   void convert_type(const typet &);
@@ -140,7 +145,7 @@ class smt2_convt:public prop_convt
   std::string benchmark, notes, logic;
   solvert solver;
 
-  bvt assumptions;
+  std::vector<exprt> assumptions;
   boolbv_widtht boolbv_width;
 
   std::size_t number_of_solver_calls = 0;
diff --git a/src/solvers/smt2/smt2_dec.h b/src/solvers/smt2/smt2_dec.h
index 611fb1725b9..e4745730f2a 100644
--- a/src/solvers/smt2/smt2_dec.h
+++ b/src/solvers/smt2/smt2_dec.h
@@ -42,12 +42,6 @@ class smt2_dect : protected smt2_stringstreamt,
   resultt dec_solve() override;
   std::string decision_procedure_text() const override;
 
-  // yes, we are incremental!
-  bool has_set_assumptions() const override
-  {
-    return true;
-  }
-
 protected:
   resultt read_result(std::istream &in);
 };
diff --git a/src/solvers/stack_decision_procedure.h b/src/solvers/stack_decision_procedure.h
new file mode 100644
index 00000000000..fa7983b84a5
--- /dev/null
+++ b/src/solvers/stack_decision_procedure.h
@@ -0,0 +1,81 @@
+/*******************************************************************\
+
+Module: Decision procedure with incremental solving with contexts
+        and assumptions
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Decision procedure with incremental solving with contexts
+/// and assumptions
+///
+/// Normally, solvers allow you only to add new conjuncts to the
+/// formula, but not to remove parts of the formula once added.
+///
+/// Solvers that offer pushing/popping of contexts or
+/// 'solving under assumptions' offer some ways to emulate
+/// removing parts of the formula.
+///
+/// Example 1: push/pop contexts:
+/// \code{.cpp}
+/// dp.set_to_true(a);     // added permanently
+/// resultt result = dp(); // solves formula 'a'
+/// stack_decision_procedure.set_to_true(b); // added permanently
+/// resultt result = dp(); // solves 'a && b'
+/// dp.push();
+/// dp.set_to_true(c);     // added inside a context: we can remove it later
+/// resultt result = dp(); // solves 'a && b && c'
+/// dp.pop();              // 'removes' c
+/// dp.push();
+/// dp.set_to_true(d);     // added inside a context: we can remove it later
+/// resultt result = dp(); // solves 'a && b && d'
+/// \endcode
+///
+/// Example 2: solving under assumptions:
+/// \code{.cpp}
+/// dp.set_to_true(a);     // added permanently
+/// resultt result = dp(); // solves formula 'a'
+/// h1 = dp.handle(c);
+/// h2 = dp.handle(d)
+/// dp.push({h1, h2});
+/// resultt result = dp(); // solves formula 'a && c && d'
+/// dp.pop();              // clear assumptions h1, h2
+/// h1 = dp.handle(not_exprt(c)); // get negated handle for 'c'
+/// dp.push({h1, h2});
+/// resultt result = dp(); // solves formula 'a && !c && d'
+/// \endcode
+
+#ifndef CPROVER_SOLVERS_STACK_DECISION_PROCEDURE_H
+#define CPROVER_SOLVERS_STACK_DECISION_PROCEDURE_H
+
+#include <vector>
+
+#include "decision_procedure.h"
+
+class stack_decision_proceduret : public decision_proceduret
+{
+public:
+  /// Pushes a new context on the stack that consists of the given
+  /// (possibly empty vector of) \p assumptions.
+  /// This context becomes a child context nested in the current context.
+  /// An assumption is usually obtained by calling
+  /// `decision_proceduret::handle`. Thus it can be a Boolean expression or
+  /// something more solver-specific such as `literal_exprt`.
+  /// An empty vector of assumptions counts as an element on the stack
+  /// (and therefore needs to be popped), but has no effect beyond that.
+  virtual void push(const std::vector<exprt> &assumptions) = 0;
+
+  /// Push a new context on the stack
+  /// This context becomes a child context nested in the current context.
+  virtual void push() = 0;
+
+  /// Pop whatever is on top of the stack.
+  /// Popping from the empty stack results in an invariant violation.
+  virtual void pop() = 0;
+
+  virtual ~stack_decision_proceduret() = default;
+};
+
+#endif // CPROVER_SOLVERS_STACK_DECISION_PROCEDURE_H