From aa4fe775b1f43d94a72635561d048dcbd3b0b9a4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 27 Nov 2012 17:18:38 -0800 Subject: [PATCH] fixed bug reported by Herman Signed-off-by: Leonardo de Moura --- RELEASE_NOTES | 2 ++ src/solver/strategic_solver.cpp | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) 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 {