[proofs] Fix tracing in CHAIN_RESOLUTION proof checker

HanielB · Apr 3, 2024 · 84e528c · 84e528c
1 parent 9eac613
commit 84e528c
Showing 1 changed file with 8 additions and 1 deletion.
diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp
@@ -278,7 +278,14 @@ Node BoolProofRuleChecker::checkInternal(ProofRule id,
       AlwaysAssert(itrhs != rhsClause.end());
       lhsClause.insert(lhsClause.end(), rhsClause.begin(), itrhs);
       lhsClause.insert(lhsClause.end(), itrhs + 1, rhsClause.end());
-      Trace("bool-pfcheck") << "\t.. after rhsClause: " << lhsClause << "\n";
+      if (TraceIsOn("bool-pfcheck"))
+      {
+        std::vector<Node> updatedRhsClause{rhsClause.begin(), itrhs};
+        updatedRhsClause.insert(
+            updatedRhsClause.end(), itrhs + 1, rhsClause.end());
+        Trace("bool-pfcheck")
+            << "\t.. after rhsClause: " << updatedRhsClause << "\n";
+      }
       rhsClause.clear();
     }
     Trace("bool-pfcheck") << "\n resulting clause: " << lhsClause << "\n"