Z3 4.0 Push and Pop In Solver

z3

Solution

The new API in Z3 4.0 has many new features. For example, it introduces several new objects: Solvers, Goals, Tactics, Probes, etc. Moreover, we also introduce a new memory management policy for objects such as ASTs and Models that existed in previous APIs. The new memory management policy is based on reference counting. Every object has APIs of the form `Z3_<object>_inc_ref` and `Z3_<object>_dec_ref`. We still support the old memory management policy for ASTs and Models. If the `Z3_context` is created using `Z3_mk_context`, then the old memory management policy is enabled for ASTs. If it is created using `Z3_mk_context_rc`, then `Z3_inc_ref` and `Z3_dec_ref` must be used to manage the reference counters. However, the new objects (Solvers, Goals, Tactics, etc) only support reference counting. We strongly encourage all users to move to the new reference counting memory management policy. So, all new objects only support this policy. Moreover, all managed APIs (.Net, Python and OCaml) are based on the reference counting policy. Note that, we provide a thin C++ layer on top of the C API. It "hides" all reference counting calls using "smart pointers". The source code for the C++ layer is included in the Z3 distribution.

That being said, your program crashes because you did not increment the reference counter of the object `Z3_solver`. Here is the corrected version of your program. I essentially added the missing calls to `Z3_solver_inc_ref` and `Z3_solver_dec_ref`. The latter is needed to avoid a memory leak. After it, I also included the same program using the C++ API. It is much simpler. The C++ API is provided in the file `include\z3++.h` in the Z3 distribution. Examples are included at `examples\c++`.

Z3_config cfg;
Z3_context ctx;
Z3_solver solver;
Z3_ast x, zero, one, x_eq_zero, x_eq_one;

cfg                = Z3_mk_config();
ctx                = Z3_mk_context(cfg);
Z3_del_config(cfg);
solver = Z3_mk_solver((Z3_context)ctx);
Z3_solver_inc_ref(ctx, solver);

x           = mk_int_var(ctx, "x");
zero        = mk_int(ctx, 0);
one         = mk_int(ctx, 1);
x_eq_zero     = Z3_mk_eq(ctx, x, zero);
x_eq_one     = Z3_mk_eq(ctx, x, one);

//Z3_solver_push (ctx,  solver);

Z3_solver_assert(ctx, solver, x_eq_zero);
printf("Scopes : %d\n", Z3_solver_get_num_scopes((Z3_context) ctx, (Z3_solver) solver));

printf("%s \n", Z3_ast_to_string(ctx, x_eq_zero));

int result = Z3_solver_check ((Z3_context) ctx, (Z3_solver) solver);
printf("Sat Result : %d\n", result);
printf("Model : %s\n", Z3_model_to_string ((Z3_context) ctx,  Z3_solver_get_model ((Z3_context) ctx,  (Z3_solver) solver)));

// Z3_solver_pop (ctx, solver, 1);
// printf("Scopes : %d\n", Z3_solver_get_num_scopes((Z3_context) ctx, (Z3_solver) solver));
Z3_solver_assert(ctx, solver, x_eq_one);
result = Z3_solver_check ((Z3_context) ctx, (Z3_solver) solver);
printf("Sat Result : %d\n", result);
// printf("Model : %s\n", Z3_model_to_string ((Z3_context) ctx,  Z3_solver_get_model ((Z3_context) ctx,  (Z3_solver) solver)));
Z3_solver_dec_ref(ctx, solver);
return 0;

C++ version

context c;
solver  s(c);
expr x = c.int_const("x");
expr x_eq_zero = x == 0;
expr x_eq_one  = x == 1;

s.add(x_eq_zero);
std::cout << "Scopes : " << Z3_solver_get_num_scopes(c, s) << "\n";
std::cout << x_eq_zero << "\n";
std::cout << s.check() << "\n";
std::cout << s.get_model() << "\n";

s.add(x_eq_one);
std::cout << s.check() << "\n";
return 0;

Problem

Original source