From a96ed1538245b2ce2cd8a8084e0288d07071ca23 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 19 Oct 2021 18:53:56 -0500 Subject: [PATCH] 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. --- src/smt/proof_post_processor.cpp | 2 +- test/regress/CMakeLists.txt | 1 + test/regress/regress1/proofs/qgu-fuzz-1-strings-pp.smt2 | 5 +++++ 3 files changed, 7 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress1/proofs/qgu-fuzz-1-strings-pp.smt2 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) -- 2.30.2