diff options
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 59fa3592d..da8233fc1 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1286,10 +1286,11 @@ void QuantifiersEngine::flushLemmas(){ } bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas ) { - //TODO: only if unsat core available + //only if unsat core available bool isUnsatCoreAvailable = false; - //if( options::proof() ){ - //} + if( options::proof() ){ + isUnsatCoreAvailable = ProofManager::currentPM()->unsatCoreAvailable(); + } if( isUnsatCoreAvailable ){ Trace("inst-unsat-core") << "Get instantiations in unsat core..." << std::endl; ProofManager::currentPM()->getLemmasInUnsatCore(theory::THEORY_QUANTIFIERS, active_lemmas); |