From 4182943e7accc8a0e05f6dfdf9db7db06e94c6cd Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 29 Sep 2015 15:17:03 +0200
Subject: Fix for fmf+incremental. Restrict cbqi to literals from ce body.  Add
 regressions.

---
 test/regress/regress0/push-pop/Makefile.am      |  3 ++-
 test/regress/regress0/push-pop/fmf-fun-dbu.smt2 | 15 +++++++++++++++
 2 files changed, 17 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress0/push-pop/fmf-fun-dbu.smt2

(limited to 'test/regress/regress0/push-pop')

diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index 6d50cc39f..bcf6403b7 100644
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -43,7 +43,8 @@ BUG_TESTS = \
   bug654-dd.smt2 \
   bug-fmf-fun-skolem.smt2 \
   bug674.smt2 \
-  inc-double-u.smt2
+  inc-double-u.smt2 \
+  fmf-fun-dbu.smt2
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/push-pop/fmf-fun-dbu.smt2 b/test/regress/regress0/push-pop/fmf-fun-dbu.smt2
new file mode 100644
index 000000000..125d5fcc9
--- /dev/null
+++ b/test/regress/regress0/push-pop/fmf-fun-dbu.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --incremental --fmf-fun --no-check-models
+(set-logic UFDTLIA)
+(set-option :produce-models true)
+(set-info :smt-lib-version 2.5)
+(declare-datatypes () ((List (Nil) (Cons (Cons$head Int) (Cons$tail List)))))
+(define-fun-rec all-z ((x List)) Bool (=> (is-Cons x) (and (= 0 (Cons$head x)) (all-z (Cons$tail x)))))
+(define-fun-rec len ((x List)) Int (ite (is-Nil x) 0 (+ 1 (len (Cons$tail x)))))
+(declare-fun root() List)
+; EXPECT: sat
+(assert (and (all-z root) (<= 1 (len root))))
+(check-sat)
+; EXPECT: sat
+(assert (= root (Cons 0 Nil)))
+(check-sat)
+
-- 
cgit v1.2.3