From 992daa6d2e7addceae95fa5bb75b705f1af8b11d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 27 Aug 2021 21:03:30 -0700
Subject: [PATCH] #5482

remove overly permissive filter on select_store axiom
---
 src/sat/smt/array_axioms.cpp | 2 --
 src/sat/smt/euf_model.cpp    | 8 +++++---
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp
index 86fc5fccefc..cd0b241fb72 100644
--- a/src/sat/smt/array_axioms.cpp
+++ b/src/sat/smt/array_axioms.cpp
@@ -181,8 +181,6 @@ namespace array {
         ptr_buffer<expr> sel1_args, sel2_args;
         unsigned num_args = select->get_num_args();
 
-        if (expr2enode(store->get_arg(0))->get_root() == expr2enode(select->get_arg(0))->get_root()) 
-            return false;
         bool has_diff = false;
         for (unsigned i = 1; i < num_args; i++) 
             has_diff |= expr2enode(select->get_arg(i))->get_root() != expr2enode(store->get_arg(i))->get_root();
diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index 1782251799d..30f81b7ca1b 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@@ -23,6 +23,7 @@ Module Name:
 namespace euf {
 
     class solver::user_sort {
+        solver& s;
         ast_manager& m;
         model_ref& mdl;
         expr_ref_vector& values;
@@ -31,7 +32,7 @@ namespace euf {
         obj_map<sort, expr_ref_vector*>    sort2values;
     public:
         user_sort(solver& s, expr_ref_vector& values, model_ref& mdl) :
-            m(s.m), mdl(mdl), values(values), factory(m) {}
+            s(s), m(s.m), mdl(mdl), values(values), factory(m) {}
 
         ~user_sort() {
             for (auto kv : sort2values)
@@ -41,10 +42,11 @@ namespace euf {
         void add(enode* r, sort* srt) {
             unsigned id = r->get_expr_id();
             expr_ref value(m);
-            if (m.is_value(r->get_expr())) 
+            if (m.is_value(r->get_expr()))
                 value = r->get_expr();
-            else 
+            else
                 value = factory.get_fresh_value(srt);
+            TRACE("model", tout << s.bpp(r) << " := " << value << "\n";);
             values.set(id, value);
             expr_ref_vector* vals = nullptr;
             if (!sort2values.find(srt, vals)) {