Skip to content

Commit

Permalink
fix #7229
Browse files Browse the repository at this point in the history
  • Loading branch information
NikolajBjorner committed May 18, 2024
1 parent 552068a commit cb50dca
Showing 1 changed file with 3 additions and 6 deletions.
9 changes: 3 additions & 6 deletions src/api/z3_api.h
Original file line number Diff line number Diff line change
Expand Up @@ -1593,12 +1593,9 @@ extern "C" {
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.
In contrast to #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.
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.
In contrast to \c Z3_mk_context_rc the life time of \c Z3_ast objects
persists with the life time of the context.
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.
Their reference counts are not handled by the context.
Expand Down

0 comments on commit cb50dca

Please sign in to comment.