+ test infrastructure fixes

+ regenerate configure script
+ add CVC4::Message output class
+ add some IllegalArgument() assertion things
+ rename NodeManager::mkExpr() to mkNode()

14 files changed, 606 insertions, 124 deletions

diff --git a/configure b/configure
index 15131cbb7..919592ca3 100755
--- a/configure
+++ b/configure
@@ -16355,7 +16355,7 @@ fi
 mk_include=include
 
 
-ac_config_files="$ac_config_files Makefile.builds Makefile contrib/Makefile doc/Makefile src/Makefile src/expr/Makefile src/smt/Makefile src/main/Makefile src/prop/minisat/Makefile src/prop/Makefile src/util/Makefile src/context/Makefile src/parser/Makefile src/parser/cvc/Makefile src/parser/smt/Makefile src/theory/Makefile src/theory/uf/Makefile test/Makefile test/regress/Makefile test/unit/Makefile"
+ac_config_files="$ac_config_files Makefile.builds Makefile contrib/Makefile doc/Makefile src/Makefile src/expr/Makefile src/smt/Makefile src/main/Makefile src/prop/minisat/Makefile src/prop/Makefile src/util/Makefile src/context/Makefile src/parser/Makefile src/parser/cvc/Makefile src/parser/smt/Makefile src/theory/Makefile src/theory/uf/Makefile test/Makefile test/regress/Makefile test/system/Makefile test/unit/Makefile"
 
 
 cat >confcache <<\_ACEOF
@@ -17454,6 +17454,7 @@ do
     "src/theory/uf/Makefile") CONFIG_FILES="$CONFIG_FILES src/theory/uf/Makefile" ;;
     "test/Makefile") CONFIG_FILES="$CONFIG_FILES test/Makefile" ;;
     "test/regress/Makefile") CONFIG_FILES="$CONFIG_FILES test/regress/Makefile" ;;
+    "test/system/Makefile") CONFIG_FILES="$CONFIG_FILES test/system/Makefile" ;;
     "test/unit/Makefile") CONFIG_FILES="$CONFIG_FILES test/unit/Makefile" ;;
 
   *) as_fn_error "invalid argument: \`$ac_config_target'" "$LINENO" 5;;
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
index 877ba9d3c..ea1649e12 100644
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager.cpp
@@ -23,27 +23,27 @@ ExprManager::~ExprManager() {
 }
 
 Expr ExprManager::mkExpr(Kind kind) {
-  return Expr(this, new Node(d_nm->mkExpr(kind)));
+  return Expr(this, new Node(d_nm->mkNode(kind)));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
-  return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode())));
+  return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode())));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
-  return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode(),
+  return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(),
                                           child2.getNode())));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                          const Expr& child3) {
-  return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode(),
+  return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(),
                                           child2.getNode(), child3.getNode())));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                          const Expr& child3, const Expr& child4) {
-  return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode(),
+  return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(),
                                           child2.getNode(), child3.getNode(),
                                           child4.getNode())));
 }
@@ -51,7 +51,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                          const Expr& child3, const Expr& child4,
                          const Expr& child5) {
-  return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode(),
+  return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(),
                                           child2.getNode(), child3.getNode(),
                                           child5.getNode())));
 }
@@ -64,7 +64,7 @@ Expr ExprManager::mkExpr(Kind kind, const vector<Expr>& children) {
     nodes.push_back(it->getNode());
     ++it;
   }
-  return Expr(this, new Node(d_nm->mkExpr(kind, nodes)));
+  return Expr(this, new Node(d_nm->mkNode(kind, nodes)));
 }
 
 Expr ExprManager::mkVar() {
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 40dd70457..334cf1b0e 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -87,35 +87,35 @@ uint64_t Node::hash() const {
 }
 
 Node Node::eqExpr(const Node& right) const {
-  return NodeManager::currentNM()->mkExpr(EQUAL, *this, right);
+  return NodeManager::currentNM()->mkNode(EQUAL, *this, right);
 }
 
 Node Node::notExpr() const {
-  return NodeManager::currentNM()->mkExpr(NOT, *this);
+  return NodeManager::currentNM()->mkNode(NOT, *this);
 }
 
 Node Node::andExpr(const Node& right) const {
-  return NodeManager::currentNM()->mkExpr(AND, *this, right);
+  return NodeManager::currentNM()->mkNode(AND, *this, right);
 }
 
 Node Node::orExpr(const Node& right) const {
-  return NodeManager::currentNM()->mkExpr(OR, *this, right);
+  return NodeManager::currentNM()->mkNode(OR, *this, right);
 }
 
 Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const {
-  return NodeManager::currentNM()->mkExpr(ITE, *this, thenpart, elsepart);
+  return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart);
 }
 
 Node Node::iffExpr(const Node& right) const {
-  return NodeManager::currentNM()->mkExpr(IFF, *this, right);
+  return NodeManager::currentNM()->mkNode(IFF, *this, right);
 }
 
 Node Node::impExpr(const Node& right) const {
-  return NodeManager::currentNM()->mkExpr(IMPLIES, *this, right);
+  return NodeManager::currentNM()->mkNode(IMPLIES, *this, right);
 }
 
 Node Node::xorExpr(const Node& right) const {
-  return NodeManager::currentNM()->mkExpr(XOR, *this, right);
+  return NodeManager::currentNM()->mkNode(XOR, *this, right);
 }
 
 }/* CVC4 namespace */
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 4b550ee3d..7e871d9c3 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -101,32 +101,32 @@ NodeValue* NodeManager::lookupNoInsert(uint64_t hash, NodeValue* ev) {
 
 // general expression-builders
 
-Node NodeManager::mkExpr(Kind kind) {
+Node NodeManager::mkNode(Kind kind) {
   return NodeBuilder<>(this, kind);
 }
 
-Node NodeManager::mkExpr(Kind kind, const Node& child1) {
+Node NodeManager::mkNode(Kind kind, const Node& child1) {
   return NodeBuilder<>(this, kind) << child1;
 }
 
-Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2) {
+Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2) {
   return NodeBuilder<>(this, kind) << child1 << child2;
 }
 
-Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3) {
+Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3) {
   return NodeBuilder<>(this, kind) << child1 << child2 << child3;
 }
 
-Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4) {
+Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4) {
   return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4;
 }
 
-Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5) {
+Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5) {
   return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4 << child5;
 }
 
 // N-ary version
-Node NodeManager::mkExpr(Kind kind, const std::vector<Node>& children) {
+Node NodeManager::mkNode(Kind kind, const std::vector<Node>& children) {
   return NodeBuilder<>(this, kind).append(children);
 }
 
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 8caa797fa..643f09f11 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -36,14 +36,14 @@ public:
   static NodeManager* currentNM() { return s_current; }
 
   // general expression-builders
-  Node mkExpr(Kind kind);
-  Node mkExpr(Kind kind, const Node& child1);
-  Node mkExpr(Kind kind, const Node& child1, const Node& child2);
-  Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3);
-  Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4);
-  Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5);
+  Node mkNode(Kind kind);
+  Node mkNode(Kind kind, const Node& child1);
+  Node mkNode(Kind kind, const Node& child1, const Node& child2);
+  Node mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3);
+  Node mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4);
+  Node mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5);
   // N-ary version
-  Node mkExpr(Kind kind, const std::vector<Node>& children);
+  Node mkNode(Kind kind, const std::vector<Node>& children);
 
   // variables are special, because duplicates are permitted
   Node mkVar();
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 4e408823f..187a0f316 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -81,6 +81,7 @@ int main(int argc, char *argv[]) {
       Trace.setStream(CVC4::null_os);
       Notice.setStream(CVC4::null_os);
       Chat.setStream(CVC4::null_os);
+      Message.setStream(CVC4::null_os);
       Warning.setStream(CVC4::null_os);
     } else {
       if(options.verbosity < 2) {
@@ -90,6 +91,7 @@ int main(int argc, char *argv[]) {
         Notice.setStream(CVC4::null_os);
       }
       if(options.verbosity < 0) {
+        Message.setStream(CVC4::null_os);
         Warning.setStream(CVC4::null_os);
       }
     }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 723263177..f07ad577e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -41,7 +41,7 @@ Node SmtEngine::processAssertionList() {
   for(std::vector<Node>::iterator i = d_assertions.begin();
       i != d_assertions.end();
       ++i)
-    asserts = asserts.isNull() ? *i : d_em->mkExpr(AND, asserts, *i);
+    asserts = asserts.isNull() ? *i : d_em->mkNode(AND, asserts, *i);
   return asserts;
 }
 
diff --git a/src/util/Assert.h b/src/util/Assert.h
index c3b81727c..26a1ee7d4 100644
--- a/src/util/Assert.h
+++ b/src/util/Assert.h
@@ -122,7 +122,8 @@ public:
     va_list args;
     va_start(args, fmt);
     construct("Illegal argument detected",
-              argDesc, function, file, line, fmt, args);
+              ( std::string(argDesc) + " invalid" ).c_str(),
+              function, file, line, fmt, args);
     va_end(args);
   }
 
@@ -130,7 +131,31 @@ public:
                            const char* file, unsigned line) :
     AssertionException() {
     construct("Illegal argument detected",
-              argDesc, function, file, line);
+              ( std::string(argDesc) + " invalid" ).c_str(),
+              function, file, line);
+  }
+
+  IllegalArgumentException(const char* condStr, const char* argDesc,
+                           const char* function, const char* file,
+                           unsigned line, const char* fmt, ...) :
+    AssertionException() {
+    va_list args;
+    va_start(args, fmt);
+    construct("Illegal argument detected",
+              ( std::string(argDesc) + " invalid; expected " +
+                condStr + " to hold" ).c_str(),
+              function, file, line, fmt, args);
+    va_end(args);
+  }
+
+  IllegalArgumentException(const char* condStr, const char* argDesc,
+                           const char* function, const char* file,
+                           unsigned line) :
+    AssertionException() {
+    construct("Illegal argument detected",
+              ( std::string(argDesc) + " invalid; expected " +
+                condStr + " to hold" ).c_str(),
+              function, file, line);
   }
 };/* class IllegalArgumentException */
 
@@ -146,11 +171,21 @@ public:
   throw UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 #define IllegalArgument(arg, msg...) \
   throw IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
+#define CheckArgument(cond, arg, msg...)         \
+  AlwaysAssertArgument(cond, arg, ## msg)
+#define AlwaysAssertArgument(cond, arg, msg...)  \
+  do { \
+    if(EXPECT_FALSE( ! (cond) )) { \
+      throw IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
+    } \
+  } while(0)
 
 #ifdef CVC4_ASSERTIONS
 #  define Assert(cond, msg...) AlwaysAssert(cond, ## msg)
+#  define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ## msg)
 #else /* ! CVC4_ASSERTIONS */
 #  define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/
+#  define AssertArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/
 #endif /* CVC4_ASSERTIONS */
 
 }/* CVC4 namespace */
diff --git a/src/util/output.cpp b/src/util/output.cpp
index e07f32a66..103a3d61a 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -22,6 +22,7 @@ std::ostream null_os(&null_sb);
 
 DebugC   Debug  (&std::cout);
 WarningC Warning(&std::cerr);
+MessageC Message(&std::cout);
 NoticeC  Notice (&std::cout);
 ChatC    Chat   (&std::cout);
 TraceC   Trace  (&std::cout);
diff --git a/src/util/output.h b/src/util/output.h
index b6532b93a..43dfe8a40 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -91,6 +91,24 @@ public:
 
 extern WarningC Warning CVC4_PUBLIC;
 
+class CVC4_PUBLIC MessageC {
+  std::ostream *d_os;
+
+public:
+  MessageC(std::ostream* os) : d_os(os) {}
+
+  void operator()(const char* s) { *d_os << s; }
+  void operator()(std::string s) { *d_os << s; }
+
+  void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+
+  std::ostream& operator()() { return *d_os; }
+
+  void setStream(std::ostream& os) { d_os = &os; }
+};/* class Message */
+
+extern MessageC Message CVC4_PUBLIC;
+
 class CVC4_PUBLIC NoticeC {
   std::ostream *d_os;
 
diff --git a/test/Makefile.in b/test/Makefile.in
index 211ec123c..c2eabd8a4 100644
--- a/test/Makefile.in
+++ b/test/Makefile.in
@@ -228,7 +228,7 @@ target_vendor = @target_vendor@
 top_build_prefix = @top_build_prefix@
 top_builddir = @top_builddir@
 top_srcdir = @top_srcdir@
-SUBDIRS = unit regress
+SUBDIRS = unit system regress
 all: all-recursive
 
 .SUFFIXES:
diff --git a/test/system/Makefile.in b/test/system/Makefile.in
new file mode 100644
index 000000000..14e1ac9c7
--- /dev/null
+++ b/test/system/Makefile.in
@@ -0,0 +1,480 @@
+# Makefile.in generated by automake 1.11 from Makefile.am.
+# @configure_input@
+
+# Copyright (C) 1994, 1995, 1996, 1997, 1998, 1999, 2000, 2001, 2002,
+# 2003, 2004, 2005, 2006, 2007, 2008, 2009  Free Software Foundation,
+# Inc.
+# This Makefile.in is free software; the Free Software Foundation
+# gives unlimited permission to copy and/or distribute it,
+# with or without modifications, as long as this notice is preserved.
+
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY, to the extent permitted by law; without
+# even the implied warranty of MERCHANTABILITY or FITNESS FOR A
+# PARTICULAR PURPOSE.
+
+@SET_MAKE@
+VPATH = @srcdir@
+pkgdatadir = $(datadir)/@PACKAGE@
+pkgincludedir = $(includedir)/@PACKAGE@
+pkglibdir = $(libdir)/@PACKAGE@
+pkglibexecdir = $(libexecdir)/@PACKAGE@
+am__cd = CDPATH="$${ZSH_VERSION+.}$(PATH_SEPARATOR)" && cd
+install_sh_DATA = $(install_sh) -c -m 644
+install_sh_PROGRAM = $(install_sh) -c
+install_sh_SCRIPT = $(install_sh) -c
+INSTALL_HEADER = $(INSTALL_DATA)
+transform = $(program_transform_name)
+NORMAL_INSTALL = :
+PRE_INSTALL = :
+POST_INSTALL = :
+NORMAL_UNINSTALL = :
+PRE_UNINSTALL = :
+POST_UNINSTALL = :
+build_triplet = @build@
+host_triplet = @host@
+target_triplet = @target@
+subdir = test/system
+DIST_COMMON = $(srcdir)/Makefile.am $(srcdir)/Makefile.in
+ACLOCAL_M4 = $(top_srcdir)/aclocal.m4
+am__aclocal_m4_deps = $(top_srcdir)/config/antlr.m4 \
+	$(top_srcdir)/config/cvc4.m4 $(top_srcdir)/config/libtool.m4 \
+	$(top_srcdir)/config/ltoptions.m4 \
+	$(top_srcdir)/config/ltsugar.m4 \
+	$(top_srcdir)/config/ltversion.m4 \
+	$(top_srcdir)/config/lt~obsolete.m4 $(top_srcdir)/configure.ac
+am__configure_deps = $(am__aclocal_m4_deps) $(CONFIGURE_DEPENDENCIES) \
+	$(ACLOCAL_M4)
+mkinstalldirs = $(install_sh) -d
+CONFIG_HEADER = $(top_builddir)/config.h
+CONFIG_CLEAN_FILES =
+CONFIG_CLEAN_VPATH_FILES =
+SOURCES =
+DIST_SOURCES =
+am__tty_colors = \
+red=; grn=; lgn=; blu=; std=
+DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST)
+ACLOCAL = @ACLOCAL@
+AMTAR = @AMTAR@
+ANTLR = @ANTLR@
+ANTLR_INCLUDES = @ANTLR_INCLUDES@
+ANTLR_LDFLAGS = @ANTLR_LDFLAGS@
+AR = @AR@
+AS = @AS@
+AUTOCONF = @AUTOCONF@
+AUTOHEADER = @AUTOHEADER@
+AUTOMAKE = @AUTOMAKE@
+AWK = @AWK@
+CC = @CC@
+CCDEPMODE = @CCDEPMODE@
+CFLAGS = @CFLAGS@
+CPP = @CPP@
+CPPFLAGS = @CPPFLAGS@
+CVC4_LIBRARY_RELEASE_CODE = @CVC4_LIBRARY_RELEASE_CODE@
+CVC4_LIBRARY_VERSION = @CVC4_LIBRARY_VERSION@
+CVC4_PARSER_LIBRARY_VERSION = @CVC4_PARSER_LIBRARY_VERSION@
+CXX = @CXX@
+CXXCPP = @CXXCPP@
+CXXDEPMODE = @CXXDEPMODE@
+CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
+CXXTESTGEN = @CXXTESTGEN@
+CYGPATH_W = @CYGPATH_W@
+DEFS = @DEFS@
+DEPDIR = @DEPDIR@
+DLLTOOL = @DLLTOOL@
+DOXYGEN = @DOXYGEN@
+DSYMUTIL = @DSYMUTIL@
+DUMPBIN = @DUMPBIN@
+ECHO_C = @ECHO_C@
+ECHO_N = @ECHO_N@
+ECHO_T = @ECHO_T@
+EGREP = @EGREP@
+EXEEXT = @EXEEXT@
+FGREP = @FGREP@
+GREP = @GREP@
+INSTALL = @INSTALL@
+INSTALL_DATA = @INSTALL_DATA@
+INSTALL_PROGRAM = @INSTALL_PROGRAM@
+INSTALL_SCRIPT = @INSTALL_SCRIPT@
+INSTALL_STRIP_PROGRAM = @INSTALL_STRIP_PROGRAM@
+LD = @LD@
+LDFLAGS = @LDFLAGS@
+LIBOBJS = @LIBOBJS@
+LIBS = @LIBS@
+LIBTOOL = @LIBTOOL@
+LIPO = @LIPO@
+LN_S = @LN_S@
+LTLIBOBJS = @LTLIBOBJS@
+MAKEINFO = @MAKEINFO@
+MKDIR_P = @MKDIR_P@
+NM = @NM@
+NMEDIT = @NMEDIT@
+OBJDUMP = @OBJDUMP@
+OBJEXT = @OBJEXT@
+OTOOL = @OTOOL@
+OTOOL64 = @OTOOL64@
+PACKAGE = @PACKAGE@
+PACKAGE_BUGREPORT = @PACKAGE_BUGREPORT@
+PACKAGE_NAME = @PACKAGE_NAME@
+PACKAGE_STRING = @PACKAGE_STRING@
+PACKAGE_TARNAME = @PACKAGE_TARNAME@
+PACKAGE_URL = @PACKAGE_URL@
+PACKAGE_VERSION = @PACKAGE_VERSION@
+PATH_SEPARATOR = @PATH_SEPARATOR@
+PERL = @PERL@
+RANLIB = @RANLIB@
+SED = @SED@
+SET_MAKE = @SET_MAKE@
+SHELL = @SHELL@
+STRIP = @STRIP@
+TEST_CPPFLAGS = @TEST_CPPFLAGS@
+TEST_CXXFLAGS = @TEST_CXXFLAGS@
+TEST_LDFLAGS = @TEST_LDFLAGS@
+VERSION = @VERSION@
+abs_builddir = @abs_builddir@
+abs_srcdir = @abs_srcdir@
+abs_top_builddir = @abs_top_builddir@
+abs_top_srcdir = @abs_top_srcdir@
+ac_ct_CC = @ac_ct_CC@
+ac_ct_CXX = @ac_ct_CXX@
+ac_ct_DUMPBIN = @ac_ct_DUMPBIN@
+am__include = @am__include@
+am__leading_dot = @am__leading_dot@
+am__quote = @am__quote@
+am__tar = @am__tar@
+am__untar = @am__untar@
+bindir = @bindir@
+build = @build@
+build_alias = @build_alias@
+build_cpu = @build_cpu@
+build_os = @build_os@
+build_vendor = @build_vendor@
+builddir = @builddir@
+datadir = @datadir@
+datarootdir = @datarootdir@
+docdir = @docdir@
+dvidir = @dvidir@
+exec_prefix = @exec_prefix@
+host = @host@
+host_alias = @host_alias@
+host_cpu = @host_cpu@
+host_os = @host_os@
+host_vendor = @host_vendor@
+htmldir = @htmldir@
+includedir = @includedir@
+infodir = @infodir@
+install_sh = @install_sh@
+libdir = @libdir@
+libexecdir = @libexecdir@
+localedir = @localedir@
+localstatedir = @localstatedir@
+lt_ECHO = @lt_ECHO@
+mandir = @mandir@
+mk_include = @mk_include@
+mkdir_p = @mkdir_p@
+oldincludedir = @oldincludedir@
+pdfdir = @pdfdir@
+prefix = @prefix@
+program_transform_name = @program_transform_name@
+psdir = @psdir@
+sbindir = @sbindir@
+sharedstatedir = @sharedstatedir@
+srcdir = @srcdir@
+sysconfdir = @sysconfdir@
+target = @target@
+target_alias = @target_alias@
+target_cpu = @target_cpu@
+target_os = @target_os@
+target_vendor = @target_vendor@
+top_build_prefix = @top_build_prefix@
+top_builddir = @top_builddir@
+top_srcdir = @top_srcdir@
+TESTS_ENVIRONMENT = @top_builddir@/bin/cvc4
+TESTS = \
+	simple.cvc \
+	simple.smt \
+	bug1.cvc
+
+all: all-am
+
+.SUFFIXES:
+$(srcdir)/Makefile.in:  $(srcdir)/Makefile.am  $(am__configure_deps)
+	@for dep in $?; do \
+	  case '$(am__configure_deps)' in \
+	    *$$dep*) \
+	      ( cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh ) \
+	        && { if test -f $@; then exit 0; else break; fi; }; \
+	      exit 1;; \
+	  esac; \
+	done; \
+	echo ' cd $(top_srcdir) && $(AUTOMAKE) --foreign test/system/Makefile'; \
+	$(am__cd) $(top_srcdir) && \
+	  $(AUTOMAKE) --foreign test/system/Makefile
+.PRECIOUS: Makefile
+Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status
+	@case '$?' in \
+	  *config.status*) \
+	    cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh;; \
+	  *) \
+	    echo ' cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe)'; \
+	    cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe);; \
+	esac;
+
+$(top_builddir)/config.status: $(top_srcdir)/configure $(CONFIG_STATUS_DEPENDENCIES)
+	cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
+
+$(top_srcdir)/configure:  $(am__configure_deps)
+	cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
+$(ACLOCAL_M4):  $(am__aclocal_m4_deps)
+	cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
+$(am__aclocal_m4_deps):
+
+mostlyclean-libtool:
+	-rm -f *.lo
+
+clean-libtool:
+	-rm -rf .libs _libs
+tags: TAGS
+TAGS:
+
+ctags: CTAGS
+CTAGS:
+
+
+check-TESTS: $(TESTS)
+	@failed=0; all=0; xfail=0; xpass=0; skip=0; \
+	srcdir=$(srcdir); export srcdir; \
+	list=' $(TESTS) '; \
+	$(am__tty_colors); \
+	if test -n "$$list"; then \
+	  for tst in $$list; do \
+	    if test -f ./$$tst; then dir=./; \
+	    elif test -f $$tst; then dir=; \
+	    else dir="$(srcdir)/"; fi; \
+	    if $(TESTS_ENVIRONMENT) $${dir}$$tst; then \
+	      all=`expr $$all + 1`; \
+	      case " $(XFAIL_TESTS) " in \
+	      *[\ \	]$$tst[\ \	]*) \
+		xpass=`expr $$xpass + 1`; \
+		failed=`expr $$failed + 1`; \
+		col=$$red; res=XPASS; \
+	      ;; \
+	      *) \
+		col=$$grn; res=PASS; \
+	      ;; \
+	      esac; \
+	    elif test $$? -ne 77; then \
+	      all=`expr $$all + 1`; \
+	      case " $(XFAIL_TESTS) " in \
+	      *[\ \	]$$tst[\ \	]*) \
+		xfail=`expr $$xfail + 1`; \
+		col=$$lgn; res=XFAIL; \
+	      ;; \
+	      *) \
+		failed=`expr $$failed + 1`; \
+		col=$$red; res=FAIL; \
+	      ;; \
+	      esac; \
+	    else \
+	      skip=`expr $$skip + 1`; \
+	      col=$$blu; res=SKIP; \
+	    fi; \
+	    echo "$${col}$$res$${std}: $$tst"; \
+	  done; \
+	  if test "$$all" -eq 1; then \
+	    tests="test"; \
+	    All=""; \
+	  else \
+	    tests="tests"; \
+	    All="All "; \
+	  fi; \
+	  if test "$$failed" -eq 0; then \
+	    if test "$$xfail" -eq 0; then \
+	      banner="$$All$$all $$tests passed"; \
+	    else \
+	      if test "$$xfail" -eq 1; then failures=failure; else failures=failures; fi; \
+	      banner="$$All$$all $$tests behaved as expected ($$xfail expected $$failures)"; \
+	    fi; \
+	  else \
+	    if test "$$xpass" -eq 0; then \
+	      banner="$$failed of $$all $$tests failed"; \
+	    else \
+	      if test "$$xpass" -eq 1; then passes=pass; else passes=passes; fi; \
+	      banner="$$failed of $$all $$tests did not behave as expected ($$xpass unexpected $$passes)"; \
+	    fi; \
+	  fi; \
+	  dashes="$$banner"; \
+	  skipped=""; \
+	  if test "$$skip" -ne 0; then \
+	    if test "$$skip" -eq 1; then \
+	      skipped="($$skip test was not run)"; \
+	    else \
+	      skipped="($$skip tests were not run)"; \
+	    fi; \
+	    test `echo "$$skipped" | wc -c` -le `echo "$$banner" | wc -c` || \
+	      dashes="$$skipped"; \
+	  fi; \
+	  report=""; \
+	  if test "$$failed" -ne 0 && test -n "$(PACKAGE_BUGREPORT)"; then \
+	    report="Please report to $(PACKAGE_BUGREPORT)"; \
+	    test `echo "$$report" | wc -c` -le `echo "$$banner" | wc -c` || \
+	      dashes="$$report"; \
+	  fi; \
+	  dashes=`echo "$$dashes" | sed s/./=/g`; \
+	  if test "$$failed" -eq 0; then \
+	    echo "$$grn$$dashes"; \
+	  else \
+	    echo "$$red$$dashes"; \
+	  fi; \
+	  echo "$$banner"; \
+	  test -z "$$skipped" || echo "$$skipped"; \
+	  test -z "$$report" || echo "$$report"; \
+	  echo "$$dashes$$std"; \
+	  test "$$failed" -eq 0; \
+	else :; fi
+
+distdir: $(DISTFILES)
+	@srcdirstrip=`echo "$(srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \
+	topsrcdirstrip=`echo "$(top_srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \
+	list='$(DISTFILES)'; \
+	  dist_files=`for file in $$list; do echo $$file; done | \
+	  sed -e "s|^$$srcdirstrip/||;t" \
+	      -e "s|^$$topsrcdirstrip/|$(top_builddir)/|;t"`; \
+	case $$dist_files in \
+	  */*) $(MKDIR_P) `echo "$$dist_files" | \
+			   sed '/\//!d;s|^|$(distdir)/|;s,/[^/]*$$,,' | \
+			   sort -u` ;; \
+	esac; \
+	for file in $$dist_files; do \
+	  if test -f $$file || test -d $$file; then d=.; else d=$(srcdir); fi; \
+	  if test -d $$d/$$file; then \
+	    dir=`echo "/$$file" | sed -e 's,/[^/]*$$,,'`; \
+	    if test -d "$(distdir)/$$file"; then \
+	      find "$(distdir)/$$file" -type d ! -perm -700 -exec chmod u+rwx {} \;; \
+	    fi; \
+	    if test -d $(srcdir)/$$file && test $$d != $(srcdir); then \
+	      cp -fpR $(srcdir)/$$file "$(distdir)$$dir" || exit 1; \
+	      find "$(distdir)/$$file" -type d ! -perm -700 -exec chmod u+rwx {} \;; \
+	    fi; \
+	    cp -fpR $$d/$$file "$(distdir)$$dir" || exit 1; \
+	  else \
+	    test -f "$(distdir)/$$file" \
+	    || cp -p $$d/$$file "$(distdir)/$$file" \
+	    || exit 1; \
+	  fi; \
+	done
+check-am: all-am
+	$(MAKE) $(AM_MAKEFLAGS) check-TESTS
+check: check-am
+all-am: Makefile
+installdirs:
+install: install-am
+install-exec: install-exec-am
+install-data: install-data-am
+uninstall: uninstall-am
+
+install-am: all-am
+	@$(MAKE) $(AM_MAKEFLAGS) install-exec-am install-data-am
+
+installcheck: installcheck-am
+install-strip:
+	$(MAKE) $(AM_MAKEFLAGS) INSTALL_PROGRAM="$(INSTALL_STRIP_PROGRAM)" \
+	  install_sh_PROGRAM="$(INSTALL_STRIP_PROGRAM)" INSTALL_STRIP_FLAG=-s \
+	  `test -z '$(STRIP)' || \
+	    echo "INSTALL_PROGRAM_ENV=STRIPPROG='$(STRIP)'"` install
+mostlyclean-generic:
+
+clean-generic:
+
+distclean-generic:
+	-test -z "$(CONFIG_CLEAN_FILES)" || rm -f $(CONFIG_CLEAN_FILES)
+	-test . = "$(srcdir)" || test -z "$(CONFIG_CLEAN_VPATH_FILES)" || rm -f $(CONFIG_CLEAN_VPATH_FILES)
+
+maintainer-clean-generic:
+	@echo "This command is intended for maintainers to use"
+	@echo "it deletes files that may require special tools to rebuild."
+clean: clean-am
+
+clean-am: clean-generic clean-libtool mostlyclean-am
+
+distclean: distclean-am
+	-rm -f Makefile
+distclean-am: clean-am distclean-generic
+
+dvi: dvi-am
+
+dvi-am:
+
+html: html-am
+
+html-am:
+
+info: info-am
+
+info-am:
+
+install-data-am:
+
+install-dvi: install-dvi-am
+
+install-dvi-am:
+
+install-exec-am:
+
+install-html: install-html-am
+
+install-html-am:
+
+install-info: install-info-am
+
+install-info-am:
+
+install-man:
+
+install-pdf: install-pdf-am
+
+install-pdf-am:
+
+install-ps: install-ps-am
+
+install-ps-am:
+
+installcheck-am:
+
+maintainer-clean: maintainer-clean-am
+	-rm -f Makefile
+maintainer-clean-am: distclean-am maintainer-clean-generic
+
+mostlyclean: mostlyclean-am
+
+mostlyclean-am: mostlyclean-generic mostlyclean-libtool
+
+pdf: pdf-am
+
+pdf-am:
+
+ps: ps-am
+
+ps-am:
+
+uninstall-am:
+
+.MAKE: check-am install-am install-strip
+
+.PHONY: all all-am check check-TESTS check-am clean clean-generic \
+	clean-libtool distclean distclean-generic distclean-libtool \
+	distdir dvi dvi-am html html-am info info-am install \
+	install-am install-data install-data-am install-dvi \
+	install-dvi-am install-exec install-exec-am install-html \
+	install-html-am install-info install-info-am install-man \
+	install-pdf install-pdf-am install-ps install-ps-am \
+	install-strip installcheck installcheck-am installdirs \
+	maintainer-clean maintainer-clean-generic mostlyclean \
+	mostlyclean-generic mostlyclean-libtool pdf pdf-am ps ps-am \
+	uninstall uninstall-am
+
+
+# Tell versions [3.59,3.63) of GNU make to not export all variables.
+# Otherwise a system limit (for SysV at least) may be exceeded.
+.NOEXPORT:
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 9c1c1c56b..f5ba6f410 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -11,43 +11,36 @@ AM_LDFLAGS_WHITE = \
 		@abs_top_builddir@/src/smt/libsmt.la \
 		@abs_top_builddir@/src/theory/libtheory.la \
 		@abs_top_builddir@/src/util/libutil.la \
