diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index 70ce6b397..384b44de7 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -541,9 +541,9 @@ namespace smt {
         bool process_atoms() const;
         unsigned get_num_conflicts() const { return m_num_conflicts; }
         var_kind get_var_kind(theory_var v) const { return m_data[v].kind(); }
-        bool is_base(theory_var v) const { return get_var_kind(v) == BASE; }
-        bool is_quasi_base(theory_var v) const { return get_var_kind(v) == QUASI_BASE; }
-        bool is_non_base(theory_var v) const { return get_var_kind(v) == NON_BASE; }
+        bool is_base(theory_var v) const { return v != null_theory_var && get_var_kind(v) == BASE; }
+        bool is_quasi_base(theory_var v) const { return v != null_theory_var && get_var_kind(v) == QUASI_BASE; }
+        bool is_non_base(theory_var v) const { return v != null_theory_var && get_var_kind(v) == NON_BASE; }
         void set_var_kind(theory_var v, var_kind k) { m_data[v].m_kind = k; }
         unsigned get_var_row(theory_var v) const { SASSERT(!is_non_base(v)); return m_data[v].m_row_id; }
         void set_var_row(theory_var v, unsigned r_id) { m_data[v].m_row_id = r_id; }
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index 9561aa089..f70e50ece 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -491,13 +491,21 @@ namespace smt {
                 if (!it->is_dead()) {
                     unsigned rid = it->m_row_id;
                     row & r = m_rows[rid];
-                    if (is_base(r.get_base_var()))
+                    theory_var v = r.get_base_var();
+                    if (v == null_theory_var) {
+                        // skip
+                    }
+                    else if (is_base(v)) {
                         return it;
+                    }
                     else if (quasi_base_rid == -1)
                         quasi_base_rid = rid;
                 }
             }
-            SASSERT(quasi_base_rid != -1); // since c.size() != 0
+            if (quasi_base_rid == -1) {
+                return nullptr;
+            }
+			
             quasi_base_row2base_row(quasi_base_rid);
             // There is no guarantee that v is still a variable of row quasi_base_rid.