From: Lachnitt <lachnitt@stanford.edu>
Date: Fri, 25 Mar 2022 18:59:26 +0000 (-0700)
Subject: [proofs] Alethe: Bug Fix in Cong Rule (#8391)
X-Git-Tag: cvc5-1.0.0~173
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=75d1a09f9d797cc3449e1a922e978d21e50f4b15;p=cvc5.git

[proofs] Alethe: Bug Fix in Cong Rule (#8391)

cvc5 suffered a segfault in the CONG rule because the refl step, e.g. (= v0 v0), was added without the cl connector, e.g. (cl (= v0 v0))
---

diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
index f698a5fbd..6e98ed8a1 100644
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -986,7 +986,8 @@ bool AletheProofPostprocessCallback::update(Node res,
         {
           Node vpi = children[0][0][i].eqNode(children[0][1][i]);
           new_args.push_back(vpi);
-          vpis.push_back(nm->mkNode(kind::SEXPR, d_cl, vpi));
+          vpi = nm->mkNode(kind::SEXPR, d_cl, vpi);
+          vpis.push_back(vpi);
           success &= addAletheStep(AletheRule::REFL, vpi, vpi, {}, {}, *cdp);
         }
         vpis.push_back(children[1]);