diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-02-02 11:17:33 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-02 11:17:33 -0300 |
| commit | 95add26e5210e53e03c55ee313279b87cc3d5660 (patch) | |
| tree | b5032ea99a12eac9c5facf66ac53fdb8c25de02d /test/regress/CMakeLists.txt | |
| parent | c48548ea68b6241bee2cb9393ef2710c5803fb06 (diff) | |
[proof-new] Fix bug in expansion of MACRO_RESOLUTION (#5845)
Evaluating the proof infrastructure in SMT-LIB has uncovered a rare case (i.e., not previously in our regressions!!) in which a crowding literal occurs in an OR node that represents a single-literal clause subsequent to the last clause that includes the crowding literal. This was leading to the clause that eliminates the crowding literal not being found. The commit fixes this issue by excluding single-literal clauses from those that can introduce crowding literals (which was already marked as necessary but not properly enforced).
Diffstat (limited to 'test/regress/CMakeLists.txt')
| -rw-r--r-- | test/regress/CMakeLists.txt | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 3bdaad2ad..de84761f0 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2493,6 +2493,8 @@ set(regression_disabled_tests regress1/nl/NAVIGATION2.smt2 # sat or unknown in different builds regress1/nl/issue3307.smt2 + # waiting until we enable proofs in master + regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2 # slow with sygus-inference after removing anti-skolemization regress1/quantifiers/anti-sk-simp.smt2 # no longer support snorm option |