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, 4 insertions, 0 deletions
diff --git a/src/main/main.cpp b/src/main/main.cpp
index fcd322e99..c740604c3 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -155,6 +155,10 @@ int runCvc4(int argc, char* argv[]) {
// If in competition mode, set output stream option to flush immediately
#ifdef CVC4_COMPETITION_MODE
*options.out << unitbuf;
+ // competition mode implies --no-checking
+ options.semanticChecks = false;
+ options.typeChecking = false;
+ options.earlyTypeChecking = false;
#endif
// We only accept one input file
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback