From 6c966bba59677589fbaf76d6c29a8aceab70eaa6 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 16 Feb 2016 13:58:49 +0000 Subject: [PATCH] Fix incorrect (off by one) bound check. Also assert that we don't increment ``m_num_segments`` beyond the maximum value (``c_max_segments``). This is related to #436. When doing an AddressSanitized build and running the ``c_example`` it looks like Z3 tries to create too many segments and index out of bounds. Fixing the checks here causes them to fail which should help us narrow down the problem. --- src/sat/sat_clause.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp index 279d84375..2881c03ae 100644 --- a/src/sat/sat_clause.cpp +++ b/src/sat/sat_clause.cpp @@ -145,7 +145,8 @@ namespace sat { return i; i = 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"); m_segments[i] = ptr; return i;