1 files changed, 15 insertions, 0 deletions
diff --git a/src/theory/arrays/skolem_cache.cpp b/src/theory/arrays/skolem_cache.cpp
index 19ab1aaae..7cf192b7f 100644
--- a/src/theory/arrays/skolem_cache.cpp
+++ b/src/theory/arrays/skolem_cache.cpp
@@ -35,6 +35,14 @@ struct ExtIndexVarAttributeId
 };
 typedef expr::Attribute<ExtIndexVarAttributeId, Node> ExtIndexVarAttribute;
 
+/**
+ * A bound variable corresponding to the index used in the eqrange expansion.
+ */
+struct EqRangeVarAttributeId
+{
+};
+typedef expr::Attribute<EqRangeVarAttributeId, Node> EqRangeVarAttribute;
+
 SkolemCache::SkolemCache() {}
 
 Node SkolemCache::getExtIndexSkolem(Node deq)
@@ -66,6 +74,13 @@ Node SkolemCache::getExtIndexSkolem(Node deq)
       "an extensional lemma index variable from the theory of arrays");
 }
 
+Node SkolemCache::getEqRangeVar(TNode eqr)
+{
+  Assert(eqr.getKind() == kind::EQ_RANGE);
+  BoundVarManager* bvm = NodeManager::currentNM()->getBoundVarManager();
+  return bvm->mkBoundVar<EqRangeVarAttribute>(eqr, eqr[2].getType());
+}
+
 Node SkolemCache::getExtIndexVar(Node deq)
 {
   Node a = deq[0][0];