mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 17:14:07 +00:00
Code Activity

use old-fashined C for test_capi

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-11-15 10:03:43 -08:00
parent 67bd90660e
commit a85a612bae
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
examples/c/test_capi.c
View file

@ -379,6 +379,7 @@ void assert_comm_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f)
Z3_sort t; Z3_sort t;
Z3_symbol f_name, t_name; Z3_symbol f_name, t_name;
Z3_ast_vector q; Z3_ast_vector q;
unsigned i;
t = Z3_get_range(ctx, f); t = Z3_get_range(ctx, f);
@ -399,7 +400,7 @@ void assert_comm_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f)
1, &t_name, &t, 1, &t_name, &t,
1, &f_name, &f); 1, &f_name, &f);
printf("assert axiom:\n%s\n", Z3_ast_vector_to_string(ctx, q)); printf("assert axiom:\n%s\n", Z3_ast_vector_to_string(ctx, q));
for (unsigned i = 0; i < Z3_ast_vector_size(ctx, q); ++i) { for (i = 0; i < Z3_ast_vector_size(ctx, q); ++i) {
Z3_solver_assert(ctx, s, Z3_ast_vector_get(ctx, q, i)); Z3_solver_assert(ctx, s, Z3_ast_vector_get(ctx, q, i));
} }
} }
@ -1644,6 +1645,7 @@ void parser_example2()
Z3_symbol names[2]; Z3_symbol names[2];
Z3_func_decl decls[2]; Z3_func_decl decls[2];
Z3_ast_vector f; Z3_ast_vector f;
unsigned i;
printf("\nparser_example2\n"); printf("\nparser_example2\n");
LOG_MSG("parser_example2"); LOG_MSG("parser_example2");
@ -1668,7 +1670,7 @@ void parser_example2()
2, names, decls); 2, names, decls);
printf("formula: %s\n", Z3_ast_vector_to_string(ctx, f)); printf("formula: %s\n", Z3_ast_vector_to_string(ctx, f));
printf("assert axiom:\n%s\n", Z3_ast_vector_to_string(ctx, f)); printf("assert axiom:\n%s\n", Z3_ast_vector_to_string(ctx, f));
for (unsigned i = 0; i < Z3_ast_vector_size(ctx, f); ++i) { for (i = 0; i < Z3_ast_vector_size(ctx, f); ++i) {
Z3_solver_assert(ctx, s, Z3_ast_vector_get(ctx, f, i)); Z3_solver_assert(ctx, s, Z3_ast_vector_get(ctx, f, i));
} }
check(ctx, s, Z3_L_TRUE); check(ctx, s, Z3_L_TRUE);