diff options
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index c1ad62cd9..5dd3816c5 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -215,12 +215,10 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine-debug") << "Done resetting all modules." << std::endl; if( e==Theory::EFFORT_LAST_CALL ){ - //if effort is last call, try to minimize model first - if( options::finiteModelFind() ){ - //first, check if we can minimize the model further FIXME: remove? - if( !((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){ - return; - } + //if effort is last call, try to minimize model first FIXME: remove? + uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver(); + if( ufss && !ufss->minimize() ){ + return; } ++(d_statistics.d_instantiation_rounds_lc); }else if( e==Theory::EFFORT_FULL ){ |