diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 3473fbb49..0df729467 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -2109,10 +2109,11 @@ namespace seq {
             // m_max_search_depth == 0 means unlimited; otherwise stop when bound exceeds it.
             m_depth_bound = 10;
             while (true) {
-                if (m_cancel_fn && m_cancel_fn()) {
+                if (!m().inc()) {
 #ifdef Z3DEBUG
                     // Examining the Nielsen graph is probably the best way of debugging
                     std::string dot = to_dot();
+                    IF_VERBOSE(1, verbose_stream() << dot << "\n";);
 #endif
                     break;
                 }
@@ -2156,7 +2157,7 @@ namespace seq {
         m_stats.m_max_depth = std::max(m_stats.m_max_depth, depth);
 
         // check for external cancellation (timeout, user interrupt)
-        if (m_cancel_fn && m_cancel_fn())
+        if (!m().inc())
             return search_result::unknown;
 
         // check DFS node budget (0 = unlimited)
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index 772be0989..e5070524f 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -744,8 +744,6 @@ namespace seq {
         unsigned                      m_num_input_mems = 0;
         nielsen_stats                 m_stats;
 
-        // external cancellation callback: returns true if solving should abort
-        std::function<bool()>         m_cancel_fn;
 
         // -----------------------------------------------
         // Integer subsolver (abstract interface)
@@ -835,9 +833,6 @@ namespace seq {
         // enable/disable Parikh image verification constraints
         void set_parikh_enabled(bool e) { m_parikh_enabled = e; }
 
-        // set a cancellation callback; solve() checks this periodically
-        void set_cancel_fn(std::function<bool()> fn) { m_cancel_fn = std::move(fn); }
-
         // generate next unique regex membership id
         unsigned next_mem_id() { return m_next_mem_id++; }
 
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index dac1a1fa0..a299b13b2 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -48,7 +48,6 @@ namespace smt {
 
     void theory_nseq::init() {
         m_arith_value.init(&get_context());
-        m_nielsen.set_cancel_fn([this]() { return get_context().get_cancel_flag(); });
     }
 
     // -----------------------------------------------------------------------