1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 9cd5020fb..5d49c914f 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -90,11 +90,11 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m ) {
           }
         }
       }
-      if( Options::current()->printModelEngine ){
+      if( Trace.isOn("model-engine") ){
         if( d_addedLemmas>0 ){
-          Message() << "InstGen, added lemmas = " << d_addedLemmas << std::endl;
+          Trace("model-engine") << "InstGen, added lemmas = " << d_addedLemmas << std::endl;
         }else{
-          Message() << "No InstGen lemmas..." << std::endl;
+          Trace("model-engine") << "No InstGen lemmas..." << std::endl;
         }
       }
       Debug("fmf-model-debug") << "---> Added lemmas = " << d_addedLemmas << std::endl;
@@ -388,11 +388,11 @@ void ModelEngineBuilder::finishProcessBuildModel( TheoryModel* m ){
 }
 
 bool ModelEngineBuilder::optUseModel() {
-  return Options::current()->fmfModelBasedInst;
+  return options::fmfModelBasedInst();
 }
 
 bool ModelEngineBuilder::optInstGen(){
-  return Options::current()->fmfInstGen;
+  return options::fmfInstGen();
 }
 
 bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){