1 files changed, 4 insertions, 10 deletions
diff --git a/src/theory/arrays/skolem_cache.cpp b/src/theory/arrays/skolem_cache.cpp
index 4028a53a8..b32e89bca 100644
--- a/src/theory/arrays/skolem_cache.cpp
+++ b/src/theory/arrays/skolem_cache.cpp
@@ -15,6 +15,7 @@
 #include "theory/arrays/skolem_cache.h"
 
 #include "expr/attribute.h"
+#include "expr/bound_var_manager.h"
 #include "expr/skolem_manager.h"
 #include "expr/type_node.h"
 
@@ -66,20 +67,13 @@ Node SkolemCache::getExtIndexSkolem(Node deq)
 
 Node SkolemCache::getExtIndexVar(Node deq)
 {
-  ExtIndexVarAttribute eiva;
-  if (deq.hasAttribute(eiva))
-  {
-    return deq.getAttribute(eiva);
-  }
   Node a = deq[0][0];
-  Node b = deq[0][1];
   TypeNode atn = a.getType();
   Assert(atn.isArray());
-  Assert(atn == b.getType());
+  Assert(atn == deq[0][1].getType());
   TypeNode atnIndex = atn.getArrayIndexType();
-  Node v = NodeManager::currentNM()->mkBoundVar(atnIndex);
-  deq.setAttribute(eiva, v);
-  return v;
+  BoundVarManager* bvm = NodeManager::currentNM()->getBoundVarManager();
+  return bvm->mkBoundVar<ExtIndexVarAttribute>(deq, atnIndex);
 }
 
 }  // namespace arrays