summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/regress/CMakeLists.txt4
-rw-r--r--test/regress/regress0/arith/bug547.2.smt23
-rw-r--r--test/regress/regress0/arith/div-chainable.smt22
-rw-r--r--test/regress/regress0/arith/mod-simp.smt22
-rw-r--r--test/regress/regress0/bug548a.smt22
-rw-r--r--test/regress/regress0/quantifiers/mix-match.smt24
-rw-r--r--test/regress/regress0/unconstrained/4481.smt28
-rw-r--r--test/regress/regress0/unconstrained/4484.smt28
-rw-r--r--test/regress/regress0/unconstrained/4486.smt28
-rw-r--r--test/regress/regress1/arith/bug547.1.smt22
-rw-r--r--test/regress/regress1/bv/bv-int-collapse2-sat.smt22
-rw-r--r--test/regress/regress1/bv/cmu-rdk-3.smt22
-rw-r--r--test/regress/regress1/bv/issue3776.smt23
-rw-r--r--test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt22
-rw-r--r--test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt22
-rw-r--r--test/regress/regress1/fmf/issue3626.smt22
-rw-r--r--test/regress/regress1/nl/issue3441.smt22
-rw-r--r--test/regress/regress1/nl/issue3955-ee-double-notify.smt22
-rw-r--r--test/regress/regress1/push-pop/model-unsound-ania.smt211
-rw-r--r--test/regress/regress1/strings/chapman150408.smt21
-rw-r--r--test/regress/regress1/strings/cmu-substr-rw.smt22
-rw-r--r--test/regress/regress1/strings/crash-1019.smt21
-rw-r--r--test/regress/regress2/bug674.smt22
-rw-r--r--test/regress/regress2/strings/cmi-split-cm-fail.smt22
24 files changed, 55 insertions, 24 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 2df07db5a..5a59f2f54 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1121,6 +1121,9 @@ set(regress_0_tests
regress0/uflra/simple.02.cvc
regress0/uflra/simple.03.cvc
regress0/uflra/simple.04.cvc
+ regress0/unconstrained/4481.smt2
+ regress0/unconstrained/4484.smt2
+ regress0/unconstrained/4486.smt2
regress0/unconstrained/arith.smt2
regress0/unconstrained/arith3.smt2
regress0/unconstrained/arith4.smt2
@@ -1472,6 +1475,7 @@ set(regress_1_tests
regress1/push-pop/fuzz_7.smt2
regress1/push-pop/fuzz_8.smt2
regress1/push-pop/fuzz_9.smt2
+ regress1/push-pop/model-unsound-ania.smt2
regress1/push-pop/quant-fun-proc-unmacro.smt2
regress1/push-pop/quant-fun-proc.smt2
regress1/quantifiers/006-cbqi-ite.smt2
diff --git a/test/regress/regress0/arith/bug547.2.smt2 b/test/regress/regress0/arith/bug547.2.smt2
index b7d114eb3..7ff2a538a 100644
--- a/test/regress/regress0/arith/bug547.2.smt2
+++ b/test/regress/regress0/arith/bug547.2.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --rewrite-divk
-; EXPECT: sat
(set-logic QF_NIA)
+(set-info :status sat)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
diff --git a/test/regress/regress0/arith/div-chainable.smt2 b/test/regress/regress0/arith/div-chainable.smt2
index 9ddc80e98..76bc4095f 100644
--- a/test/regress/regress0/arith/div-chainable.smt2
+++ b/test/regress/regress0/arith/div-chainable.smt2
@@ -1,5 +1,3 @@
-; COMMAND-LINE: --rewrite-divk
-; EXPECT: sat
(set-logic QF_LIA)
(set-info :status sat)
diff --git a/test/regress/regress0/arith/mod-simp.smt2 b/test/regress/regress0/arith/mod-simp.smt2
index 7294cd863..1a9c50590 100644
--- a/test/regress/regress0/arith/mod-simp.smt2
+++ b/test/regress/regress0/arith/mod-simp.smt2
@@ -1,5 +1,3 @@
-; COMMAND-LINE: --rewrite-divk
-; EXPECT: unsat
(set-logic QF_LIA)
(set-info :status unsat)
diff --git a/test/regress/regress0/bug548a.smt2 b/test/regress/regress0/bug548a.smt2
index 75d82d98f..581c34f2d 100644
--- a/test/regress/regress0/bug548a.smt2
+++ b/test/regress/regress0/bug548a.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --rewrite-divk --tlimit 1000
+; COMMAND-LINE: --tlimit 1000
; EXPECT: unknown
(set-logic AUFLIA)
(declare-fun f (Int) Int)
diff --git a/test/regress/regress0/quantifiers/mix-match.smt2 b/test/regress/regress0/quantifiers/mix-match.smt2
index c6ac3b56f..fbf996a0a 100644
--- a/test/regress/regress0/quantifiers/mix-match.smt2
+++ b/test/regress/regress0/quantifiers/mix-match.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --no-check-unsat-cores
+; EXPECT: unsat
(set-logic ALL_SUPPORTED)
(set-info :status unsat)
(declare-fun P (Real) Bool)
@@ -7,4 +9,4 @@
(assert (is_int a))
(assert (not (P a)))
-(check-sat) \ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/unconstrained/4481.smt2 b/test/regress/regress0/unconstrained/4481.smt2
new file mode 100644
index 000000000..028607093
--- /dev/null
+++ b/test/regress/regress0/unconstrained/4481.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --unconstrained-simp
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun a () Int)
+(assert (= (div a 2) 2))
+(assert (= (div a 3) 0))
+(check-sat)
diff --git a/test/regress/regress0/unconstrained/4484.smt2 b/test/regress/regress0/unconstrained/4484.smt2
new file mode 100644
index 000000000..f2f11295b
--- /dev/null
+++ b/test/regress/regress0/unconstrained/4484.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --unconstrained-simp
+; EXPECT: unsat
+(set-logic QF_NIRA)
+(set-info :status unsat)
+(declare-fun a () Real)
+(assert (= (to_int a) 2))
+(assert (= (to_int (/ a 2.0)) 2))
+(check-sat)
diff --git a/test/regress/regress0/unconstrained/4486.smt2 b/test/regress/regress0/unconstrained/4486.smt2
new file mode 100644
index 000000000..01771ce66
--- /dev/null
+++ b/test/regress/regress0/unconstrained/4486.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --unconstrained-simp
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () Real)
+(assert (is_int x))
+(assert (is_int (+ x 1)))
+(check-sat)
diff --git a/test/regress/regress1/arith/bug547.1.smt2 b/test/regress/regress1/arith/bug547.1.smt2
index 38d1dfcb1..75894eb60 100644
--- a/test/regress/regress1/arith/bug547.1.smt2
+++ b/test/regress/regress1/arith/bug547.1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --rewrite-divk --nl-ext-tplanes
+; COMMAND-LINE: --nl-ext-tplanes --quiet
; EXPECT: sat
(set-logic QF_NIA)
(declare-fun x () Int)
diff --git a/test/regress/regress1/bv/bv-int-collapse2-sat.smt2 b/test/regress/regress1/bv/bv-int-collapse2-sat.smt2
index 3d932a076..07f2dae6a 100644
--- a/test/regress/regress1/bv/bv-int-collapse2-sat.smt2
+++ b/test/regress/regress1/bv/bv-int-collapse2-sat.smt2
@@ -1,5 +1,3 @@
-; COMMAND-LINE: --rewrite-divk
-; EXPECT: sat
(set-logic ALL_SUPPORTED)
(set-info :status sat)
(declare-fun t () Int)
diff --git a/test/regress/regress1/bv/cmu-rdk-3.smt2 b/test/regress/regress1/bv/cmu-rdk-3.smt2
index 9e7733889..742dd593b 100644
--- a/test/regress/regress1/bv/cmu-rdk-3.smt2
+++ b/test/regress/regress1/bv/cmu-rdk-3.smt2
@@ -1,5 +1,3 @@
-; COMMAND-LINE: --rewrite-divk
-; EXPECT: sat
(set-logic ALL_SUPPORTED)
(set-info :status sat)
diff --git a/test/regress/regress1/bv/issue3776.smt2 b/test/regress/regress1/bv/issue3776.smt2
index 30c034c70..3e86a4974 100644
--- a/test/regress/regress1/bv/issue3776.smt2
+++ b/test/regress/regress1/bv/issue3776.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --rewrite-divk
-; EXPECT: sat
(set-logic QF_BVLIA)
+(set-info :status sat)
(declare-fun t () Int)
(assert (= t (bv2nat ((_ int2bv 1) t))))
(check-sat)
diff --git a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2
index 0618e28cb..dd9cb6886 100644
--- a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2
+++ b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-fun --no-check-models --rewrite-divk
+; COMMAND-LINE: --fmf-fun --no-check-models
; EXPECT: sat
(set-logic UFLIA)
(set-info :status sat)
diff --git a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2
index 07f1e6674..ea5a5e4b7 100644
--- a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2
+++ b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-fun --no-check-models --rewrite-divk
+; COMMAND-LINE: --fmf-fun --no-check-models
; EXPECT: sat
(set-logic UFLIA)
(set-info :status sat)
diff --git a/test/regress/regress1/fmf/issue3626.smt2 b/test/regress/regress1/fmf/issue3626.smt2
index 9f27dee01..25dc80223 100644
--- a/test/regress/regress1/fmf/issue3626.smt2
+++ b/test/regress/regress1/fmf/issue3626.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-bound
+; COMMAND-LINE: --fmf-bound --no-cegqi
; EXPECT: sat
(set-logic ALL)
(assert (forall ((a Int)) (or (distinct (/ 0 0) a) (= (/ 0 a) 0))))
diff --git a/test/regress/regress1/nl/issue3441.smt2 b/test/regress/regress1/nl/issue3441.smt2
index 19fe98bc5..6be4e7d7e 100644
--- a/test/regress/regress1/nl/issue3441.smt2
+++ b/test/regress/regress1/nl/issue3441.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --quiet
+; EXPECT: sat
(set-logic QF_NIA)
(set-info :status sat)
(declare-fun a () Int)
diff --git a/test/regress/regress1/nl/issue3955-ee-double-notify.smt2 b/test/regress/regress1/nl/issue3955-ee-double-notify.smt2
index 8aa8793df..21f26df2d 100644
--- a/test/regress/regress1/nl/issue3955-ee-double-notify.smt2
+++ b/test/regress/regress1/nl/issue3955-ee-double-notify.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --quiet
+; EXPECT: sat
(set-logic QF_UFNRA)
(set-option :snorm-infer-eq true)
(set-info :status sat)
diff --git a/test/regress/regress1/push-pop/model-unsound-ania.smt2 b/test/regress/regress1/push-pop/model-unsound-ania.smt2
new file mode 100644
index 000000000..6f7f2752a
--- /dev/null
+++ b/test/regress/regress1/push-pop/model-unsound-ania.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: unsat
+(set-logic QF_ANIA)
+(declare-fun _substvar_16_ () Int)
+(push 1)
+(assert (not (= (mod _substvar_16_ 2) 0)))
+(check-sat)
+(pop 1)
+(assert (= (- (mod _substvar_16_ 2) 2) 0))
+(check-sat)
diff --git a/test/regress/regress1/strings/chapman150408.smt2 b/test/regress/regress1/strings/chapman150408.smt2
index f03718556..e6047498e 100644
--- a/test/regress/regress1/strings/chapman150408.smt2
+++ b/test/regress/regress1/strings/chapman150408.smt2
@@ -1,7 +1,6 @@
(set-logic SLIA)
(set-info :status sat)
(set-option :strings-exp true)
-(set-option :rewrite-divk true)
(declare-fun string () String)
(assert (and
(and (not (not (not (= (ite (> (str.indexof string ";" 0) 0) 1 0)
diff --git a/test/regress/regress1/strings/cmu-substr-rw.smt2 b/test/regress/regress1/strings/cmu-substr-rw.smt2
index 20bf979dd..a4d649d7f 100644
--- a/test/regress/regress1/strings/cmu-substr-rw.smt2
+++ b/test/regress/regress1/strings/cmu-substr-rw.smt2
@@ -1,8 +1,6 @@
(set-logic ALL_SUPPORTED)
(set-info :status sat)
(set-option :strings-exp true)
-;(set-option :produce-models true)
-;(set-option :rewrite-divk true)
(declare-fun uri () String)
diff --git a/test/regress/regress1/strings/crash-1019.smt2 b/test/regress/regress1/strings/crash-1019.smt2
index 9f2e99b02..317840ddb 100644
--- a/test/regress/regress1/strings/crash-1019.smt2
+++ b/test/regress/regress1/strings/crash-1019.smt2
@@ -1,6 +1,5 @@
(set-logic ALL_SUPPORTED)
(set-option :strings-exp true)
-(set-option :rewrite-divk true)
(set-info :status unsat)
(declare-fun s () String)
diff --git a/test/regress/regress2/bug674.smt2 b/test/regress/regress2/bug674.smt2
index 31eaa5aba..cce0c963a 100644
--- a/test/regress/regress2/bug674.smt2
+++ b/test/regress/regress2/bug674.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --quant-ind --incremental --rewrite-divk
+; COMMAND-LINE: --quant-ind --incremental
(set-logic ALL_SUPPORTED)
(declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil))))
(define-fun-rec app ((l1 Lst) (l2 Lst)) Lst (ite ((_ is nil) l1) l2 (cons (head l1) (app (tail l1) l2))))
diff --git a/test/regress/regress2/strings/cmi-split-cm-fail.smt2 b/test/regress/regress2/strings/cmi-split-cm-fail.smt2
index e2ae94a27..4782fa7f8 100644
--- a/test/regress/regress2/strings/cmi-split-cm-fail.smt2
+++ b/test/regress/regress2/strings/cmi-split-cm-fail.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --rewrite-divk
+; COMMAND-LINE: --strings-exp
; EXPECT: sat
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback