diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index fec10fe0e..a8b3abc8a 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -184,6 +184,7 @@ struct solver::imp {
         lbool r = l_undef;
         statistics& st = m_nla_core.lp_settings().stats().m_st;
         try {
+            //verbose_stream() << m_limit.
             r = m_nlsat->check();
         }
         catch (z3_exception&) {
diff --git a/src/math/polynomial/upolynomial.cpp b/src/math/polynomial/upolynomial.cpp
index a73d3e5fb..56d8524d4 100644
--- a/src/math/polynomial/upolynomial.cpp
+++ b/src/math/polynomial/upolynomial.cpp
@@ -3094,6 +3094,9 @@ namespace upolynomial {
                 A.swap(D);
                 // D is of the form             P_{j+1} * P_{j+2}   * ... * P_k
                 j++;
+                if (j > 10000) {
+                    display(verbose_stream(), A) << "\n";
+                }
             }
             TRACE(factor_bug, tout << "A: "; display(tout, A); tout << "\n";);
             SASSERT(A.size() == 1 && m().is_one(A[0]));
diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp
index 28656bc63..3a3cdbc87 100644
--- a/src/util/rlimit.cpp
+++ b/src/util/rlimit.cpp
@@ -78,6 +78,8 @@ char const* reslimit::get_cancel_msg() const {
 
 void reslimit::push_child(reslimit* r) {
     lock_guard lock(*g_rlimit_mux);
+    r->m_limit = std::min(r->m_limit, m_limit - std::min(m_limit, m_count));
+    r->m_count = 0;
     m_children.push_back(r);    
 }