Make --var-elim-quant true by default. Add rewrite engine to quantifiers module.

1 files changed, 4 insertions, 0 deletions

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 77df69456..38ee4a57f 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -197,6 +197,7 @@ 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 );
+      //it is not active if we have found the skolemized negation is unsat
       if( options::cbqi() && hasAddedCbqiLemma( n ) ){
         Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( n );
         bool active, value;
@@ -226,6 +227,9 @@ 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 if( n.hasAttribute(QRewriteRuleAttribute()) ){
+        d_quant_active[n] = false;
       }else{
         d_quant_active[n] = true;
         quantActive = true;