diff options
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index e9a69bd30..0388a2979 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -49,11 +49,14 @@ d_lemmas_produced_c(u){ d_eem = new EfficientEMatcher( this ); d_hasAddedLemma = false; + Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; //the model object - if( options::fmfFullModelCheck() || options::fmfBoundInt() ){ + if( options::mbqiMode()==quantifiers::MBQI_FMC || options::fmfBoundInt() ){ d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" ); + }else if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){ + d_model = new quantifiers::FirstOrderModelQInt( this, c, "FirstOrderModelQInt" ); }else{ - d_model = new quantifiers::FirstOrderModelIG( c, "FirstOrderModelIG" ); + d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" ); } //add quantifiers modules |