summaryrefslogtreecommitdiff
path: root/test/regress/Makefile.tests
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-04-10 20:24:34 -0500
committerGitHub <noreply@github.com>2018-04-10 20:24:34 -0500
commite5d09628376cc101cbd3646dd64041170dacb402 (patch)
tree6a08f0ac7d28c348947c1ae085b11fed3f5103ad /test/regress/Makefile.tests
parentf1d4d477d7cbfb6c8ba79232986a4135c5647e4a (diff)
Properly implement function extensionality based on cardinality (#1765)
Diffstat (limited to 'test/regress/Makefile.tests')
-rw-r--r--test/regress/Makefile.tests1
1 files changed, 1 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 \
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback