diff --git a/src/solvers/prop/prop.cpp b/src/solvers/prop/prop.cpp
index e09ca017474..fc8499bf58b 100644
--- a/src/solvers/prop/prop.cpp
+++ b/src/solvers/prop/prop.cpp
@@ -38,8 +38,15 @@ bvt propt::new_variables(std::size_t width)
 
 propt::resultt propt::prop_solve()
 {
+  static const bvt empty_assumptions;
   ++number_of_solver_calls;
-  return do_prop_solve();
+  return do_prop_solve(empty_assumptions);
+}
+
+propt::resultt propt::prop_solve(const bvt &assumptions)
+{
+  ++number_of_solver_calls;
+  return do_prop_solve(assumptions);
 }
 
 std::size_t propt::get_number_of_solver_calls() const
diff --git a/src/solvers/prop/prop.h b/src/solvers/prop/prop.h
index a2450e84470..dda20bfef39 100644
--- a/src/solvers/prop/prop.h
+++ b/src/solvers/prop/prop.h
@@ -84,9 +84,11 @@ class propt
   // They overload this to return false and thus avoid some optimisations
   virtual bool cnf_handled_well() const { return true; }
 
-  // assumptions
-  virtual void set_assumptions(const bvt &) { }
-  virtual bool has_set_assumptions() const { return false; }
+  // solving with assumptions
+  virtual bool has_assumptions() const
+  {
+    return false;
+  }
 
   // variables
   virtual literalt new_variable()=0;
@@ -98,6 +100,7 @@ class propt
   virtual std::string solver_text() const = 0;
   enum class resultt { P_SATISFIABLE, P_UNSATISFIABLE, P_ERROR };
   resultt prop_solve();
+  resultt prop_solve(const bvt &assumptions);
 
   // satisfying assignment
   virtual tvt l_get(literalt a) const=0;
@@ -122,7 +125,8 @@ class propt
   std::size_t get_number_of_solver_calls() const;
 
 protected:
-  virtual resultt do_prop_solve() = 0;
+  // solve under the given assumption
+  virtual resultt do_prop_solve(const bvt &assumptions) = 0;
 
   // to avoid a temporary for lcnf(...)
   bvt lcnf_bv;
diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp
index 49021dc5e46..b82ad7f342b 100644
--- a/src/solvers/prop/prop_conv_solver.cpp
+++ b/src/solvers/prop/prop_conv_solver.cpp
@@ -459,7 +459,7 @@ decision_proceduret::resultt prop_conv_solvert::dec_solve()
 
   log.statistics() << "Solving with " << prop.solver_text() << messaget::eom;
 
-  switch(prop.prop_solve())
+  switch(prop.prop_solve(assumption_stack))
   {
   case propt::resultt::P_SATISFIABLE:
     return resultt::D_SATISFIABLE;
@@ -531,8 +531,6 @@ void prop_conv_solvert::push(const std::vector<exprt> &assumptions)
   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()
@@ -543,8 +541,6 @@ void prop_conv_solvert::push()
 
   assumption_stack.push_back(context_literal);
   context_size_stack.push_back(1);
-
-  prop.set_assumptions(assumption_stack);
 }
 
 void prop_conv_solvert::pop()
@@ -552,8 +548,6 @@ 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);
 }
 
 // This method out-of-line because gcc-5.5.0-12ubuntu1 20171010 miscompiles it
diff --git a/src/solvers/refinement/bv_refinement_loop.cpp b/src/solvers/refinement/bv_refinement_loop.cpp
index 6db58bf898b..9d193280855 100644
--- a/src/solvers/refinement/bv_refinement_loop.cpp
+++ b/src/solvers/refinement/bv_refinement_loop.cpp
@@ -16,7 +16,7 @@ bv_refinementt::bv_refinementt(const infot &info)
     config_(info)
 {
   // check features we need
-  PRECONDITION(prop.has_set_assumptions());
+  PRECONDITION(prop.has_assumptions());
   PRECONDITION(prop.has_set_to());
   PRECONDITION(prop.has_is_in_conflict());
 }
@@ -102,7 +102,7 @@ decision_proceduret::resultt bv_refinementt::prop_solve()
   }
 
   push(assumptions);
-  propt::resultt result=prop.prop_solve();
+  propt::resultt result = prop.prop_solve(assumption_stack);
   pop();
 
   // clang-format off
diff --git a/src/solvers/sat/cnf_clause_list.h b/src/solvers/sat/cnf_clause_list.h
index f6ffee089b1..70c42ea6405 100644
--- a/src/solvers/sat/cnf_clause_list.h
+++ b/src/solvers/sat/cnf_clause_list.h
@@ -77,7 +77,7 @@ class cnf_clause_listt:public cnft
   }
 
 protected:
-  resultt do_prop_solve() override
+  resultt do_prop_solve(const bvt &) override
   {
     return resultt::P_ERROR;
   }
