mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 12:21:21 +00:00
Code Activity

Merge pull request #453 from delcypher/fix_clause_allocator_bound_check

Browse source 
Fix incorrect (off by one) bound check in clause_allocator
This commit is contained in:
Nikolaj Bjorner 2016-02-17 08:50:51 -08:00
commit 16ced7cda5
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/sat/sat_clause.cpp
View file

@ -145,7 +145,8 @@ namespace sat {
return i; return i;
i = m_num_segments; i = m_num_segments;
m_num_segments++; m_num_segments++;
if (i > c_max_segments) SASSERT(m_num_segments <= c_max_segments);
if (i >= c_max_segments)
throw default_exception("segment out of range"); throw default_exception("segment out of range");
m_segments[i] = ptr; m_segments[i] = ptr;
return i; return i;