diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 83ad607ba..15a9f5bae 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -664,12 +664,9 @@ extern "C" { Z3_TRY; LOG_Z3_get_bool_value(c, a); RESET_ERROR_CODE(); + CHECK_IS_EXPR(a, Z3_L_UNDEF); ast_manager & m = mk_c(c)->m(); ast * n = to_ast(a); - if (!is_expr(n)) { - SET_ERROR_CODE(Z3_INVALID_ARG); - return Z3_L_UNDEF; - } if (m.is_true(to_expr(n))) return Z3_L_TRUE; if (m.is_false(to_expr(n))) diff --git a/src/api/api_context.h b/src/api/api_context.h index b5a15d657..719902f89 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -244,6 +244,7 @@ inline api::context * mk_c(Z3_context c) { return reinterpret_castcheck_searching(); inline bool is_expr(Z3_ast a) { return is_expr(to_ast(a)); } +#define CHECK_IS_EXPR(_p_, _ret_) { if (!is_expr(_p_)) { SET_ERROR_CODE(Z3_INVALID_ARG); return _ret_; } } inline bool is_bool_expr(Z3_context c, Z3_ast a) { return is_expr(a) && mk_c(c)->m().is_bool(to_expr(a)); } #define CHECK_FORMULA(_a_, _ret_) { if (_a_ == 0 || !CHECK_REF_COUNT(_a_) || !is_bool_expr(c, _a_)) { SET_ERROR_CODE(Z3_INVALID_ARG); return _ret_; } } inline void check_sorts(Z3_context c, ast * n) { mk_c(c)->check_sorts(n); } diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index 5ae36532b..633d51fab 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -153,6 +153,7 @@ extern "C" { if (v) *v = 0; RESET_ERROR_CODE(); CHECK_NON_NULL(m, Z3_FALSE); + CHECK_IS_EXPR(t, Z3_FALSE); model * _m = to_model_ref(m); expr_ref result(mk_c(c)->m()); _m->eval(to_expr(t), result, model_completion == Z3_TRUE);