summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2009-12-17 17:07:57 +0000
committerMorgan Deters <mdeters@gmail.com>2009-12-17 17:07:57 +0000
commit3b06265b82d48074b3b733d655efd6dab6481150 (patch)
treeba75106a30f295d48d2645f7ccfa4b735e73e7b5
parent801e3d30b6c436963d2fcbc7ef5c407d1fe84b86 (diff)
add system regression testing infrastructure
-rw-r--r--configure.ac1
-rw-r--r--test/Makefile.am2
-rw-r--r--test/system/Makefile.am5
3 files changed, 7 insertions, 1 deletions
diff --git a/configure.ac b/configure.ac
index 0b8f8a5f3..f16844f4d 100644
--- a/configure.ac
+++ b/configure.ac
@@ -357,6 +357,7 @@ AC_CONFIG_FILES([
src/theory/uf/Makefile
test/Makefile
test/regress/Makefile
+ test/system/Makefile
test/unit/Makefile
])
diff --git a/test/Makefile.am b/test/Makefile.am
index ff449f768..2be47b41b 100644
--- a/test/Makefile.am
+++ b/test/Makefile.am
@@ -1 +1 @@
-SUBDIRS = unit regress
+SUBDIRS = unit system regress
diff --git a/test/system/Makefile.am b/test/system/Makefile.am
new file mode 100644
index 000000000..61527e4d8
--- /dev/null
+++ b/test/system/Makefile.am
@@ -0,0 +1,5 @@
+TESTS_ENVIRONMENT = @top_builddir@/bin/cvc4
+TESTS = \
+ simple.cvc \
+ simple.smt \
+ bug1.cvc
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback