diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-11-05 17:43:52 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-11-05 17:43:52 +0000 |
commit | dbcc42c807706a20fcc2c45619d3cd949b6de37a (patch) | |
tree | fade7cca77d013921ea8bfa0b20c1102ec905ec8 /src/util/options.h | |
parent | 93e6b2f2514295c15950ea5cc44948835f830a85 (diff) |
Moving Options fiddling to options.h
Diffstat (limited to 'src/util/options.h')
-rw-r--r-- | src/util/options.h | 2 |
1 files changed, 1 insertions, 1 deletions
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 |