3 files changed, 23 insertions, 8 deletions
diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
index b3563bf28..0324f8128 100644
--- a/src/prop/cadical.cpp
+++ b/src/prop/cadical.cpp
@@ -61,6 +61,7 @@ CadicalSolver::CadicalSolver(StatisticsRegistry* registry,
       // Note: CaDiCaL variables start with index 1 rather than 0 since negated
       //       literals are represented as the negation of the index.
       d_nextVarIdx(1),
+      d_inSatMode(false),
       d_statistics(registry, name)
 {
 }
@@ -111,10 +112,10 @@ SatVariable CadicalSolver::falseVar() { return d_false; }
 
 SatValue CadicalSolver::solve()
 {
-  d_assumptions.clear();
   TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
+  d_assumptions.clear();
   SatValue res = toSatValue(d_solver->solve());
-  d_okay = (res == SAT_VALUE_TRUE);
+  d_inSatMode = (res == SAT_VALUE_TRUE);
   ++d_statistics.d_numSatCalls;
   return res;
 }
@@ -126,19 +127,25 @@ SatValue CadicalSolver::solve(long unsigned int&)
 
 SatValue CadicalSolver::solve(const std::vector<SatLiteral>& assumptions)
 {
-  d_assumptions.clear();
   TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
+  d_assumptions.clear();
   for (const SatLiteral& lit : assumptions)
   {
     d_solver->assume(toCadicalLit(lit));
     d_assumptions.push_back(lit);
   }
   SatValue res = toSatValue(d_solver->solve());
-  d_okay = (res == SAT_VALUE_TRUE);
+  d_inSatMode = (res == SAT_VALUE_TRUE);
   ++d_statistics.d_numSatCalls;
   return res;
 }
 
+bool CadicalSolver::setPropagateOnly()
+{
+  d_solver->limit("decisions", 0); /* Gets reset after next solve() call. */
+  return true;
+}
+
 void CadicalSolver::getUnsatAssumptions(std::vector<SatLiteral>& assumptions)
 {
   for (const SatLiteral& lit : d_assumptions)
@@ -154,13 +161,13 @@ void CadicalSolver::interrupt() { d_solver->terminate(); }
 
 SatValue CadicalSolver::value(SatLiteral l)
 {
-  Assert(d_okay);
+  Assert(d_inSatMode);
   return toSatValueLit(d_solver->val(toCadicalLit(l)));
 }
 
 SatValue CadicalSolver::modelValue(SatLiteral l)
 {
-  Assert(d_okay);
+  Assert(d_inSatMode);
   return value(l);
 }
 
@@ -169,7 +176,7 @@ unsigned CadicalSolver::getAssertionLevel() const
   Unreachable() << "CaDiCaL does not support assertion levels.";
 }
 
-bool CadicalSolver::ok() const { return d_okay; }
+bool CadicalSolver::ok() const { return d_inSatMode; }
 
 CadicalSolver::Statistics::Statistics(StatisticsRegistry* registry,
                                       const std::string& prefix)
diff --git a/src/prop/cadical.h b/src/prop/cadical.h
index 6a7258091..f8b2d3bcd 100644
--- a/src/prop/cadical.h
+++ b/src/prop/cadical.h
@@ -50,6 +50,7 @@ class CadicalSolver : public SatSolver
   SatValue solve() override;
   SatValue solve(long unsigned int&) override;
   SatValue solve(const std::vector<SatLiteral>& assumptions) override;
+  bool setPropagateOnly() override;
   void getUnsatAssumptions(std::vector<SatLiteral>& assumptions) override;
 
   void interrupt() override;
@@ -82,7 +83,7 @@ class CadicalSolver : public SatSolver
   std::vector<SatLiteral> d_assumptions;
 
   unsigned d_nextVarIdx;
-  bool d_okay;
+  bool d_inSatMode;
   SatVariable d_true;
   SatVariable d_false;
 
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 896233f41..d421155ae 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -81,6 +81,13 @@ public:
     return SAT_VALUE_UNKNOWN;
   };
 
+  /**
+   * Tell SAT solver to only do propagation on next solve().
+   *
+   * @return true if feature is supported, otherwise false.
+   */
+  virtual bool setPropagateOnly() { return false; }
+
   /** Interrupt the solver */
   virtual void interrupt() = 0;