From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 17 Apr 2014 19:16:42 +0000 (-0400)
Subject: Allow fmf-bound-int to be set with set-option and via API.
X-Git-Tag: cvc5-1.0.0~6964
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e77289614a61d8658f8fc56073fa3334c14139b8;p=cvc5.git

Allow fmf-bound-int to be set with set-option and via API.
---

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"