diff options
Diffstat (limited to 'src/theory/quantifiers/instantiation_engine.cpp')
-rwxr-xr-x[-rw-r--r--] | src/theory/quantifiers/instantiation_engine.cpp | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 955dc5d86..db597d031 100644..100755 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -137,11 +137,7 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ doInstantiationRound( e ); if( d_quantEngine->inConflict() ){ Assert( d_quantEngine->getNumLemmasWaiting()>lastWaiting ); - Trace("inst-engine") << "Conflict = " << d_quantEngine->getNumLemmasWaiting() << " / " << d_quantEngine->getNumLemmasAddedThisRound(); - if( lastWaiting>0 ){ - Trace("inst-engine") << " (prev " << lastWaiting << ")"; - } - Trace("inst-engine") << std::endl; + Trace("inst-engine") << "Conflict, added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl; }else if( d_quantEngine->hasAddedLemma() ){ Trace("inst-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl; } |