+		@abs_top_builddir@/src/prop/libprop.la \
 		@abs_top_builddir@/src/prop/minisat/libminisat.la
 AM_LDFLAGS_BLACK = \
 		$(AM_LDFLAGS_WHITE)
 AM_LDFLAGS_PUBLIC = \
 		@abs_top_builddir@/src/libcvc4.la
 
-TESTS_WHITE = \
-	expr/node_white
-
-TESTS_BLACK = \
-	expr/node_black
-
-TESTS_PUBLIC =
-
 TESTS = \
-	$(TESTS_WHITE) \
-	$(TESTS_BLACK) \
-	$(TESTS_PUBLIC)
+	expr/node_white \
+	expr/node_black
 
-lib_LTLIBRARIES = libdummy.la
+# without these here, LTCXXCOMPILE, CXXLINK, etc., aren't set :-(
+noinst_LTLIBRARIES = libdummy.la
 libdummy_la_SOURCES = expr/node_black.cpp
 libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la
 
 $(TESTS:%=%.cpp): %.cpp: %.h
 	mkdir -p `dirname "$@"`
 	@CXXTESTGEN@ --have-eh --have-std --error-printer -o "$@" "$<"
-$(TESTS_WHITE): %: %.cpp
+$(filter %_white,$(TESTS)): %_white: %_white.cpp
 #	get these in here somehow
 #	$(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS)
 	$(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@.lo $<
 	$(CXXLINK) $(AM_LDFLAGS_WHITE) $@.lo
-$(TESTS_BLACK): %: %.cpp
+$(filter %_black,$(TESTS)): %_black: %_black.cpp
 #	get these in here somehow
 #	$(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS)
 	$(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -c -o $@.lo $<
 	$(CXXLINK) $(AM_LDFLAGS_BLACK) $@.lo
-$(TESTS_PUBLIC): %: %.cpp
+$(filter %_public,$(TESTS)): %_public: %_public.cpp
 #	get these in here somehow
 #	$(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS)
 	$(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@.lo $<
diff --git a/test/unit/Makefile.in b/test/unit/Makefile.in
index 5432c809e..23153db83 100644
--- a/test/unit/Makefile.in
+++ b/test/unit/Makefile.in
@@ -35,9 +35,6 @@ POST_UNINSTALL = :
 build_triplet = @build@
 host_triplet = @host@
 target_triplet = @target@
-@HAVE_CXXTESTGEN_FALSE@TESTS = no_cxxtest
-@HAVE_CXXTESTGEN_TRUE@TESTS = $(TESTS_WHITE) $(TESTS_BLACK) \
-@HAVE_CXXTESTGEN_TRUE@	$(am__EXEEXT_1)
 subdir = test/unit
 DIST_COMMON = $(srcdir)/Makefile.am $(srcdir)/Makefile.in
 ACLOCAL_M4 = $(top_srcdir)/aclocal.m4
@@ -53,35 +50,13 @@ mkinstalldirs = $(install_sh) -d
 CONFIG_HEADER = $(top_builddir)/config.h
 CONFIG_CLEAN_FILES =
 CONFIG_CLEAN_VPATH_FILES =
-am__vpath_adj_setup = srcdirstrip=`echo "$(srcdir)" | sed 's|.|.|g'`;
-am__vpath_adj = case $$p in \
-    $(srcdir)/*) f=`echo "$$p" | sed "s|^$$srcdirstrip/||"`;; \
-    *) f=$$p;; \
-  esac;
-am__strip_dir = f=`echo $$p | sed -e 's|^.*/||'`;
-am__install_max = 40
-am__nobase_strip_setup = \
-  srcdirstrip=`echo "$(srcdir)" | sed 's/[].[^$$\\*|]/\\\\&/g'`
-am__nobase_strip = \
-  for p in $$list; do echo "$$p"; done | sed -e "s|$$srcdirstrip/||"
-am__nobase_list = $(am__nobase_strip_setup); \
-  for p in $$list; do echo "$$p $$p"; done | \
-  sed "s| $$srcdirstrip/| |;"' / .*\//!s/ .*/ ./; s,\( .*\)/[^/]*$$,\1,' | \
-  $(AWK) 'BEGIN { files["."] = "" } { files[$$2] = files[$$2] " " $$1; \
-    if (++n[$$2] == $(am__install_max)) \
-      { print $$2, files[$$2]; n[$$2] = 0; files[$$2] = "" } } \
-    END { for (dir in files) print dir, files[dir] }'
-am__base_list = \
-  sed '$$!N;$$!N;$$!N;$$!N;$$!N;$$!N;$$!N;s/\n/ /g' | \
-  sed '$$!N;$$!N;$$!N;$$!N;s/\n/ /g'
-am__installdirs = "$(DESTDIR)$(libdir)"
-LTLIBRARIES = $(lib_LTLIBRARIES)
+LTLIBRARIES = $(noinst_LTLIBRARIES)
 @HAVE_CXXTESTGEN_TRUE@libdummy_la_DEPENDENCIES =  \
 @HAVE_CXXTESTGEN_TRUE@	@abs_top_builddir@/src/libcvc4.la
 am__libdummy_la_SOURCES_DIST = expr/node_black.cpp
 @HAVE_CXXTESTGEN_TRUE@am_libdummy_la_OBJECTS = node_black.lo
 libdummy_la_OBJECTS = $(am_libdummy_la_OBJECTS)
-@HAVE_CXXTESTGEN_TRUE@am_libdummy_la_rpath = -rpath $(libdir)
+@HAVE_CXXTESTGEN_TRUE@am_libdummy_la_rpath =
 DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
 depcomp = $(SHELL) $(top_srcdir)/config/depcomp
 am__depfiles_maybe = depfiles
@@ -101,7 +76,6 @@ ETAGS = etags
 CTAGS = ctags
 am__tty_colors = \
 red=; grn=; lgn=; blu=; std=
-am__EXEEXT_1 =
 DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST)
 ACLOCAL = @ACLOCAL@
 AMTAR = @AMTAR@
@@ -242,15 +216,16 @@ top_srcdir = @top_srcdir@
 @HAVE_CXXTESTGEN_TRUE@AM_CPPFLAGS = \
 @HAVE_CXXTESTGEN_TRUE@	-I. "-I@CXXTEST@" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src"
 
-@HAVE_CXXTESTGEN_TRUE@AM_CXXFLGAS_WHITE = -fno-access-control
-@HAVE_CXXTESTGEN_TRUE@AM_CXXFLGAS_BLACK = 
-@HAVE_CXXTESTGEN_TRUE@AM_CXXFLGAS_PUBLIC = 
+@HAVE_CXXTESTGEN_TRUE@AM_CXXFLAGS_WHITE = -fno-access-control
+@HAVE_CXXTESTGEN_TRUE@AM_CXXFLAGS_BLACK = 
+@HAVE_CXXTESTGEN_TRUE@AM_CXXFLAGS_PUBLIC = 
 @HAVE_CXXTESTGEN_TRUE@AM_LDFLAGS_WHITE = \
 @HAVE_CXXTESTGEN_TRUE@		@abs_top_builddir@/src/context/libcontext.la \
 @HAVE_CXXTESTGEN_TRUE@		@abs_top_builddir@/src/expr/libexpr.la \
 @HAVE_CXXTESTGEN_TRUE@		@abs_top_builddir@/src/smt/libsmt.la \
 @HAVE_CXXTESTGEN_TRUE@		@abs_top_builddir@/src/theory/libtheory.la \
 @HAVE_CXXTESTGEN_TRUE@		@abs_top_builddir@/src/util/libutil.la \
+@HAVE_CXXTESTGEN_TRUE@		@abs_top_builddir@/src/prop/libprop.la \
 @HAVE_CXXTESTGEN_TRUE@		@abs_top_builddir@/src/prop/minisat/libminisat.la
 
 @HAVE_CXXTESTGEN_TRUE@AM_LDFLAGS_BLACK = \
@@ -259,14 +234,16 @@ top_srcdir = @top_srcdir@
 @HAVE_CXXTESTGEN_TRUE@AM_LDFLAGS_PUBLIC = \
 @HAVE_CXXTESTGEN_TRUE@		@abs_top_builddir@/src/libcvc4.la
 
-@HAVE_CXXTESTGEN_TRUE@TESTS_WHITE = \
-@HAVE_CXXTESTGEN_TRUE@	expr/node_white
 
-@HAVE_CXXTESTGEN_TRUE@TESTS_BLACK = \
+# force a user-visible failure for "make check"
+@HAVE_CXXTESTGEN_FALSE@TESTS = no_cxxtest
+@HAVE_CXXTESTGEN_TRUE@TESTS = \
+@HAVE_CXXTESTGEN_TRUE@	expr/node_white \
 @HAVE_CXXTESTGEN_TRUE@	expr/node_black
 
-@HAVE_CXXTESTGEN_TRUE@TESTS_PUBLIC = 
-@HAVE_CXXTESTGEN_TRUE@lib_LTLIBRARIES = libdummy.la
+
+# without these here, LTCXXCOMPILE, CXXLINK, etc., aren't set :-(
+@HAVE_CXXTESTGEN_TRUE@noinst_LTLIBRARIES = libdummy.la
 @HAVE_CXXTESTGEN_TRUE@libdummy_la_SOURCES = expr/node_black.cpp
 @HAVE_CXXTESTGEN_TRUE@libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la
 @HAVE_CXXTESTGEN_TRUE@MOSTLYCLEANFILES = $(TESTS) $(TESTS:%=%.cpp)
@@ -304,32 +281,10 @@ $(top_srcdir)/configure:  $(am__configure_deps)
 $(ACLOCAL_M4):  $(am__aclocal_m4_deps)
 	cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
 $(am__aclocal_m4_deps):
-install-libLTLIBRARIES: $(lib_LTLIBRARIES)
-	@$(NORMAL_INSTALL)
-	test -z "$(libdir)" || $(MKDIR_P) "$(DESTDIR)$(libdir)"
-	@list='$(lib_LTLIBRARIES)'; test -n "$(libdir)" || list=; \
-	list2=; for p in $$list; do \
-	  if test -f $$p; then \
-	    list2="$$list2 $$p"; \
-	  else :; fi; \
-	done; \
-	test -z "$$list2" || { \
-	  echo " $(LIBTOOL) $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) --mode=install $(INSTALL) $(INSTALL_STRIP_FLAG) $$list2 '$(DESTDIR)$(libdir)'"; \
-	  $(LIBTOOL) $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) --mode=install $(INSTALL) $(INSTALL_STRIP_FLAG) $$list2 "$(DESTDIR)$(libdir)"; \
-	}
-
-uninstall-libLTLIBRARIES:
-	@$(NORMAL_UNINSTALL)
-	@list='$(lib_LTLIBRARIES)'; test -n "$(libdir)" || list=; \
-	for p in $$list; do \
-	  $(am__strip_dir) \
-	  echo " $(LIBTOOL) $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) --mode=uninstall rm -f '$(DESTDIR)$(libdir)/$$f'"; \
-	  $(LIBTOOL) $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) --mode=uninstall rm -f "$(DESTDIR)$(libdir)/$$f"; \
-	done
 
