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