From 6203bcb456d5450770c8ac6cdb775ec0f73e0325 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 16 Apr 2021 09:36:40 -0500
Subject: [PATCH] Fix ONCE for post-rewrite (#6372)

---
 src/expr/term_conversion_proof_generator.cpp | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp
index 22e1309d2..2233dcc7b 100644
--- 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")
-- 
2.30.2