diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h
index b64dbfff5..06f587949 100644
--- a/src/sat/smt/array_solver.h
+++ b/src/sat/smt/array_solver.h
@@ -267,6 +267,6 @@ namespace array {
         void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {}
         void unmerge_eh(theory_var v1, theory_var v2) {}
 
-        euf::enode_vector const& parent_selects(euf::enode* n) const { return m_var_data[n->get_th_var(get_id())]->m_parent_selects; }
+        euf::enode_vector const& parent_selects(euf::enode* n) { return m_var_data[find(n->get_th_var(get_id()))]->m_parent_selects; }
     };
 }
diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp
index 930ca4fed..a297d7951 100644
--- a/src/sat/smt/euf_model.cpp
+++ b/src/sat/smt/euf_model.cpp
@@ -63,6 +63,7 @@ namespace euf {
     };
 
     void solver::update_model(model_ref& mdl) {
+        TRACE("model", tout << "create model\n";);
         mdl->reset_eval_cache();
         for (auto* mb : m_solvers)
             mb->init_model();
@@ -117,7 +118,7 @@ namespace euf {
         for (enode* n : fresh_values)
             n->unmark1();
         
-        TRACE("euf",
+        TRACE("model",
               for (auto const& d : deps.deps()) 
                   if (d.m_value) {
                       tout << bpp(d.m_key) << ":\n";
@@ -254,7 +255,7 @@ namespace euf {
                 m_values2root.insert(m_values.get(n->get_expr_id()), n);
         TRACE("model", 
               for (auto kv : m_values2root) 
-                  tout << mk_pp(kv.m_key, m) << " -> " << bpp(kv.m_value) << "\n";);
+                  tout << mk_bounded_pp(kv.m_key, m) << "\n    -> " << bpp(kv.m_value) << "\n";);
         
         return m_values2root;
     }