Fix ONCE for post-rewrite (#6372)

diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp
index 22e1309d2fee2839b93eab5fd5e7e8555044408a..2233dcc7bc0d62715932019ef7da6f322778d650 100644 (file)
--- a/src/expr/term_conversion_proof_generator.cpp
+++ b/src/expr/term_conversion_proof_generator.cpp
@@ -533,6 +533,16 @@ Node TConvProofGenerator::getProofForRewriting(Node t,
         }
         else
         {
+          // If we changed due to congruence, and then rewrote, then we
+          // require a trans step to connect here
+          if (!rret.isNull() && childChanged)
+          {
+            std::vector<Node> pfChildren;
+            pfChildren.push_back(cur.eqNode(ret));
+            pfChildren.push_back(ret.eqNode(rret));
+            Node result = cur.eqNode(rret);
+            pf.addStep(result, PfRule::TRANS, pfChildren, {});
+          }
           // take its rewrite if it rewrote and we have ONCE rewriting policy
           ret = rret.isNull() ? ret : rret;
           Trace("tconv-pf-gen-rewrite")