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();