Add owner map to better manage QuantifiersModules. Initial infrastructure for cegqi.

1 files changed, 2 insertions, 2 deletions

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 7207ceefb..9c3673bc2 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -215,7 +215,7 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
     for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       Node n = d_quantEngine->getModel()->getAssertedQuantifier( i );
       //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
-      if( TermDb::isRewriteRule( n ) ){
+      if( !d_quantEngine->hasOwnership( n, this ) ){
         d_quant_active[n] = false;
       }else if( !d_quantEngine->getModel()->isQuantifierActive( n ) ){
         d_quant_active[n] = false;
@@ -300,7 +300,7 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
 }
 
 void InstantiationEngine::registerQuantifier( Node f ){
-  if( !TermDb::isRewriteRule( f ) ){
+  if( d_quantEngine->hasOwnership( f, this ) ){
     //Notice() << "do cbqi " << f << " ? " << std::endl;
     if( options::cbqi() ){
       Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f );