Set instantiation level on skolemized bodies of quantifiers. Rename inst-level attribute to quant-inst-max-level

1 files changed, 5 insertions, 2 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index d6bd8e574..a00592e8b 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -446,8 +446,11 @@ void QuantifiersEngine::setInstantiationLevelAttr( Node n, Node qn, uint64_t lev
 }
 
 void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){
-  InstLevelAttribute ila;
-  n.setAttribute(ila,level);
+  if( !n.hasAttribute(InstLevelAttribute()) ){
+    InstLevelAttribute ila;
+    n.setAttribute(ila,level);
+    Trace("inst-level-debug") << "Set instantiation level " << n << " to " << level << std::endl;
+  }
   for( int i=0; i<(int)n.getNumChildren(); i++ ){
     setInstantiationLevelAttr( n[i], level );
   }