diff options
| -rw-r--r-- | src/expr/term_conversion_proof_generator.cpp | 13 |
1 files changed, 8 insertions, 5 deletions
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; |