diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
| -rw-r--r-- | test/regress/regress0/ho/finite-fun-ext.smt2 | 14 |
2 files changed, 15 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 46d856156..3899ff367 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -443,6 +443,7 @@ REG0_TESTS = \ regress0/ho/ext-ho.smt2 \ regress0/ho/ext-sat-partial-eval.smt2 \ regress0/ho/ext-sat.smt2 \ + regress0/ho/finite-fun-ext.smt2 \ regress0/ho/ho-match-fun-suffix.smt2 \ regress0/ho/ho-matching-enum.smt2 \ regress0/ho/ho-matching-nested-app.smt2 \ diff --git a/test/regress/regress0/ho/finite-fun-ext.smt2 b/test/regress/regress0/ho/finite-fun-ext.smt2 new file mode 100644 index 000000000..005a2109a --- /dev/null +++ b/test/regress/regress0/ho/finite-fun-ext.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --uf-ho +; EXPECT: unsat +(set-logic ALL) + +(declare-datatype Unit ((unit))) + +(declare-fun f (Int) Unit) +(declare-fun g (Int) Unit) +(declare-fun P ((-> Int Unit)) Bool) + +(assert (P f)) +(assert (not (P g))) + +(check-sat) |