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, 32 insertions, 0 deletions

diff --git a/test/regress/regress0/quantifiers/qarray-sel-over-store.smt2 b/test/regress/regress0/quantifiers/qarray-sel-over-store.smt2
new file mode 100644
index 000000000..f7e5a3a04
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qarray-sel-over-store.smt2
@@ -0,0 +1,32 @@
+; EXPECT: unsat
+(set-logic AUFBV)
+(set-info :status unsat)
+(set-info :category "crafted")
+(declare-sort Element 0)
+
+(declare-fun a1 () (Array (_ BitVec 8) Element))
+(declare-fun a2 () (Array (_ BitVec 8) Element))
+(declare-fun a3 () (Array (_ BitVec 8) Element))
+(declare-fun a4 () (Array (_ BitVec 8) Element))
+
+(declare-fun i2 () (_ BitVec 8))
+(declare-fun i3 () (_ BitVec 8))
+
+(declare-fun e1 () Element)
+(declare-fun e2 () Element)
+
+(assert (not (= e1 e2)))
+(assert (= a3 (store a1 (_ bv3 8) e1)))
+(assert (= a4 (store a2 (_ bv3 8) e1)))
+(assert (= (select a3 (_ bv2 8)) e1))
+(assert (= (select a4 (_ bv2 8)) e2))
+
+; (assert (eqrange a3 a4 (_ bv0 8) (_ bv2 8)))
+
+(assert (forall ((x (_ BitVec 8)))
+    (=> (and (bvule (_ bv0 8) x) (bvule x (_ bv2 8))) (= (select a3 x) (select a4 x)))
+    ))
+
+
+(check-sat)
+(exit)