1 files changed, 17 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 8961a7c90..808137fd6 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -30,7 +30,8 @@ namespace quantifiers {
 
 bool QAttributes::isStandard() const
 {
-  return !d_sygus && !d_quant_elim && !isFunDef() && d_name.isNull();
+  return !d_sygus && !d_quant_elim && !isFunDef() && d_name.isNull()
+         && !d_isInternal;
 }
 
 QuantAttributes::QuantAttributes( QuantifiersEngine * qe ) : 
@@ -250,6 +251,11 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
           qa.d_quant_elim_partial = true;
           //don't set owner, should happen naturally
         }
+        if (avar.getAttribute(InternalQuantAttribute()))
+        {
+          Trace("quant-attr") << "Attribute : internal : " << q << std::endl;
+          qa.d_isInternal = true;
+        }
         if( avar.hasAttribute(QuantIdNumAttribute()) ){
           qa.d_qid_num = avar;
           Trace("quant-attr") << "Attribute : id number " << qa.d_qid_num.getAttribute(QuantIdNumAttribute()) << " : " << q << std::endl;
@@ -304,6 +310,16 @@ bool QuantAttributes::isQuantElimPartial( Node q ) {
   }
 }
 
+bool QuantAttributes::isInternal(Node q) const
+{
+  std::map<Node, QAttributes>::const_iterator it = d_qattr.find(q);
+  if (it != d_qattr.end())
+  {
+    return it->second.d_isInternal;
+  }
+  return false;
+}
+
 Node QuantAttributes::getQuantName(Node q) const
 {
   std::map<Node, QAttributes>::const_iterator it = d_qattr.find(q);