From 4247dc59f1219695750a33db776ae02b244cee7f Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 23 Mar 2015 17:54:55 +0100 Subject: Parsing support for define-fun-rec/define-funs-rec. --- test/regress/regress0/quantifiers/is-even-pred.smt2 | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 test/regress/regress0/quantifiers/is-even-pred.smt2 (limited to 'test/regress/regress0/quantifiers/is-even-pred.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) -- cgit v1.2.3