diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/theory_preprocessor.cpp | 11 |
1 files changed, 8 insertions, 3 deletions
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; } |