changed default option for quantifier instantiation

diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 222fc4425e62622f98ca41724a8e4e594981adda..e12a7d70f729226920620688307708d7d06efaee 100644 (file)
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -56,7 +56,7 @@ option relevantTriggers /--disable-relevant-triggers bool :default true
 option registerQuantBodyTerms --register-quant-body-terms bool :default false
  consider ground terms within bodies of quantified formulas for matching
 
-option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h"
+option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h"
  when to apply instantiation
  
 option eagerInstQuant --eager-inst-quant bool :default false

diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 312261d3cb63b63a6613224c478329229b69598b..01538d8cbf3f56ef5bcbb55eecaf2c4bb4f14dc8 100644 (file)
--- 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\