mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

Merge pull request #646 from martin-neuhaeusser/ocaml-c89

Browse source 
Make C-layer of OCaml bindings C89 compatible.
This commit is contained in:
Christoph M. Wintersteiger 2016-06-24 13:40:50 +01:00 • committed by GitHub
commit d90a575981
2 changed files with 69 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/api/ml/z3native_stubs.c.pre
View file

@ -227,6 +227,7 @@ void Z3_ast_finalize(value v) {
int Z3_ast_compare(value v1, value v2) {
Z3_ast_plus * a1 = (Z3_ast_plus*)Data_custom_val(v1);
Z3_ast_plus * a2 = (Z3_ast_plus*)Data_custom_val(v2);
unsigned id1, id2;
/* if the two ASTs belong to different contexts, we take
their contexts' addresses to order them (arbitrarily, but fixed) */
@ -242,8 +243,8 @@ int Z3_ast_compare(value v1, value v2) {
return +1;
/* Comparison according to AST ids. */
unsigned id1 = Z3_get_ast_id(a1->cp->ctx, a1->p);
unsigned id2 = Z3_get_ast_id(a2->cp->ctx, a2->p);
id1 = Z3_get_ast_id(a1->cp->ctx, a1->p);
id2 = Z3_get_ast_id(a2->cp->ctx, a2->p);
if (id1 == id2)
return 0;
else if (id1 < id2)
@ -255,7 +256,7 @@ int Z3_ast_compare(value v1, value v2) {
int Z3_ast_compare_ext(value v1, value v2) {
Z3_ast_plus * a1 = (Z3_ast_plus*)Data_custom_val(v1);
unsigned id1;
int id2 = Val_int(v2);
unsigned id2 = (unsigned)Val_int(v2);
if (a1->p == NULL && id2 == 0)
return 0;
if (a1->p == NULL)