summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/options_handlers.h
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2015-09-10 10:12:36 +0200
committerajreynol <andrew.j.reynolds@gmail.com>2015-09-10 10:12:36 +0200
commit26b8cc7f672d580dfc7355dac1c4352a3c7c32e8 (patch)
treebb10dfe7883e73345815bd47b5bb62214cb1035f /src/theory/quantifiers/options_handlers.h
parent68d3518e446b1e0f1ac16c2146c162580fa377f9 (diff)
Fix bug 670. Minor.
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 791ad6e90..e5e484625 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -207,13 +207,13 @@ relevant \n\
static const std::string iteLiftQuantHelp = "\
Modes for term database, supported by --ite-lift-quant:\n\
\n\
-all \n\
+none \n\
+ Do not lift if-then-else in quantified formulas.\n\
\n\
simple \n\
+ Lift if-then-else in quantified formulas if results in smaller term size.\n\
\n\
-none \n\
+all \n\
+ Lift if-then-else in quantified formulas. \n\
\n\
";
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback