You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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:
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.
The docs for
Z3_mk_context()
says the following:However it appears an AST object is still reachable after popping the scope. To reproduce, add the following to examples/c/test_capi.c:
The text was updated successfully, but these errors were encountered: