diff options
| -rw-r--r-- | src/proof/conv_proof_generator.cpp | 6 | ||||
| -rw-r--r-- | src/theory/theory_preprocessor.cpp | 11 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/preprocess/issue6754-tpp.smt2 | 5 |
4 files changed, 17 insertions, 6 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; } diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index 230c23424..53c90c88a 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -310,9 +310,14 @@ TrustNode TheoryPreprocessor::theoryPreprocess( rtfNode = ttfr.getNode(); registerTrustedRewrite(ttfr, d_tpgRtf.get(), true); } - // Finish the conversion by rewriting. This is registered as a - // post-rewrite, since it is the last step applied for theory atoms. - Node retNode = rewriteWithProof(rtfNode, d_tpgRtf.get(), false); + // Finish the conversion by rewriting. Notice that we must consider this a + // pre-rewrite since we do not recursively register the rewriting steps + // of subterms of rtfNode. For example, if this step rewrites + // (not A) ---> B, then if registered a pre-rewrite, it will apply when + // reconstructing proofs via d_tpgRtf. However, if it is a post-rewrite + // it will fail to apply if another call to this class registers A -> C, + // in which case (not C) will be returned instead of B (see issue 6754). + Node retNode = rewriteWithProof(rtfNode, d_tpgRtf.get(), true); d_rtfCache[current] = retNode; continue; } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 63d34ebe1..da67705f5 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -794,6 +794,7 @@ set(regress_0_tests regress0/preprocess/circuit-prop.smt2 regress0/preprocess/issue5729-rewritten-assertions.smt2 regress0/preprocess/issue5943-non-clausal-simp.smt2 + regress0/preprocess/issue6754-tpp.smt2 regress0/preprocess/preprocess_00.cvc regress0/preprocess/preprocess_01.cvc regress0/preprocess/preprocess_02.cvc diff --git a/test/regress/regress0/preprocess/issue6754-tpp.smt2 b/test/regress/regress0/preprocess/issue6754-tpp.smt2 new file mode 100644 index 000000000..9d34429c6 --- /dev/null +++ b/test/regress/regress0/preprocess/issue6754-tpp.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun a () Bool) +(assert (> (mod (ite a 0 1) 2) 1)) +(check-sat) |