diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp
index 5259f3168..129026b34 100644
--- a/src/sat/smt/array_axioms.cpp
+++ b/src/sat/smt/array_axioms.cpp
@@ -175,7 +175,7 @@ namespace array {
         ptr_buffer<expr> sel1_args, sel2_args;
         unsigned num_args = select->get_num_args();
 
-        if (expr2enode(select->get_arg(0))->get_root() == expr2enode(store)->get_root())
+        if (select->get_arg(0) != store && expr2enode(select->get_arg(0))->get_root() == expr2enode(store)->get_root()) 
             return false;
         bool has_diff = false;
         for (unsigned i = 1; i < num_args; i++) 
diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index bdf7bee11..bb075d7cc 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@@ -73,6 +73,7 @@ namespace euf {
         values2model(deps, mdl);
         for (auto* mb : m_solvers)
             mb->finalize_model(*mdl);
+        TRACE("model", tout << "created model " << *mdl << "\n";);
         validate_model(*mdl);
     }
 
diff --git a/src/sat/smt/euf_relevancy.cpp b/src/sat/smt/euf_relevancy.cpp
index 51388fa80..f5c05cea9 100644
--- a/src/sat/smt/euf_relevancy.cpp
+++ b/src/sat/smt/euf_relevancy.cpp
@@ -106,8 +106,8 @@ namespace euf {
 
         TRACE("euf",
             for (enode* n : m_egraph.nodes())
-                if (is_relevant(n))
-                    tout << "relevant " << mk_bounded_pp(n->get_expr(), m) << "\n";);
-        return true;
+                if (is_relevant(n)) 
+                    tout << "relevant " << n->get_expr_id() << " [r" << n->get_root_id() << "]: " << mk_bounded_pp(n->get_expr(), m) << "\n";);
+              return true;
     }
 }