mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nuno Lopes 2014-09-16 14:57:22 +01:00
parent 919e0a5ea2 67b802c9d9
commit d3570484bb
3 changed files with 9 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_context.cpp
View file

@ -128,6 +128,7 @@ namespace api {
for (unsigned i = 0; i < m_replay_stack.size(); ++i) {
dealloc(m_replay_stack[i]);
}
m_ast_trail.reset();
}
reset_parser();
dealloc(m_solver);
@ -360,6 +361,7 @@ namespace api {
}
}
}
SASSERT(num_scopes <= get_smt_kernel().get_scope_level());
get_smt_kernel().pop(num_scopes);
}

2
src/api/api_solver_old.cpp
View file

@ -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;
}

7
src/api/z3_api.h
View file

@ -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