From 95add26e5210e53e03c55ee313279b87cc3d5660 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Tue, 2 Feb 2021 11:17:33 -0300 Subject: [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). --- test/regress/CMakeLists.txt | 2 ++ 1 file changed, 2 insertions(+) (limited to 'test/regress/CMakeLists.txt') 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 -- cgit v1.2.3