diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-11-04 21:01:31 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-11-04 21:01:31 +0000 |
| commit | 93e6b2f2514295c15950ea5cc44948835f830a85 (patch) | |
| tree | 6766fe4db743ff3e22687e584bdcddd635dbdbef /src/main | |
| parent | d837718bfa4a2b8cb46add5f1c510b0d2a7785f5 (diff) | |
competition mode implies --no-checking
Diffstat (limited to 'src/main')
| -rw-r--r-- | src/main/main.cpp | 4 |
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 |