-clean-libLTLIBRARIES:
-	-test -z "$(lib_LTLIBRARIES)" || rm -f $(lib_LTLIBRARIES)
-	@list='$(lib_LTLIBRARIES)'; for p in $$list; do \
+clean-noinstLTLIBRARIES:
+	-test -z "$(noinst_LTLIBRARIES)" || rm -f $(noinst_LTLIBRARIES)
+	@list='$(noinst_LTLIBRARIES)'; for p in $$list; do \
 	  dir="`echo $$p | sed -e 's|/[^/]*$$||'`"; \
 	  test "$$dir" != "$$p" || dir=.; \
 	  echo "rm -f \"$${dir}/so_locations\""; \
@@ -559,9 +514,6 @@ check-am: all-am
 check: check-am
 all-am: Makefile $(LTLIBRARIES)
 installdirs:
-	for dir in "$(DESTDIR)$(libdir)"; do \
-	  test -z "$$dir" || $(MKDIR_P) "$$dir"; \
-	done
 install: install-am
 install-exec: install-exec-am
 install-data: install-data-am
@@ -590,7 +542,7 @@ maintainer-clean-generic:
 	@echo "it deletes files that may require special tools to rebuild."
 clean: clean-am
 
-clean-am: clean-generic clean-libLTLIBRARIES clean-libtool \
+clean-am: clean-generic clean-libtool clean-noinstLTLIBRARIES \
 	mostlyclean-am
 
 distclean: distclean-am
