diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-17 15:16:42 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-17 15:16:42 -0400 |
| commit | e77289614a61d8658f8fc56073fa3334c14139b8 (patch) | |
| tree | b0de7ce99577fc14edf4b4fa9e31db5a0471126c /src | |
| parent | 78fa095e7cac7a59062a0bbf8cc862d0bbaa1e0a (diff) | |
Allow fmf-bound-int to be set with set-option and via API.
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/quantifiers/options | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index b7f015f47..32e65438e 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -112,7 +112,7 @@ option fmfFreshDistConst --fmf-fresh-dc bool :default false use fresh distinguished representative when applying Inst-Gen techniques option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true disable simple models in full model check for finite model finding -option fmfBoundInt --fmf-bound-int bool :default false :read-write +option fmfBoundInt fmf-bound-int --fmf-bound-int bool :default false :read-write finite model finding on bounded integer quantification option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h" |