From 244c641234e0df2b84a4ea575a708fbe74913b70 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 12 Aug 2016 13:19:12 +0100 Subject: [PATCH] debug check fix --- src/api/api_context.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/api_context.h b/src/api/api_context.h index 7cba15c44..d2c0b3ad4 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -245,7 +245,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_; } } +#define CHECK_IS_EXPR(_p_, _ret_) { if (_p_ == 0 || !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); }