diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 55e873997..e6b63d62d 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -14,6 +14,8 @@ Version 4.3.2 - Removed 'autoconf' dependency. We do not need to execute 'autoconf' and './configure' anymore to build Z3. +- Fixed incorrect result returned by Z3_solver_get_num_scopes. (Thanks to Herman Venter). This bug was introduced in Z3 4.3.0 + Version 4.3.1 ============= diff --git a/src/solver/strategic_solver.cpp b/src/solver/strategic_solver.cpp index 616ec5342..b6eb98b42 100644 --- a/src/solver/strategic_solver.cpp +++ b/src/solver/strategic_solver.cpp @@ -308,7 +308,7 @@ void strategic_solver::pop(unsigned n) { unsigned strategic_solver::get_scope_level() const { if (m_ctx == 0) return 0; - return m_ctx->m_assertions.size(); + return m_ctx->m_scopes.size(); } struct aux_timeout_eh : public event_handler {