mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-07 15:55:46 +00:00
Code Activity

use Z3_char_ptr

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-10-08 09:14:10 -07:00
parent f4b803de95
commit 7e174f50c1
10 changed files with 29 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/api_util.h
View file

@ -54,7 +54,7 @@ inline Z3_ast of_ast(ast* a) { return reinterpret_cast<Z3_ast>(a); }
inline expr * to_expr(Z3_ast a) { return reinterpret_cast<expr*>(a); }
inline Z3_ast of_expr(expr* e) { return reinterpret_cast<Z3_ast>(e); }
inline expr * const * to_exprs(Z3_ast const* a) { return reinterpret_cast<expr* const*>(a); }
inline expr * const * to_exprs(unsigned n, Z3_ast const* a) { return reinterpret_cast<expr* const*>(a); }
inline Z3_ast * const * of_exprs(expr* const* e) { return reinterpret_cast<Z3_ast* const*>(e); }
inline app * to_app(Z3_app a) { return reinterpret_cast<app*>(a); }
@ -165,7 +165,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned num_args, Z3_ast const* args) { \
LOG_ ## NAME(c, num_args, args); \
RESET_ERROR_CODE(); \
EXTRA_CODE; \
ast* a = mk_c(c)->m().mk_app(FID, OP, 0, 0, num_args, to_exprs(args)); \
ast* a = mk_c(c)->m().mk_app(FID, OP, 0, 0, num_args, to_exprs(num_args, args)); \
mk_c(c)->save_ast_trail(a); \
check_sorts(c, a); \
RETURN_Z3(of_ast(a)); \