mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

fix bounds check to fix segfault reported in issue #565

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-04-16 12:25:29 -07:00
parent 1c8e0918d8
commit 0094b36636
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/opt/opt_context.cpp
View file

@ -1205,7 +1205,7 @@ namespace opt {
} }
inf_eps context::get_lower_as_num(unsigned idx) { inf_eps context::get_lower_as_num(unsigned idx) {
if (idx > m_objectives.size()) { if (idx >= m_objectives.size()) {
throw default_exception("index out of bounds"); throw default_exception("index out of bounds");
} }
objective const& obj = m_objectives[idx]; objective const& obj = m_objectives[idx];
@ -1223,7 +1223,7 @@ namespace opt {
} }
inf_eps context::get_upper_as_num(unsigned idx) { inf_eps context::get_upper_as_num(unsigned idx) {
if (idx > m_objectives.size()) { if (idx >= m_objectives.size()) {
throw default_exception("index out of bounds"); throw default_exception("index out of bounds");
} }
objective const& obj = m_objectives[idx]; objective const& obj = m_objectives[idx];