Minor clean up, fixes related to sygus.

4 files changed, 8 insertions, 10 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;
       }
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 0bbca88eb..3063e7a2f 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -221,11 +221,12 @@ int ModelEngine::checkModel(){
 
   //print debug information
   if( d_quantEngine->inConflict() ){
-    Trace("model-engine") << "Conflict = " << d_quantEngine->getNumLemmasWaiting() << " / " << d_quantEngine->getNumLemmasAddedThisRound() << std::endl;
+    Trace("model-engine") << "Conflict, added lemmas = ";
   }else{
-    Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / ";
-    Trace("model-engine") << d_totalLemmas << std::endl;
-  }
+    Trace("model-engine") << "Added Lemmas = ";
+  } 
+  Trace("model-engine") << d_addedLemmas << " / " << d_triedLemmas << " / ";
+  Trace("model-engine") << d_totalLemmas << std::endl;
   return d_addedLemmas;
 }
 
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 6963f7e62..e41dfc67a 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -230,7 +230,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
     ret = ret.negate();
     status = REWRITE_AGAIN_FULL;
   }else if( in.getKind()==FORALL ){
-    if( in[1].isConst() ){
+    if( in[1].isConst() && in.getNumChildren()==2 ){
       return RewriteResponse( status, in[1] );
     }else{
       //compute attributes
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 61c02d3ac..ae9426172 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -3111,6 +3111,7 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
           std::string name = std::string( str.begin() + found +1, str.end() );
           out << name;
         }else{
+          Trace("ajr-temp") << "[[print operator " << op << "]]" << std::endl;
           out << op;
         }
         if( n.getNumChildren()>0 ){