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 adc15ca2c82effe7ccac663673bbdd0e9660e08b..a547c43625ea9a4ab9e9c8ccc5eafa3072e28eb0 100644 (file)
--- 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 a0f6f79990c1a0ac1be83fa078f1699b3f302732..81b2bd0c98b74480cc951da30a453c982732a4fc 100644 (file)
--- 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 (file)
index 0000000..c0c1f16
--- /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)