diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index bdc1b8b9e..c809ba0f8 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -304,16 +304,16 @@ struct goal2sat::imp : public sat::sat_internalizer {
                 convert_euf(t, root, sign);
                 return;
             }
-            else if (!is_uninterp_const(t)) {
-                if (!is_app(t)) {
-                    std::ostringstream strm;
-                    strm << mk_ismt2_pp(t, m);
-                    throw_op_not_handled(strm.str());
-                }
-                else
-                    m_unhandled_funs.push_back(to_app(t)->get_decl());
-            }
             else {
+                if (!is_uninterp_const(t)) {
+                    if (!is_app(t)) {
+                        std::ostringstream strm;
+                        strm << mk_ismt2_pp(t, m);
+                        throw_op_not_handled(strm.str());
+                    }
+                    m_unhandled_funs.push_back(to_app(t)->get_decl());
+                }
+
                 v = mk_bool_var(t);
                 l = sat::literal(v, sign);
                 bool ext = m_default_external || !is_uninterp_const(t) || m_interface_vars.contains(t);