summaryrefslogtreecommitdiff
path: root/src/main/main.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/main/main.cpp')
-rw-r--r--src/main/main.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 2a8bc7ab2..37c122732 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -50,14 +50,14 @@ int main(int argc, char* argv[]) {
try {
return runCvc4(argc, argv, opts);
} catch(OptionException& e) {
-#ifdef CVC4_COMPETITION_MODE
+#ifdef CVC5_COMPETITION_MODE
*opts.getOut() << "unknown" << endl;
#endif
cerr << "(error \"" << e << "\")" << endl
<< endl
<< "Please use --help to get help on command-line options." << endl;
} catch(Exception& e) {
-#ifdef CVC4_COMPETITION_MODE
+#ifdef CVC5_COMPETITION_MODE
*opts.getOut() << "unknown" << endl;
#endif
if (language::isOutputLang_smt2(opts.getOutputLanguage()))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback