diff options
Diffstat (limited to 'test/regress')
17 files changed, 45 insertions, 13 deletions
diff --git a/test/regress/regress0/bv/bv-int-collapse2-sat.smt2 b/test/regress/regress0/bv/bv-int-collapse2-sat.smt2 index 1a355a495..4b97a3de9 100644 --- a/test/regress/regress0/bv/bv-int-collapse2-sat.smt2 +++ b/test/regress/regress0/bv/bv-int-collapse2-sat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores +; COMMAND-LINE: --rewrite-divk --no-check-proofs --no-check-unsat-cores ; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress0/bv/cmu-rdk-3.smt2 b/test/regress/regress0/bv/cmu-rdk-3.smt2 index 742dd593b..9e7733889 100644 --- a/test/regress/regress0/bv/cmu-rdk-3.smt2 +++ b/test/regress/regress0/bv/cmu-rdk-3.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --rewrite-divk +; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith.smt2 b/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith.smt2 index dd9cb6886..0618e28cb 100644 --- a/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith.smt2 +++ b/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --fmf-fun --no-check-models +; COMMAND-LINE: --fmf-fun --no-check-models --rewrite-divk ; EXPECT: sat (set-logic UFLIA) (set-info :status sat) diff --git a/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith2.smt2 b/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith2.smt2 index ea5a5e4b7..07f1e6674 100644 --- a/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith2.smt2 +++ b/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --fmf-fun --no-check-models +; COMMAND-LINE: --fmf-fun --no-check-models --rewrite-divk ; EXPECT: sat (set-logic UFLIA) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index faa2abe9a..9c31204e8 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -88,7 +88,8 @@ TESTS = \ quaternion_ds1_symm_0428.fof.smt2 \ bug749-rounding.smt2 \ RNDPRE_4_1-dd-nqe.smt2 \ - mix-complete-strat.smt2 + mix-complete-strat.smt2 \ + cbqi-sdlx-fixpoint-3-dd.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/RND-small.smt2 b/test/regress/regress0/quantifiers/RND-small.smt2 index 1401e5de8..cf5c3bc7e 100644 --- a/test/regress/regress0/quantifiers/RND-small.smt2 +++ b/test/regress/regress0/quantifiers/RND-small.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-recurse +; COMMAND-LINE: --no-check-models ; EXPECT: sat (set-logic LRA) (declare-fun y1 () Real) diff --git a/test/regress/regress0/quantifiers/anti-sk-simp.smt2 b/test/regress/regress0/quantifiers/anti-sk-simp.smt2 index ba4f9cbb9..2ae54a075 100644 --- a/test/regress/regress0/quantifiers/anti-sk-simp.smt2 +++ b/test/regress/regress0/quantifiers/anti-sk-simp.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --quant-anti-skolem +; COMMAND-LINE: --cbqi --quant-anti-skolem ; EXPECT: unsat (set-logic ALL_SUPPORTED) (set-info :status unsat) diff --git a/test/regress/regress0/quantifiers/ari056.smt2 b/test/regress/regress0/quantifiers/ari056.smt2 index ed4d2bf4a..a1f4aef04 100644 --- a/test/regress/regress0/quantifiers/ari056.smt2 +++ b/test/regress/regress0/quantifiers/ari056.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --cbqi +; EXPECT: unsat (set-logic UFNIRA) (set-info :status unsat) (assert (forall ((X Int)) (= X 12) )) diff --git a/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 b/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 index bd7ca19cd..b8b1683a9 100644 --- a/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 +++ b/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --dt-rewrite-error-sel +; COMMAND-LINE: --cbqi --dt-rewrite-error-sel ; EXPECT: unsat (set-logic ALL_SUPPORTED) (declare-datatypes () ((List (cons (head Int) (tail List)) (nil)))) diff --git a/test/regress/regress0/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 b/test/regress/regress0/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 new file mode 100644 index 000000000..4d5cf4ec4 --- /dev/null +++ b/test/regress/regress0/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: --cbqi --decision=internal +; EXPECT: unsat +(set-logic LIA) +(set-info :status unsat) + +(assert (or +(forall ((H Int) (G Int)) (= (= G 0) (= H 0))) + +(forall ((C Int) (D Int) (E Int)) (or +(= (= D 0) (= C 0)) +(and +(not (forall ((G Int)) (= (= E 0) (= G 0)))) +(not (forall ((A Int)) + (not (= (ite (= A 0) 0 1) (ite (= C 0) 0 2))) +)) +))) +)) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/delta-simp.smt2 b/test/regress/regress0/quantifiers/delta-simp.smt2 index f18a4fbd9..e5883134f 100644 --- a/test/regress/regress0/quantifiers/delta-simp.smt2 +++ b/test/regress/regress0/quantifiers/delta-simp.smt2 @@ -1,5 +1,7 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat (set-logic LRA) (set-info :status sat) (declare-fun c () Real) (assert (forall ((x Real)) (or (<= x 0) (>= x (+ c 3))))) -(check-sat)
\ No newline at end of file +(check-sat) diff --git a/test/regress/regress0/quantifiers/mix-coeff.smt2 b/test/regress/regress0/quantifiers/mix-coeff.smt2 index a20867b1c..23ecba49e 100644 --- a/test/regress/regress0/quantifiers/mix-coeff.smt2 +++ b/test/regress/regress0/quantifiers/mix-coeff.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic LIRA) (set-info :status unsat) (assert (forall ((x Int) (y Int) (a Real) (z Int)) (or (> x (+ a (* (/ 2 3) y) (* (/ 4 5) z))) (< x (+ 10 (* 3 a) (* (/ 2 5) y) (* (/ 4 7) z)))))) -(check-sat)
\ No newline at end of file +(check-sat) diff --git a/test/regress/regress0/quantifiers/mix-complete-strat.smt2 b/test/regress/regress0/quantifiers/mix-complete-strat.smt2 index c2209f697..e75591dec 100644 --- a/test/regress/regress0/quantifiers/mix-complete-strat.smt2 +++ b/test/regress/regress0/quantifiers/mix-complete-strat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find +; COMMAND-LINE: --cbqi --finite-model-find --no-check-models ; EXPECT: sat (set-logic UFLIA) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/mix-simp.smt2 b/test/regress/regress0/quantifiers/mix-simp.smt2 index 0b8c5067d..b7142c6e9 100644 --- a/test/regress/regress0/quantifiers/mix-simp.smt2 +++ b/test/regress/regress0/quantifiers/mix-simp.smt2 @@ -1,4 +1,6 @@ -(set-logic ALL_SUPPORTED) +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic LIRA) (set-info :status sat) (assert (forall ((x Real)) (exists ((y Int)) (and (>= y x) (< y (+ x 1)))))) (check-sat) diff --git a/test/regress/regress0/quantifiers/psyco-196.smt2 b/test/regress/regress0/quantifiers/psyco-196.smt2 index 356e62752..fef1a24c6 100644 --- a/test/regress/regress0/quantifiers/psyco-196.smt2 +++ b/test/regress/regress0/quantifiers/psyco-196.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat (set-logic LIA) (set-info :status sat) (declare-fun W_S1_V5 () Bool) diff --git a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 index 5c11a57f5..0ce96285c 100644 --- a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 +++ b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --cbqi --no-check-models +; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) (declare-datatypes () ((nat (Suc (pred nat)) (zero)))) diff --git a/test/regress/regress1/bug519.smt2 b/test/regress/regress1/bug519.smt2 index 72ec634a8..6cabbaa64 100644 --- a/test/regress/regress1/bug519.smt2 +++ b/test/regress/regress1/bug519.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: -mi +; COMMAND-LINE: --cbqi -mi --no-check-models ; EXPECT: sat ; EXPECT: unsat |