From 84e528c87f6d86e89d674785a9f71706dc32b0e3 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 3 Apr 2024 18:26:53 -0300
Subject: [PATCH] [proofs] Fix tracing in CHAIN_RESOLUTION proof checker

---
 src/theory/booleans/proof_checker.cpp | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

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