merged golden

1 files changed, 13 insertions, 4 deletions

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 77df69456..628f8b14a 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -92,7 +92,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
           NodeBuilder<> nb(kind::OR);
           nb << f << ceLit;
           Node lem = nb;
-          Debug("cbqi-debug") << "Counterexample lemma : " << lem << std::endl;
+          Trace("cbqi") << "Counterexample lemma : " << lem << std::endl;
           d_quantEngine->getOutputChannel().lemma( lem );
           addedLemma = true;
         }
@@ -197,7 +197,10 @@ void InstantiationEngine::check( Theory::Effort e ){
                          << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl;
     for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       Node n = d_quantEngine->getModel()->getAssertedQuantifier( i );
-      if( options::cbqi() && hasAddedCbqiLemma( n ) ){
+      //it is not active if we have found the skolemized negation is unsat
+      if( n.hasAttribute(QRewriteRuleAttribute()) ){
+        d_quant_active[n] = false;
+      }else if( options::cbqi() && hasAddedCbqiLemma( n ) ){
         Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( n );
         bool active, value;
         bool ceValue = false;
@@ -210,7 +213,9 @@ void InstantiationEngine::check( Theory::Effort e ){
         d_quant_active[n] = active;
         if( active ){
           Debug("quantifiers") << "  Active : " << n;
-          quantActive = true;
+          if( !TermDb::hasInstConstAttr(n) ){
+            quantActive = true;
+          }
         }else{
           Debug("quantifiers") << "  NOT active : " << n;
           if( d_quantEngine->getValuation().isDecision( cel ) ){
@@ -226,14 +231,18 @@ void InstantiationEngine::check( Theory::Effort e ){
           Debug("quantifiers") << ", ce is asserted";
         }
         Debug("quantifiers") << std::endl;
+      //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
       }else{
         d_quant_active[n] = true;
-        quantActive = true;
+        if( !TermDb::hasInstConstAttr(n) ){
+          quantActive = true;
+        }
         Debug("quantifiers") << "  Active : " << n << ", no ce assigned." << std::endl;
       }
       Debug("quantifiers-relevance")  << "Quantifier : " << n << std::endl;
       Debug("quantifiers-relevance")  << "   Relevance : " << d_quantEngine->getQuantifierRelevance()->getRelevance( n ) << std::endl;
       Debug("quantifiers") << "   Relevance : " << d_quantEngine->getQuantifierRelevance()->getRelevance( n ) << std::endl;
+      Trace("inst-engine-debug") << "Process : " << n << " " << d_quant_active[n] << std::endl;
     }
     if( quantActive ){
       bool addedLemmas = doInstantiationRound( e );