diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 52a204191..c723d9961 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -217,10 +217,7 @@ namespace nlsat {
         }
 
         void checkpoint() {
-            if (!m_rlimit.inc()) {
-                if (m_rlimit.cancel_flag_set()) throw solver_exception(Z3_CANCELED_MSG);
-                throw solver_exception(Z3_MAX_RESOURCE_MSG);
-            }
+            if (!m_rlimit.inc()) throw solver_exception(m_rlimit.get_cancel_msg());
             if (memory::get_allocation_size() > m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG);
         }
 
diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp
index 44d4603d4..0728c48be 100644
--- a/src/util/rlimit.cpp
+++ b/src/util/rlimit.cpp
@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 #include "rlimit.h"
+#include "common_msgs.h"
 
 reslimit::reslimit():
     m_cancel(false),
@@ -57,7 +58,7 @@ void reslimit::pop() {
     m_cancel = false;
 }
 
-char const* get_cancel_msg() const {
+char const* reslimit::get_cancel_msg() const {
     if (m_cancel) {
         return Z3_CANCELED_MSG;
     }