Fix issues with cyclic proofs due to double SYMM applications (#7083)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 1 Sep 2021 02:51:46 +0000 (21:51 -0500)
committerGitHub <noreply@github.com>
Wed, 1 Sep 2021 02:51:46 +0000 (02:51 +0000)
commit12fd4e1a87a33dc541a71747a9a3250fe3854aa9
tree3bb01472ab83d8f881cd73ec7cfcf8874441bf1b
parent5303c2c85c2d57a2e7c180e639661b071e18f2bc
Fix issues with cyclic proofs due to double SYMM applications (#7083)

Our way of constructing proofs from the equality engine in very rare cases may cause cyclic proofs due to constructing double applications of SYMM, which are not recognized as assumptions in CDProof. This is due to an interplay between LazyProofChain using an underlying CDProof as its default proof generator, where the proof chain would use the proofs from the CDProof to form a cyclic proof.

This was encountered in 9 SMT-LIB benchmarks in QF_SLIA.

This makes us safer in several places related to double SYMM steps.
src/proof/lazy_proof.cpp
src/proof/proof.cpp
src/proof/proof_node_manager.cpp
src/proof/proof_node_manager.h
test/regress/CMakeLists.txt
test/regress/regress2/strings/proof-fail-083021-delta.smt2 [new file with mode: 0644]