diff options
Diffstat (limited to 'test')
6 files changed, 15 insertions, 10 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 0592bdeab..73fa07bf9 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -22,7 +22,6 @@ TESTS = \ bug269.smt2 \ bug290.smt2 \ bug291.smt2 \ - ex3.smt2 \ Arrays_Q1-noinfer.smt2 \ bignum_quant.smt2 \ bug269.smt2 \ @@ -55,8 +54,10 @@ TESTS = \ RND-small.smt2 \ clock-3.smt2 \ 006-cbqi-ite.smt2 \ - cbqi-lia-dt-simp.smt2 - + cbqi-lia-dt-simp.smt2 \ + is-int.smt2 \ + floor.smt2 \ + array-unsat-simp3.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine @@ -64,17 +65,12 @@ TESTS = \ # removed because they take more than 20s -# ex1.smt2 \ -# ex6.smt2 \ -# ex7.smt2 \ -# array-unsat-simp3.smt2are # javafe.ast.ArrayInit.35.smt2 \ # javafe.ast.StandardPrettyPrint.319.smt2 \ # javafe.ast.StmtVec.009.smt2 \ # javafe.ast.WhileStmt.447.smt2 \ # javafe.tc.CheckCompilationUnit.001.smt2 \ # javafe.tc.FlowInsensitiveChecks.682.smt2 \ -# array-unsat-simp3.smt2 \ # clock-10.smt2 # diff --git a/test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect b/test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect deleted file mode 100644 index b4ea773f0..000000000 --- a/test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect +++ /dev/null @@ -1 +0,0 @@ -% EXPECT: unsat diff --git a/test/regress/regress0/quantifiers/bug291.smt2 b/test/regress/regress0/quantifiers/bug291.smt2 index dbc230599..b39e415a8 100644 --- a/test/regress/regress0/quantifiers/bug291.smt2 +++ b/test/regress/regress0/quantifiers/bug291.smt2 @@ -10,4 +10,5 @@ (declare-fun store2 (Int) Int) (assert (forall ((?A Int) (?o Int) (?f Int) (?p Int) (?g Int) (?v Int)) (=> (not (= ?o ?p)) (= (select2 (store2 ?A)) (select2 ?A))))) (check-sat) +(get-info :reason-unknown) (exit) diff --git a/test/regress/regress0/quantifiers/bug291.smt2.expect b/test/regress/regress0/quantifiers/bug291.smt2.expect index 7856f23b4..f97ed61b6 100644 --- a/test/regress/regress0/quantifiers/bug291.smt2.expect +++ b/test/regress/regress0/quantifiers/bug291.smt2.expect @@ -1 +1,2 @@ -% EXPECT: sat +% EXPECT: unknown +% EXPECT: (:reason-unknown incomplete)
\ No newline at end of file diff --git a/test/regress/regress0/quantifiers/floor.smt2 b/test/regress/regress0/quantifiers/floor.smt2 new file mode 100755 index 000000000..cb20c1056 --- /dev/null +++ b/test/regress/regress0/quantifiers/floor.smt2 @@ -0,0 +1,4 @@ +(set-logic LIRA)
+(set-info :status unsat)
+(assert (forall ((X Real)) (not (>= (+ (to_int (* 2 X)) (* (- 2) (to_int X))) 1)) ))
+(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/quantifiers/is-int.smt2 b/test/regress/regress0/quantifiers/is-int.smt2 new file mode 100755 index 000000000..07e8dd246 --- /dev/null +++ b/test/regress/regress0/quantifiers/is-int.smt2 @@ -0,0 +1,4 @@ +(set-logic LIRA)
+(set-info :status unsat)
+(assert (forall ((X Real) (Y Real)) (or (not (is_int X)) (not (>= (+ X (* (- (/ 2 3)) Y)) (- (/ 1 6)))) (not (>= (+ (* (- 1) X) (* (- (/ 1 4)) Y)) (- (/ 61 8)))) (not (>= (+ (* (- 1) X) (* (/ 5 2) Y)) 13))) ))
+(check-sat)
\ No newline at end of file |