diff options
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 89d1ad55a..c663e1aa2 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -48,7 +48,11 @@ d_lemmas_produced_c(u){ d_hasAddedLemma = false; //the model object - d_model = new quantifiers::FirstOrderModel( c, "FirstOrderModel" ); + if( options::fmfFullModelCheck() ){ + d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" ); + }else{ + d_model = new quantifiers::FirstOrderModelIG( c, "FirstOrderModelIG" ); + } //add quantifiers modules if( !options::finiteModelFind() || options::fmfInstEngine() ){ |