From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 17 Dec 2020 16:50:49 +0000 (-0600)
Subject: (proof-new) Minor updates to term conversion proof generator (#5691)
X-Git-Tag: cvc5-1.0.0~2426
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9b099b715cec0dc60048fdc64b4d61b977d14096;p=cvc5.git

(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 858ca9f64..d351d88b6 100644
--- 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;