diff options
Diffstat (limited to 'test')
-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) |