@@ -617,7 +569,7 @@ install-dvi: install-dvi-am
 
 install-dvi-am:
 
-install-exec-am: install-libLTLIBRARIES
+install-exec-am:
 
 install-html: install-html-am
 
@@ -657,39 +609,39 @@ ps: ps-am
 
 ps-am:
 
-uninstall-am: uninstall-libLTLIBRARIES
+uninstall-am:
 
 .MAKE: check-am install-am install-strip
 
 .PHONY: CTAGS GTAGS all all-am check check-TESTS check-am clean \
-	clean-generic clean-libLTLIBRARIES clean-libtool ctags \
+	clean-generic clean-libtool clean-noinstLTLIBRARIES ctags \
 	distclean distclean-compile distclean-generic \
 	distclean-libtool distclean-tags distdir dvi dvi-am html \
 	html-am info info-am install install-am install-data \
 	install-data-am install-dvi install-dvi-am install-exec \
 	install-exec-am install-html install-html-am install-info \
-	install-info-am install-libLTLIBRARIES install-man install-pdf \
-	install-pdf-am install-ps install-ps-am install-strip \
-	installcheck installcheck-am installdirs maintainer-clean \
+	install-info-am install-man install-pdf install-pdf-am \
+	install-ps install-ps-am install-strip installcheck \
+	installcheck-am installdirs maintainer-clean \
 	maintainer-clean-generic mostlyclean mostlyclean-compile \
 	mostlyclean-generic mostlyclean-libtool pdf pdf-am ps ps-am \
