diff --git a/src/smt/proto_model/value_factory.h b/src/smt/proto_model/value_factory.h
index 5bd0a1f75..92ad2373b 100644
--- a/src/smt/proto_model/value_factory.h
+++ b/src/smt/proto_model/value_factory.h
@@ -189,11 +189,12 @@ public:
             max_size = Number(usz);
             has_max = true;
         }
+        Number start = set->m_next;
         Number & next    = set->m_next;
         while (!is_new) {
             result = mk_value(next, s, is_new);
             next++;
-            if (has_max && next > max_size + set->m_next) {
+            if (has_max && next > max_size + start) {
                 return 0;
             }
         }