From e77289614a61d8658f8fc56073fa3334c14139b8 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 17 Apr 2014 15:16:42 -0400 Subject: [PATCH] Allow fmf-bound-int to be set with set-option and via API. --- src/theory/quantifiers/options | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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" -- 2.30.2