diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp
index ce182a97b..ff2abde75 100644
--- a/src/qe/qe_lite.cpp
+++ b/src/qe/qe_lite.cpp
@@ -2342,6 +2342,7 @@ private:
     elim_star    m_elim_star;
     th_rewriter  m_rewriter;
 
+    bool m_use_array_der;
     bool has_unique_non_ground(expr_ref_vector const& fmls, unsigned& index) {
         index = fmls.size();
         if (index <= 1) {
@@ -2359,13 +2360,14 @@ private:
     }
 
 public:
-    impl(ast_manager & m, params_ref const & p):
+    impl(ast_manager & m, params_ref const & p, bool use_array_der):
         m(m),
         m_der(m, p),
         m_fm(m),
         m_array_der(m),
         m_elim_star(*this),
-        m_rewriter(m) {}
+        m_rewriter(m),
+        m_use_array_der(use_array_der) {}
 
     void operator()(app_ref_vector& vars, expr_ref& fml) {
         if (vars.empty()) {
@@ -2445,14 +2447,15 @@ public:
         m_array_der.set_is_variable_proc(is_var);
         m_der(fmls);
         m_fm(fmls);
-        m_array_der(fmls);
+        // AG: disalble m_array_der() since it interferes with other array handling
+        if (m_use_array_der) m_array_der(fmls);
         TRACE("qe_lite", for (unsigned i = 0; i < fmls.size(); ++i) tout << mk_pp(fmls[i].get(), m) << "\n";);
     }
 
 };
 
-qe_lite::qe_lite(ast_manager & m, params_ref const & p) {
-    m_impl = alloc(impl, m, p);
+qe_lite::qe_lite(ast_manager & m, params_ref const & p, bool use_array_der) {
+    m_impl = alloc(impl, m, p, use_array_der);
 }
 
 qe_lite::~qe_lite() {
@@ -2484,7 +2487,7 @@ class qe_lite_tactic : public tactic {
 
         imp(ast_manager& m, params_ref const & p):
             m(m),
-            m_qe(m, p)
+            m_qe(m, p, true)
         {}
 
         void checkpoint() {
diff --git a/src/qe/qe_lite.h b/src/qe/qe_lite.h
index cff547f36..a918ab33d 100644
--- a/src/qe/qe_lite.h
+++ b/src/qe/qe_lite.h
@@ -31,7 +31,10 @@ class qe_lite {
     class impl;
     impl * m_impl;
 public:
-    qe_lite(ast_manager & m, params_ref const & p);
+    /** 
+        use_array_der controls whether equalities over array reads are simplified
+     */
+    qe_lite(ast_manager& m, params_ref const & p, bool use_array_der = true);
 
     ~qe_lite();