diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index c7cacdb24..8230606c0 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -109,7 +109,7 @@ namespace euf {
         if (m.is_bool(e))
             attach_lit(literal(si.add_bool_var(e), false), e);
 
-        if (!m.is_bool(e) && e->get_sort()->get_family_id() != null_family_id) {
+        if (!m.is_bool(e) && !m.is_uninterp(e->get_sort())) {
             auto* e_ext = expr2solver(e);
             auto* s_ext = sort2solver(e->get_sort());
             if (s_ext && s_ext != e_ext)
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 9d3cc9716..e6ff53e93 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -153,6 +153,7 @@ namespace euf {
         m_unhandled_functions.push_back(f);
         m_trail.push(push_back_vector<func_decl_ref_vector>(m_unhandled_functions));
         IF_VERBOSE(0, verbose_stream() << mk_pp(f, m) << " not handled\n");
+        SASSERT(false);
     }
 
     void solver::init_search() {