mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 14:53:40 +00:00
Code Activity

Z3_lbool should be signed in API

Browse source
This commit is contained in:
Zachary Kincaid 2015-07-26 21:17:59 -04:00
parent fc3e1af4a9
commit 6214ba900b
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/z3_api.h
View file

@ -4237,7 +4237,7 @@ END_MLAPI_EXCLUDE
/** /**
\brief Return Z3_L_TRUE if \c a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF otherwise. \brief Return Z3_L_TRUE if \c a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF otherwise.
def_API('Z3_get_bool_value', UINT, (_in(CONTEXT), _in(AST))) def_API('Z3_get_bool_value', INT, (_in(CONTEXT), _in(AST)))
*/ */
Z3_lbool Z3_API Z3_get_bool_value(Z3_context c, Z3_ast a); Z3_lbool Z3_API Z3_get_bool_value(Z3_context c, Z3_ast a);
@ -7578,7 +7578,7 @@ END_MLAPI_EXCLUDE
\deprecated To be moved outside of API. \deprecated To be moved outside of API.
def_API('Z3_get_implied_equalities', UINT, (_in(CONTEXT), _in(SOLVER), _in(UINT), _in_array(2, AST), _out_array(2, UINT))) def_API('Z3_get_implied_equalities', INT, (_in(CONTEXT), _in(SOLVER), _in(UINT), _in_array(2, AST), _out_array(2, UINT)))
*/ */
Z3_lbool Z3_API Z3_get_implied_equalities( Z3_lbool Z3_API Z3_get_implied_equalities(
Z3_context c, Z3_context c,