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, 0 insertions, 4 deletions
diff --git a/src/main/main.cpp b/src/main/main.cpp
index c740604c3..fcd322e99 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -155,10 +155,6 @@ 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