(proof-new) Minor updates to term conversion proof generator (#5691)

Minor updates to term conversion proof generator

diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp
index 858ca9f647f5dc75a483d78df22adbc047b541f4..d351d88b693be165da84ac9d66b963a52e36f425 100644 (file)
--- a/src/expr/term_conversion_proof_generator.cpp
+++ b/src/expr/term_conversion_proof_generator.cpp
@@ -84,7 +84,6 @@ void TConvProofGenerator::addRewriteStep(Node t,
   Node eq = registerRewriteStep(t, s, tctx);
   if (!eq.isNull())
   {
-    AlwaysAssert(ps.d_rule != PfRule::ASSUME);
     d_proof.addStep(eq, ps);
   }
 }
@@ -99,7 +98,6 @@ void TConvProofGenerator::addRewriteStep(Node t,
   Node eq = registerRewriteStep(t, s, tctx);
   if (!eq.isNull())
   {
-    AlwaysAssert(id != PfRule::ASSUME);
     d_proof.addStep(eq, id, children, args);
   }
 }
@@ -180,16 +178,21 @@ std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f)
     Node conc = getProofForRewriting(f[0], lpf, d_tcontext);
     if (conc != f)
     {
+      bool debugTraceEnabled = Trace.isOn("tconv-pf-gen-debug");
       Assert(conc.getKind() == EQUAL && conc[0] == f[0]);
       std::stringstream serr;
       serr << "TConvProofGenerator::getProofFor: " << toStringDebug()
-           << ": failed, mismatch (see -t tconv-pf-gen-debug for details)"
-           << std::endl;
+           << ": failed, mismatch";
+      if (!debugTraceEnabled)
+      {
+        serr << " (see -t tconv-pf-gen-debug for details)";
+      }
+      serr << std::endl;
       serr << "                  source: " << f[0] << std::endl;
       serr << "expected after rewriting: " << f[1] << std::endl;
       serr << "  actual after rewriting: " << conc[1] << std::endl;
 
-      if (Trace.isOn("tconv-pf-gen-debug"))
+      if (debugTraceEnabled)
       {
         Trace("tconv-pf-gen-debug") << "Printing rewrite steps..." << std::endl;
         serr << "Rewrite steps: " << std::endl;