Add regressions for fixed issues (#7369)

Fixes #4393. Fixes #3966.

These issues do not occur on current master.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 819bb94e4d6154246130674fae1a1e53d75a9406..54fb91db42ae45230aa7fcde72cc21dabac156ee 100644 (file)
--- 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 (file)
index 0000000..950cb61
--- /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 (file)
index 0000000..7bfbf41
--- /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)