Fix quantifiers selector over store rewrite (#2510)

Due an ordering on if's the rewrite sel( store( a, i, j ), k ) ---> ite( k=i, j, sel( a, k ) ) was very rarely kicking in.

After the change, we are +61-7 on SMT LIB:
https://www.starexec.org/starexec/secure/details/job.jsp?id=30581

1 files changed, 22 insertions, 20 deletions

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 1f94dd3df..e2a26f6e6 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -667,7 +667,28 @@ Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol
           }
         }
       }
-    }else if( elimExtArith ){
+    }
+    else if (ret.getKind() == SELECT && ret[0].getKind() == STORE)
+    {
+      Node st = ret[0];
+      Node index = ret[1];
+      std::vector<Node> iconds;
+      std::vector<Node> elements;
+      while (st.getKind() == STORE)
+      {
+        iconds.push_back(index.eqNode(st[1]));
+        elements.push_back(st[2]);
+        st = st[0];
+      }
+      ret = nm->mkNode(SELECT, st, index);
+      // conditions
+      for (int i = (iconds.size() - 1); i >= 0; i--)
+      {
+        ret = nm->mkNode(ITE, iconds[i], elements[i], ret);
+      }
+    }
+    else if( elimExtArith )
+    {
       if( ret.getKind()==INTS_DIVISION_TOTAL || ret.getKind()==INTS_MODULUS_TOTAL ){
         Node num = ret[0];
         Node den = ret[1];
@@ -711,25 +732,6 @@ Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol
         }
       }
     }
-    else if (ret.getKind() == SELECT && ret[0].getKind() == STORE)
-    {
-      Node st = ret[0];
-      Node index = ret[1];
-      std::vector<Node> iconds;
-      std::vector<Node> elements;
-      while (st.getKind() == STORE)
-      {
-        iconds.push_back(index.eqNode(st[1]));
-        elements.push_back(st[2]);
-        st = st[0];
-      }
-      ret = nm->mkNode(SELECT, st, index);
-      // conditions
-      for (int i = (iconds.size() - 1); i >= 0; i--)
-      {
-        ret = nm->mkNode(ITE, iconds[i], elements[i], ret);
-      }
-    }
     icache[prev] = ret;
     return ret;
   }