diff --git a/src/solvers/sat/dimacs_cnf.h b/src/solvers/sat/dimacs_cnf.h
index eb6bd91f99b..d938c7ce5ed 100644
--- a/src/solvers/sat/dimacs_cnf.h
+++ b/src/solvers/sat/dimacs_cnf.h
@@ -66,7 +66,7 @@ class dimacs_cnf_dumpt:public cnft
   }
 
 protected:
-  resultt do_prop_solve() override
+  resultt do_prop_solve(const bvt &) override
   {
     return resultt::P_ERROR;
   }
diff --git a/src/solvers/sat/external_sat.cpp b/src/solvers/sat/external_sat.cpp
index 17482139a54..bbda26ca8a5 100644
--- a/src/solvers/sat/external_sat.cpp
+++ b/src/solvers/sat/external_sat.cpp
@@ -36,7 +36,7 @@ void external_satt::set_assignment(literalt, bool)
   UNIMPLEMENTED;
 }
 
-void external_satt::write_cnf_file(std::string cnf_file)
+void external_satt::write_cnf_file(std::string cnf_file, const bvt &assumptions)
 {
   log.status() << "Writing temporary CNF" << messaget::eom;
   std::ofstream out(cnf_file);
@@ -167,7 +167,7 @@ external_satt::resultt external_satt::parse_result(std::string solver_output)
   return resultt::P_ERROR;
 }
 
-external_satt::resultt external_satt::do_prop_solve()
+external_satt::resultt external_satt::do_prop_solve(const bvt &assumptions)
 {
   // are we assuming 'false'?
   if(
@@ -179,7 +179,7 @@ external_satt::resultt external_satt::do_prop_solve()
 
   // create a temporary file
   temporary_filet cnf_file("external-sat", ".cnf");
-  write_cnf_file(cnf_file());
+  write_cnf_file(cnf_file(), assumptions);
   auto output = execute_solver(cnf_file());
   return parse_result(output);
 }
diff --git a/src/solvers/sat/external_sat.h b/src/solvers/sat/external_sat.h
index 5aa98825f61..418879170b9 100644
--- a/src/solvers/sat/external_sat.h
+++ b/src/solvers/sat/external_sat.h
@@ -12,7 +12,7 @@ class external_satt : public cnf_clause_list_assignmentt
 public:
   explicit external_satt(message_handlert &message_handler, std::string cmd);
 
-  bool has_set_assumptions() const override final
+  bool has_assumptions() const override final
   {
     return true;
   }
@@ -27,17 +27,11 @@ class external_satt : public cnf_clause_list_assignmentt
   bool is_in_conflict(literalt) const override;
   void set_assignment(literalt, bool) override;
 
-  void set_assumptions(const bvt &_assumptions) override
-  {
-    assumptions = _assumptions;
-  }
-
 protected:
   std::string solver_cmd;
-  bvt assumptions;
 
-  resultt do_prop_solve() override;
-  void write_cnf_file(std::string);
+  resultt do_prop_solve(const bvt &assumptions) override;
+  void write_cnf_file(std::string, const bvt &);
   std::string execute_solver(std::string);
   resultt parse_result(std::string);
 };
diff --git a/src/solvers/sat/pbs_dimacs_cnf.cpp b/src/solvers/sat/pbs_dimacs_cnf.cpp
index 8bf33eee15d..31b35862565 100644
--- a/src/solvers/sat/pbs_dimacs_cnf.cpp
+++ b/src/solvers/sat/pbs_dimacs_cnf.cpp
@@ -205,8 +205,10 @@ bool pbs_dimacs_cnft::pbs_solve()
   return satisfied;
 }
 
-propt::resultt pbs_dimacs_cnft::do_prop_solve()
+propt::resultt pbs_dimacs_cnft::do_prop_solve(const bvt &assumptions)
 {
+  PRECONDITION(assumptions.empty());
+
   std::ofstream file("temp.cnf");
 
   write_dimacs_cnf(file);
diff --git a/src/solvers/sat/pbs_dimacs_cnf.h b/src/solvers/sat/pbs_dimacs_cnf.h
index 9042ade923f..75827ab3607 100644
--- a/src/solvers/sat/pbs_dimacs_cnf.h
+++ b/src/solvers/sat/pbs_dimacs_cnf.h
@@ -58,7 +58,7 @@ class pbs_dimacs_cnft:public dimacs_cnft
   }
 
 protected:
-  resultt do_prop_solve() override;
+  resultt do_prop_solve(const bvt &assumptions) override;
 
   std::set<int> assigned;
 };
diff --git a/src/solvers/sat/satcheck_booleforce.cpp b/src/solvers/sat/satcheck_booleforce.cpp
index 1d4bef89750..2cd6e7c7c04 100644
--- a/src/solvers/sat/satcheck_booleforce.cpp
+++ b/src/solvers/sat/satcheck_booleforce.cpp
@@ -79,8 +79,9 @@ void satcheck_booleforce_baset::lcnf(const bvt &bv)
   clause_counter++;
 }
 
