mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix scope accounting bug and documentation per Konrad's request
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
c917c1c53d
commit
67b802c9d9
|
@ -361,6 +361,7 @@ namespace api {
|
|||
}
|
||||
}
|
||||
}
|
||||
SASSERT(num_scopes <= get_smt_kernel().get_scope_level());
|
||||
get_smt_kernel().pop(num_scopes);
|
||||
}
|
||||
|
||||
|
|
|
@ -40,7 +40,7 @@ extern "C" {
|
|||
LOG_Z3_pop(c, num_scopes);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_SEARCHING(c);
|
||||
if (num_scopes > mk_c(c)->get_smt_kernel().get_scope_level()) {
|
||||
if (num_scopes > mk_c(c)->get_num_scopes()) {
|
||||
SET_ERROR_CODE(Z3_IOB);
|
||||
return;
|
||||
}
|
||||
|
|
|
@ -7069,7 +7069,7 @@ END_MLAPI_EXCLUDE
|
|||
\mlonly then a valid model is returned. Otherwise, it is unsafe to use the returned model.\endmlonly
|
||||
\conly The caller is responsible for deleting the model using the function #Z3_del_model.
|
||||
|
||||
\conly \remark In constrast with the rest of the Z3 API, the reference counter of the
|
||||
\conly \remark In contrast with the rest of the Z3 API, the reference counter of the
|
||||
\conly model is incremented. This is to guarantee backward compatibility. In previous
|
||||
\conly versions, models did not support reference counting.
|
||||
|
||||
|
@ -7182,6 +7182,11 @@ END_MLAPI_EXCLUDE
|
|||
\brief Delete a model object.
|
||||
|
||||
\sa Z3_check_and_get_model
|
||||
|
||||
\conly \remark The Z3_check_and_get_model automatically increments a reference count on the model.
|
||||
\conly The expected usage is that models created by that method are deleted using Z3_del_model.
|
||||
\conly This is for backwards compatibility and in contrast to the rest of the API where
|
||||
\conly callers are responsible for managing reference counts.
|
||||
|
||||
\deprecated Subsumed by Z3_solver API
|
||||
|
||||
|
|
Loading…
Reference in a new issue