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/fmf-fun-dbu.smt2 | |
| parent | ef7b7bba7bc9b207d5a2198518f21b13490caa32 (diff) | |
Fix for fmf+incremental. Restrict cbqi to literals from ce body. Add regressions.
Diffstat (limited to 'test/regress/regress0/push-pop/fmf-fun-dbu.smt2')
| -rw-r--r-- | test/regress/regress0/push-pop/fmf-fun-dbu.smt2 | 15 |
1 files changed, 15 insertions, 0 deletions
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) + |