-propt::resultt satcheck_booleforce_baset::do_prop_solve()
+propt::resultt satcheck_booleforce_baset::do_prop_solve(const bvt &assumptions)
 {
+  PRECONDITION(assumptions.empty());
   PRECONDITION(status == SAT || status == INIT);
 
   int result=booleforce_sat();
diff --git a/src/solvers/sat/satcheck_booleforce.h b/src/solvers/sat/satcheck_booleforce.h
index 155918922b5..2cec6aa1a9f 100644
--- a/src/solvers/sat/satcheck_booleforce.h
+++ b/src/solvers/sat/satcheck_booleforce.h
@@ -26,7 +26,7 @@ class satcheck_booleforce_baset:public cnf_solvert
   void lcnf(const bvt &bv) override;
 
 protected:
-  resultt do_prop_solve() override;
+  resultt do_prop_solve(const bvt &assumptions) override;
 };
 
 class satcheck_booleforcet:public satcheck_booleforce_baset
diff --git a/src/solvers/sat/satcheck_cadical.cpp b/src/solvers/sat/satcheck_cadical.cpp
index bc1f9ffcbfd..26d1e07f4c0 100644
--- a/src/solvers/sat/satcheck_cadical.cpp
+++ b/src/solvers/sat/satcheck_cadical.cpp
@@ -85,7 +85,7 @@ void satcheck_cadicalt::lcnf(const bvt &bv)
   clause_counter++;
 }
 
-propt::resultt satcheck_cadicalt::do_prop_solve()
+propt::resultt satcheck_cadicalt::do_prop_solve(const bvt &assumptions)
 {
   INVARIANT(status != statust::ERROR, "there cannot be an error");
 
@@ -105,7 +105,8 @@ propt::resultt satcheck_cadicalt::do_prop_solve()
   }
 
   for(const auto &a : assumptions)
-    solver->assume(a.dimacs());
+    if(!a.is_true())
+      solver->assume(a.dimacs());
 
   switch(solver->solve())
   {
@@ -144,19 +145,6 @@ satcheck_cadicalt::~satcheck_cadicalt()
   delete solver;
 }
 
-void satcheck_cadicalt::set_assumptions(const bvt &bv)
-{
-  // We filter out 'true' assumptions which cause spurious results with CaDiCaL.
-  assumptions.clear();
-  for(const auto &assumption : bv)
-  {
-    if(!assumption.is_true())
-    {
-      assumptions.push_back(assumption);
-    }
-  }
-}
-
 bool satcheck_cadicalt::is_in_conflict(literalt a) const
 {
   return solver->failed(a.dimacs());
diff --git a/src/solvers/sat/satcheck_cadical.h b/src/solvers/sat/satcheck_cadical.h
index 0c9c708e315..d989d6a8705 100644
--- a/src/solvers/sat/satcheck_cadical.h
+++ b/src/solvers/sat/satcheck_cadical.h
@@ -31,8 +31,7 @@ class satcheck_cadicalt : public cnf_solvert, public hardness_collectort
   void lcnf(const bvt &bv) override;
   void set_assignment(literalt a, bool value) override;
 
-  void set_assumptions(const bvt &_assumptions) override;
-  bool has_set_assumptions() const override
+  bool has_assumptions() const override
   {
     return true;
   }
@@ -43,12 +42,10 @@ class satcheck_cadicalt : public cnf_solvert, public hardness_collectort
   bool is_in_conflict(literalt a) const override;
 
 protected:
-  resultt do_prop_solve() override;
+  resultt do_prop_solve(const bvt &assumptions) override;
 
   // NOLINTNEXTLINE(readability/identifiers)
-  CaDiCaL::Solver * solver;
-
-  bvt assumptions;
+  CaDiCaL::Solver *solver;
 };
 
 #endif // CPROVER_SOLVERS_SAT_SATCHECK_CADICAL_H
diff --git a/src/solvers/sat/satcheck_glucose.cpp b/src/solvers/sat/satcheck_glucose.cpp
index e3a2595d9bc..14bda00a080 100644
--- a/src/solvers/sat/satcheck_glucose.cpp
+++ b/src/solvers/sat/satcheck_glucose.cpp
@@ -32,6 +32,17 @@ void convert(const bvt &bv, Glucose::vec<Glucose::Lit> &dest)
   }
 }
 
+void convert_assumptions(const bvt &bv, Glucose::vec<Glucose::Lit> &dest)
+{
+  dest.capacity(bv.size());
+
+  for(const auto &literal : bv)
+  {
+    if(!literal.is_true())
+      dest.push(Glucose::mkLit(literal.var_no(), literal.sign()));
+  }
+}
+
 template<typename T>
 tvt satcheck_glucose_baset<T>::l_get(literalt a) const
 {
@@ -153,7 +164,7 @@ void satcheck_glucose_baset<T>::lcnf(const bvt &bv)
 }
 
 template <typename T>
