diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-29 15:17:03 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-29 15:17:03 +0200 |
| commit | 4182943e7accc8a0e05f6dfdf9db7db06e94c6cd (patch) | |
| tree | d4f3bad70e464321a4e7fe977f1528f783dcd1b1 /test/regress/regress0/push-pop | |
| parent | ef7b7bba7bc9b207d5a2198518f21b13490caa32 (diff) | |
Fix for fmf+incremental. Restrict cbqi to literals from ce body. Add regressions.
Diffstat (limited to 'test/regress/regress0/push-pop')
| -rw-r--r-- | test/regress/regress0/push-pop/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/push-pop/fmf-fun-dbu.smt2 | 15 |
2 files changed, 17 insertions, 1 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) + |