diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp index 88791f627bd..7b540a1a0da 100644 --- 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 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"