5 files changed, 24 insertions, 15 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index a05d30517..dcf4813fc 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -537,7 +537,7 @@ EqualityStatus TheoryArrays::getEqualityStatus(TNode a, TNode b) {
 void TheoryArrays::computeCareGraph()
 {
   if (d_sharedArrays.size() > 0) {
-    context::CDHashSet<TNode, TNodeHashFunction>::iterator it1 = d_sharedArrays.begin(), it2, iend = d_sharedArrays.end();
+    CDNodeSet::key_iterator it1 = d_sharedArrays.key_begin(), it2, iend = d_sharedArrays.key_end();
     for (; it1 != iend; ++it1) {
       for (it2 = it1, ++it2; it2 != iend; ++it2) {
         if ((*it1).getType() != (*it2).getType()) {
@@ -1261,7 +1261,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b)
 
 void TheoryArrays::queueRowLemma(RowLemmaType lem)
 {
-  if (d_conflict || d_RowAlreadyAdded.count(lem) != 0) {
+  if (d_conflict || d_RowAlreadyAdded.contains(lem)) {
     return;
   }
   TNode a = lem.first;
@@ -1324,7 +1324,9 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
 
   // Prefer equality between indexes so as not to introduce new read terms
   if (d_eagerIndexSplitting && !bothExist && !d_equalityEngine.areDisequal(i,j, false)) {
-    d_decisionRequests.push(i.eqNode(j));
+    Node i_eq_j = d_valuation.ensureLiteral(i.eqNode(j));
+    getOutputChannel().requirePhase(i_eq_j, true);
+    d_decisionRequests.push(i_eq_j);
   }
 
   // TODO: maybe add triggers here
@@ -1392,7 +1394,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
 
 Node TheoryArrays::getNextDecisionRequest() {
   if(! d_decisionRequests.empty()) {
-    Node n = d_valuation.ensureLiteral(d_decisionRequests.front());
+    Node n = d_decisionRequests.front();
     d_decisionRequests.pop();
     return n;
   } else {
@@ -1407,7 +1409,7 @@ void TheoryArrays::dischargeLemmas()
   for (unsigned count = 0; count < sz; ++count) {
     RowLemmaType l = d_RowQueue.front();
     d_RowQueue.pop();
-    if (d_RowAlreadyAdded.count(l) != 0) {
+    if (d_RowAlreadyAdded.contains(l)) {
       continue;
     }
 
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 240cfad9a..172482e71 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -333,8 +333,10 @@ class TheoryArrays : public Theory {
   context::CDQueue<RowLemmaType> d_RowQueue;
   context::CDHashSet<RowLemmaType, RowLemmaTypeHashFunction > d_RowAlreadyAdded;
 
-  context::CDHashSet<TNode, TNodeHashFunction> d_sharedArrays;
-  context::CDHashSet<TNode, TNodeHashFunction> d_sharedOther;
+  typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
+
+  CDNodeSet d_sharedArrays;
+  CDNodeSet d_sharedOther;
   context::CDO<bool> d_sharedTerms;
   context::CDList<TNode> d_reads;
   std::hash_map<TNode, Node, TNodeHashFunction> d_diseqCache;
diff --git a/src/theory/arrays/theory_arrays_model.cpp b/src/theory/arrays/theory_arrays_model.cpp
index 86bdad53f..4f7584ac1 100644
--- a/src/theory/arrays/theory_arrays_model.cpp
+++ b/src/theory/arrays/theory_arrays_model.cpp
@@ -41,7 +41,7 @@ Node ArrayModel::getValue( TheoryModel* m, Node i ){
     return it->second;
   }else{
     return NodeManager::currentNM()->mkNode( SELECT, getArrayValue(), i );
-    //return d_default_value;   //TODO: guarentee I can return this here
+    //return d_default_value;   //TODO: guarantee I can return this here
   }
 }
 
diff --git a/src/theory/arrays/theory_arrays_model.h b/src/theory/arrays/theory_arrays_model.h
index 4825c710d..c82c7635d 100644
--- a/src/theory/arrays/theory_arrays_model.h
+++ b/src/theory/arrays/theory_arrays_model.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
 /*! \file theory_arrays_model.h
  ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
+ ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com>
+ ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu>
  ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index da479616d..9cbb0c9e8 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -37,8 +37,12 @@ typedef expr::Attribute<attr::ArrayConstantMostFrequentValueCountTag, uint64_t>
 typedef expr::Attribute<attr::ArrayConstantMostFrequentValueTag, Node> ArrayConstantMostFrequentValueAttr;
 
 class TheoryArraysRewriter {
-
   static Node normalizeConstant(TNode node) {
+    return normalizeConstant(node, node[1].getType().getCardinality());
+  }
+public:
+  //this function is called by printers when using the option "--model-u-dt-enum"
+  static Node normalizeConstant(TNode node, Cardinality indexCard) {
     TNode store = node[0];
     TNode index = node[1];
     TNode value = node[2];
@@ -112,7 +116,6 @@ class TheoryArraysRewriter {
       return n;
     }
 
-    Cardinality indexCard = index.getType().getCardinality();
     if (indexCard.isInfinite()) {
       return n;
     }
@@ -189,13 +192,15 @@ class TheoryArraysRewriter {
     std::vector<Node> newIndices;
     TypeEnumerator te(index.getType());
     bool needToSort = false;
-    while (!te.isFinished()) {
+    unsigned numTe = 0;
+    while (!te.isFinished() && (!indexCard.isFinite() || numTe<indexCard.getFiniteCardinality().toUnsignedInt())) {
       if (indexSet.find(*te) == indexSet.end()) {
         if (!newIndices.empty() && (!(newIndices.back() < (*te)))) {
           needToSort = true;
         }
         newIndices.push_back(*te);
       }
+      ++numTe;
       ++te;
     }
     Assert(indexCard.compare(newIndices.size() + depth) == Cardinality::EQUAL);