projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bda77d2) | patch
Fix expected conclusion for EQ_RESOLVE when expanding MACRO_SR_PRED_TRANSFORM (#7412)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 19 Oct 2021 23:53:56 +0000 (18:53 -0500)
committerGitHub <noreply@github.com>
Tue, 19 Oct 2021 23:53:56 +0000 (23:53 +0000)
commita96ed1538245b2ce2cd8a8084e0288d07071ca23
treeac443e783a216f37edf0262a36f1d9496ad73e3ctree
parentbda77d20d51b0ebdd8dec4bd50c6ce5faef7f218commit | diff
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 diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/proofs/qgu-fuzz-1-strings-pp.smt2 [new file with mode: 0644] blob