From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 4 Nov 2010 21:01:31 +0000 (+0000)
Subject: competition mode implies --no-checking
X-Git-Tag: cvc5-1.0.0~8746
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=93e6b2f2514295c15950ea5cc44948835f830a85;p=cvc5.git

competition mode implies --no-checking
---

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