-propt::resultt satcheck_glucose_baset<T>::do_prop_solve()
+propt::resultt satcheck_glucose_baset<T>::do_prop_solve(const bvt &assumptions)
 {
   PRECONDITION(status != statust::ERROR);
 
@@ -189,7 +200,7 @@ propt::resultt satcheck_glucose_baset<T>::do_prop_solve()
       else
       {
         Glucose::vec<Glucose::Lit> solver_assumptions;
-        convert(assumptions, solver_assumptions);
+        convert_assumptions(assumptions, solver_assumptions);
 
         if(solver->solve(solver_assumptions))
         {
@@ -262,18 +273,6 @@ bool satcheck_glucose_baset<T>::is_in_conflict(literalt a) const
   return false;
 }
 
-template<typename T>
-void satcheck_glucose_baset<T>::set_assumptions(const bvt &bv)
-{
-  assumptions=bv;
-
-  for(const auto &literal : assumptions)
-  {
-    INVARIANT(
-      !literal.is_constant(), "assumption literals must not be constant");
-  }
-}
-
 template class satcheck_glucose_baset<Glucose::Solver>;
 template class satcheck_glucose_baset<Glucose::SimpSolver>;
 
diff --git a/src/solvers/sat/satcheck_glucose.h b/src/solvers/sat/satcheck_glucose.h
index dbf3c5d32bc..8bb49800351 100644
--- a/src/solvers/sat/satcheck_glucose.h
+++ b/src/solvers/sat/satcheck_glucose.h
@@ -41,14 +41,11 @@ class satcheck_glucose_baset : public cnf_solvert, public hardness_collectort
   void lcnf(const bvt &bv) override;
   void set_assignment(literalt a, bool value) override;
 
-  // extra MiniSat feature: solve with assumptions
-  void set_assumptions(const bvt &_assumptions) override;
-
   // extra MiniSat feature: default branching decision
   void set_polarity(literalt a, bool value);
 
   bool is_in_conflict(literalt a) const override;
-  bool has_set_assumptions() const override
+  bool has_assumptions() const override
   {
     return true;
   }
@@ -58,12 +55,11 @@ class satcheck_glucose_baset : public cnf_solvert, public hardness_collectort
   }
 
 protected:
-  resultt do_prop_solve() override;
+  resultt do_prop_solve(const bvt &assumptions) override;
 
   std::unique_ptr<T> solver;
 
   void add_variables();
-  bvt assumptions;
 };
 
 class satcheck_glucose_no_simplifiert:
diff --git a/src/solvers/sat/satcheck_ipasir.cpp b/src/solvers/sat/satcheck_ipasir.cpp
index 98ed4d6e538..6a525523692 100644
--- a/src/solvers/sat/satcheck_ipasir.cpp
+++ b/src/solvers/sat/satcheck_ipasir.cpp
@@ -110,7 +110,7 @@ void satcheck_ipasirt::lcnf(const bvt &bv)
   clause_counter++;
 }
 
-propt::resultt satcheck_ipasirt::do_prop_solve()
+propt::resultt satcheck_ipasirt::do_prop_solve(const bvt &assumptions)
 {
   INVARIANT(status!=statust::ERROR, "there cannot be an error");
 
@@ -131,7 +131,7 @@ propt::resultt satcheck_ipasirt::do_prop_solve()
   {
     for(const auto &literal : assumptions)
     {
-      if(!literal.is_false())
+      if(!literal.is_true())
         ipasir_assume(solver, literal.dimacs());
     }
 
@@ -185,18 +185,4 @@ bool satcheck_ipasirt::is_in_conflict(literalt a) const
   return ipasir_failed(solver, a.var_no());
 }
 
-void satcheck_ipasirt::set_assumptions(const bvt &bv)
-{
-  bvt::const_iterator it = std::find_if(bv.begin(), bv.end(), is_true);
-  const bool has_true = it != bv.end();
-
-  if(has_true)
-  {
-    assumptions.clear();
-    return;
-  }
-  // only copy assertions, if there is no false in bt parameter
-  assumptions=bv;
-}
-
 #endif
diff --git a/src/solvers/sat/satcheck_ipasir.h b/src/solvers/sat/satcheck_ipasir.h
index e8bc4895d26..65e1741b902 100644
--- a/src/solvers/sat/satcheck_ipasir.h
+++ b/src/solvers/sat/satcheck_ipasir.h
@@ -34,10 +34,8 @@ class satcheck_ipasirt : public cnf_solvert, public hardness_collectort
   /* This method is not supported, and currently not called anywhere in CBMC */
   void set_assignment(literalt a, bool value) override;
 
-  void set_assumptions(const bvt &_assumptions) override;
-
   bool is_in_conflict(literalt a) const override;
-  bool has_set_assumptions() const override final
+  bool has_assumptions() const override final
   {
     return true;
   }
@@ -47,11 +45,9 @@ class satcheck_ipasirt : public cnf_solvert, public hardness_collectort
   }
 
 protected:
-  resultt do_prop_solve() override;
+  resultt do_prop_solve(const bvt &assumptions) override;
 
   void *solver;
-
-  bvt assumptions;
 };
 
 #endif // CPROVER_SOLVERS_SAT_SATCHECK_IPASIR_H
