summaryrefslogtreecommitdiff
path: root/src/util/options.h
diff options
context:
space:
mode:
authorChristopher L. Conway <christopherleeconway@gmail.com>2010-05-04 21:57:57 +0000
committerChristopher L. Conway <christopherleeconway@gmail.com>2010-05-04 21:57:57 +0000
commit65d24277bfb9f76b612fa51770d5d63e1d34b528 (patch)
tree023841d60bff520093c40ffeddf40288b97615d3 /src/util/options.h
parent1571e73e83ecb5fec2f2ddd599bd3823e8f532e7 (diff)
Disabling semantic checks in competition mode.
Adding function debugTagIsOn to safely test for tracing in any compilation mode. Removing irrelevant command-line options from usage message in muzzled mode.
Diffstat (limited to 'src/util/options.h')
-rw-r--r--src/util/options.h2
1 files changed, 0 insertions, 2 deletions
diff --git a/src/util/options.h b/src/util/options.h
index 63f1cb99e..d095d98d3 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -29,7 +29,6 @@ struct CVC4_PUBLIC Options {
std::string binary_name;
- bool smtcomp_mode;
bool statistics;
std::ostream *out;
@@ -55,7 +54,6 @@ struct CVC4_PUBLIC Options {
bool memoryMap;
Options() : binary_name(),
- smtcomp_mode(false),
statistics(false),
out(0),
err(0),
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback