summaryrefslogtreecommitdiff
path: root/test/system/cvc3_main.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'test/system/cvc3_main.cpp')
-rw-r--r--test/system/cvc3_main.cpp15
1 files changed, 0 insertions, 15 deletions
diff --git a/test/system/cvc3_main.cpp b/test/system/cvc3_main.cpp
index 9b5a70d9e..51ca0ea2d 100644
--- a/test/system/cvc3_main.cpp
+++ b/test/system/cvc3_main.cpp
@@ -40,7 +40,6 @@
//#include "typecheck_exception.h"
//#include "command_line_flags.h"
//#include "debug.h"
-#include "cvc3_george.h"
using namespace std;
@@ -2201,20 +2200,6 @@ int main(int argc, char** argv)
cout << "\n}\ntest25(): {" << endl;
test25();
- /*
- if (regressLevel > 1) {
- cout << "\n}\ntestgeorge1(): {" << endl;
- testgeorge1();
- cout << "\n}\ntestgeorge2(): {" << endl;
- testgeorge2();
- cout << "\n}\ntestgeorge3(): {" << endl;
- testgeorge3();
- cout << "\n}\ntestgeorge4(): {" << endl;
- testgeorge4();
- cout << "\n}\ntestgeorge5(): {" << endl;
- testgeorge5();
- }
- */
cout << "\n}" << endl;
} catch(const Exception& e) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback