Z3 4.0 Push and Pop In Solver

Question

I want to verify my problem using the solver for 2 different constraints. I wrote a sample program for the same, where I have a variable x which I want to check and get a model for x = 0 and x = 1.

I am trying to use Push and Pop in the Solver. However I am not sure about how to do it exactly. I have written the following code. When I try to push the context and pop it back, I get a crash. I do not understand the reason for the crash, but its a Seg Fault. Even if I comment out the push and pop instructions as below, I am still getting the crash.

Could someone please give some pointers to solve the problem.

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);

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)));
return 0;

Answer 1

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;