From 77d68409c29102c53e550c6bb72779ddb59fa531 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Aug 2018 08:43:32 -0700 Subject: [PATCH] handle null declarations for kind Signed-off-by: Nikolaj Bjorner --- src/api/api_ast.cpp | 2 +- src/smt/theory_bv.cpp | 6 ++++++ 2 files changed, 7 insertions(+), 1 deletion(-) 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) \