diff options
Diffstat (limited to 'src/theory/quantifiers/fmf/model_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers/fmf/model_engine.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index b3d9af953..f05246ddb 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -218,7 +218,9 @@ int ModelEngine::checkModel(){ Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl; // FMC uses two sub-effort levels - int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 ); + int e_max = options::mbqiMode() == MBQI_FMC + ? 2 + : (options::mbqiMode() == MBQI_TRUST ? 0 : 1); for( int e=0; e<e_max; e++) { d_incomplete_quants.clear(); for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ |