diff options
Diffstat (limited to 'test')
4 files changed, 27 insertions, 1 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index f8cc9ea35..ff3607b5b 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -45,7 +45,10 @@ TESTS = \ bi-artm-s.smt2 \ simp-typ-test.smt2 \ macros-int-real.smt2 \ - stream-x2014-09-18-unsat.smt2 + stream-x2014-09-18-unsat.smt2 \ + simp-len.smt2 \ + is-even.smt2 \ + is-even-pred.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine # set3.smt2 diff --git a/test/regress/regress0/quantifiers/is-even-pred.smt2 b/test/regress/regress0/quantifiers/is-even-pred.smt2 new file mode 100644 index 000000000..9808f4936 --- /dev/null +++ b/test/regress/regress0/quantifiers/is-even-pred.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(define-funs-rec ((is-even ((x Int)) Bool) (is-odd ((x Int)) Bool)) ((or (= x 0) (is-odd (- x 1))) (and (not (= x 0)) (is-even (- x 1))))) + +(assert (is-even 5)) +(check-sat) diff --git a/test/regress/regress0/quantifiers/is-even.smt2 b/test/regress/regress0/quantifiers/is-even.smt2 new file mode 100644 index 000000000..9aaac5e09 --- /dev/null +++ b/test/regress/regress0/quantifiers/is-even.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(define-funs-rec ((is-even ((x Int)) Int) (is-odd ((y Int)) Int)) ((ite (= x 0) 1 (ite (= (is-odd (- x 1)) 0) 1 0)) (ite (= y 0) 0 (ite (= (is-even (- y 1)) 0) 1 0)))) + +(assert (= (is-even 4) 0)) +(check-sat) diff --git a/test/regress/regress0/quantifiers/simp-len.smt2 b/test/regress/regress0/quantifiers/simp-len.smt2 new file mode 100644 index 000000000..d213e3426 --- /dev/null +++ b/test/regress/regress0/quantifiers/simp-len.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-datatypes () ((Lst (cons (head Int) (tail Lst)) (nil)))) + +(define-fun-rec len ((x Lst)) Int (ite (is-cons x) (+ 1 (len (tail x))) 0)) + +(assert (= (len (cons 0 nil)) 0)) +(check-sat)
\ No newline at end of file |