diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index efccdd434..eafc771d0 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -210,7 +210,7 @@ func_decl * func_decls::find(unsigned arity, sort * const * domain, sort * range if (f->get_domain(i) != domain[i]) break; } - if (i == arity) + if (i == arity || !domain) return f; } return nullptr; diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index b1614bc8a..085e6298a 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -1512,12 +1512,11 @@ namespace smt2 { f = m_ctx.find_func_decl(C, 0, nullptr, vars.size(), nullptr, srt); } catch (cmd_exception &) { - if (!args.empty()) { + if (!vars.empty()) { throw; } - } - - if (!f && !args.empty()) { + } + if (!f && !vars.empty()) { throw parser_exception("expecting a constructor that has been declared"); } if (!f) {