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;
     }