From d5ca902bf6240a5527c15e6b0744dec87a7d274b Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Wed, 21 Jun 2017 20:54:22 -0400
Subject: [PATCH] (mev) bug fix in expanding array equalities

The stores were processed in the wrong order so that

  (store (store a x y) x u)

was reduced to

  (store a x y)

instead of

  (store a x u)
---
 src/model/model_evaluator.cpp | 42 ++++++++++++++++++-----------------
 1 file changed, 22 insertions(+), 20 deletions(-)

diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 4d3092cf6..f88beba4c 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -213,7 +213,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
                 args.append(stores[i].size(), stores[i].c_ptr());
                 val = m_ar.mk_store(args.size(), args.c_ptr());
             }
-        }        
+        }
     }
 
     bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) {
@@ -291,13 +291,13 @@ struct evaluator_cfg : public default_rewriter_cfg {
             else {
                 conj.push_back(m().mk_eq(else1, else2));
             }
-            args1.push_back(a);
-            args2.push_back(b);
             if (args_are_unique1 && args_are_unique2 && !stores1.empty()) {
-                return mk_array_eq(stores1, else1, stores2, else2, conj, result);
+                return mk_array_eq_core(stores1, else1, stores2, else2, conj, result);
             }
 
             // TBD: this is too inefficient.
+            args1.push_back(a);
+            args2.push_back(b);
             stores1.append(stores2);
             for (unsigned i = 0; i < stores1.size(); ++i) {
                 args1.resize(1); args1.append(stores1[i].size() - 1, stores1[i].c_ptr());
@@ -338,20 +338,22 @@ struct evaluator_cfg : public default_rewriter_cfg {
 
     typedef hashtable<expr*const*, args_hash, args_eq> args_table;
 
-    br_status mk_array_eq(vector<expr_ref_vector> const& stores1, expr* else1, 
-                          vector<expr_ref_vector> const& stores2, expr* else2, 
-                          expr_ref_vector& conj, expr_ref& result) {
+    br_status mk_array_eq_core(vector<expr_ref_vector> const& stores1, expr* else1,
+                               vector<expr_ref_vector> const& stores2, expr* else2,
+                               expr_ref_vector& conj, expr_ref& result) {
         unsigned arity = stores1[0].size()-1; // TBD: fix arity.
         args_hash ah(arity);
         args_eq   ae(arity);
         args_table table1(DEFAULT_HASHTABLE_INITIAL_CAPACITY, ah, ae);
         args_table table2(DEFAULT_HASHTABLE_INITIAL_CAPACITY, ah, ae);
 
-        for (unsigned i = 0; i < stores1.size(); ++i) {
-            table1.insert(stores1[i].c_ptr());            
-        }
-        for (unsigned i = stores2.size(); i > 0; ) {
+        // stores with smaller index take precedence
+        for (unsigned i = stores1.size(); i > 0; ) {
             --i;
+            table1.insert(stores1[i].c_ptr());
+        }
+
+        for (unsigned i = 0, sz = stores2.size(); i < sz; ++i) {
             if (table2.contains(stores2[i].c_ptr())) {
                 // first insertion takes precedence.
                 continue;
@@ -361,7 +363,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
             expr* val = stores2[i][arity];
             if (table1.find(stores2[i].c_ptr(), args)) {
                 switch (compare(args[arity], val)) {
-                case l_true: table1.remove(stores2[i].c_ptr()); break;
+                case l_true: table1.remove(args); break;
                 case l_false: result = m().mk_false(); return BR_DONE;
                 default: conj.push_back(m().mk_eq(val, args[arity])); break;
                 }
@@ -389,10 +391,10 @@ struct evaluator_cfg : public default_rewriter_cfg {
     lbool compare(expr* a, expr* b) {
         if (m().are_equal(a, b)) return l_true;
         if (m().are_distinct(a, b)) return l_false;
-        return l_undef;        
+        return l_undef;
     }
 
-    
+
     bool args_are_values(expr_ref_vector const& store, bool& are_unique) {
         bool are_values = true;
         for (unsigned j = 0; are_values && j + 1 < store.size(); ++j) {
@@ -402,7 +404,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
         SASSERT(!are_unique || are_values);
         return are_values;
     }
-    
+
 
     bool extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case, bool& are_unique) {
         SASSERT(m_ar.is_array(a));
@@ -417,14 +419,14 @@ struct evaluator_cfg : public default_rewriter_cfg {
             stores.push_back(store);
             a = to_app(a)->get_arg(0);
         }
-    
+
         if (m_ar.is_const(a)) {
             else_case = to_app(a)->get_arg(0);
             return true;
         }
-    
+
         if (!m_ar.is_as_array(a)) {
-            TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m()) << "\n";);        
+            TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m()) << "\n";);
             return false;
         }
 
@@ -444,7 +446,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
                 }
             }
             stores.push_back(store);
-        }        
+        }
         else_case = g->get_else();
         if (!else_case) {
             TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m()) << "\n";
@@ -524,7 +526,7 @@ unsigned model_evaluator::get_num_steps() const {
 void model_evaluator::cleanup(params_ref const & p) {
     model_core & md = m_imp->cfg().m_model;
     dealloc(m_imp);
-    m_imp = alloc(imp, md, p);    
+    m_imp = alloc(imp, md, p);
 }
 
 void model_evaluator::reset(params_ref const & p) {