summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bv/Makefile.am
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2011-04-18 19:08:11 +0000
committerMorgan Deters <mdeters@gmail.com>2011-04-18 19:08:11 +0000
commitd1ba1ccd5a3c55ba7a0e63b33fd921642e44752d (patch)
treef3d22cdd12076a488dff2e9176dd1f619c731902 /test/regress/regress0/bv/Makefile.am
parent267858307741675cb78e829270e619f57cf21a27 (diff)
more work on CVC language
Diffstat (limited to 'test/regress/regress0/bv/Makefile.am')
-rw-r--r--test/regress/regress0/bv/Makefile.am5
1 files changed, 3 insertions, 2 deletions
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index dd4246e16..92db8d453 100644
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -14,12 +14,13 @@ SMT_TESTS =
SMT2_TESTS =
# Regression tests for PL inputs
-CVC_TESTS =
+CVC_TESTS = bvsimple.cvc
# Regression tests derived from bug reports
BUG_TESTS =
TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
-EXTRA_DIST = $(TESTS)
+EXTRA_DIST = $(TESTS) \
+ test00.smt
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback