Minor clean up, fixes related to sygus.

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
--- 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;
       }