summaryrefslogtreecommitdiff
path: root/src/decision
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-08-16 19:41:36 -0400
committerMorgan Deters <mdeters@cs.nyu.edu>2013-09-05 15:17:37 -0400
commit30c92d9a634a0643fd2dad51cc09486d38ba3893 (patch)
tree0ffbff19495257febc4ab052b2758221c5d4c73c /src/decision
parent2f3976ab39799149ea4dce5a45f75cf98bb39887 (diff)
Permit setOption(decision-mode)
Diffstat (limited to 'src/decision')
-rw-r--r--src/decision/options2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/decision/options b/src/decision/options
index 5f89e9611..1f0b137cb 100644
--- a/src/decision/options
+++ b/src/decision/options
@@ -6,7 +6,7 @@
module DECISION "decision/options.h" Decision heuristics
# When/whether to use any decision strategies
-option decisionMode --decision=MODE decision::DecisionMode :handler CVC4::decision::stringToDecisionMode :default decision::DECISION_STRATEGY_INTERNAL :read-write :include "decision/decision_mode.h" :handler-include "decision/options_handlers.h"
+option decisionMode decision-mode --decision=MODE decision::DecisionMode :handler CVC4::decision::stringToDecisionMode :default decision::DECISION_STRATEGY_INTERNAL :read-write :include "decision/decision_mode.h" :handler-include "decision/options_handlers.h"
choose decision mode, see --decision=help
# only use DE to determine when to stop, not to make decisions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback