#5324

Z3Prover · Jun 6, 2021 · 29ac26e · 29ac26e
1 parent 34fc0cd
commit 29ac26e
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git 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
@@ -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() {