diff options
Diffstat (limited to 'test')
| -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) |