diff --git a/src/smt/proto_model/datatype_factory.cpp b/src/smt/proto_model/datatype_factory.cpp
index 5be802714..a45b53155 100644
--- a/src/smt/proto_model/datatype_factory.cpp
+++ b/src/smt/proto_model/datatype_factory.cpp
@@ -67,6 +67,7 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) {
     value_set * set = get_value_set(s);
     if (set->empty()) {
         expr * val = get_some_value(s);
+        SASSERT(val);
         if (m_util.is_recursive(s))
             m_last_fresh_value.insert(s, val);
         return val;
@@ -185,10 +186,16 @@ expr * datatype_factory::get_fresh_value(sort * s) {
                     if (!found_sibling && m_util.is_datatype(s_arg) && m_util.are_siblings(s, s_arg)) {
                         found_sibling = true;
                         expr * maybe_new_arg = get_almost_fresh_value(s_arg);
+                        if (!maybe_new_arg) {
+                            maybe_new_arg = m_model.get_some_value(s_arg);
+                            found_sibling = false;
+                        }
+                        SASSERT(maybe_new_arg);
                         args.push_back(maybe_new_arg);
                     }
                     else {
                         expr * some_arg = m_model.get_some_value(s_arg);
+                        SASSERT(some_arg);
                         args.push_back(some_arg);
                     }
                 }
diff --git a/src/smt/proto_model/value_factory.h b/src/smt/proto_model/value_factory.h
index 115a01345..92ad2373b 100644
--- a/src/smt/proto_model/value_factory.h
+++ b/src/smt/proto_model/value_factory.h
@@ -184,18 +184,17 @@ public:
         sort_size const* sz = s_info?&s_info->get_num_elements():0;
         bool has_max = false;
         Number max_size;
-        if (sz && sz->is_finite()) {
-            if (sz->size() < UINT_MAX) {
-                unsigned usz = static_cast<unsigned>(sz->size());
-                max_size = Number(usz);
-                has_max = true;
-            }
+        if (sz && sz->is_finite() && sz->size() < UINT_MAX) {
+            unsigned usz = static_cast<unsigned>(sz->size());
+            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) {
+            if (has_max && next > max_size + start) {
                 return 0;
             }
         }
diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp
index 69e1c8bc3..eb806e23c 100644
--- a/src/tactic/sls/sls_tactic.cpp
+++ b/src/tactic/sls/sls_tactic.cpp
@@ -1343,6 +1343,7 @@ class sls_tactic : public tactic {
             m_zero(m_mpz_manager.mk_z(0)),
             m_one(m_mpz_manager.mk_z(1)),
             m_two(m_mpz_manager.mk_z(2)),
+            m_cancel(false),
             m_bv_util(m),
             m_tracker(m, m_bv_util, m_mpz_manager, m_powers)
         {
diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp
index e25abc48c..8b6577b3f 100644
--- a/src/test/qe_arith.cpp
+++ b/src/test/qe_arith.cpp
@@ -106,7 +106,7 @@ static void test2(char const *ex) {
         sorts.push_back(m.get_sort(vars[i].get()));
     }
     expr_abstract(m, 0, bound.size(), bound.c_ptr(), fml, fml2);
-    fml2 = m.mk_exists(boud.size(), sorts.c_ptr(), names.c_ptr(), fml2);
+    fml2 = m.mk_exists(bound.size(), sorts.c_ptr(), names.c_ptr(), fml2);
     qe::expr_quant_elim qe(m, params);
     expr_ref pr1 = qe::arith_project(*md, vars, lits);
     qe(m.mk_true(), fml2, pr2);