Fix spurious checks to closed proofs (#7484)

This leads to issues when (1) proofs are enabled, (2) unsat cores are enabled and full proofs are disabled in a subsolver.

This is the case for the abduction algorithm that uses unsat core learning, when proofs are explicitly enabled. This led to spurious assertion failures when testing proof new.

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 0f3260920bc7e07b9c233e577032fda1422f473f..ee1528f4d67718288d45eae2f266a50f78561804 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1428,14 +1428,14 @@ void TheoryEngine::conflict(TrustNode tconflict, TheoryId theoryId)
 
     // Process the explanation
     TrustNode tncExp = getExplanation(vec);
-    Trace("te-proof-debug")
-        << "Check closed conflict explained with sharing" << std::endl;
-    tncExp.debugCheckClosed("te-proof-debug",
-                            "TheoryEngine::conflict_explained_sharing");
     Node fullConflict = tncExp.getNode();
 
     if (isProofEnabled())
     {
+      Trace("te-proof-debug")
+          << "Check closed conflict explained with sharing" << std::endl;
+      tncExp.debugCheckClosed("te-proof-debug",
+                              "TheoryEngine::conflict_explained_sharing");
       Trace("te-proof-debug") << "Process conflict: " << conflict << std::endl;
       Trace("te-proof-debug") << "Conflict " << tconflict << " from "
                               << tconflict.identifyGenerator() << std::endl;
@@ -1498,7 +1498,10 @@ void TheoryEngine::conflict(TrustNode tconflict, TheoryId theoryId)
     Assert(properConflict(fullConflict));
     Trace("te-proof-debug")
         << "Check closed conflict with sharing" << std::endl;
-    tconf.debugCheckClosed("te-proof-debug", "TheoryEngine::conflict:sharing");
+    if (isProofEnabled())
+    {
+      tconf.debugCheckClosed("te-proof-debug", "TheoryEngine::conflict:sharing");
+    }
     lemma(tconf, LemmaProperty::REMOVABLE);
   } else {
     // When only one theory, the conflict should need no processing