Add documentation for --disable-fmf-inst-gen, which removes a warning
authorMorgan Deters <mdeters@cs.nyu.edu>
Fri, 10 May 2013 16:57:58 +0000 (12:57 -0400)
committerMorgan Deters <mdeters@cs.nyu.edu>
Fri, 10 May 2013 16:57:58 +0000 (12:57 -0400)
src/theory/quantifiers/options

index 6bbcb2c3d5a9bee04a553fdb4946f9cdc442a95c..9facdbc5ff321dc7847638dbbf44bc9cf3e8a3a9 100644 (file)
@@ -109,7 +109,8 @@ option fmfRelevantDomain --fmf-relevant-domain bool :default false
 option fmfNewInstGen --fmf-new-inst-gen bool :default false
  use new inst gen technique for answering sat without exhaustive instantiation
 option fmfInstGen --fmf-inst-gen/--disable-fmf-inst-gen bool :read-write :default true
- enable/disable Inst-Gen instantiation techniques for finite model finding
+ enable Inst-Gen instantiation techniques for finite model finding (default)
+/disable Inst-Gen instantiation techniques for finite model finding
 option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false
  only perform Inst-Gen instantiation techniques on one quantifier per round
 option fmfFreshDistConst --fmf-fresh-dc bool :default false