From 4247dc59f1219695750a33db776ae02b244cee7f Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 23 Mar 2015 17:54:55 +0100
Subject: Parsing support for define-fun-rec/define-funs-rec.

---
 test/regress/regress0/quantifiers/Makefile.am       | 5 ++++-
 test/regress/regress0/quantifiers/is-even-pred.smt2 | 7 +++++++
 test/regress/regress0/quantifiers/is-even.smt2      | 7 +++++++
 test/regress/regress0/quantifiers/simp-len.smt2     | 9 +++++++++
 4 files changed, 27 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress0/quantifiers/is-even-pred.smt2
 create mode 100644 test/regress/regress0/quantifiers/is-even.smt2
 create mode 100644 test/regress/regress0/quantifiers/simp-len.smt2

(limited to 'test/regress/regress0/quantifiers')

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
-- 
cgit v1.2.3