mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

style/formatting

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-09-16 19:34:48 +01:00
parent b70cc47a9d
commit 27ea7d8e9d
1 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/sat/sat_clause.cpp
View file

@ -153,11 +153,11 @@ namespace sat {
ptr &= 0xFFFFFFFF00000000ull; // Keep only high part ptr &= 0xFFFFFFFF00000000ull; // Keep only high part
unsigned i = 0; unsigned i = 0;
for (i = 0; i < m_num_segments; ++i) for (i = 0; i < m_num_segments; ++i)
if (m_segments[i] == ptr) if (m_segments[i] == ptr)
return i; return i;
i = m_num_segments; i = m_num_segments;
#if defined(Z3DEBUG)
SASSERT(i <= c_last_segment); SASSERT(i <= c_last_segment);
#if defined(Z3DEBUG)
if (i == c_last_segment) { if (i == c_last_segment) {
if (!m_last_seg_id2cls.contains(cls->id())) if (!m_last_seg_id2cls.contains(cls->id()))
m_last_seg_id2cls.insert(cls->id(), cls); m_last_seg_id2cls.insert(cls->id(), cls);
@ -167,7 +167,6 @@ namespace sat {
m_segments[i] = ptr; m_segments[i] = ptr;
} }
#else #else
SASSERT(i <= c_last_segment);
if (i == c_last_segment) { if (i == c_last_segment) {
throw default_exception("segment out of range"); throw default_exception("segment out of range");
} }