From 1d18e5ebed9a5b20ed6a8fe21d11842acf6fa7ea Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 2 Sep 2011 20:41:08 +0000
Subject: Merge from my post-smtcomp branch.  Includes:

Dumping infrastructure.  Can dump preprocessed queries and clauses.  Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc.  For a
full list of options see --dump=help.

CUDD building much cleaner.

Documentation and assertion fixes.

Printer improvements, printing of commands in language-defined way, etc.

Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.

CVC3 compatibility layer (builds as libcompat).

SWIG detection and language binding support (infrastructure).

Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).

Copyright and file headers regenerated.
---
 test/system/Makefile.am | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

(limited to 'test/system/Makefile.am')

diff --git a/test/system/Makefile.am b/test/system/Makefile.am
index 40c045a74..66e2bd251 100644
--- a/test/system/Makefile.am
+++ b/test/system/Makefile.am
@@ -2,10 +2,14 @@ TESTS_ENVIRONMENT =
 TESTS = \
 	boilerplate \
 	ouroborous
+#	cvc3_main.cpp
 
 # Things that aren't tests but that tests rely on and need to
 # go into the distribution
-TEST_DEPS_DIST =
+TEST_DEPS_DIST = \
+	cvc3_main.cpp \
+	cvc3_george.h \
+	cvc3_george.cpp
 
 # Make-level dependencies; these don't go in the source distribution
 # but should trigger a re-compile of all unit tests.  Libraries are
@@ -15,7 +19,9 @@ TEST_DEPS_DIST =
 # changes made in the header files.
 TEST_DEPS_NODIST = \
 	$(abs_top_builddir)/src/libcvc4.la \
-	$(abs_top_builddir)/src/parser/libcvc4parser.la
+	$(abs_top_builddir)/src/parser/libcvc4parser.la \
+	$(abs_top_builddir)/src/compat/libcvc4compat.la \
+	cvc3_george.lo
 
 TEST_DEPS = \
 	$(TEST_DEPS_DIST) \
@@ -43,6 +49,7 @@ AM_CPPFLAGS = \
 	-D __BUILDING_CVC4_SYSTEM_TEST \
 	$(TEST_CPPFLAGS)
 LIBADD = \
+	@abs_top_builddir@/src/compat/libcvc4compat.la \
 	@abs_top_builddir@/src/parser/libcvc4parser.la \
 	@abs_top_builddir@/src/libcvc4.la
 
@@ -51,6 +58,8 @@ $(TESTS:%=%.lo): %.lo: %.cpp
 	$(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS) -c -o $@ $+
 $(TESTS): %: %.lo $(LIBADD)
 	$(AM_V_CXXLD)$(system_LINK) $(LIBADD) $(AM_LDFLAGS) $<
+cvc3_main: cvc3_george.lo $(LIBADD)
+	$(AM_V_CXXLD)$(system_LINK) $(LIBADD) $(AM_LDFLAGS) $+
 
 # trick automake into setting LTCXXCOMPILE, CXXLINK, etc.
 if CVC4_FALSE
-- 
cgit v1.2.3