diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-10 20:24:34 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-10 20:24:34 -0500 |
| commit | e5d09628376cc101cbd3646dd64041170dacb402 (patch) | |
| tree | 6a08f0ac7d28c348947c1ae085b11fed3f5103ad /test | |
| parent | f1d4d477d7cbfb6c8ba79232986a4135c5647e4a (diff) | |
Properly implement function extensionality based on cardinality (#1765)
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) |