1 files changed, 7 insertions, 23 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 460289439..5add52d1f 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -24,6 +24,7 @@
 #include "theory/rewriter.h"
 #include "expr/command.h"
 #include "theory/arrays/theory_arrays_instantiator.h"
+#include "theory/model.h"
 
 using namespace std;
 
@@ -57,7 +58,7 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
   d_checkTimer("theory::arrays::checkTime"),
   d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP"),
   d_ppFacts(u),
-  //  d_ppCache(u),  
+  //  d_ppCache(u),
   d_literalsToPropagate(c),
   d_literalsToPropagateIndex(c, 0),
   d_isPreRegistered(c),
@@ -211,7 +212,7 @@ Node TheoryArrays::ppRewrite(TNode term) {
                 for (j = leftWrites - 1; j > i; --j) {
                   index_j = write_j[1];
                   if (!ppDisequal(index_i, index_j)) {
-                    Node hyp2(index_i.getType() == nm->booleanType()? 
+                    Node hyp2(index_i.getType() == nm->booleanType()?
                               index_i.iffNode(index_j) : index_i.eqNode(index_j));
                     hyp << hyp2.notNode();
                   }
@@ -623,27 +624,10 @@ void TheoryArrays::computeCareGraph()
 // MODEL GENERATION
 /////////////////////////////////////////////////////////////////////////////
 
-
-Node TheoryArrays::getValue(TNode n)
-{
-  // TODO: Implement this
-  NodeManager* nodeManager = NodeManager::currentNM();
-
-  switch(n.getKind()) {
-
-  case kind::VARIABLE:
-    Unhandled(kind::VARIABLE);
-
-  case kind::EQUAL: // 2 args
-    return nodeManager->
-      mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) );
-
-  default:
-    Unhandled(n.getKind());
-  }
+void TheoryArrays::collectModelInfo( TheoryModel* m ){
+  m->assertEqualityEngine( &d_equalityEngine );
 }
 
-
 /////////////////////////////////////////////////////////////////////////////
 // NOTIFICATIONS
 /////////////////////////////////////////////////////////////////////////////
@@ -663,7 +647,7 @@ void TheoryArrays::presolve()
 void TheoryArrays::check(Effort e) {
   TimerStat::CodeTimer codeTimer(d_checkTimer);
 
-  while (!done() && !d_conflict) 
+  while (!done() && !d_conflict)
   {
     // Get all the assertions
     Assertion assertion = get();
@@ -1306,7 +1290,7 @@ void TheoryArrays::dischargeLemmas()
       d_equalityEngine.assertEquality(eq2, true, d_true);
       continue;
     }
-    
+
     Node lem = nm->mkNode(kind::OR, eq2_r, eq1_r);
 
     Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lem<<"\n";