diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-02 20:08:53 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-07-02 20:08:53 -0500 |
| commit | 0dec323ac1b45ce1ca194e9bb2a335c8def525d2 (patch) | |
| tree | c201933c725ddfd7f68a1e03db8e4f85242d0d6c /src/theory/quantifiers/fmf/model_engine.cpp | |
| parent | be58c8ead1d36ab3625faf848b2ebdce8d5de8a9 (diff) | |
Remove miscellaneous dead and unused code from quantifiers (#2121)
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++ ){ |