diff --git a/src/solvers/sat/satcheck_lingeling.cpp b/src/solvers/sat/satcheck_lingeling.cpp
index 5c24abc3291..41a86b64c66 100644
--- a/src/solvers/sat/satcheck_lingeling.cpp
+++ b/src/solvers/sat/satcheck_lingeling.cpp
@@ -63,7 +63,7 @@ void satcheck_lingelingt::lcnf(const bvt &bv)
   clause_counter++;
 }
 
-propt::resultt satcheck_lingelingt::do_prop_solve()
+propt::resultt satcheck_lingelingt::do_prop_solve(const bvt &assumptions)
 {
   PRECONDITION(status != ERROR);
 
@@ -78,7 +78,8 @@ propt::resultt satcheck_lingelingt::do_prop_solve()
   std::string msg;
 
   for(const auto &literal : assumptions)
-    lglassume(solver, literal.dimacs());
+    if(!literal.is_true())
+      lglassume(solver, literal.dimacs());
 
   const int res=lglsat(solver);
   CHECK_RETURN(res == 10 || res == 20);
@@ -117,18 +118,6 @@ satcheck_lingelingt::~satcheck_lingelingt()
   solver=0;
 }
 
-void satcheck_lingelingt::set_assumptions(const bvt &bv)
-{
-  assumptions=bv;
-
-  INVARIANT(
-    std::all_of(
-      assumptions.begin(),
-      assumptions.end(),
-      [](const literalt &l) { return !l.is_constant(); }),
-    "assumptions should be non-constant");
-}
-
 void satcheck_lingelingt::set_frozen(literalt a)
 {
   if(!a.is_constant())
diff --git a/src/solvers/sat/satcheck_lingeling.h b/src/solvers/sat/satcheck_lingeling.h
index 02eb1f4d5a5..368ed9c9569 100644
--- a/src/solvers/sat/satcheck_lingeling.h
+++ b/src/solvers/sat/satcheck_lingeling.h
@@ -27,8 +27,7 @@ class satcheck_lingelingt:public cnf_solvert
   void lcnf(const bvt &bv) override;
   void set_assignment(literalt a, bool value) override;
 
-  void set_assumptions(const bvt &_assumptions) override;
-  bool has_set_assumptions() const override
+  bool has_assumptions() const override
   {
     return true;
   }
@@ -40,11 +39,10 @@ class satcheck_lingelingt:public cnf_solvert
   void set_frozen(literalt a) override;
 
 protected:
-  resultt do_prop_solve() override;
+  resultt do_prop_solve(const bvt &assumptions) override;
 
   // NOLINTNEXTLINE(readability/identifiers)
-  struct LGL * solver;
-  bvt assumptions;
+  struct LGL *solver;
 };
 
 #endif // CPROVER_SOLVERS_SAT_SATCHECK_LINGELING_H
diff --git a/src/solvers/sat/satcheck_minisat.cpp b/src/solvers/sat/satcheck_minisat.cpp
index 34d3fa7c684..bafacd17434 100644
--- a/src/solvers/sat/satcheck_minisat.cpp
+++ b/src/solvers/sat/satcheck_minisat.cpp
@@ -150,7 +150,7 @@ void satcheck_minisat1_baset::lcnf(const bvt &bv)
   clause_counter++;
 }
 
-propt::resultt satcheck_minisat1_baset::do_prop_solve()
+propt::resultt satcheck_minisat1_baset::do_prop_solve(const bvt &assumptions)
 {
   PRECONDITION(status != ERROR);
 
@@ -214,16 +214,6 @@ bool satcheck_minisat1_baset::is_in_conflict(literalt a) const
   return false;
 }
 
-void satcheck_minisat1_baset::set_assumptions(const bvt &bv)
-{
-  assumptions=bv;
-
-  for(bvt::const_iterator it=assumptions.begin();
-      it!=assumptions.end();
-      it++)
-    INVARIANT(!it->is_constant(), "assumptions should be non-constant");
-}
-
 satcheck_minisat1t::satcheck_minisat1t()
 {
   empty_clause_added=false;
@@ -262,11 +252,11 @@ std::string satcheck_minisat1_prooft::solver_text() const
   return "MiniSAT + Proof";
 }
 
-propt::resultt satcheck_minisat1_coret::do_prop_solve()
+propt::resultt satcheck_minisat1_coret::do_prop_solve(const bvt &assumptions)
 {
   propt::resultt r;
 
-  r = satcheck_minisat1_prooft::do_prop_solve();
+  r = satcheck_minisat1_prooft::do_prop_solve(assumptions);
 
   if(status==UNSAT)
   {
diff --git a/src/solvers/sat/satcheck_minisat.h b/src/solvers/sat/satcheck_minisat.h
index 672ad77f797..6af0a685bb2 100644
--- a/src/solvers/sat/satcheck_minisat.h
+++ b/src/solvers/sat/satcheck_minisat.h
@@ -31,11 +31,8 @@ class satcheck_minisat1_baset:public cnf_solvert
 
   void set_assignment(literalt a, bool value) override;
 
-  // extra MiniSat feature: solve with assumptions
-  void set_assumptions(const bvt &_assumptions) override;
-
   // features
-  bool has_set_assumptions() const override
+  bool has_assumptions() const override
   {
     return true;
   }
@@ -47,12 +44,11 @@ class satcheck_minisat1_baset:public cnf_solvert
   bool is_in_conflict(literalt l) const override;
 
 protected:
-  resultt do_prop_solve() override;
+  resultt do_prop_solve(const bvt &assumptions) override;
 
   // NOLINTNEXTLINE(readability/identifiers)
   class Solver *solver;
   void add_variables();
-  bvt assumptions;
   bool empty_clause_added;
 };
 
@@ -100,6 +96,6 @@ class satcheck_minisat1_coret:public satcheck_minisat1_prooft
 protected:
   std::vector<bool> in_core;
 
-  resultt do_prop_solve() override;
+  resultt do_prop_solve(const bvt &assumptions) override;
 };
 #endif // CPROVER_SOLVERS_SAT_SATCHECK_MINISAT_H
diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp
index 9815d86046c..2c9799cc700 100644
--- a/src/solvers/sat/satcheck_minisat2.cpp
+++ b/src/solvers/sat/satcheck_minisat2.cpp
@@ -39,6 +39,20 @@ void convert(const bvt &bv, Minisat::vec<Minisat::Lit> &dest)
   }
 }
 
+void convert_assumptions(const bvt &bv, Minisat::vec<Minisat::Lit> &dest)
+{
+  PRECONDITION(
+    bv.size() <= static_cast<std::size_t>(std::numeric_limits<int>::max()));
+  dest.capacity(static_cast<int>(bv.size()));
+
+  for(const auto &literal : bv)
+  {
+    // when converting assumptions, ignore 'true'
+    if(!literal.is_true())
+      dest.push(Minisat::mkLit(literal.var_no(), literal.sign()));
+  }
+}
+
 template<typename T>
 tvt satcheck_minisat2_baset<T>::l_get(literalt a) const
 {
@@ -186,7 +200,7 @@ static void interrupt_solver(int signum)
 #endif
 
 template <typename T>
-propt::resultt satcheck_minisat2_baset<T>::do_prop_solve()
+propt::resultt satcheck_minisat2_baset<T>::do_prop_solve(const bvt &assumptions)
 {
   PRECONDITION(status != statust::ERROR);
 
@@ -218,7 +232,7 @@ propt::resultt satcheck_minisat2_baset<T>::do_prop_solve()
     }
 
     Minisat::vec<Minisat::Lit> solver_assumptions;
-    convert(assumptions, solver_assumptions);
+    convert_assumptions(assumptions, solver_assumptions);
 
     using Minisat::lbool;
 
@@ -331,21 +345,6 @@ bool satcheck_minisat2_baset<T>::is_in_conflict(literalt a) const
   return false;
 }
 
-template<typename T>
-void satcheck_minisat2_baset<T>::set_assumptions(const bvt &bv)
-{
-  // We filter out 'true' assumptions which cause an assertion violation
-  // in Minisat2.
-  assumptions.clear();
-  for(const auto &assumption : bv)
-  {
-    if(!assumption.is_true())
-    {
-      assumptions.push_back(assumption);
-    }
-  }
-}
-
 template class satcheck_minisat2_baset<Minisat::Solver>;
 template class satcheck_minisat2_baset<Minisat::SimpSolver>;
 
diff --git a/src/solvers/sat/satcheck_minisat2.h b/src/solvers/sat/satcheck_minisat2.h
index 6c3cfc62a09..1aa2280feb8 100644
--- a/src/solvers/sat/satcheck_minisat2.h
+++ b/src/solvers/sat/satcheck_minisat2.h
@@ -43,9 +43,6 @@ class satcheck_minisat2_baset : public cnf_solvert, public hardness_collectort
   void lcnf(const bvt &bv) override final;
   void set_assignment(literalt a, bool value) override;
 
-  // extra MiniSat feature: solve with assumptions
-  void set_assumptions(const bvt &_assumptions) override;
-
   // extra MiniSat feature: default branching decision
   void set_polarity(literalt a, bool value);
 
@@ -56,7 +53,7 @@ class satcheck_minisat2_baset : public cnf_solvert, public hardness_collectort
   void clear_interrupt();
 
   bool is_in_conflict(literalt a) const override;
-  bool has_set_assumptions() const override final
+  bool has_assumptions() const override final
   {
     return true;
   }
@@ -71,13 +68,12 @@ class satcheck_minisat2_baset : public cnf_solvert, public hardness_collectort
   }
 
 protected:
-  resultt do_prop_solve() override;
+  resultt do_prop_solve(const bvt &) override;
 
   std::unique_ptr<T> solver;
   uint32_t time_limit_seconds;
 
   void add_variables();
-  bvt assumptions;
 };
 
 class satcheck_minisat_no_simplifiert:
