diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp
index 6dab74d9f..87510293f 100644
--- a/src/api/api_opt.cpp
+++ b/src/api/api_opt.cpp
@@ -124,7 +124,7 @@ extern "C" {
         LOG_Z3_optimize_check(c, o);
         RESET_ERROR_CODE();
         lbool r = l_undef;
-        cancel_eh<opt::context> eh(*to_optimize_ptr(o));
+        cancel_eh<reslimit> eh(mk_c(c)->m().limit());
         unsigned timeout = to_optimize_ptr(o)->get_params().get_uint("timeout", mk_c(c)->get_timeout());
         unsigned rlimit = mk_c(c)->get_rlimit();
         api::context::set_interruptable si(*(mk_c(c)), eh);        
diff --git a/src/ast/ast.h b/src/ast/ast.h
index e4e1b4d58..1348bf2f9 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1522,6 +1522,7 @@ public:
     }
 
     reslimit& limit() { return m_limit; }
+    bool canceled() { return !limit().inc(); }
 
     void register_plugin(symbol const & s, decl_plugin * plugin);
     
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index c2e02a1cd..77da6785f 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -578,8 +578,12 @@ void rewriter_tpl<Config>::resume_core(expr_ref & result, proof_ref & result_pr)
     while (!frame_stack().empty()) {
         if (m_cancel)
             throw rewriter_exception(Z3_CANCELED_MSG);
-        if (!m().limit().inc()) 
+        if (!m().canceled()) {
+            if (m().limit().cancel_flag_set()) {
+                throw rewriter_exception(Z3_CANCELED_MSG);
+            }
             throw rewriter_exception(Z3_MAX_RESOURCE_MSG);
+        }
         SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size());
         frame & fr = frame_stack().back();
         expr * t   = fr.m_curr;
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 3e76481d6..3eb710180 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1418,7 +1418,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
     if (m_opt && !m_opt->empty()) {
         was_opt = true;
         m_check_sat_result = get_opt();
-        cancel_eh<opt_wrapper> eh(*get_opt());
+        cancel_eh<reslimit> eh(m().limit());
         scoped_ctrl_c ctrlc(eh);
         scoped_timer timer(timeout, &eh);
         scoped_rlimit _rlimit(m().limit(), rlimit);
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 013ca7554..833977a1c 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -116,9 +116,6 @@ public:
     virtual bool empty() = 0;
     virtual void push() = 0;
     virtual void pop(unsigned n) = 0;
-    virtual void set_cancel(bool f) = 0;
-    virtual void reset_cancel() = 0;
-    virtual void cancel() = 0;
     virtual lbool optimize() = 0;
     virtual void set_hard_constraints(ptr_vector<expr> & hard) = 0;
     virtual void display_assignment(std::ostream& out) = 0;
diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 36e46d125..8566482c4 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -749,16 +749,6 @@ namespace datalog {
         m_background.push_back(e); 
     }
 
-
-#if 0
-    void context::cancel() {
-        m_cancel = true;
-        m_last_status = CANCELED;
-        m_transf.cancel();
-        if (m_engine) m_engine->cancel();
-    }
-#endif
-
     void context::cleanup() {
         m_last_status = OK;
         if (m_engine) m_engine->cleanup();
diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index 92ff429a3..e5639959b 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -209,7 +209,6 @@ namespace datalog {
         execution_result   m_last_status;
         expr_ref           m_last_answer;
         DL_ENGINE          m_engine_type;
-        volatile bool      m_cancel;
 
 
 
diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp
index 221832fed..0ca54fcd2 100644
--- a/src/muz/bmc/dl_bmc_engine.cpp
+++ b/src/muz/bmc/dl_bmc_engine.cpp
@@ -483,7 +483,7 @@ namespace datalog {
         }
 
         proof_ref get_proof(model_ref& md, func_decl* pred, app* prop, unsigned level) {
-            if (b.m_cancel) {
+            if (!m.limit().inc()) {
                 return proof_ref(0, m);
             }
             TRACE("bmc", tout << "Predicate: " << pred->get_name() << "\n";);
@@ -1172,7 +1172,7 @@ namespace datalog {
     private:
 
         void get_model(unsigned level) {
-            if (b.m_cancel) {
+            if (!m.limit().inc()) {
                 return;
             }
             rule_manager& rm = b.m_ctx.get_rule_manager();
@@ -1426,8 +1426,7 @@ namespace datalog {
         m_solver(m, m_fparams),
         m_rules(ctx),
         m_query_pred(m),
-        m_answer(m),
-        m_cancel(false) {
+        m_answer(m) {
     }
 
     bmc::~bmc() {}
@@ -1510,21 +1509,11 @@ namespace datalog {
     }
 
     void bmc::checkpoint() {
-        if (m_cancel) {
+        if (!m.limit().inc()) {
             throw default_exception("bmc canceled");
         }
     }
 
-    void bmc::cancel() {
-        m_cancel = true;
-        m_solver.cancel();
-    }
-
-    void bmc::cleanup() {
-        m_cancel = false;
-        m_solver.reset();
-    }
-
     void bmc::display_certificate(std::ostream& out) const {
         out << mk_pp(m_answer, m) << "\n";
     }
diff --git a/src/muz/bmc/dl_bmc_engine.h b/src/muz/bmc/dl_bmc_engine.h
index b9b161753..a9ef44066 100644
--- a/src/muz/bmc/dl_bmc_engine.h
+++ b/src/muz/bmc/dl_bmc_engine.h
@@ -38,7 +38,6 @@ namespace datalog {
         rule_set         m_rules;
         func_decl_ref    m_query_pred;
         expr_ref         m_answer;
-        volatile bool    m_cancel;
 
         void checkpoint();
 
@@ -59,10 +58,6 @@ namespace datalog {
 
         lbool query(expr* query);
 
-        void cancel();
-
-        void cleanup();
-
         void display_certificate(std::ostream& out) const;
 
         void collect_statistics(statistics& st) const;
diff --git a/src/muz/clp/clp_context.cpp b/src/muz/clp/clp_context.cpp
index acc38f9e6..7c5d9799f 100644
--- a/src/muz/clp/clp_context.cpp
+++ b/src/muz/clp/clp_context.cpp
@@ -84,17 +84,7 @@ namespace datalog {
             m_goals.push_back(to_app(head));
             return search(20, 0);
         }
-    
-        void cancel() {
-            m_cancel = true;
-            m_solver.cancel();
-        }
-        
-        void cleanup() {
-            m_cancel = false;
-            m_goals.reset();
-            m_solver.reset_cancel();
-        }
+            
 
         void reset_statistics() {
             m_stats.reset();
@@ -223,12 +213,7 @@ namespace datalog {
     lbool clp::query(expr* query) {
         return m_imp->query(query);
     }
-    void clp::cancel() {
-        m_imp->cancel();
-    }
-    void clp::cleanup() {
-        m_imp->cleanup();
-    }
+
     void clp::reset_statistics() {
         m_imp->reset_statistics();
     }
diff --git a/src/muz/clp/clp_context.h b/src/muz/clp/clp_context.h
index de0b25b7f..214dd891a 100644
--- a/src/muz/clp/clp_context.h
+++ b/src/muz/clp/clp_context.h
@@ -34,8 +34,6 @@ namespace datalog {
         clp(context& ctx);
         ~clp();
         virtual lbool query(expr* query);
-        virtual void cancel();
-        virtual void cleanup();
         virtual void reset_statistics();
         virtual void collect_statistics(statistics& st) const;
         virtual void display_certificate(std::ostream& out) const;        
diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index 5140c9eff..0d5d8de7d 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -1453,8 +1453,7 @@ namespace pdr {
           m_search(m_params.pdr_bfs_model_search()),
           m_last_result(l_undef),
           m_inductive_lvl(0),
-          m_expanded_lvl(0),
-          m_cancel(false)
+          m_expanded_lvl(0)
     {
     }
 
@@ -1465,7 +1464,6 @@ namespace pdr {
 
     void context::reset() {
         TRACE("pdr", tout << "\n";);
-        cleanup();
         decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
         for (; it != end; ++it) {
             dealloc(it->m_value);
@@ -1912,16 +1910,8 @@ namespace pdr {
         return l_undef;
     }
 
-    void context::cancel() {
-        m_cancel = true;
-    }
-
-    void context::cleanup() {
-        m_cancel = false;
-    }
-
     void context::checkpoint() {
-        if (m_cancel) {
+        if (!m.limit().inc()) {
             throw default_exception("pdr canceled");
         }
     }
diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h
index ad4b44d90..54bf5a691 100644
--- a/src/muz/pdr/pdr_context.h
+++ b/src/muz/pdr/pdr_context.h
@@ -336,7 +336,6 @@ namespace pdr {
         unsigned             m_expanded_lvl;
         ptr_vector<core_generalizer>  m_core_generalizers;
         stats                m_stats;
-        volatile bool        m_cancel;
         model_converter_ref  m_mc;
         proof_converter_ref  m_pc;
         
@@ -411,9 +410,6 @@ namespace pdr {
 
         lbool solve();
 
-        void cancel();
-
-        void cleanup();
 
         void reset();
 
diff --git a/src/muz/pdr/pdr_dl_interface.cpp b/src/muz/pdr/pdr_dl_interface.cpp
index 0a05d1ff3..37f708009 100644
--- a/src/muz/pdr/pdr_dl_interface.cpp
+++ b/src/muz/pdr/pdr_dl_interface.cpp
@@ -206,13 +206,7 @@ expr_ref dl_interface::get_answer() {
     return m_context->get_answer();
 }
 
-void dl_interface::cancel() {
-    m_context->cancel();
-}
 
-void dl_interface::cleanup() {
-    m_context->cleanup();
-}
 
 void dl_interface::updt_params() {
     dealloc(m_context);
diff --git a/src/muz/pdr/pdr_dl_interface.h b/src/muz/pdr/pdr_dl_interface.h
index f9e54d85b..008655a0b 100644
--- a/src/muz/pdr/pdr_dl_interface.h
+++ b/src/muz/pdr/pdr_dl_interface.h
@@ -51,10 +51,6 @@ namespace pdr {
         
         virtual lbool query(expr* query);
 
-        virtual void cancel();
-
-        virtual void cleanup();
-
         virtual void display_certificate(std::ostream& out) const;
 
         virtual void collect_statistics(statistics& st) const;
diff --git a/src/muz/rel/karr_relation.cpp b/src/muz/rel/karr_relation.cpp
index 7be271b3e..3b9198dc6 100644
--- a/src/muz/rel/karr_relation.cpp
+++ b/src/muz/rel/karr_relation.cpp
@@ -498,9 +498,6 @@ namespace datalog {
         return dynamic_cast<karr_relation const&>(r);
     }  
 
-    void karr_relation_plugin::set_cancel(bool f) {
-    }
-
     relation_base * karr_relation_plugin::mk_empty(const relation_signature & s) {
         return alloc(karr_relation, *this, 0, s, true);
     }
diff --git a/src/muz/rel/karr_relation.h b/src/muz/rel/karr_relation.h
index f4fd5312c..4f8612d7f 100644
--- a/src/muz/rel/karr_relation.h
+++ b/src/muz/rel/karr_relation.h
@@ -51,8 +51,6 @@ namespace datalog {
 
         static symbol get_name() { return symbol("karr_relation"); }
 
-        virtual void set_cancel(bool f);
-
         virtual relation_base * mk_empty(const relation_signature & s);
 
         virtual relation_base * mk_full(func_decl* p, const relation_signature & s);
diff --git a/src/opt/bcd2.cpp b/src/opt/bcd2.cpp
index e69275b27..50c3f7e51 100644
--- a/src/opt/bcd2.cpp
+++ b/src/opt/bcd2.cpp
@@ -118,7 +118,7 @@ namespace opt {
             expr_ref_vector asms(m);
             init();
             init_bcd();
-            if (m_cancel) {
+            if (m.canceled()) {
                 normalize_bounds();
                 return l_undef;
             }
@@ -130,7 +130,7 @@ namespace opt {
                 TRACE("opt", display(tout););
                 assert_cores();
                 set2asms(m_asm_set, asms);                
-                if (m_cancel) {
+                if (m.canceled()) {
                     normalize_bounds();
                     return l_undef;
                 }
diff --git a/src/opt/maxhs.cpp b/src/opt/maxhs.cpp
index 6c67dcbb5..0e16af30e 100644
--- a/src/opt/maxhs.cpp
+++ b/src/opt/maxhs.cpp
@@ -83,10 +83,6 @@ namespace opt {
         }
         virtual ~maxhs() {}
 
-        virtual void set_cancel(bool f) { 
-            maxsmt_solver_base::set_cancel(f); 
-        }
-
         virtual void collect_statistics(statistics& st) const {
             maxsmt_solver_base::collect_statistics(st);
             m_hs.collect_statistics(st);
@@ -113,7 +109,7 @@ namespace opt {
                 ++m_stats.m_num_iterations;
                 trace_bounds("maxhs");
                 TRACE("opt", tout << "(maxhs [" << m_lower << ":" << m_upper << "])\n";);
-                if (m_cancel) {
+                if (m.canceled()) {
                     return l_undef;
                 }
                 
diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index f776fa3e9..204276835 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -200,7 +200,7 @@ public:
                   display(tout);
                   );
             is_sat = check_sat_hill_climb(m_asms);
-            if (m_cancel) {
+            if (m.canceled()) {
                 return l_undef;
             }
             switch (is_sat) {
@@ -233,7 +233,7 @@ public:
         exprs cs;
         while (m_lower < m_upper) {
             lbool is_sat = check_sat_hill_climb(m_asms);
-            if (m_cancel) {
+            if (m.canceled()) {
                 return l_undef;
             }
             switch (is_sat) {
@@ -786,11 +786,6 @@ public:
         remove_soft(core, m_asms);
     }
 
-    virtual void set_cancel(bool f) {
-        maxsmt_solver_base::set_cancel(f);
-        m_mus.set_cancel(f);
-    }
-
     virtual void updt_params(params_ref& p) {
         maxsmt_solver_base::updt_params(p);
         opt_params _p(p);
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index cb598617c..8f3de6693 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -39,7 +39,6 @@ namespace opt {
         maxsat_context& c, vector<rational> const& ws, expr_ref_vector const& soft):
         m(c.get_manager()), 
         m_c(c),
-        m_cancel(false), 
         m_soft(soft),
         m_weights(ws),
         m_assertions(m) {
@@ -150,7 +149,7 @@ namespace opt {
 
 
     maxsmt::maxsmt(maxsat_context& c):
-        m(c.get_manager()), m_c(c), m_cancel(false), 
+        m(c.get_manager()), m_c(c), 
         m_soft_constraints(m), m_answer(m) {}
 
     lbool maxsmt::operator()() {
@@ -274,13 +273,6 @@ namespace opt {
         }
     }
     
-    void maxsmt::set_cancel(bool f) {
-        m_cancel = f;
-        
-        if (m_msolver) {
-            m_msolver->set_cancel(f);
-        }
-    }
     
     bool maxsmt::is_maxsat_problem(vector<rational> const& ws) const {
         for (unsigned i = 0; i < ws.size(); ++i) {
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
index 7dbf763e2..0e1e75a84 100644
--- a/src/opt/maxsmt.h
+++ b/src/opt/maxsmt.h
@@ -44,7 +44,6 @@ namespace opt {
         virtual rational get_lower() const = 0;
         virtual rational get_upper() const = 0;
         virtual bool get_assignment(unsigned index) const = 0;
-        virtual void set_cancel(bool f) = 0;
         virtual void collect_statistics(statistics& st) const = 0;
         virtual void get_model(model_ref& mdl, svector<symbol>& labels) = 0;
         virtual void updt_params(params_ref& p) = 0;
@@ -60,7 +59,6 @@ namespace opt {
     protected:
         ast_manager&     m;
         maxsat_context&  m_c;
-        volatile bool    m_cancel;
         const expr_ref_vector  m_soft;
         vector<rational> m_weights;
         expr_ref_vector  m_assertions;
@@ -78,7 +76,6 @@ namespace opt {
         virtual rational get_lower() const { return m_lower; }
         virtual rational get_upper() const { return m_upper; }
         virtual bool get_assignment(unsigned index) const { return m_assignment[index]; }
-        virtual void set_cancel(bool f) { m_cancel = f; if (f) s().cancel(); else s().reset_cancel(); }
         virtual void collect_statistics(statistics& st) const { }
         virtual void get_model(model_ref& mdl, svector<symbol>& labels) { mdl = m_model.get(); labels = m_labels;}
         virtual void commit_assignment();
@@ -115,7 +112,6 @@ namespace opt {
         ast_manager&              m;
         maxsat_context&           m_c;
         scoped_ptr<maxsmt_solver_base> m_msolver;
-        volatile bool    m_cancel;
         expr_ref_vector  m_soft_constraints;
         expr_ref_vector  m_answer;
         vector<rational> m_weights;
@@ -128,7 +124,6 @@ namespace opt {
     public:
         maxsmt(maxsat_context& c);
         lbool operator()();
-        void set_cancel(bool f);
         void updt_params(params_ref& p);
         void add(expr* f, rational const& w); 
         void set_adjust_value(adjust_value& adj) { m_adjust_value = adj; }
diff --git a/src/opt/mss.cpp b/src/opt/mss.cpp
index 9d44180a6..8c3a70e9e 100644
--- a/src/opt/mss.cpp
+++ b/src/opt/mss.cpp
@@ -26,7 +26,7 @@ Notes:
 namespace opt {
 
 
-    mss::mss(solver& s, ast_manager& m): m_s(s), m(m), m_cancel(false) {
+    mss::mss(solver& s, ast_manager& m): m_s(s), m(m) {
     }
     
     mss::~mss() {
@@ -191,7 +191,7 @@ namespace opt {
         if (core.empty()) {
             return l_true;
         }
-        if (m_cancel) {
+        if (m.canceled()) {
             return l_undef;
         }
         if (sz == 1 && core.size() == 1 && is_last && !has_mcs) {
diff --git a/src/opt/mss.h b/src/opt/mss.h
index ba9cda95d..af383634a 100644
--- a/src/opt/mss.h
+++ b/src/opt/mss.h
@@ -23,7 +23,6 @@ namespace opt {
     class mss {
         solver&       m_s;
         ast_manager&  m;
-        volatile bool m_cancel;
         typedef ptr_vector<expr> exprs;
         typedef obj_hashtable<expr>  expr_set;
         exprs         m_mss;
@@ -38,7 +37,6 @@ namespace opt {
         
         lbool operator()(model* initial_model, vector<exprs> const& cores, exprs& literals, exprs& mcs);
                 
-        void set_cancel(bool f) { m_cancel = f; }
 
         void get_model(model_ref& mdl) { mdl = m_model; }
 
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index d20b2e5f6..5d95af0a4 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -1259,26 +1259,6 @@ namespace opt {
         }
     }
 
-    void context::set_cancel(bool f) {
-        #pragma omp critical (opt_context)
-        {
-            if (m_solver) {
-                if (f) m_solver->cancel(); else m_solver->reset_cancel();
-            }
-            if (m_pareto) {
-                m_pareto->set_cancel(f);
-            }
-            if (m_simplify) {
-                if (f) m_simplify->cancel(); else m_solver->reset_cancel();
-            }
-            map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end();
-            for (; it != end; ++it) {
-                it->m_value->set_cancel(f);
-            }            
-        }
-        m_optsmt.set_cancel(f);
-    }
-
     void context::collect_statistics(statistics& stats) const {
         if (m_solver) {
             m_solver->collect_statistics(stats);
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index f581c7df2..a919d1575 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -174,9 +174,6 @@ namespace opt {
         virtual void push();
         virtual void pop(unsigned n);
         virtual bool empty() { return m_scoped_state.m_objectives.empty(); }
-        virtual void set_cancel(bool f);
-        virtual void reset_cancel() { set_cancel(false); }
-        virtual void cancel() { set_cancel(true); }
         virtual void set_hard_constraints(ptr_vector<expr> & hard);
         virtual lbool optimize();
         virtual bool print_model() const;
diff --git a/src/opt/opt_pareto.cpp b/src/opt/opt_pareto.cpp
index dea744a72..1418eb0f9 100644
--- a/src/opt/opt_pareto.cpp
+++ b/src/opt/opt_pareto.cpp
@@ -34,7 +34,7 @@ namespace opt {
             {
                 solver::scoped_push _s(*m_solver.get());
                 while (is_sat == l_true) {
-                    if (m_cancel) {
+                    if (m.canceled()) {
                         return l_undef;
                     }
                     m_solver->get_model(m_model);
@@ -92,7 +92,7 @@ namespace opt {
     lbool oia_pareto::operator()() {
         solver::scoped_push _s(*m_solver.get());
         lbool is_sat = m_solver->check_sat(0, 0);
-        if (m_cancel) {
+        if (m.canceled()) {
             is_sat = l_undef;
         }
         if (is_sat == l_true) {
diff --git a/src/opt/opt_pareto.h b/src/opt/opt_pareto.h
index 122f29c55..25b327045 100644
--- a/src/opt/opt_pareto.h
+++ b/src/opt/opt_pareto.h
@@ -37,7 +37,6 @@ namespace opt {
     protected:
         ast_manager&     m;
         pareto_callback& cb;
-        volatile bool    m_cancel;
         ref<solver>      m_solver;
         params_ref       m_params;
         model_ref        m_model;
@@ -50,7 +49,6 @@ namespace opt {
             params_ref & p):
             m(m),
             cb(cb),            
-            m_cancel(false),
             m_solver(s),
             m_params(p) {
         }
@@ -65,13 +63,6 @@ namespace opt {
         virtual void collect_statistics(statistics & st) const {
             m_solver->collect_statistics(st);
         }
-        virtual void set_cancel(bool f) {
-            if (f) 
-                m_solver->cancel();
-            else 
-                m_solver->reset_cancel();
-            m_cancel = f;
-        }
         virtual void display(std::ostream & out) const {
             m_solver->display(out);
         }
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index c9ee61ebc..b692cb18c 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -41,11 +41,6 @@ Notes:
 namespace opt {
 
 
-    void optsmt::set_cancel(bool f) {
-        TRACE("opt", tout << "set cancel: " << f << "\n";);
-        m_cancel = f;
-    }
-
     void optsmt::set_max(vector<inf_eps>& dst, vector<inf_eps> const& src, expr_ref_vector& fmls) {
         for (unsigned i = 0; i < src.size(); ++i) {
             if (src[i] >= dst[i]) {
@@ -74,7 +69,7 @@ namespace opt {
         expr* vars[1];
 
         solver::scoped_push _push(*m_s);
-        while (is_sat == l_true && !m_cancel) {
+        while (is_sat == l_true && !m.canceled()) {
 
             tmp = m.mk_fresh_const("b", m.mk_bool_sort());            
             vars[0] = tmp;
@@ -86,7 +81,7 @@ namespace opt {
             }
         }      
         
-        if (m_cancel || is_sat == l_undef) {
+        if (m.canceled() || is_sat == l_undef) {
             return l_undef;
         }
 
@@ -110,11 +105,11 @@ namespace opt {
 
         lbool is_sat = l_true;
 
-        while (is_sat == l_true && !m_cancel) {
+        while (is_sat == l_true && !m.canceled()) {
             is_sat = update_upper();
         }      
         
-        if (m_cancel || is_sat == l_undef) {
+        if (m.canceled() || is_sat == l_undef) {
             return l_undef;
         }
 
@@ -150,7 +145,7 @@ namespace opt {
             lbool is_sat = l_true;
 
             solver::scoped_push _push(*m_s);
-            while (!m_cancel) {
+            while (!m.canceled()) {
                 m_s->assert_expr(fml);
                 TRACE("opt", tout << fml << "\n";);
                 is_sat = m_s->check_sat(1,vars);
@@ -185,7 +180,7 @@ namespace opt {
         bound = m.mk_or(m_lower_fmls.size(), m_lower_fmls.c_ptr());
         m_s->assert_expr(bound);
         
-        if (m_cancel) {
+        if (m.canceled()) {
             return l_undef;
         }
         return basic_opt();
@@ -242,7 +237,7 @@ namespace opt {
 
         vector<inf_eps> mid;
 
-        for (unsigned i = 0; i < m_lower.size() && !m_cancel; ++i) {
+        for (unsigned i = 0; i < m_lower.size() && !m.canceled(); ++i) {
             if (m_lower[i] < m_upper[i]) {
                 mid.push_back((m_upper[i]+m_lower[i])/rational(2));
                 bound = m_s->mk_ge(i, mid[i]);
@@ -254,7 +249,7 @@ namespace opt {
             }
         }
         bool progress = false;
-        for (unsigned i = 0; i < m_lower.size() && !m_cancel; ++i) {
+        for (unsigned i = 0; i < m_lower.size() && !m.canceled(); ++i) {
             if (m_lower[i] <= mid[i] && mid[i] <= m_upper[i] && m_lower[i] < m_upper[i]) {
                 th.enable_record_conflict(bounds[i].get());
                 lbool is_sat = m_s->check_sat(1, bounds.c_ptr() + i);
@@ -284,7 +279,7 @@ namespace opt {
                 progress = true;
             }
         }
-        if (m_cancel) {
+        if (m.canceled()) {
             return l_undef;
         }
         if (!progress) {
@@ -328,7 +323,7 @@ namespace opt {
         for (unsigned i = 0; i < obj_index; ++i) {
             commit_assignment(i);
         }
-        while (is_sat == l_true && !m_cancel) {
+        while (is_sat == l_true && !m.canceled()) {
             is_sat = m_s->check_sat(0, 0); 
             if (is_sat != l_true) break;
             
@@ -357,8 +352,8 @@ namespace opt {
             // on current state.
         }
         
-        if (m_cancel || is_sat == l_undef) {
-            TRACE("opt", tout << "undef: " << m_cancel << " " << is_sat << "\n";);
+        if (m.canceled() || is_sat == l_undef) {
+            TRACE("opt", tout << "undef: " << m.canceled() << " " << is_sat << "\n";);
             return l_undef;
         }
 
diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h
index f4efa25f9..d11b84370 100644
--- a/src/opt/optsmt.h
+++ b/src/opt/optsmt.h
@@ -30,7 +30,6 @@ namespace opt {
     class optsmt {
         ast_manager&     m;
         opt_solver*      m_s;
-        volatile bool    m_cancel;
         vector<inf_eps>  m_lower;
         vector<inf_eps>  m_upper;
         app_ref_vector   m_objs;
@@ -42,7 +41,7 @@ namespace opt {
         sref_vector<model> m_models;
     public:
         optsmt(ast_manager& m): 
-            m(m), m_s(0), m_cancel(false), m_objs(m), m_lower_fmls(m) {}
+            m(m), m_s(0), m_objs(m), m_lower_fmls(m) {}
 
         void setup(opt_solver& solver);
 
@@ -52,8 +51,6 @@ namespace opt {
 
         unsigned add(app* t);
 
-        void set_cancel(bool f);
-
         void updt_params(params_ref& p);
 
         unsigned get_num_objectives() const { return m_objs.size(); }
diff --git a/src/opt/pb_sls.cpp b/src/opt/pb_sls.cpp
index 05bdd5cf8..098af68ee 100644
--- a/src/opt/pb_sls.cpp
+++ b/src/opt/pb_sls.cpp
@@ -60,7 +60,6 @@ namespace smt {
         pb_util          pb;
         unsynch_mpz_manager mgr;
         th_rewriter      m_rewrite;
-        volatile bool    m_cancel;
         vector<clause>   m_clauses;      // clauses to be satisfied        
         expr_ref_vector  m_orig_clauses; // for debugging
         model_ref        m_orig_model;   // for debugging
@@ -86,7 +85,6 @@ namespace smt {
             m(m),
             pb(m),
             m_rewrite(m),
-            m_cancel(false),
             m_orig_clauses(m),
             m_trail(m),
             one(mgr)
@@ -157,7 +155,7 @@ namespace smt {
                 while (m_max_flips > 0) {
                     --m_max_flips;
                     literal lit = flip();
-                    if (m_cancel) {
+                    if (m.canceled()) {
                         return l_undef;
                     }
                     IF_VERBOSE(3, verbose_stream() 
@@ -203,9 +201,6 @@ namespace smt {
         bool get_value(literal l) {
             return l.sign() ^ m_assignment[l.var()];
         }
-        void set_cancel(bool f) {
-            m_cancel = f;
-        }
         void get_model(model_ref& mdl) {
             mdl = alloc(model, m);
             for (unsigned i = 1; i < m_var2decl.size(); ++i) {
@@ -719,9 +714,6 @@ namespace smt {
     lbool pb_sls::operator()() {
         return (*m_imp)();
     }
-    void pb_sls::set_cancel(bool f) {
-        m_imp->set_cancel(f);
-    }
     void pb_sls::collect_statistics(statistics& st) const {
         m_imp->collect_statistics(st);
     }
diff --git a/src/opt/pb_sls.h b/src/opt/pb_sls.h
index 655d04b45..0ed7e30cc 100644
--- a/src/opt/pb_sls.h
+++ b/src/opt/pb_sls.h
@@ -38,7 +38,6 @@ namespace smt {
         bool soft_holds(unsigned index);
         void set_model(model_ref& mdl);
         lbool operator()();
-        void set_cancel(bool f);
         void collect_statistics(::statistics& st) const;
         void get_model(model_ref& mdl);
         void updt_params(params_ref& p);
diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp
index 5f7f76f25..ef4989cee 100644
--- a/src/opt/wmax.cpp
+++ b/src/opt/wmax.cpp
@@ -47,7 +47,7 @@ namespace opt {
             }
             while (l_true == is_sat) {
                 is_sat = s().check_sat(0,0);
-                if (m_cancel) {
+                if (m.canceled()) {
                     is_sat = l_undef;
                 }
                 if (is_sat == l_true) {
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index 34b697a94..846cb6c68 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -898,7 +898,6 @@ namespace qe {
 
         virtual void eliminate(bool is_forall, unsigned num_vars, app* const* vars, expr_ref& fml) = 0;      
 
-        virtual void set_cancel(bool f) = 0;
 
         virtual void updt_params(params_ref const& p) {}
         
@@ -1408,10 +1407,6 @@ namespace qe {
             m_conjs.add_plugin(p);
         }
 
-        void set_cancel(bool f) {
-            m_solver.set_cancel(f);
-            m_rewriter.set_cancel(f);
-        }
 
         void check(unsigned num_vars, app* const* vars, 
                    expr* assumption, expr_ref& fml, bool get_first,
@@ -2032,7 +2027,6 @@ namespace qe {
         expr_ref                m_assumption;
         bool                    m_produce_models;
         ptr_vector<quant_elim_plugin> m_plugins;
-        volatile bool            m_cancel;
         bool                     m_eliminate_variables_as_block;
 
     public:
@@ -2041,7 +2035,6 @@ namespace qe {
             m_fparams(p),
             m_assumption(m),
             m_produce_models(m_fparams.m_model),
-            m_cancel(false),
             m_eliminate_variables_as_block(true)
           {
           }
@@ -2055,16 +2048,9 @@ namespace qe {
                 dealloc(m_plugins[i]);
             }
         }
-        
-        void set_cancel(bool f) {
-            for (unsigned i = 0; i < m_plugins.size(); ++i) {
-                m_plugins[i]->set_cancel(f);
-            }
-            m_cancel = f;
-        }
-        
+                
         void checkpoint() {
-            if (m_cancel)
+            if (m.canceled()) 
                 throw tactic_exception(TACTIC_CANCELED_MSG);
             cooperate("qe");
         }
@@ -2409,11 +2395,6 @@ namespace qe {
         return is_sat != l_undef;
     }
 
-    void expr_quant_elim::set_cancel(bool f) {
-        if (m_qe) {
-            m_qe->set_cancel(f);
-        }
-    }
 
 
 
diff --git a/src/qe/qe.h b/src/qe/qe.h
index 7a3337887..0370ff3a0 100644
--- a/src/qe/qe.h
+++ b/src/qe/qe.h
@@ -313,8 +313,6 @@ namespace qe {
         bool solve_for_vars(unsigned num_vars, app* const* vars, expr* fml, guarded_defs& defs);
 
 
-        void set_cancel(bool f);
-
     private:
         void instantiate_expr(expr_ref_vector& bound, expr_ref& fml);
         void abstract_expr(unsigned sz, expr* const* bound, expr_ref& fml);
@@ -343,7 +341,6 @@ namespace qe {
             return m_quant_elim.first_elim(num_vars, vars, fml, defs);
         }
 
-        void set_cancel(bool f) {} // TBD: replace simplifier by rewriter
 
     };
 
diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp
index f045e406e..c3fed3676 100644
--- a/src/qe/qe_lite.cpp
+++ b/src/qe/qe_lite.cpp
@@ -93,7 +93,6 @@ namespace eq {
         expr_ref_vector  m_subst_map;
         expr_ref_buffer  m_new_args;
         th_rewriter      m_rewriter;
-        volatile bool    m_cancel;
         
         void der_sort_vars(ptr_vector<var> & vars, ptr_vector<expr> & definitions, unsigned_vector & order) {
             order.reset();
@@ -738,7 +737,7 @@ namespace eq {
 
         void checkpoint() {
             cooperate("der");
-            if (m_cancel)
+            if (m.canceled()) 
                 throw tactic_exception(TACTIC_CANCELED_MSG);
         }
 
@@ -752,8 +751,7 @@ namespace eq {
             m_new_exprs(m), 
             m_subst_map(m), 
             m_new_args(m), 
-            m_rewriter(m), 
-            m_cancel(false) {}
+            m_rewriter(m) {}
         
         void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;}
         
@@ -790,10 +788,6 @@ namespace eq {
         
         ast_manager& get_manager() const { return m; }
 
-        void set_cancel(bool f) {
-            m_rewriter.set_cancel(f);
-            m_cancel = f;
-        }
 
     };
 }; // namespace eq
@@ -808,7 +802,6 @@ namespace ar {
         is_variable_proc*        m_is_variable;
         ptr_vector<expr>         m_todo;
         expr_mark                m_visited;
-        volatile bool            m_cancel;
         
         bool is_variable(expr * e) const {
             return (*m_is_variable)(e);
@@ -923,13 +916,13 @@ namespace ar {
 
         void checkpoint() {
             cooperate("der");
-            if (m_cancel)
+            if (m.canceled())
                 throw tactic_exception(TACTIC_CANCELED_MSG);
         }
 
     public:
 
-        der(ast_manager& m): m(m), a(m), m_is_variable(0), m_cancel(false) {}
+        der(ast_manager& m): m(m), a(m), m_is_variable(0) {}
 
         void operator()(expr_ref_vector& fmls) {
             for (unsigned i = 0; i < fmls.size(); ++i) {
@@ -942,10 +935,6 @@ namespace ar {
         void operator()(expr* e) {}
 
         void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;}
-
-        void set_cancel(bool f) {
-            m_cancel = f;
-        }
         
     };
 }; // namespace ar
@@ -1066,7 +1055,6 @@ namespace fm {
         vector<constraints>      m_uppers;
         uint_set                 m_forbidden_set; // variables that cannot be eliminated because occur in non OCC ineq part
         expr_ref_vector          m_new_fmls;
-        volatile bool            m_cancel;
         id_gen                   m_id_gen;
         bool                     m_fm_real_only;
         unsigned                 m_fm_limit;
@@ -1459,7 +1447,6 @@ namespace fm {
             m_var2expr(m),
             m_new_fmls(m),
             m_inconsistent_core(m) {
-            m_cancel = false;
             updt_params();
             m_counter = 0;
             m_inconsistent = false;
@@ -1478,9 +1465,6 @@ namespace fm {
             m_fm_occ         = true;
         }
         
-        void set_cancel(bool f) {
-            m_cancel = f;
-        }
     private:
         
         struct forbidden_proc {
@@ -2222,7 +2206,7 @@ namespace fm {
         
         void checkpoint() {
             cooperate("fm");
-            if (m_cancel)
+            if (m.canceled())
                 throw tactic_exception(TACTIC_CANCELED_MSG);
         }
     public:
@@ -2453,14 +2437,6 @@ public:
         TRACE("qe_lite", for (unsigned i = 0; i < fmls.size(); ++i) tout << mk_pp(fmls[i].get(), m) << "\n";);
     }
 
-    void set_cancel(bool f) {
-        m_der.set_cancel(f);
-        m_array_der.set_cancel(f);
-        m_fm.set_cancel(f);
-        m_elim_star.set_cancel(f);
-        m_rewriter.set_cancel(f);
-    }
-
 };
 
 qe_lite::qe_lite(ast_manager& m) {
@@ -2475,9 +2451,6 @@ void qe_lite::operator()(app_ref_vector& vars, expr_ref& fml) {
     (*m_impl)(vars, fml);
 }
 
-void qe_lite::set_cancel(bool f) {
-    m_impl->set_cancel(f);
-}
 
 void qe_lite::operator()(expr_ref& fml, proof_ref& pr) {
     (*m_impl)(fml, pr);
@@ -2496,21 +2469,14 @@ class qe_lite_tactic : public tactic {
     struct imp {
         ast_manager&             m;
         qe_lite                  m_qe;
-        volatile bool            m_cancel;
 
         imp(ast_manager& m, params_ref const& p): 
             m(m),
-            m_qe(m),
-            m_cancel(false)
+            m_qe(m)
         {}
 
-        void set_cancel(bool f) {
-            m_cancel = f;
-            m_qe.set_cancel(f);
-        }
-
         void checkpoint() {
-            if (m_cancel)
+            if (m.canceled())
                 throw tactic_exception(TACTIC_CANCELED_MSG);
             cooperate("qe-lite");
         }
diff --git a/src/qe/qe_lite.h b/src/qe/qe_lite.h
index aa81780ba..48874f5cf 100644
--- a/src/qe/qe_lite.h
+++ b/src/qe/qe_lite.h
@@ -59,8 +59,6 @@ public:
         \brief full rewriting based light-weight quantifier elimination round.
     */
     void operator()(expr_ref& fml, proof_ref& pr);
-
-    void set_cancel(bool f);
 };
 
 tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p = params_ref());
diff --git a/src/qe/qe_sat_tactic.cpp b/src/qe/qe_sat_tactic.cpp
index 35be20660..d3e145e1b 100644
--- a/src/qe/qe_sat_tactic.cpp
+++ b/src/qe/qe_sat_tactic.cpp
@@ -58,7 +58,6 @@ namespace qe {
 
         ast_manager&            m;
         expr_ref                m_false;
-        volatile bool           m_cancel;
         smt_params              m_fparams;
         params_ref              m_params;
         unsigned                m_extrapolate_strategy_param;
@@ -209,7 +208,6 @@ namespace qe {
         sat_tactic(ast_manager& m, params_ref const& p = params_ref()):
             m(m),
             m_false(m.mk_false(), m),
-            m_cancel(false),
             m_params(p),
             m_extrapolate_strategy_param(0),
             m_projection_mode_param(true),
@@ -233,17 +231,6 @@ namespace qe {
             reset();
         }
 
-        virtual void set_cancel(bool f) { 
-            m_cancel = f; 
-            // not thread-safe when solvers are reset.
-            // TBD: lock - this, reset() and init_Ms.
-            for (unsigned i = 0; i < m_solvers.size(); ++i) {
-                m_solvers[i]->set_cancel(f);
-            }
-            m_solver.set_cancel(f);
-            m_ctx_rewriter.set_cancel(f);
-        }
-
         virtual void operator()(
             goal_ref const& goal,  
             goal_ref_buffer& result, 
@@ -674,7 +661,7 @@ namespace qe {
         }
 
         void checkpoint() {
-            if (m_cancel) {
+            if (m.canceled()) {
                 throw tactic_exception(TACTIC_CANCELED_MSG);
             }
             cooperate("qe-sat");
diff --git a/src/qe/qe_tactic.cpp b/src/qe/qe_tactic.cpp
index 8819d704b..0c3a79f68 100644
--- a/src/qe/qe_tactic.cpp
+++ b/src/qe/qe_tactic.cpp
@@ -25,14 +25,12 @@ class qe_tactic : public tactic {
     struct     imp {
         ast_manager &            m;
         smt_params               m_fparams;
-        volatile bool            m_cancel;
         qe::expr_quant_elim      m_qe;
 
         imp(ast_manager & _m, params_ref const & p):
             m(_m),
             m_qe(m, m_fparams) {
             updt_params(p);
-            m_cancel = false;
         }
 
         void updt_params(params_ref const & p) {
@@ -45,13 +43,8 @@ class qe_tactic : public tactic {
             m_qe.collect_param_descrs(r);
         }
 
-        void set_cancel(bool f) {
-            m_cancel = f;
-            m_qe.set_cancel(f);
-        }
-
         void checkpoint() {
-            if (m_cancel)
+            if (m.canceled()) 
                 throw tactic_exception(TACTIC_CANCELED_MSG);
             cooperate("qe");
         }
@@ -141,11 +134,6 @@ public:
         }
     }
     
-protected:
-    virtual void set_cancel(bool f) {
-        if (m_imp)
-            m_imp->set_cancel(f);
-    }
 };
 
 tactic * mk_qe_tactic(ast_manager & m, params_ref const & p) {
diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp
index fa8da4e12..0c1a1f1fa 100644
--- a/src/shell/opt_frontend.cpp
+++ b/src/shell/opt_frontend.cpp
@@ -307,7 +307,7 @@ static void display_statistics() {
 
 static void on_ctrl_c(int) {
     if (g_opt && g_first_interrupt) {
-        g_opt->set_cancel(true);
+        g_opt->get_manager().limit().cancel();
         g_first_interrupt = false;
     }
     else {
diff --git a/src/util/rlimit.h b/src/util/rlimit.h
index f120fe433..10f58f5d5 100644
--- a/src/util/rlimit.h
+++ b/src/util/rlimit.h
@@ -35,6 +35,8 @@ public:
     bool inc(unsigned offset);
     uint64 count() const; 
 
+
+    bool cancel_flag_set() { return m_cancel; }
     void cancel() { m_cancel = true; }
     void reset_cancel() { m_cancel = false; }
 };