Best heuristics for handling decision requests from arrays

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index aabd3a62d74af9ab547e4884eb85feb6498a5a1d..dcf4813fcc1824a391958d8ff0ba8eeaff3acd36 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -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 {