From dbcc42c807706a20fcc2c45619d3cd949b6de37a Mon Sep 17 00:00:00 2001
From: "Christopher L. Conway" <christopherleeconway@gmail.com>
Date: Fri, 5 Nov 2010 17:43:52 +0000
Subject: [PATCH] Moving Options fiddling to options.h

---
 src/main/main.cpp  | 4 ----
 src/util/options.h | 2 +-
 2 files changed, 1 insertion(+), 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
-- 
2.30.2