From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 16 Apr 2021 14:36:40 +0000 (-0500)
Subject: Fix ONCE for post-rewrite (#6372)
X-Git-Tag: cvc5-1.0.0~1889
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6203bcb456d5450770c8ac6cdb775ec0f73e0325;p=cvc5.git

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 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")