diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp
index ec3a7d09f..4d46929a9 100644
--- a/src/qe/qe_arith.cpp
+++ b/src/qe/qe_arith.cpp
@@ -345,6 +345,9 @@ namespace qe {
                 if (is_arith(v) && !tids.contains(v)) {
                     rational r;
                     expr_ref val = eval(v);
+                    if (!m.inc())
+                        return vector<def>();
+
                     VERIFY(a.is_numeral(val, r));
                     TRACE("qe", tout << mk_pp(v, m) << " " << val << "\n";);
                     tids.insert(v, mbo.add_var(r, a.is_int(v)));
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 8f78a9106..4f903e815 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -647,8 +647,10 @@ namespace qe {
                 switch (res) {
                 case l_true:
                     s.get_model(m_model);
+                    if (!m_model)
+                        return l_undef;
                     SASSERT(validate_defs("check_sat"));
-                    SASSERT(validate_assumptions(*m_model.get(), asms));
+                    SASSERT(!m_model.get() || validate_assumptions(*m_model.get(), asms));
                     SASSERT(validate_model(asms));
                     TRACE("qe", s.display(tout); display(tout << "\n", *m_model.get()); display(tout, asms); );
                     if (m_level == 0) {