diff options
Diffstat (limited to 'src/decision/options_handlers.h')
| -rw-r--r-- | src/decision/options_handlers.h | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/decision/options_handlers.h b/src/decision/options_handlers.h index fd05a0c9f..826bd8acb 100644 --- a/src/decision/options_handlers.h +++ b/src/decision/options_handlers.h @@ -36,6 +36,9 @@ justification\n\ \n\ justification-stoponly\n\ + Use the justification heuristic only to stop early, not for decisions\n\ +"; +/** Under-development options, commenting out from help for the release */ +/* \n\ relevancy\n\ + Under development may-relevancy\n\ @@ -52,7 +55,7 @@ justification-rel\n\ justification-must\n\ + Start deciding on literals close to root instead of those\n\ + near leaves (don't expect it to work well) [Unimplemented]\n\ -"; +";*/ inline DecisionMode stringToDecisionMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { options::decisionRelevancyLeaves.set(false); |