mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

fix #7229

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-05-17 18:28:08 -07:00
parent 552068a71e
commit cb50dcabda
1 changed files with 3 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/api/z3_api.h
View file

@ -1593,12 +1593,9 @@ extern "C" {
although some parameters can be changed using #Z3_update_param_value. although some parameters can be changed using #Z3_update_param_value.
All main interaction with Z3 happens in the context of a \c Z3_context. All main interaction with Z3 happens in the context of a \c Z3_context.
In contrast to #Z3_mk_context_rc, the life time of \c Z3_ast objects In contrast to \c Z3_mk_context_rc the life time of \c Z3_ast objects
are determined by the scope level of #Z3_solver_push and #Z3_solver_pop. persists with the life time of the context.
In other words, a \c 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.
Note that all other reference counted objects, including \c Z3_model, Note that all other reference counted objects, including \c Z3_model,
\c Z3_solver, \c Z3_func_interp have to be managed by the caller. \c Z3_solver, \c Z3_func_interp have to be managed by the caller.
Their reference counts are not handled by the context. Their reference counts are not handled by the context.