From 75d1a09f9d797cc3449e1a922e978d21e50f4b15 Mon Sep 17 00:00:00 2001 From: Lachnitt Date: Fri, 25 Mar 2022 11:59:26 -0700 Subject: [PATCH] [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)) --- src/proof/alethe/alethe_post_processor.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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]); -- 2.30.2