Avoid using ProofManager in non-proof CMS build (#2814)

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.

1 files changed, 16 insertions, 6 deletions

diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index c04fb8b56..970ba13cf 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -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;