-	tags uninstall uninstall-am uninstall-libLTLIBRARIES
+	tags uninstall uninstall-am
 
 
 @HAVE_CXXTESTGEN_TRUE@$(TESTS:%=%.cpp): %.cpp: %.h
 @HAVE_CXXTESTGEN_TRUE@	mkdir -p `dirname "$@"`
 @HAVE_CXXTESTGEN_TRUE@	@CXXTESTGEN@ --have-eh --have-std --error-printer -o "$@" "$<"
-@HAVE_CXXTESTGEN_TRUE@$(TESTS_WHITE): %: %.cpp
+@HAVE_CXXTESTGEN_TRUE@$(filter %_white,$(TESTS)): %_white: %_white.cpp
 #	get these in here somehow
 #	$(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS)
 @HAVE_CXXTESTGEN_TRUE@	$(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@.lo $<
 @HAVE_CXXTESTGEN_TRUE@	$(CXXLINK) $(AM_LDFLAGS_WHITE) $@.lo
-@HAVE_CXXTESTGEN_TRUE@$(TESTS_BLACK): %: %.cpp
+@HAVE_CXXTESTGEN_TRUE@$(filter %_black,$(TESTS)): %_black: %_black.cpp
 #	get these in here somehow
 #	$(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS)
 @HAVE_CXXTESTGEN_TRUE@	$(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -c -o $@.lo $<
 @HAVE_CXXTESTGEN_TRUE@	$(CXXLINK) $(AM_LDFLAGS_BLACK) $@.lo
-@HAVE_CXXTESTGEN_TRUE@$(TESTS_PUBLIC): %: %.cpp
+@HAVE_CXXTESTGEN_TRUE@$(filter %_public,$(TESTS)): %_public: %_public.cpp
 #	get these in here somehow
 #	$(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS)
 @HAVE_CXXTESTGEN_TRUE@	$(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@.lo $<