diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp
index f40eb2c75..cba31665c 100644
--- a/src/ast/static_features.cpp
+++ b/src/ast/static_features.cpp
@@ -165,7 +165,8 @@ void static_features::update_core(expr * e) {
     // even if a benchmark does not contain any theory interpreted function decls, we still have to install
     // the theory if the benchmark contains constants or function applications of an interpreted sort.
     sort * s      = m_manager.get_sort(e);
-    mark_theory(s->get_family_id());
+    if (!m_manager.is_uninterp(s))
+        mark_theory(s->get_family_id());
     
     bool _is_gate = is_gate(e);
     bool _is_eq   = m_manager.is_eq(e);
@@ -255,9 +256,11 @@ void static_features::update_core(expr * e) {
                 m_num_simple_eqs++;
         }
         sort * s      = m_manager.get_sort(to_app(e)->get_arg(0));
-        family_id fid = s->get_family_id();
-        if (fid != null_family_id && fid != m_bfid)
-            inc_theory_eqs(fid);
+        if (!m_manager.is_uninterp(s)) {
+            family_id fid = s->get_family_id();
+            if (fid != null_family_id && fid != m_bfid)
+                inc_theory_eqs(fid);
+        }
     }
     if (!m_has_int && m_autil.is_int(e))
         m_has_int  = true;
@@ -295,9 +298,11 @@ void static_features::update_core(expr * e) {
             if (to_app(e)->get_num_args() == 0) {
                 m_num_uninterpreted_constants++;
                 sort * s      = m_manager.get_sort(e);
-                family_id fid = s->get_family_id();
-                if (fid != null_family_id && fid != m_bfid)
-                    inc_theory_constants(fid);
+                if (!m_manager.is_uninterp(s)) {
+                    family_id fid = s->get_family_id();
+                    if (fid != null_family_id && fid != m_bfid)
+                        inc_theory_constants(fid);
+                }
             }
         }
         func_decl * d = to_app(e)->get_decl();
@@ -312,18 +317,20 @@ void static_features::update_core(expr * e) {
             for (unsigned i = 0; i < num_args; i++) {
                 expr * arg   = to_app(e)->get_arg(i);
                 sort * arg_s = m_manager.get_sort(arg); 
-                family_id fid_arg = arg_s->get_family_id();
-                if (fid_arg != fid && fid_arg != null_family_id) {
-                    m_num_aliens++;
-                    inc_num_aliens(fid_arg);
-                    if (fid_arg == m_afid) {
-                        SASSERT(!_is_le_ge);
-                        m_num_arith_terms++;
-                        rational k;
-                        TRACE("diff_term", tout << "diff_term: " << is_diff_term(arg, k) << "\n" << mk_pp(arg, m_manager) << "\n";);
-                        if (is_diff_term(arg, k)) {
-                            m_num_diff_terms++;
-                            acc_num(k);
+                if (!m_manager.is_uninterp(arg_s)) {
+                    family_id fid_arg = arg_s->get_family_id();
+                    if (fid_arg != fid && fid_arg != null_family_id) {
+                        m_num_aliens++;
+                        inc_num_aliens(fid_arg);
+                        if (fid_arg == m_afid) {
+                            SASSERT(!_is_le_ge);
+                            m_num_arith_terms++;
+                            rational k;
+                            TRACE("diff_term", tout << "diff_term: " << is_diff_term(arg, k) << "\n" << mk_pp(arg, m_manager) << "\n";);
+                            if (is_diff_term(arg, k)) {
+                                m_num_diff_terms++;
+                                acc_num(k);
+                            }
                         }
                     }
                 }
diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp
index d7a06f14f..70287728e 100644
--- a/src/smt/proto_model/proto_model.cpp
+++ b/src/smt/proto_model/proto_model.cpp
@@ -526,49 +526,56 @@ bool proto_model::is_finite(sort * s) const {
 }
 
 expr * proto_model::get_some_value(sort * s) {
-    family_id fid = s->get_family_id();
-    if (fid == null_family_id) {
+    if (m_manager.is_uninterp(s)) {
+        return m_user_sort_factory->get_some_value(s);
+    }
+    else {
+        family_id fid = s->get_family_id();
+        value_factory * f = get_factory(fid);
+        if (f) 
+            return f->get_some_value(s);
+        // there is no factory for the family id, then assume s is uninterpreted.
         return m_user_sort_factory->get_some_value(s);
     }
-    value_factory * f = get_factory(fid);
-    if (f) 
-        return f->get_some_value(s);
-    // there is no factory for the family id, then assume s is uninterpreted.
-    return m_user_sort_factory->get_some_value(s);
 }
 
 bool proto_model::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
-    family_id fid = s->get_family_id();
-    if (fid == null_family_id) {
+    if (m_manager.is_uninterp(s)) {
         return m_user_sort_factory->get_some_values(s, v1, v2);
     }
-    value_factory * f = get_factory(fid);
-    if (f) 
-        return f->get_some_values(s, v1, v2);
-    else
-        return false;
+    else {
+        family_id fid = s->get_family_id();
+        value_factory * f = get_factory(fid);
+        if (f) 
+            return f->get_some_values(s, v1, v2);
+        else
+            return false;
+    }
 }
 
 expr * proto_model::get_fresh_value(sort * s) {
-    family_id fid = s->get_family_id();
-    if (fid == null_family_id)
-        return m_user_sort_factory->get_fresh_value(s);
-    value_factory * f = get_factory(fid);
-    if (f) 
-        return f->get_fresh_value(s);
-    else
-        // Use user_sort_factory if the theory has no support for model construnction.
-        // This is needed when dummy theories are used for arithmetic or arrays.
+    if (m_manager.is_uninterp(s)) {
         return m_user_sort_factory->get_fresh_value(s);
+    }
+    else {
+        family_id fid = s->get_family_id();    
+        value_factory * f = get_factory(fid);
+        if (f) 
+            return f->get_fresh_value(s);
+        else
+            // Use user_sort_factory if the theory has no support for model construnction.
+            // This is needed when dummy theories are used for arithmetic or arrays.
+            return m_user_sort_factory->get_fresh_value(s);
+    }
 }
 
 void proto_model::register_value(expr * n) {
     sort * s = m_manager.get_sort(n);
-    family_id fid = s->get_family_id();
-    if (fid == null_family_id) {
+    if (m_manager.is_uninterp(s)) {
         m_user_sort_factory->register_value(n);
     }
     else {
+        family_id fid = s->get_family_id();
         value_factory * f = get_factory(fid);
         if (f)
             f->register_value(n);