From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 23 Jan 2019 18:08:11 +0000 (-0800)
Subject: Avoid using ProofManager in non-proof CMS build (#2814)
X-Git-Tag: cvc5-1.0.0~4271
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=495787793b07a05f384824c92eef4e26d92228fc;p=cvc5.git

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.
---

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;