Z3_solver_pop() does not clear ASTs

[remysucre]

The docs for Z3_mk_context() says the following:

the life time of Z3_ast objects are determined by the scope level of Z3_solver_push and Z3_solver_pop. In other words, a Z3_ast object remains valid until there is a call to Z3_solver_pop that takes the current scope below the level where the object was created

However it appears an AST object is still reachable after popping the scope. To reproduce, add the following to examples/c/test_capi.c:

void push_pop()
{
    Z3_context ctx;
    Z3_solver s;
    Z3_ast x, number;
    Z3_ast c;

    ctx    = mk_context();
    s      = mk_solver(ctx);

    Z3_solver_push(ctx, s);

    x      = mk_int_var(ctx, "x");
    number = mk_int(ctx, 2);
    c      = Z3_mk_divides(ctx, number, x);

    Z3_solver_pop(ctx, s, 1);

    Z3_solver_assert(ctx, s, c);

    check2(ctx, s, Z3_L_TRUE);

    del_solver(ctx, s);
    Z3_del_context(ctx);
}

[NikolajBjorner]

That documentation is very stale. It was true when there were no separate solver objects. All assertions were associated with a context. With multiple solver objects there is no association between ast life time and solver objects. You could have two solver objects pushing and popping independently and at the same time create expressions used in one or both solvers. I will fix the documentation. If you need life time behavior then mk_context_rc() is your "friend" at the cost of lots of inc/dec ref on your own. You can also use C++ (or Rust?) which has awesome lexical scope.