From 1935e8696673371077b49f109143b3c24163aea0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 5 Jun 2021 18:07:10 -0700 Subject: [PATCH] #5324 --- src/sat/smt/euf_internalize.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index d3a95c689..c7cacdb24 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -114,6 +114,8 @@ namespace euf { auto* s_ext = sort2solver(e->get_sort()); if (s_ext && s_ext != e_ext) s_ext->apply_sort_cnstr(n, e->get_sort()); + else if (!s_ext && !e_ext && is_app(e)) + unhandled_function(to_app(e)->get_decl()); } expr* a = nullptr, * b = nullptr; if (m.is_eq(e, a, b) && a->get_sort()->get_family_id() != null_family_id) {