1
2 /*++
3 Copyright (c) 2015 Microsoft Corporation
4
5 --*/
6
7 #include<stdio.h>
8 #include "api/z3.h"
9
tst_api_bug()10 void tst_api_bug() {
11 unsigned vmajor, vminor, vbuild, vrevision;
12
13 Z3_get_version(&vmajor, &vminor, &vbuild, &vrevision);
14
15 printf("Using Z3 Version %u.%u (build %u, revision %u)\n", vmajor, vminor, vbuild, vrevision);
16
17
18 Z3_config cfg = Z3_mk_config();
19 Z3_set_param_value(cfg, "MODEL", "true");
20 Z3_context ctx = Z3_mk_context(cfg);
21 Z3_solver s = Z3_mk_solver(ctx);
22 Z3_solver_inc_ref(ctx, s);
23
24 Z3_sort is = Z3_mk_int_sort(ctx);
25 Z3_sort ss = Z3_mk_set_sort(ctx, is);
26 Z3_ast e = Z3_mk_empty_set(ctx, is);
27 // { 42 }
28 Z3_ast fortytwo = Z3_mk_set_add(ctx, e, Z3_mk_int(ctx, 42, is));
29 // { 42, 43 }
30 Z3_ast fortythree = Z3_mk_set_add(ctx, fortytwo, Z3_mk_int(ctx, 43, is));
31 // { 42 } U { 42, 43 }
32
33 Z3_ast uargs[2] = { fortytwo, fortythree };
34 Z3_ast u = Z3_mk_set_union(ctx, 2, uargs);
35
36 Z3_symbol sym = Z3_mk_string_symbol(ctx, "mySet");
37 Z3_ast sc = Z3_mk_const(ctx, sym, ss);
38 Z3_ast c = Z3_mk_eq(ctx, sc, u);
39
40 Z3_solver_push(ctx, s);
41 Z3_solver_assert(ctx, s, c);
42
43 printf("result %d\n", Z3_solver_check(ctx, s));
44 Z3_model m = Z3_solver_get_model(ctx, s);
45 Z3_string ms = Z3_model_to_string(ctx, m);
46 printf("model : %s\n", ms);
47 Z3_solver_dec_ref(ctx, s);
48 Z3_del_config(cfg);
49 Z3_del_context(ctx);
50 }
51
52
53