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

@@ -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;