diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 216bcd559..d7a537ee8 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -274,8 +274,10 @@ class theory_lra::imp {
 
         lbool check(lp::explanation_t& ex) {
             if (m_use_niil) {
-                if (m_niil != nullptr)
+                if (m_niil != nullptr) {
+                    std::cout << "check niil\n";
                     return (*m_niil)->check(ex);
+                }
             }
             else {
                 if (m_nra != nullptr)
@@ -2047,16 +2049,7 @@ public:
         return lia_check;
     }
 
-    lbool check_nra() {
-        m_use_nra_model = false;
-        if (m.canceled()) {
-            TRACE("arith", tout << "canceled\n";);
-            return l_undef;
-        }
-        if (!m_nra) return l_true;
-        if (!m_switcher.need_check()) return l_true;
-        m_a1 = nullptr; m_a2 = nullptr;
-        lbool r = m_switcher.check(m_explanation);
+    lbool check_aftermath_nra(lbool r) {
         m_a1 = alloc(scoped_anum, m_nra->am());
         m_a2 = alloc(scoped_anum, m_nra->am());
         switch (r) {
@@ -2077,6 +2070,23 @@ public:
         return r;
     }
 
+    lbool check_aftermath_niil(lbool r) {
+        return r;
+    }
+    
+    lbool check_nra() {
+        m_use_nra_model = false;
+        if (m.canceled()) {
+            TRACE("arith", tout << "canceled\n";);
+            return l_undef;
+        }
+        if (!m_nra && !m_niil) return l_true;
+        if (!m_switcher.need_check()) return l_true;
+        m_a1 = nullptr; m_a2 = nullptr;
+        lbool r = m_switcher.check(m_explanation);
+        return m_nra? check_aftermath_nra(r) : check_aftermath_niil(r);
+    }
+
     /**
        \brief We must redefine this method, because theory of arithmetic contains
        underspecified operators such as division by 0.
diff --git a/src/util/lp/niil_solver.cpp b/src/util/lp/niil_solver.cpp
index 838308710..db2b80d33 100644
--- a/src/util/lp/niil_solver.cpp
+++ b/src/util/lp/niil_solver.cpp
@@ -48,6 +48,12 @@ struct solver::imp {
         m_monomials.shrink(m_monomials_lim[m_monomials_lim.size() - n]);
         m_monomials_lim.shrink(m_monomials_lim.size() - n);       
     }
+
+    lbool check(lp::explanation_t& ex) {
+        lp_assert(m_solver.get_status() == lp::lp_status::OPTIMAL);
+        return l_undef;
+    }
+    
 };
 void solver::add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs) {
     std::cout << "called add_monomial\n";
@@ -56,8 +62,7 @@ void solver::add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs)
 bool solver::need_check() { return true; }
 
 lbool solver::check(lp::explanation_t& ex) {
-    lp_assert(false);
-    return l_undef;
+    return m_imp->check(ex);
 }