summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/options_handlers.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2013-03-15 09:15:23 -0500
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2013-03-15 09:15:32 -0500
commit0891afc4553d43475643145e3c8687a7c2b1af49 (patch)
tree3be0dc50ef7b921eeeea7d6a2cc58f9b080499f8 /src/theory/quantifiers/options_handlers.h
parentd1a8a1854d9a71d409f6af23a1f52471fc34deb0 (diff)
changed default option for quantifier instantiation
Diffstat (limited to 'src/theory/quantifiers/options_handlers.h')
-rw-r--r--src/theory/quantifiers/options_handlers.h4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 312261d3c..01538d8cb 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -29,10 +29,10 @@ namespace quantifiers {
static const std::string instWhenHelp = "\
Modes currently supported by the --inst-when option:\n\
\n\
-full\n\
+full (default)\n\
+ Run instantiation round at full effort, before theory combination.\n\
\n\
-full-last-call (default)\n\
+full-last-call\n\
+ Alternate running instantiation rounds at full effort and last\n\
call. In other words, interleave instantiation and theory combination.\n\
\n\
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback