diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-15 13:11:08 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-15 13:11:08 -0500 |
| commit | 6bac5cef88d22a2593d5da40dbb5cd45f63a266a (patch) | |
| tree | 9073dde12d6015a30c23b89f51bffcb358ae7670 /test/regress/regress0/fmf | |
| parent | 37c800cc6b7e6308482726a32e2353b63f63db48 (diff) | |
Allow 0 argument recursive functions. Fixes bug 782.
Diffstat (limited to 'test/regress/regress0/fmf')
| -rw-r--r-- | test/regress/regress0/fmf/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/fmf/bug782.smt2 | 24 |
2 files changed, 26 insertions, 1 deletions
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 79cff2947..ec5255db7 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -67,7 +67,8 @@ TESTS = \ ko-bound-set.cvc \ cons-sets-bounds.smt2 \ bug651.smt2 \ - bug652.smt2 + bug652.smt2 \ + bug782.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/bug782.smt2 b/test/regress/regress0/fmf/bug782.smt2 new file mode 100644 index 000000000..603c783d3 --- /dev/null +++ b/test/regress/regress0/fmf/bug782.smt2 @@ -0,0 +1,24 @@ +; COMMAND-LINE: --fmf-fun --no-check-models +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(define-fun $$Bool.isTrue$$ ((b Bool)) Bool b) +(define-fun $$Bool.isFalse$$ ((b Bool)) Bool (not b)) + +(define-funs-rec + ( + (f123454321$multipleArgsFunction((x$$645421 Bool) (y$$645422 Bool)) Bool) + (f12345678$myConst() Int) + ) + ( + (= x$$645421 y$$645422) + 3 + ) +) + +(declare-fun i1000$$1000() Bool) +(declare-fun i1001$$1001() Bool) +(declare-fun i1002$$1002() Int) +(assert (f123454321$multipleArgsFunction i1000$$1000 i1001$$1001)) +(assert (= i1002$$1002 f12345678$myConst)) +(check-sat) |