Avoid using ProofManager in non-proof CMS build (#2814)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 23 Jan 2019 18:08:11 +0000 (10:08 -0800)
committerGitHub <noreply@github.com>
Wed, 23 Jan 2019 18:08:11 +0000 (10:08 -0800)
PR #2786 changed `CryptoMinisatSolver::addClause()` to register clauses
with the bit-vector proof if proofs are turned on. The new code
requested the `ProofManager` even when proofs were turned off, which
made the `eager-inc-cryptominisat.smt2` regression and our nightlies
fail. This commit guards the access to the `ProofManager`, restoring the
semantics of the original code when proofs are turned off.

src/prop/cryptominisat.cpp

index c04fb8b56f29cb2e69572ab4c7f6bae032fb627e..970ba13cf9bc6f4ab68541e4c3145a71d215704d 100644 (file)
@@ -119,13 +119,23 @@ ClauseId CryptoMinisatSolver::addClause(SatClause& clause, bool removable){
   std::vector<CMSat::Lit> internal_clause;
   toInternalClause(clause, internal_clause);
   bool nowOkay = d_solver->add_clause(internal_clause);
-  ClauseId freshId = ClauseId(ProofManager::currentPM()->nextId());
 
-  THEORY_PROOF(
-      // If this clause results in a conflict, then `nowOkay` may be false, but
-      // we still need to register this clause as used. Thus, we look at
-      // `d_okay` instead
-      if (d_bvp && d_okay) { d_bvp->registerUsedClause(freshId, clause); })
+  ClauseId freshId;
+  if (THEORY_PROOF_ON())
+  {
+    freshId = ClauseId(ProofManager::currentPM()->nextId());
+    // If this clause results in a conflict, then `nowOkay` may be false, but
+    // we still need to register this clause as used. Thus, we look at
+    // `d_okay` instead
+    if (d_bvp && d_okay)
+    {
+      d_bvp->registerUsedClause(freshId, clause);
+    }
+  }
+  else
+  {
+    freshId = ClauseIdError;
+  }
 
   d_okay &= nowOkay;
   return freshId;