diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 74cec1191..e465adb9a 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -353,7 +353,6 @@ cmd_context::~cmd_context() {
 
 void cmd_context::set_cancel(bool f) {
     if (has_manager()) {
-        m().set_cancel(f);
         if (f) {
             m().limit().cancel();
         }
diff --git a/src/cmd_context/extra_cmds/subpaving_cmds.cpp b/src/cmd_context/extra_cmds/subpaving_cmds.cpp
index 632f558dc..d6496bccc 100644
--- a/src/cmd_context/extra_cmds/subpaving_cmds.cpp
+++ b/src/cmd_context/extra_cmds/subpaving_cmds.cpp
@@ -27,7 +27,7 @@ static void to_subpaving(cmd_context & ctx, expr * t) {
     ast_manager & m = ctx.m();
     unsynch_mpq_manager qm;
     scoped_ptr<subpaving::context> s;
-    s = subpaving::mk_mpq_context(qm);
+    s = subpaving::mk_mpq_context(ctx.m().limit(), qm);
     expr2var e2v(m);
     expr2subpaving e2s(m, *s, &e2v);
     params_ref p;
diff --git a/src/cmd_context/simplify_cmd.cpp b/src/cmd_context/simplify_cmd.cpp
index 3a1828a51..ba78abc7f 100644
--- a/src/cmd_context/simplify_cmd.cpp
+++ b/src/cmd_context/simplify_cmd.cpp
@@ -74,7 +74,7 @@ public:
         unsigned num_steps = 0;
         unsigned timeout   = m_params.get_uint("timeout", UINT_MAX);
         bool failed = false;
-        cancel_eh<th_rewriter> eh(s);
+        cancel_eh<reslimit> eh(ctx.m().limit());
         { 
             scoped_ctrl_c ctrlc(eh);
             scoped_timer timer(timeout, &eh);
diff --git a/src/math/interval/interval_def.h b/src/math/interval/interval_def.h
index aba4c3975..9d720f6c5 100644
--- a/src/math/interval/interval_def.h
+++ b/src/math/interval/interval_def.h
@@ -62,7 +62,7 @@ void interval_manager<C>::del(interval & a) {
 
 template<typename C>
 void interval_manager<C>::checkpoint() {
-    if (m_limit.canceled())
+    if (!m_limit.inc())
         throw default_exception("canceled");
     cooperate("interval");
 }
diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp
index 13a9ab030..a9ce346b9 100644
--- a/src/math/realclosure/realclosure.cpp
+++ b/src/math/realclosure/realclosure.cpp
@@ -501,8 +501,8 @@ namespace realclosure {
             m_qm(qm),
             m_mm(m_qm, *m_allocator),
             m_bqm(m_qm),
-            m_qim(m_qm),
-            m_bqim(m_bqm),
+            m_qim(lim, m_qm),
+            m_bqim(lim, m_bqm),
             m_plus_inf_approx(m_bqm),
             m_minus_inf_approx(m_bqm) {
             mpq one(1);
diff --git a/src/math/subpaving/subpaving.cpp b/src/math/subpaving/subpaving.cpp
index ad0819ad8..8aa394abe 100644
--- a/src/math/subpaving/subpaving.cpp
+++ b/src/math/subpaving/subpaving.cpp
@@ -37,7 +37,7 @@ namespace subpaving {
     protected:
         CTX m_ctx;
     public:
-        context_wrapper(typename CTX::numeral_manager & m, params_ref const & p, small_object_allocator * a):m_ctx(m, p, a) {}
+        context_wrapper(reslimit& lim, typename CTX::numeral_manager & m, params_ref const & p, small_object_allocator * a):m_ctx(lim, m, p, a) {}
         virtual ~context_wrapper() {}
         virtual unsigned num_vars() const { return m_ctx.num_vars(); }
         virtual var mk_var(bool is_int) { return m_ctx.mk_var(is_int); }
@@ -47,7 +47,6 @@ namespace subpaving {
         virtual void dec_ref(ineq * a) { m_ctx.dec_ref(reinterpret_cast<typename CTX::ineq*>(a)); }
         virtual void add_clause(unsigned sz, ineq * const * atoms) { m_ctx.add_clause(sz, reinterpret_cast<typename CTX::ineq * const *>(atoms)); }
         virtual void display_constraints(std::ostream & out, bool use_star) const { m_ctx.display_constraints(out, use_star); }
-        virtual void set_cancel(bool f) { m_ctx.set_cancel(f); }
         virtual void set_display_proc(display_var_proc * p) { m_ctx.set_display_proc(p); }
         virtual void reset_statistics() { m_ctx.reset_statistics(); }
         virtual void collect_statistics(statistics & st) const { m_ctx.collect_statistics(st); }
@@ -61,8 +60,8 @@ namespace subpaving {
         scoped_mpq        m_c;
         scoped_mpq_vector m_as;
     public:
-        context_mpq_wrapper(unsynch_mpq_manager & m, params_ref const & p, small_object_allocator * a):
-            context_wrapper<context_mpq>(m, p, a), 
+        context_mpq_wrapper(reslimit& lim, unsynch_mpq_manager & m, params_ref const & p, small_object_allocator * a):
+            context_wrapper<context_mpq>(lim, m, p, a), 
             m_c(m), 
             m_as(m) 
         {}
@@ -100,8 +99,8 @@ namespace subpaving {
         }
         
     public:
-        context_mpf_wrapper(f2n<mpf_manager> & fm, params_ref const & p, small_object_allocator * a):
-            context_wrapper<context_mpf>(fm, p, a),
+        context_mpf_wrapper(reslimit& lim, f2n<mpf_manager> & fm, params_ref const & p, small_object_allocator * a):
+            context_wrapper<context_mpf>(lim, fm, p, a),
             m_qm(fm.m().mpq_manager()),
             m_c(fm.m()),
             m_as(fm.m()),
@@ -161,8 +160,8 @@ namespace subpaving {
         }
         
     public:
-        context_hwf_wrapper(f2n<hwf_manager> & fm, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a):
-            context_wrapper<context_hwf>(fm, p, a),
+        context_hwf_wrapper(reslimit& lim,f2n<hwf_manager> & fm, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a):
+            context_wrapper<context_hwf>(lim, fm, p, a),
             m_qm(qm) {
         }
 
@@ -215,8 +214,8 @@ namespace subpaving {
         }
         
     public:
-        context_fpoint_wrapper(typename context_fpoint::numeral_manager & m, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a):
-            context_wrapper<context_fpoint>(m, p, a),
+        context_fpoint_wrapper(reslimit& lim, typename context_fpoint::numeral_manager & m, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a):
+            context_wrapper<context_fpoint>(lim, m, p, a),
             m_qm(qm), 
             m_c(m),
             m_as(m),
@@ -261,24 +260,24 @@ namespace subpaving {
     typedef context_fpoint_wrapper<context_mpff> context_mpff_wrapper;
     typedef context_fpoint_wrapper<context_mpfx> context_mpfx_wrapper;
 
-    context * mk_mpq_context(unsynch_mpq_manager & m, params_ref const & p, small_object_allocator * a) {
-        return alloc(context_mpq_wrapper, m, p, a);
+    context * mk_mpq_context(reslimit& lim, unsynch_mpq_manager & m, params_ref const & p, small_object_allocator * a) {
+        return alloc(context_mpq_wrapper, lim, m, p, a);
     }
 
-    context * mk_mpf_context(f2n<mpf_manager> & m, params_ref const & p, small_object_allocator * a) {
-        return alloc(context_mpf_wrapper, m, p, a);
+    context * mk_mpf_context(reslimit& lim, f2n<mpf_manager> & m, params_ref const & p, small_object_allocator * a) {
+        return alloc(context_mpf_wrapper, lim, m, p, a);
     }
 
-    context * mk_hwf_context(f2n<hwf_manager> & m, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a) {
-        return alloc(context_hwf_wrapper, m, qm, p, a);
+    context * mk_hwf_context(reslimit& lim, f2n<hwf_manager> & m, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a) {
+        return alloc(context_hwf_wrapper, lim, m, qm, p, a);
     }
 
-    context * mk_mpff_context(mpff_manager & m, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a) {
-        return alloc(context_mpff_wrapper, m, qm, p, a);
+    context * mk_mpff_context(reslimit& lim, mpff_manager & m, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a) {
+        return alloc(context_mpff_wrapper, lim, m, qm, p, a);
     }
 
-    context * mk_mpfx_context(mpfx_manager & m, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a) {
-        return alloc(context_mpfx_wrapper, m, qm, p, a);
+    context * mk_mpfx_context(reslimit& lim, mpfx_manager & m, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a) {
+        return alloc(context_mpfx_wrapper, lim, m, qm, p, a);
     }
 
 };
diff --git a/src/math/subpaving/subpaving.h b/src/math/subpaving/subpaving.h
index d3db92741..c6daca5cc 100644
--- a/src/math/subpaving/subpaving.h
+++ b/src/math/subpaving/subpaving.h
@@ -95,7 +95,6 @@ public:
     */
     virtual void display_constraints(std::ostream & out, bool use_star = false) const = 0;
 
-    virtual void set_cancel(bool f) = 0;
 
     virtual void collect_param_descrs(param_descrs & r) = 0;
 
@@ -112,11 +111,11 @@ public:
     virtual void display_bounds(std::ostream & out) const = 0;
 };
 
-context * mk_mpq_context(unsynch_mpq_manager & m, params_ref const & p = params_ref(), small_object_allocator * a = 0);
-context * mk_mpf_context(f2n<mpf_manager> & m, params_ref const & p = params_ref(), small_object_allocator * a = 0);
-context * mk_hwf_context(f2n<hwf_manager> & m, unsynch_mpq_manager & qm, params_ref const & p = params_ref(), small_object_allocator * a = 0);
-context * mk_mpff_context(mpff_manager & m, unsynch_mpq_manager & qm, params_ref const & p = params_ref(), small_object_allocator * a = 0);
-context * mk_mpfx_context(mpfx_manager & m, unsynch_mpq_manager & qm, params_ref const & p = params_ref(), small_object_allocator * a = 0);
+ context * mk_mpq_context(reslimit& lim, unsynch_mpq_manager & m, params_ref const & p = params_ref(), small_object_allocator * a = 0);
+context * mk_mpf_context(reslimit& lim, f2n<mpf_manager> & m, params_ref const & p = params_ref(), small_object_allocator * a = 0);
+context * mk_hwf_context(reslimit& lim, f2n<hwf_manager> & m, unsynch_mpq_manager & qm, params_ref const & p = params_ref(), small_object_allocator * a = 0);
+context * mk_mpff_context(reslimit& lim, mpff_manager & m, unsynch_mpq_manager & qm, params_ref const & p = params_ref(), small_object_allocator * a = 0);
+context * mk_mpfx_context(reslimit& lim, mpfx_manager & m, unsynch_mpq_manager & qm, params_ref const & p = params_ref(), small_object_allocator * a = 0);
 
 };
 
diff --git a/src/math/subpaving/subpaving_hwf.h b/src/math/subpaving/subpaving_hwf.h
index 71cb03be4..f57035b01 100644
--- a/src/math/subpaving/subpaving_hwf.h
+++ b/src/math/subpaving/subpaving_hwf.h
@@ -40,7 +40,7 @@ public:
 
 class context_hwf : public context_t<config_hwf> {
 public:
-    context_hwf(f2n<hwf_manager> & m, params_ref const & p, small_object_allocator * a):context_t<config_hwf>(config_hwf(m), p, a) {}
+ context_hwf(reslimit& lim, f2n<hwf_manager> & m, params_ref const & p, small_object_allocator * a):context_t<config_hwf>(lim, config_hwf(m), p, a) {}
 };
 
 };
diff --git a/src/math/subpaving/subpaving_mpf.h b/src/math/subpaving/subpaving_mpf.h
index 5cc11e6ab..16e4b38cc 100644
--- a/src/math/subpaving/subpaving_mpf.h
+++ b/src/math/subpaving/subpaving_mpf.h
@@ -41,7 +41,7 @@ public:
 
 class context_mpf : public context_t<config_mpf> {
 public:
-    context_mpf(f2n<mpf_manager> & m, params_ref const & p, small_object_allocator * a):context_t<config_mpf>(config_mpf(m), p, a) {}
+ context_mpf(reslimit& lim, f2n<mpf_manager> & m, params_ref const & p, small_object_allocator * a):context_t<config_mpf>(lim, config_mpf(m), p, a) {}
 };
 
 };
diff --git a/src/math/subpaving/subpaving_t.h b/src/math/subpaving/subpaving_t.h
index f138899cc..a6aa3cf32 100644
--- a/src/math/subpaving/subpaving_t.h
+++ b/src/math/subpaving/subpaving_t.h
@@ -467,6 +467,7 @@ public:
     typedef _scoped_numeral_vector<numeral_manager> scoped_numeral_vector;
 
 private:
+    reslimit&                 m_limit;
     C                         m_c;
     bool                      m_arith_failed; //!< True if the arithmetic module produced an exception.
     bool                      m_own_allocator;
diff --git a/src/math/subpaving/subpaving_t_def.h b/src/math/subpaving/subpaving_t_def.h
index f94692532..8cdd016aa 100644
--- a/src/math/subpaving/subpaving_t_def.h
+++ b/src/math/subpaving/subpaving_t_def.h
@@ -413,12 +413,13 @@ void context_t<C>::polynomial::display(std::ostream & out, numeral_manager & nm,
 }
 
 template<typename C>
-context_t<C>::context_t(C const & c, params_ref const & p, small_object_allocator * a):
+context_t<C>::context_t(reslimit& lim, C const & c, params_ref const & p, small_object_allocator * a):
+    m_limit(lim),
     m_c(c),
     m_own_allocator(a == 0),
     m_allocator(a == 0 ? alloc(small_object_allocator, "subpaving") : a),
     m_bm(*this, *m_allocator),
-    m_im(interval_config(m_c.m())),
+    m_im(lim, interval_config(m_c.m())),
     m_num_buffer(nm()) {
     m_arith_failed  = false;
     m_timestamp     = 0;
@@ -458,7 +459,7 @@ context_t<C>::~context_t() {
 
 template<typename C>
 void context_t<C>::checkpoint() {
-    if (m_limit.canceled())
+    if (!m_limit.inc())
         throw default_exception("canceled");
     if (memory::get_allocation_size() > m_max_memory)
         throw default_exception(Z3_MAX_MEMORY_MSG);
diff --git a/src/math/subpaving/tactic/subpaving_tactic.cpp b/src/math/subpaving/tactic/subpaving_tactic.cpp
index 35935ff22..a0f84c04c 100644
--- a/src/math/subpaving/tactic/subpaving_tactic.cpp
+++ b/src/math/subpaving/tactic/subpaving_tactic.cpp
@@ -103,11 +103,11 @@ class subpaving_tactic : public tactic {
             if (m_kind != new_kind) {
                 m_kind = new_kind;
                 switch (m_kind) {
-                case MPQ:  m_ctx = subpaving::mk_mpq_context(m_qm); break;
-                case MPF:  m_ctx = subpaving::mk_mpf_context(m_fm); break;
-                case HWF:  m_ctx = subpaving::mk_hwf_context(m_hm, m_qm); break;
-                case MPFF: m_ctx = subpaving::mk_mpff_context(m_ffm, m_qm); break;
-                case MPFX: m_ctx = subpaving::mk_mpfx_context(m_fxm, m_qm); break;
+                case MPQ:  m_ctx = subpaving::mk_mpq_context(m().limit(), m_qm); break;
+                case MPF:  m_ctx = subpaving::mk_mpf_context(m().limit(), m_fm); break;
+                case HWF:  m_ctx = subpaving::mk_hwf_context(m().limit(), m_hm, m_qm); break;
+                case MPFF: m_ctx = subpaving::mk_mpff_context(m().limit(), m_ffm, m_qm); break;
+                case MPFX: m_ctx = subpaving::mk_mpfx_context(m().limit(), m_fxm, m_qm); break;
                 default: UNREACHABLE(); break;
                 }
                 m_e2s = alloc(expr2subpaving, m_manager, *m_ctx, &m_e2v);
@@ -123,10 +123,6 @@ class subpaving_tactic : public tactic {
             m_ctx->reset_statistics();
         }
 
-        void set_cancel(bool f) {
-            m_ctx->set_cancel(f);
-        }
-
         subpaving::ineq * mk_ineq(expr * a) {
             bool neg = false;
             while (m().is_not(a, a))
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index 91e1b8bf5..c1f21226b 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -84,7 +84,7 @@ private:
         volatile bool   m_canceled;
         aux_timeout_eh(solver * s):m_solver(s), m_canceled(false) {}
         virtual void operator()() {
-            m_solver->get_manager().cancel();
+            m_solver->get_manager().limit().cancel();
             m_canceled = true;
         }
     };