#5482

remove overly permissive filter on select_store axiom

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();

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)) {