1 files changed, 21 insertions, 1 deletions
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index d9f77d50f..f14788ed5 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -66,11 +66,23 @@ public:
   context::CDO<bool> rIntro1Applied;
   context::CDO<TNode> modelRep;
   context::CDO<TNode> constArr;
+  context::CDO<TNode> weakEquivPointer;
+  context::CDO<TNode> weakEquivIndex;
+  context::CDO<TNode> weakEquivSecondary;
+  context::CDO<TNode> weakEquivSecondaryReason;
   CTNodeList* indices;
   CTNodeList* stores;
   CTNodeList* in_stores;
 
-  Info(context::Context* c, Backtracker<TNode>* bck) : isNonLinear(c, false), rIntro1Applied(c, false), modelRep(c,TNode()), constArr(c,TNode()) {
+  Info(context::Context* c, Backtracker<TNode>* bck)
+    : isNonLinear(c, false),
+      rIntro1Applied(c, false),
+      modelRep(c,TNode()),
+      constArr(c,TNode()),
+      weakEquivPointer(c,TNode()),
+      weakEquivIndex(c,TNode()),
+      weakEquivSecondary(c,TNode()),
+      weakEquivSecondaryReason(c,TNode()) {
     indices = new(true)CTNodeList(c);
     stores = new(true)CTNodeList(c);
     in_stores = new(true)CTNodeList(c);
@@ -213,6 +225,10 @@ public:
   void setModelRep(const TNode a, const TNode rep);
 
   void setConstArr(const TNode a, const TNode constArr);
+  void setWeakEquivPointer(const TNode a, const TNode pointer);
+  void setWeakEquivIndex(const TNode a, const TNode index);
+  void setWeakEquivSecondary(const TNode a, const TNode secondary);
+  void setWeakEquivSecondaryReason(const TNode a, const TNode reason);
   /**
    * Returns the information associated with TNode a
    */
@@ -226,6 +242,10 @@ public:
   const TNode getModelRep(const TNode a) const;
 
   const TNode getConstArr(const TNode a) const;
+  const TNode getWeakEquivPointer(const TNode a) const;
+  const TNode getWeakEquivIndex(const TNode a) const;
+  const TNode getWeakEquivSecondary(const TNode a) const;
+  const TNode getWeakEquivSecondaryReason(const TNode a) const;
 
   const CTNodeList* getIndices(const TNode a) const;