diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h index 5fdfe6297..2a4b3ead7 100644 --- a/src/muz/rel/doc.h +++ b/src/muz/rel/doc.h @@ -175,17 +175,17 @@ public: if (m.contains(*m_elems[i], *t)) { found = true; } - if (m.contains(*t, *m_elems[i])) { + else if (m.contains(*t, *m_elems[i])) { m.deallocate(m_elems[i]); --j; + continue; } - else if (i != j) { + if (i != j) { m_elems[j] = m_elems[i]; } } if (j != sz) m_elems.resize(j); if (found) { - SASSERT(j == i); m.deallocate(t); } else {