Disable automatic symmetry in proofs of theory explanations (#7493)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 26 Oct 2021 20:08:19 +0000 (15:08 -0500)
committerGitHub <noreply@github.com>
Tue, 26 Oct 2021 20:08:19 +0000 (20:08 +0000)
commit836d8d1ba22ad4ffbcb124998a04f8eb0de5500a
treead3c539b23bfa0f92e88c8d970603253ee88529a
parent77dfb2623f3cb8ce8e9795f319d6ae574012debf
Disable automatic symmetry in proofs of theory explanations (#7493)

This avoids cyclic proofs in a rare case where theory explanations involve an equality and its symmetric form.

This PR disables auto-symmetry on lazy proofs used for theory explanations, which is slightly less convenient but avoids potentials for cyclic proofs. Note this complication would not arise if the theory engine did not allow non-rewritten equalities to be propagated between theories.

Fixes cvc5/cvc5-projects#311.
src/proof/lazy_proof.cpp
src/proof/lazy_proof.h
src/theory/theory_engine.cpp
test/regress/CMakeLists.txt
test/regress/regress1/proofs/qgu-fuzz-arrays-1-dd-te-auto.smt2 [new file with mode: 0644]