diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-26 15:08:19 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-26 20:08:19 +0000 |
| commit | 836d8d1ba22ad4ffbcb124998a04f8eb0de5500a (patch) | |
| tree | ad3c539b23bfa0f92e88c8d970603253ee88529a /test/regress/CMakeLists.txt | |
| parent | 77dfb2623f3cb8ce8e9795f319d6ae574012debf (diff) | |
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.
Diffstat (limited to 'test/regress/CMakeLists.txt')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 34ef1a9f7..625d5faea 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1805,6 +1805,7 @@ set(regress_1_tests 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/qgu-fuzz-arrays-1-dd-te-auto.smt2 regress1/proofs/quant-alpha-eq.smt2 regress1/proofs/sat-trivial-cycle.smt2 regress1/proofs/unsat-cores-proofs.smt2 |