diff options
| -rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/issue4393-cdt-model.smt2 | 8 | ||||
| -rw-r--r-- | test/regress/regress1/nl/issue3966-conf-coeff.smt2 | 22 |
3 files changed, 32 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 819bb94e4..54fb91db4 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -498,6 +498,7 @@ set(regress_0_tests regress0/datatypes/is_test.smt2 regress0/datatypes/issue1433.smt2 regress0/datatypes/issue2838.cvc.smt2 + regress0/datatypes/issue4393-cdt-model.smt2 regress0/datatypes/issue5280-no-nrec.smt2 regress0/datatypes/jsat-2.6.smt2 regress0/datatypes/list-bool.smt2 @@ -1709,6 +1710,7 @@ set(regress_1_tests regress1/nl/issue3656.smt2 regress1/nl/issue3803-nl-check-model.smt2 regress1/nl/issue3955-ee-double-notify.smt2 + regress1/nl/issue3966-conf-coeff.smt2 regress1/nl/issue4791-llr.smt2 regress1/nl/issue5372-2-no-m-presolve.smt2 regress1/nl/issue5662-nl-tc.smt2 diff --git a/test/regress/regress0/datatypes/issue4393-cdt-model.smt2 b/test/regress/regress0/datatypes/issue4393-cdt-model.smt2 new file mode 100644 index 000000000..950cb61a9 --- /dev/null +++ b/test/regress/regress0/datatypes/issue4393-cdt-model.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_DTLIA) +(set-info :status sat) +(declare-codatatypes ((a 0)) (((b (c Int) (d a))))) +(declare-fun e () a) +(declare-fun f () a) +(assert (distinct f (b 0 f))) +(assert (= e f)) +(check-sat) diff --git a/test/regress/regress1/nl/issue3966-conf-coeff.smt2 b/test/regress/regress1/nl/issue3966-conf-coeff.smt2 new file mode 100644 index 000000000..7bfbf4140 --- /dev/null +++ b/test/regress/regress1/nl/issue3966-conf-coeff.smt2 @@ -0,0 +1,22 @@ +(set-logic QF_UFNIA) +(set-info :status sat) +(set-option :nl-ext-ent-conf true) +(declare-const v0 Bool) +(declare-const v1 Bool) +(declare-const v2 Bool) +(declare-const v3 Bool) +(declare-const i0 Int) +(declare-const i1 Int) +(declare-const i2 Int) +(declare-const i4 Int) +(declare-const i5 Int) +(declare-const i9 Int) +(declare-const i10 Int) +(declare-const i12 Int) +(declare-const i13 Int) +(assert v0) +(declare-sort S0 0) +(declare-const v4 Bool) +(assert (xor v2 v1 (> i12 i2) (and v3 v3) (> i12 i2) v4 v2 v1 v0 v3)) +(assert (xor (<= 52 (div 15 (- i1 84 i0 99 i5))) v4 (=> v4 (>= i5 88)) (> i12 i2) (and v3 v3) (<= 52 (div 15 (- i1 84 i0 99 i5))) v1 (> i12 i2) (distinct i0 615) v0)) +(check-sat) |