5 files changed, 39 insertions, 6 deletions
diff --git a/cmake/ConfigureCVC4.cmake b/cmake/ConfigureCVC4.cmake
index 67c1f414d..cdf8e4d9a 100644
--- a/cmake/ConfigureCVC4.cmake
+++ b/cmake/ConfigureCVC4.cmake
@@ -67,6 +67,20 @@ check_symbol_exists(sigaltstack "signal.h" HAVE_SIGALTSTACK)
 check_symbol_exists(strerror_r "string.h" HAVE_STRERROR_R)
 check_symbol_exists(strtok_r "string.h" HAVE_STRTOK_R)
 
+# Check whether the verison of CaDiCaL used supports incremental solving
+if(USE_CADICAL)
+  check_cxx_source_compiles(
+    "
+    #include <${CaDiCaL_HOME}/src/cadical.hpp>
+    int main() { return sizeof(&CaDiCaL::Solver::assume); }
+    "
+    CVC4_INCREMENTAL_CADICAL
+  )
+  if(CVC4_INCREMENTAL_CADICAL)
+    add_definitions(-DCVC4_INCREMENTAL_CADICAL)
+  endif()
+endif()
+
 # Determine if we have the POSIX (int) or GNU (char *) variant of strerror_r.
 check_c_source_compiles(
   "
diff --git a/contrib/run-script-smtcomp2019-application b/contrib/run-script-smtcomp2019-application
index 58db84d36..a7d4d985c 100755
--- a/contrib/run-script-smtcomp2019-application
+++ b/contrib/run-script-smtcomp2019-application
@@ -44,7 +44,7 @@ QF_AUFLIA)
   runcvc4 --no-arrays-eager-index --arrays-eager-lemmas --incremental
   ;;
 QF_BV)
-  runcvc4 --tear-down-incremental=4 --bv-eq-slicer=auto --bv-div-zero-const --bv-intro-pow2
+  runcvc4 --incremental --bitblast=eager --bv-sat-solver=cadical
   ;;
 QF_LIA)
   runcvc4 --tear-down-incremental=1 --unconstrained-simp
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 2a59ace11..5e98f8f5a 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -1175,14 +1175,16 @@ theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option,
   }
   else if (optarg == "cadical")
   {
+#ifndef CVC4_INCREMENTAL_CADICAL
     if (options::incrementalSolving()
         && options::incrementalSolving.wasSetByUser())
     {
-      throw OptionException(
-          std::string("CaDiCaL does not support incremental mode. \n\
-                         Try --bv-sat-solver=cryptominisat or "
-                      "--bv-sat-solver=minisat"));
+      throw OptionException(std::string(
+          "CaDiCaL version used does not support incremental mode. \n\
+                       Update CaDiCal or Try --bv-sat-solver=cryptominisat or "
+          "--bv-sat-solver=minisat"));
     }
+#endif
 
     if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY
         && options::bitblastMode.wasSetByUser())
diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
index 5a0968ec8..b4851f945 100644
--- a/src/prop/cadical.cpp
+++ b/src/prop/cadical.cpp
@@ -117,6 +117,23 @@ SatValue CadicalSolver::solve(long unsigned int&)
   Unimplemented("Setting limits for CaDiCaL not supported yet");
 };
 
+SatValue CadicalSolver::solve(const std::vector<SatLiteral>& assumptions)
+{
+#ifdef CVC4_INCREMENTAL_CADICAL
+  TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
+  for (const SatLiteral& lit : assumptions)
+  {
+    d_solver->assume(toCadicalLit(lit));
+  }
+  SatValue res = toSatValue(d_solver->solve());
+  d_okay = (res == SAT_VALUE_TRUE);
+  ++d_statistics.d_numSatCalls;
+  return res;
+#else
+  Unimplemented("CaDiCaL version used does not support incremental solving");
+#endif
+}
+
 void CadicalSolver::interrupt() { d_solver->terminate(); }
 
 SatValue CadicalSolver::value(SatLiteral l)
diff --git a/src/prop/cadical.h b/src/prop/cadical.h
index e43a2d278..6ab0c2850 100644
--- a/src/prop/cadical.h
+++ b/src/prop/cadical.h
@@ -48,8 +48,8 @@ class CadicalSolver : public SatSolver
   SatVariable falseVar() override;
 
   SatValue solve() override;
-
   SatValue solve(long unsigned int&) override;
+  SatValue solve(const std::vector<SatLiteral>& assumptions) override;
 
   void interrupt() override;