diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-27 16:18:28 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-27 16:18:28 -0500 |
| commit | b9062490a7590708bcf158d4670a23d859fe3355 (patch) | |
| tree | 9bb487795a7753de1c631494012133508ecc374e /test/regress | |
| parent | 8d63f44d93ae91c5b89a9cf866ba33c954465398 (diff) | |
Fix CEGQI for datatypes with Boolean subfields (#6630)
Fixes a solution soundness issue caused by allowing ineligible terms of kind BOOLEAN_TERM_VARIABLE to appear in instantiations.
This also corrects the expected solution on a benchmark that had an incorrect status.
Fixes #6603.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/issue5645-dt-cm-spurious.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/issue6603-dt-bool-cegqi.smt2 | 5 |
3 files changed, 7 insertions, 1 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 81e5ca8c6..35d2553de 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -872,6 +872,7 @@ set(regress_0_tests regress0/quantifiers/issue4576.smt2 regress0/quantifiers/issue5645-dt-cm-spurious.smt2 regress0/quantifiers/issue5693-prenex.smt2 + regress0/quantifiers/issue6603-dt-bool-cegqi.smt2 regress0/quantifiers/lra-triv-gn.smt2 regress0/quantifiers/macro-back-subs-sat.smt2 regress0/quantifiers/macros-int-real.smt2 diff --git a/test/regress/regress0/quantifiers/issue5645-dt-cm-spurious.smt2 b/test/regress/regress0/quantifiers/issue5645-dt-cm-spurious.smt2 index 0d3f711bf..6ed3a1867 100644 --- a/test/regress/regress0/quantifiers/issue5645-dt-cm-spurious.smt2 +++ b/test/regress/regress0/quantifiers/issue5645-dt-cm-spurious.smt2 @@ -1,5 +1,5 @@ (set-logic ALL) -(set-info :status sat) +(set-info :status unsat) (declare-datatypes ((Enum1 0)) (((None) (cons (data Bool))))) (assert (forall ((var_1 Enum1)) (data var_1))) (check-sat) diff --git a/test/regress/regress0/quantifiers/issue6603-dt-bool-cegqi.smt2 b/test/regress/regress0/quantifiers/issue6603-dt-bool-cegqi.smt2 new file mode 100644 index 000000000..fce67f4d0 --- /dev/null +++ b/test/regress/regress0/quantifiers/issue6603-dt-bool-cegqi.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-datatypes ((E 0)) (((c (a Bool))))) +(assert (forall ((v E)) (a v))) +(check-sat) |