diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 0a61a5ce6..14618887a 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1609,12 +1609,16 @@ void cmd_context::set_diagnostic_stream(char const * name) {
     }
 }
 
-struct contains_array_op_proc {
+struct contains_underspecified_op_proc {
     struct found {};
     family_id m_array_fid;
-    contains_array_op_proc(ast_manager & m):m_array_fid(m.mk_family_id("array")) {}
+    datatype_util m_dt;
+    
+    contains_underspecified_op_proc(ast_manager & m):m_array_fid(m.mk_family_id("array")), m_dt(m) {}
     void operator()(var * n)        {}
     void operator()(app * n)        {
+        if (m_dt.is_accessor(n->get_decl())) 
+            throw found();
         if (n->get_family_id() != m_array_fid)
             return;
         decl_kind k = n->get_decl_kind();
@@ -1713,7 +1717,7 @@ void cmd_context::validate_model() {
     p.set_bool("completion", true);
     model_evaluator evaluator(*(md.get()), p);
     evaluator.set_expand_array_equalities(false);
-    contains_array_op_proc contains_array(m());
+    contains_underspecified_op_proc contains_underspecified(m());
     {
         scoped_rlimit _rlimit(m().limit(), 0);
         cancel_eh<reslimit> eh(m().limit());
@@ -1739,9 +1743,9 @@ void cmd_context::validate_model() {
                     continue;
                 }
                 try {
-                    for_each_expr(contains_array, r);
+                    for_each_expr(contains_underspecified, r);
                 }
-                catch (contains_array_op_proc::found) {
+                catch (contains_underspecified_op_proc::found) {
                     continue;
                 }
                 TRACE("model_validate", model_smt2_pp(tout, *this, *(md.get()), 0););
diff --git a/src/smt/proto_model/datatype_factory.cpp b/src/smt/proto_model/datatype_factory.cpp
index 03f008fe6..550b694da 100644
--- a/src/smt/proto_model/datatype_factory.cpp
+++ b/src/smt/proto_model/datatype_factory.cpp
@@ -38,7 +38,7 @@ expr * datatype_factory::get_some_value(sort * s) {
     }
     expr * r = m_manager.mk_app(c, args.size(), args.c_ptr());
     register_value(r);
-    TRACE("datatype_factory", tout << mk_pp(r, m_util.get_manager()) << "\n";);
+    TRACE("datatype", tout << mk_pp(r, m_util.get_manager()) << "\n";);
     return r;
 }
 
@@ -48,7 +48,7 @@ expr * datatype_factory::get_some_value(sort * s) {
 expr * datatype_factory::get_last_fresh_value(sort * s) {
     expr * val = 0;
     if (m_last_fresh_value.find(s, val)) {
-        TRACE("datatype_factory", tout << "cached fresh value: " << mk_pp(val, m_manager) << "\n";);
+        TRACE("datatype", tout << "cached fresh value: " << mk_pp(val, m_manager) << "\n";);
         return val;
     }
     value_set * set = get_value_set(s);
@@ -68,7 +68,7 @@ bool datatype_factory::is_subterm_of_last_value(app* e) {
     }
     contains_app contains(m_manager, e);
     bool result = contains(last);
-    TRACE("datatype_factory", tout << mk_pp(e, m_manager) << " in " << mk_pp(last, m_manager) << " " << result << "\n";);
+    TRACE("datatype", tout << mk_pp(e, m_manager) << " in " << mk_pp(last, m_manager) << " " << result << "\n";);
     return result;
 }
 
@@ -126,7 +126,7 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) {
                     m_last_fresh_value.insert(s, new_value);
                 }
             }
-            TRACE("datatype_factory", tout << "almost fresh: " << mk_pp(new_value, m_manager) << "\n";);
+            TRACE("datatype", tout << "almost fresh: " << mk_pp(new_value, m_manager) << "\n";);
             return new_value;
         }
     }
@@ -136,7 +136,7 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) {
 
 
 expr * datatype_factory::get_fresh_value(sort * s) {
-    TRACE("datatype_factory", tout << "generating fresh value for: " << s->get_name() << "\n";);
+    TRACE("datatype", tout << "generating fresh value for: " << s->get_name() << "\n";);
     value_set * set = get_value_set(s);
     // Approach 0) 
     // if no value for s was generated so far, then used get_some_value
@@ -144,7 +144,7 @@ expr * datatype_factory::get_fresh_value(sort * s) {
         expr * val = get_some_value(s);
         if (m_util.is_recursive(s))
             m_last_fresh_value.insert(s, val);
-        TRACE("datatype_factory", tout << "0. result: " << mk_pp(val, m_manager) << "\n";);
+        TRACE("datatype", tout << "0. result: " << mk_pp(val, m_manager) << "\n";);
         return val;
     }
     // Approach 1)
@@ -171,13 +171,13 @@ expr * datatype_factory::get_fresh_value(sort * s) {
         }
         expr_ref new_value(m_manager);
         new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr());
-        CTRACE("datatype_factory", found_fresh_arg && set->contains(new_value), tout << mk_pp(new_value, m_manager) << "\n";);
+        CTRACE("datatype", found_fresh_arg && set->contains(new_value), tout << mk_pp(new_value, m_manager) << "\n";);
         SASSERT(!found_fresh_arg || !set->contains(new_value));
         if (!set->contains(new_value)) {
             register_value(new_value);
             if (m_util.is_recursive(s))
                 m_last_fresh_value.insert(s, new_value);
-            TRACE("datatype_factory", tout << "1. result: " << mk_pp(new_value, m_manager) << "\n";);
+            TRACE("datatype", tout << "1. result: " << mk_pp(new_value, m_manager) << "\n";);
             return new_value;
         }
     }
@@ -188,16 +188,16 @@ expr * datatype_factory::get_fresh_value(sort * s) {
     if (m_util.is_recursive(s)) {
         while(true) {
             ++num_iterations;
-            TRACE("datatype_factory", tout << mk_pp(get_last_fresh_value(s), m_manager) << "\n";);
+            TRACE("datatype", tout << mk_pp(get_last_fresh_value(s), m_manager) << "\n";);
             ptr_vector<func_decl> const & constructors = *m_util.get_datatype_constructors(s);
             for (func_decl * constructor : constructors) {
                 expr_ref_vector args(m_manager);
                 bool found_sibling   = false;
                 unsigned num         = constructor->get_arity();
-                TRACE("datatype_factory", tout << "checking constructor: " << constructor->get_name() << "\n";);
+                TRACE("datatype", tout << "checking constructor: " << constructor->get_name() << "\n";);
                 for (unsigned i = 0; i < num; i++) {
                     sort * s_arg        = constructor->get_domain(i);
-                    TRACE("datatype_factory", tout << mk_pp(s, m_manager) << " " 
+                    TRACE("datatype", tout << mk_pp(s, m_manager) << " " 
                           << mk_pp(s_arg, m_manager) << " are_siblings " 
                           << m_util.are_siblings(s, s_arg) << "  is_datatype " 
                           << m_util.is_datatype(s_arg) << " found_sibling " 
@@ -212,7 +212,7 @@ expr * datatype_factory::get_fresh_value(sort * s) {
                             maybe_new_arg = get_fresh_value(s_arg);
                         }
                         if (!maybe_new_arg) {
-                            TRACE("datatype_factory", 
+                            TRACE("datatype", 
                                   tout << "no argument found for " << mk_pp(s_arg, m_manager) << "\n";);
                             maybe_new_arg = m_model.get_some_value(s_arg);
                             found_sibling = false;
@@ -229,11 +229,11 @@ expr * datatype_factory::get_fresh_value(sort * s) {
                 if (found_sibling) {
                     expr_ref new_value(m_manager);
                     new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr());
-                    TRACE("datatype_factory", tout << "potential new value: " << mk_pp(new_value, m_manager) << "\n";);
+                    TRACE("datatype", tout << "potential new value: " << mk_pp(new_value, m_manager) << "\n";);
                     m_last_fresh_value.insert(s, new_value);
                     if (!set->contains(new_value)) {
                         register_value(new_value);
-                        TRACE("datatype_factory", tout << "2. result: " << mk_pp(new_value, m_manager) << "\n";);
+                        TRACE("datatype", tout << "2. result: " << mk_pp(new_value, m_manager) << "\n";);
                         return new_value;
                     }
                 }