Fix for fmf+incremental. Restrict cbqi to literals from ce body. Add regressions.

4 files changed, 33 insertions, 2 deletions

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)
+
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index 6bd732c76..a1f91a6ce 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -44,7 +44,8 @@ TESTS = commutative.sy \
         uminus_one.sy \
         sygus-dt.sy \
         dt-no-syntax.sy \
-        list-head-x.sy
+        list-head-x.sy \
+        clock-inc-tuple.sy
 
 # sygus tests currently taking too long for make regress
 EXTRA_DIST = $(TESTS) \
diff --git a/test/regress/regress0/sygus/clock-inc-tuple.sy b/test/regress/regress0/sygus/clock-inc-tuple.sy
new file mode 100644
index 000000000..09bdb8b4d
--- /dev/null
+++ b/test/regress/regress0/sygus/clock-inc-tuple.sy
@@ -0,0 +1,14 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si --no-dump-synth
+
+(set-logic ALL_SUPPORTED)
+(declare-var m Int)
+(declare-var s Int)
+(declare-var inc Int)
+(declare-datatypes () ( (tuple2 (tuple2 (_m Int) (_s Int))) ))
+
+(synth-fun x12 ((m Int) (s Int) (inc Int)) tuple2)
+(constraint (=> 
+(and (>= m 0) (>= s 0) (< s 3) (> inc 0)) 
+(and (>= (_m (x12 m s inc)) 0) (>= (_s (x12 m s inc)) 0) (< (_s (x12 m s inc)) 3) (= (+ (* (_m (x12 m s inc)) 3) (_s (x12 m s inc))) (+ (+ (* m 3) s) inc)))))
+(check-synth)