diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 4f4da6bd4..52be66e77 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -895,7 +895,7 @@ extern "C" { RESET_ERROR_CODE(); func_decl* _d = to_func_decl(d); - if (null_family_id == _d->get_family_id()) { + if (d == nullptr || null_family_id == _d->get_family_id()) { return Z3_OP_UNINTERPRETED; } if (mk_c(c)->get_basic_fid() == _d->get_family_id()) { diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index e693c4531..a9b3e6131 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -850,6 +850,7 @@ namespace smt { } bool theory_bv::internalize_term(app * term) { + try { SASSERT(term->get_family_id() == get_family_id()); TRACE("bv", tout << "internalizing term: " << mk_bounded_pp(term, get_manager()) << "\n";); if (approximate_term(term)) { @@ -907,6 +908,11 @@ namespace smt { UNREACHABLE(); return false; } + } + catch (z3_exception& ex) { + IF_VERBOSE(1, verbose_stream() << ex.msg() << "\n";); + throw; + } } #define MK_NO_OVFL(NAME, OP) \