diff options
-rw-r--r-- | src/main/main.cpp | 4 | ||||
-rw-r--r-- | src/util/options.h | 2 |
2 files changed, 1 insertions, 5 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 diff --git a/src/util/options.h b/src/util/options.h index a7e9c8a2a..350c031c7 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -27,7 +27,7 @@ # define USE_EARLY_TYPE_CHECKING_BY_DEFAULT false #endif /* CVC4_DEBUG */ -#ifdef CVC4_MUZZLED +#if defined(CVC4_MUZZLED) || defined(CVC4_COMPETITION_MODE) # define DO_SEMANTIC_CHECKS_BY_DEFAULT false #else # define DO_SEMANTIC_CHECKS_BY_DEFAULT true |