From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 19 Oct 2021 23:53:56 +0000 (-0500)
Subject: Fix expected conclusion for EQ_RESOLVE when expanding MACRO_SR_PRED_TRANSFORM (#7412)
X-Git-Tag: cvc5-1.0.0~1049
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a96ed1538245b2ce2cd8a8084e0288d07071ca23;p=cvc5.git

Fix expected conclusion for EQ_RESOLVE when expanding MACRO_SR_PRED_TRANSFORM (#7412)

Fixes a proof checking failure during post-processing.

Fixes a rare case where the RHS of equality resolve step requires a symmetry step.
---

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index adc15ca2c..a547c4362 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -654,7 +654,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
     // apply transitivity if necessary
     Node eq = addProofForTrans(tchildren, cdp);
 
-    cdp->addStep(args[0], PfRule::EQ_RESOLVE, {children[0], eq}, {});
+    cdp->addStep(eq[1], PfRule::EQ_RESOLVE, {children[0], eq}, {});
     return args[0];
   }
   else if (id == PfRule::MACRO_RESOLUTION
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a0f6f7999..81b2bd0c9 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1763,6 +1763,7 @@ set(regress_1_tests
   regress1/proofs/issue6625-unsat-core-proofs.smt2
   regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2
   regress1/proofs/macro-res-exp-singleton-after-elimCrowd.smt2
+  regress1/proofs/qgu-fuzz-1-strings-pp.smt2
   regress1/proofs/quant-alpha-eq.smt2
   regress1/proofs/sat-trivial-cycle.smt2
   regress1/proofs/unsat-cores-proofs.smt2
diff --git a/test/regress/regress1/proofs/qgu-fuzz-1-strings-pp.smt2 b/test/regress/regress1/proofs/qgu-fuzz-1-strings-pp.smt2
new file mode 100644
index 000000000..c0c1f16f7
--- /dev/null
+++ b/test/regress/regress1/proofs/qgu-fuzz-1-strings-pp.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun x () String)
+(assert (let ((_let_1 (str.to_re "B"))) (and (str.in_re x (re.++ re.allchar  (str.to_re (str.++ "B" "A")))) (str.in_re x (re.* (re.union re.allchar  (str.to_re "A")))) (str.in_re x (re.* (re.union re.allchar  _let_1))) (str.in_re x (re.* (re.++ re.allchar  _let_1))))))
+(check-sat)