diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index b5c99f5ce..6bcca936a 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1123,7 +1123,7 @@ bool cmd_context::try_mk_builtin_app(symbol const & s, unsigned num_args, expr * result = m().mk_app(fid, k, num_indices, indices, num_args, args, range); } CHECK_SORT(result.get()); - return true; + return nullptr != result.get(); } bool cmd_context::try_mk_declared_app(symbol const & s, unsigned num_args, expr * const * args, diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 65a6f5ed5..344c61283 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -1944,6 +1944,8 @@ namespace smt2 { expr ** expr_it = expr_stack().data() + fr->m_expr_spos; expr ** expr_end = expr_it + num_decls; for (; expr_it != expr_end; ++expr_it, ++sym_it) { + if (!(*expr_it)) + throw parser_exception("invalid let expression"); TRACE("let_frame", tout << "declaring: " << *sym_it << " " << mk_pp(*expr_it, m()) << "\n";); m_env.insert(*sym_it, local(*expr_it, m_num_bindings)); }