From ee125b4fe3e33f0062ab525da3640038f89b6237 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie@cmu.edu>
Date: Wed, 23 Mar 2016 19:05:21 -0400
Subject: [PATCH 1/2] extend model with the value of a fresh variable

---
 src/qe/qe_arrays.cpp | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp
index 88b0290d5..162a4fb78 100644
--- a/src/qe/qe_arrays.cpp
+++ b/src/qe/qe_arrays.cpp
@@ -309,12 +309,19 @@ namespace qe {
                 expr_ref_vector args(m);
                 sort* range = get_array_range(m.get_sort(s));
                 for (unsigned i = 0; i < idxs.size(); ++i) {
-                    app_ref var(m);
+                    app_ref var(m), sel(m);
+                    expr_ref val(m);
                     var = m.mk_fresh_const("value", range);
                     vars.push_back(var);
                     args.reset();
-                    args.push_back(result);
+                    
+                    args.push_back (s);
                     args.append(idxs[i].m_values.size(), idxs[i].m_vars);
+                    sel = a.mk_select (args.size (), args.c_ptr ());
+                    VERIFY (model.eval (sel, val));
+                    model.register_decl (var->get_decl (), val);
+                    
+                    args[0] = result;
                     args.push_back(var);
                     result = a.mk_store(args.size(), args.c_ptr());
                 }
@@ -398,6 +405,7 @@ namespace qe {
                 // TBD chase definition of nested array.
                 return l_undef;
             }
+            // AG: Shouldn't this be l_false
             return l_true;
         }            
     };

From 4e7b6b6586ee6c223086ca81d0586b4d414f30fd Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie@cmu.edu>
Date: Wed, 23 Mar 2016 19:20:27 -0400
Subject: [PATCH 2/2] proposed fix to compare

---
 src/qe/qe_arrays.cpp | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp
index 162a4fb78..f8f44b6d9 100644
--- a/src/qe/qe_arrays.cpp
+++ b/src/qe/qe_arrays.cpp
@@ -397,16 +397,15 @@ namespace qe {
         }
 
         lbool compare(expr* val1, expr* val2) {
-            if (val1 == val2) {
-                return l_true;
-            }
+            if (m.are_equal (val1, val2)) return l_true;
+            if (m.are_distinct (val1, val2)) return l_false;
+            
             if (is_uninterp(val1) ||
                 is_uninterp(val2)) {
                 // TBD chase definition of nested array.
                 return l_undef;
             }
-            // AG: Shouldn't this be l_false
-            return l_true;
+            return l_undef;
         }            
     };