diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp
index 3180c58eb..c5403b66f 100644
--- a/src/math/lp/nla_solver.cpp
+++ b/src/math/lp/nla_solver.cpp
@@ -34,7 +34,7 @@ lbool solver::run_nra(lp::explanation & expl) {
 lbool solver::check(vector<lemma>& l, lp::explanation& expl) {    
     set_use_nra_model(false);
     lbool ret = m_core->check(l);
-    if (ret == l_undef) {
+    if (false && ret == l_undef) { // disable the call to nlsat
         ret = run_nra(expl);
         if (ret == l_true || expl.size() > 0) {
             set_use_nra_model(true);