diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-01-18 22:33:22 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-01-18 22:33:22 +0100 |
| commit | 4d3e24e52765b03d8e6f36afe7de6168e8740693 (patch) | |
| tree | c5b3e7230e56db21cef630bbc95d94b7e3476618 /test | |
| parent | 9d677333439c15677b6891ee8f6bd368a5df9f0a (diff) | |
Bug fix rewriter for fun defs.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/fmf/Makefile.am | 6 | ||||
| -rw-r--r-- | test/regress/regress0/fmf/fd-false.smt2 | 6 | ||||
| -rwxr-xr-x | test/regress/regress0/fmf/tail_rec.smt2 | 11 |
3 files changed, 21 insertions, 2 deletions
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 5abadbcb8..ff2591a5b 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -42,8 +42,10 @@ TESTS = \ syn002-si-real-int.smt2 \ krs-sat.smt2 \ forall_unit_data2.smt2 \ - sc_bad_model_1221.smt2 \ - dt-proper-model.smt2 + sc_bad_model_1221.smt2 \ + dt-proper-model.smt2 \ + fd-false.smt2 \ + tail_rec.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/fd-false.smt2 b/test/regress/regress0/fmf/fd-false.smt2 new file mode 100644 index 000000000..4e1ff64b5 --- /dev/null +++ b/test/regress/regress0/fmf/fd-false.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --fmf-fun --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(define-fun-rec f ((x Int)) Bool false) +(assert (not (f 0))) +(check-sat) diff --git a/test/regress/regress0/fmf/tail_rec.smt2 b/test/regress/regress0/fmf/tail_rec.smt2 new file mode 100755 index 000000000..87b2d53a6 --- /dev/null +++ b/test/regress/regress0/fmf/tail_rec.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --fmf-fun --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(declare-sort elem 0) +(declare-datatypes () ((list (Nil) (Cons (hd elem) (tl list))))) +(define-fun-rec f ((x list)) elem + (ite (is-Nil x) (f x) (hd x)) +) +(declare-fun t () elem) +(assert (= t (f Nil))) +(check-sat) |