1 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 88fb7cd8f..fbf3ce59c 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -39,6 +39,10 @@ TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_curr_model( c, NULL ), d_qe
   d_addedLemmas = 0;
 }
 
+bool QModelBuilder::isQuantifierActive( Node f ) {
+  return !f.hasAttribute(QRewriteRuleAttribute());
+}
+
 
 bool QModelBuilder::optUseModel() {
   return options::fmfModelBasedInst();
@@ -355,7 +359,8 @@ QModelBuilderIG::Statistics::~Statistics(){
 }
 
 bool QModelBuilderIG::isQuantifierActive( Node f ){
-  return ( d_considerAxioms || !f.getAttribute(AxiomAttribute()) ) && d_quant_sat.find( f )==d_quant_sat.end();
+  return !f.hasAttribute(QRewriteRuleAttribute()) &&
+         ( d_considerAxioms || !f.getAttribute(AxiomAttribute()) ) && d_quant_sat.find( f )==d_quant_sat.end();
 }
 
 bool QModelBuilderIG::isTermActive( Node n ){