diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-10 12:57:58 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-10 12:57:58 -0400 |
| commit | 315eb7e44cada64fd9b8a2b4ab9b9cac66758769 (patch) | |
| tree | d4188467a2cacbb277ed08417c11f4e963df11b6 /src/theory/quantifiers | |
| parent | 20cde072ebef5eddfc1562bebdd9438c77a22c8e (diff) | |
Add documentation for --disable-fmf-inst-gen, which removes a warning
Diffstat (limited to 'src/theory/quantifiers')
| -rw-r--r-- | src/theory/quantifiers/options | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 6bbcb2c3d..9facdbc5f 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -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 |