Fix pre vs. post-rewrite in proofs for theory preprocessor (#6801)

This changes an annotation of a step of rewriting from "post" to "pre" in the theory preprocessor.
Fixes #6754.

1 files changed, 3 insertions, 3 deletions

diff --git a/src/proof/conv_proof_generator.cpp b/src/proof/conv_proof_generator.cpp
index 3635f3dea..1c4e2de5d 100644
--- a/src/proof/conv_proof_generator.cpp
+++ b/src/proof/conv_proof_generator.cpp
@@ -213,7 +213,7 @@ std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f)
 
       if (debugTraceEnabled)
       {
-        Trace("tconv-pf-gen-debug") << "Printing rewrite steps..." << std::endl;
+        Trace("tconv-pf-gen-debug") << "Rewrite steps:" << std::endl;
         for (size_t r = 0; r < 2; r++)
         {
           const NodeNodeMap& rm = r == 0 ? d_preRewriteMap : d_postRewriteMap;
@@ -233,7 +233,7 @@ std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f)
   std::shared_ptr<ProofNode> pfn = lpf.getProofFor(f);
   Trace("tconv-pf-gen") << "... success" << std::endl;
   Assert(pfn != nullptr);
-  Trace("tconv-pf-gen-debug") << "... proof is " << *pfn << std::endl;
+  Trace("tconv-pf-gen-debug-pf") << "... proof is " << *pfn << std::endl;
   return pfn;
 }
 
@@ -251,7 +251,7 @@ std::shared_ptr<ProofNode> TConvProofGenerator::getProofForRewriting(Node n)
   }
   std::shared_ptr<ProofNode> pfn = lpf.getProofFor(conc);
   Assert(pfn != nullptr);
-  Trace("tconv-pf-gen-debug") << "... proof is " << *pfn << std::endl;
+  Trace("tconv-pf-gen-debug-pf") << "... proof is " << *pfn << std::endl;
   return pfn;
 }