diff options
Diffstat (limited to 'src/theory/quantifiers/model_builder.cpp')
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 10 |
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(){ |