diff --git a/src/solvers/sat/satcheck_picosat.cpp b/src/solvers/sat/satcheck_picosat.cpp
index 88c027edc9d..955aae03478 100644
--- a/src/solvers/sat/satcheck_picosat.cpp
+++ b/src/solvers/sat/satcheck_picosat.cpp
@@ -65,7 +65,7 @@ void satcheck_picosatt::lcnf(const bvt &bv)
   clause_counter++;
 }
 
-propt::resultt satcheck_picosatt::do_prop_solve()
+propt::resultt satcheck_picosatt::do_prop_solve(const bvt &assumptions)
 {
   PRECONDITION(status != ERROR);
 
@@ -79,7 +79,8 @@ propt::resultt satcheck_picosatt::do_prop_solve()
   std::string msg;
 
   for(const auto &literal : assumptions)
-    picosat_assume(picosat, literal.dimacs());
+    if(!literal.is_true())
+      picosat_assume(picosat, literal.dimacs());
 
   const int res=picosat_sat(picosat, -1);
   if(res==PICOSAT_SATISFIABLE)
@@ -123,15 +124,3 @@ bool satcheck_picosatt::is_in_conflict(literalt a) const
 
   return picosat_failed_assumption(picosat, a.dimacs())!=0;
 }
-
-void satcheck_picosatt::set_assumptions(const bvt &bv)
-{
-  assumptions=bv;
-
-  INVARIANT(
-    std::all_of(
-      assumptions.begin(),
-      assumptions.end(),
-      [](const literalt &l) { return !l.is_constant(); }),
-    "assumptions should be non-constant");
-}
diff --git a/src/solvers/sat/satcheck_picosat.h b/src/solvers/sat/satcheck_picosat.h
index aa30db94e22..0ebf2e7cfa3 100644
--- a/src/solvers/sat/satcheck_picosat.h
+++ b/src/solvers/sat/satcheck_picosat.h
@@ -28,8 +28,7 @@ class satcheck_picosatt:public cnf_solvert
   void set_assignment(literalt a, bool value) override;
 
   bool is_in_conflict(literalt a) const override;
-  void set_assumptions(const bvt &_assumptions) override;
-  bool has_set_assumptions() const override
+  bool has_assumptions() const override
   {
     return true;
   }
@@ -39,9 +38,7 @@ class satcheck_picosatt:public cnf_solvert
   }
 
 protected:
-  resultt do_prop_solve() override;
-
-  bvt assumptions;
+  resultt do_prop_solve(const bvt &assumptions) override;
 
 private:
   PicoSAT *picosat;
diff --git a/src/solvers/sat/satcheck_zchaff.cpp b/src/solvers/sat/satcheck_zchaff.cpp
index 4bf5163839a..1b84ebf233c 100644
--- a/src/solvers/sat/satcheck_zchaff.cpp
+++ b/src/solvers/sat/satcheck_zchaff.cpp
@@ -70,9 +70,10 @@ void satcheck_zchaff_baset::copy_cnf()
       reinterpret_cast<int*>(&((*it)[0])), it->size());
 }
 
-propt::resultt satcheck_zchaff_baset::do_prop_solve()
+propt::resultt satcheck_zchaff_baset::do_prop_solve(const bvt &assumptions)
 {
   // this is *not* incremental
+  PRECONDITION(assumptions.empty());
   PRECONDITION(status == INIT);
 
   copy_cnf();
diff --git a/src/solvers/sat/satcheck_zchaff.h b/src/solvers/sat/satcheck_zchaff.h
index 13b36f1b9fe..7b061815994 100644
--- a/src/solvers/sat/satcheck_zchaff.h
+++ b/src/solvers/sat/satcheck_zchaff.h
@@ -35,7 +35,7 @@ class satcheck_zchaff_baset:public cnf_clause_listt
   }
 
 protected:
-  resultt do_prop_solve() override;
+  resultt do_prop_solve(const bvt &assumptions) override;
 
   CSolver *solver;
 
diff --git a/src/solvers/sat/satcheck_zcore.cpp b/src/solvers/sat/satcheck_zcore.cpp
index 711092efdb2..833bc4506d7 100644
--- a/src/solvers/sat/satcheck_zcore.cpp
+++ b/src/solvers/sat/satcheck_zcore.cpp
@@ -34,8 +34,10 @@ std::string satcheck_zcoret::solver_text() const
   return "ZCore";
 }
 
-propt::resultt satcheck_zcoret::do_prop_solve()
+propt::resultt satcheck_zcoret::do_prop_solve(const bvt &assumptions)
 {
+  PRECONDITION(assumptions.empty());
+
   // We start counting at 1, thus there is one variable fewer.
   {
     std::string msg=
diff --git a/src/solvers/sat/satcheck_zcore.h b/src/solvers/sat/satcheck_zcore.h
index bf0655f6b7c..175c92d033f 100644
--- a/src/solvers/sat/satcheck_zcore.h
+++ b/src/solvers/sat/satcheck_zcore.h
@@ -29,7 +29,7 @@ class satcheck_zcoret:public dimacs_cnft
   }
 
 protected:
-  resultt do_prop_solve() override;
+  resultt do_prop_solve(const bvt &assumptions) override;
 
   std::set<unsigned> in_core;
 };
