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.

1 files changed, 24 insertions, 0 deletions

diff --git a/test/system/cvc3_george.h b/test/system/cvc3_george.h
new file mode 100644
index 000000000..c904fd0c6
--- /dev/null
+++ b/test/system/cvc3_george.h
@@ -0,0 +1,24 @@
+/*********************                                                        */
+/*! \file cvc3_main.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Test of CVC3 compatibility interface
+ **
+ ** This is part of a test of the CVC3 compatibility interface present in
+ ** CVC4.  It is a test copied from CVC3's "test" directory.
+ **/
+
+void testgeorge1();
+void testgeorge2();
+void testgeorge3();
+void testgeorge4();
+void testgeorge5();