diff --git a/unit/solvers/bdd/miniBDD/miniBDD.cpp b/unit/solvers/bdd/miniBDD/miniBDD.cpp
index a814b79a183..18d3d5ede06 100644
--- a/unit/solvers/bdd/miniBDD/miniBDD.cpp
+++ b/unit/solvers/bdd/miniBDD/miniBDD.cpp
@@ -152,7 +152,7 @@ class bdd_propt : public propt
     return "BDDs";
   }
 
-  resultt do_prop_solve() override
+  resultt do_prop_solve(const bvt &) override
   {
     UNREACHABLE;
     return {};
diff --git a/unit/solvers/sat/satcheck_cadical.cpp b/unit/solvers/sat/satcheck_cadical.cpp
index e2a170bc375..169b5104414 100644
--- a/unit/solvers/sat/satcheck_cadical.cpp
+++ b/unit/solvers/sat/satcheck_cadical.cpp
@@ -35,8 +35,8 @@ SCENARIO("satcheck_cadical", "[core][solvers][sat][satcheck_cadical]")
     {
       bvt assumptions;
       assumptions.push_back(const_literal(false));
-      satcheck.set_assumptions(assumptions);
-      REQUIRE(satcheck.prop_solve() == propt::resultt::P_UNSATISFIABLE);
+      REQUIRE(
+        satcheck.prop_solve(assumptions) == propt::resultt::P_UNSATISFIABLE);
     }
   }
 
@@ -63,22 +63,22 @@ SCENARIO("satcheck_cadical", "[core][solvers][sat][satcheck_cadical]")
     {
       bvt assumptions;
       assumptions.push_back(a);
-      satcheck.set_assumptions(assumptions);
-      REQUIRE(satcheck.prop_solve() == propt::resultt::P_UNSATISFIABLE);
+      REQUIRE(
+        satcheck.prop_solve(assumptions) == propt::resultt::P_UNSATISFIABLE);
     }
     THEN("is still unsatisfiable under assumption a and true")
     {
       bvt assumptions;
       assumptions.push_back(const_literal(true));
       assumptions.push_back(a);
-      satcheck.set_assumptions(assumptions);
-      REQUIRE(satcheck.prop_solve() == propt::resultt::P_UNSATISFIABLE);
+      REQUIRE(
+        satcheck.prop_solve(assumptions) == propt::resultt::P_UNSATISFIABLE);
     }
     THEN("becomes satisfiable when assumption a is lifted")
     {
       bvt assumptions;
-      satcheck.set_assumptions(assumptions);
-      REQUIRE(satcheck.prop_solve() == propt::resultt::P_SATISFIABLE);
+      REQUIRE(
+        satcheck.prop_solve(assumptions) == propt::resultt::P_SATISFIABLE);
     }
   }
 }
diff --git a/unit/solvers/sat/satcheck_minisat2.cpp b/unit/solvers/sat/satcheck_minisat2.cpp
index 3e78202356e..55c7cd209d1 100644
--- a/unit/solvers/sat/satcheck_minisat2.cpp
+++ b/unit/solvers/sat/satcheck_minisat2.cpp
@@ -36,8 +36,8 @@ SCENARIO("satcheck_minisat2", "[core][solvers][sat][satcheck_minisat2]")
     {
       bvt assumptions;
       assumptions.push_back(const_literal(false));
-      satcheck.set_assumptions(assumptions);
-      REQUIRE(satcheck.prop_solve() == propt::resultt::P_UNSATISFIABLE);
+      REQUIRE(
+        satcheck.prop_solve(assumptions) == propt::resultt::P_UNSATISFIABLE);
     }
   }
 
@@ -64,22 +64,22 @@ SCENARIO("satcheck_minisat2", "[core][solvers][sat][satcheck_minisat2]")
     {
       bvt assumptions;
       assumptions.push_back(a);
-      satcheck.set_assumptions(assumptions);
-      REQUIRE(satcheck.prop_solve() == propt::resultt::P_UNSATISFIABLE);
+      REQUIRE(
+        satcheck.prop_solve(assumptions) == propt::resultt::P_UNSATISFIABLE);
     }
     THEN("is still unsatisfiable under assumption a and true")
     {
       bvt assumptions;
       assumptions.push_back(const_literal(true));
       assumptions.push_back(a);
-      satcheck.set_assumptions(assumptions);
-      REQUIRE(satcheck.prop_solve() == propt::resultt::P_UNSATISFIABLE);
+      REQUIRE(
+        satcheck.prop_solve(assumptions) == propt::resultt::P_UNSATISFIABLE);
     }
     THEN("becomes satisfiable when assumption a is lifted")
     {
       bvt assumptions;
-      satcheck.set_assumptions(assumptions);
-      REQUIRE(satcheck.prop_solve() == propt::resultt::P_SATISFIABLE);
+      REQUIRE(
+        satcheck.prop_solve(assumptions) == propt::resultt::P_SATISFIABLE);
     }
   }
 }