diff --git a/src/api/api_datalog.h b/src/api/api_datalog.h
index 1dc0a9cbd..51dbb72ec 100644
--- a/src/api/api_datalog.h
+++ b/src/api/api_datalog.h
@@ -55,6 +55,7 @@ namespace api {
         std::string get_last_status();
         std::string to_string(unsigned num_queries, expr*const* queries);
         void cancel() { m_context.cancel(); }
+        void reset_cancel() { m_context.reset_cancel(); }
 
         unsigned get_num_levels(func_decl* pred);
         expr_ref get_cover_delta(int level, func_decl* pred);
diff --git a/src/ast/ast.h b/src/ast/ast.h
index e9da41377..6af95e3a7 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1404,6 +1404,8 @@ public:
 
     // propagate cancellation signal to decl_plugins
     void set_cancel(bool f);
+    void cancel() { set_cancel(true); }
+    void reset_cancel() { set_cancel(false); }
 
     bool has_trace_stream() const { return m_trace_stream != 0; }
     std::ostream & trace_stream() { SASSERT(has_trace_stream()); return *m_trace_stream; }
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index e86e56b69..3f32c77d3 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -343,6 +343,13 @@ cmd_context::~cmd_context() {
     m_check_sat_result = 0;
 }
 
+void cmd_context::set_cancel(bool f) {
+    if (m_solver)
+        m_solver->set_cancel(f);
+    if (has_manager())
+        m().set_cancel(f);
+}
+
 void cmd_context::global_params_updated() {
     m_params.updt_params();
     if (m_solver) {
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 63e5e7040..07b0cf456 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -249,6 +249,9 @@ protected:
 public:
     cmd_context(bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null);
     ~cmd_context(); 
+    void set_cancel(bool f);
+    void cancel() { set_cancel(true); }
+    void reset_cancel() { set_cancel(false); }
     context_params  & params() { return m_params; }
     void global_params_updated(); // this method should be invoked when global (and module) params are updated.
     void set_logic(symbol const & s);
diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp
index 90ad6ea9d..804a134e0 100644
--- a/src/math/polynomial/algebraic_numbers.cpp
+++ b/src/math/polynomial/algebraic_numbers.cpp
@@ -2796,72 +2796,58 @@ namespace algebraic_numbers {
     }
 
     void manager::del(numeral & a) {
-        set_cancel(false);
         return m_imp->del(a);
     }
         
     void manager::reset(numeral & a) {
-        set_cancel(false);
         return m_imp->reset(a);
     }
     
     bool manager::is_zero(numeral const & a) {
-        set_cancel(false);
         return m_imp->is_zero(const_cast<numeral&>(a));
     }
 
     bool manager::is_pos(numeral const & a) {
-        set_cancel(false);
         return m_imp->is_pos(const_cast<numeral&>(a));
     }
 
     bool manager::is_neg(numeral const & a) {
-        set_cancel(false);
         return m_imp->is_neg(const_cast<numeral&>(a));
     }
 
     bool manager::is_rational(numeral const & a) {
-        set_cancel(false);
         return m_imp->is_rational(const_cast<numeral&>(a));
     }
 
     bool manager::is_int(numeral const & a) {
-        set_cancel(false);
         return m_imp->is_int(const_cast<numeral&>(a));
     }
 
     unsigned manager::degree(numeral const & a) {
-        set_cancel(false);
         return m_imp->degree(const_cast<numeral&>(a));
     }
 
     void manager::to_rational(numeral const & a, mpq & r) {
-        set_cancel(false);
         return m_imp->to_rational(const_cast<numeral&>(a), r);
     }
 
     void manager::to_rational(numeral const & a, rational & r) {
-        set_cancel(false);
         return m_imp->to_rational(const_cast<numeral&>(a), r);
     }
     
     void manager::swap(numeral & a, numeral & b) {
-        set_cancel(false);
         return m_imp->swap(a, b);
     }
 
     void manager::int_lt(numeral const & a, numeral & b) {
-        set_cancel(false);
         m_imp->int_lt(const_cast<numeral&>(a), b);
     }
 
     void manager::int_gt(numeral const & a, numeral & b) {
-        set_cancel(false);
         m_imp->int_gt(const_cast<numeral&>(a), b);
     }
 
     void manager::select(numeral const & prev, numeral const & curr, numeral & result) {
-        set_cancel(false);
         m_imp->select(const_cast<numeral&>(prev), const_cast<numeral&>(curr), result);
     }
 
@@ -2878,55 +2864,45 @@ namespace algebraic_numbers {
     }
     
     void manager::set(numeral & a, mpq const & n) {
-        set_cancel(false);
         m_imp->set(a, n);
     }
 
     void manager::set(numeral & a, numeral const & n) {
-        set_cancel(false);
         m_imp->set(a, n);
     }
         
     void manager::isolate_roots(polynomial_ref const & p, numeral_vector & roots) {
-        set_cancel(false);
         m_imp->isolate_roots(p, roots);
     }
 
     void manager::isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots) {
-        set_cancel(false);
         m_imp->isolate_roots(p, x2v, roots);
     }
 
     void manager::isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector<int> & signs) {
-        set_cancel(false);
         m_imp->isolate_roots(p, x2v, roots, signs);
     }
 
     void manager::mk_root(polynomial_ref const & p, unsigned i, numeral & r) {
-        set_cancel(false);
         m_imp->mk_root(p, i, r);
     }
 
     void manager::mk_root(sexpr const * p, unsigned i, numeral & r) {
-        set_cancel(false);
         m_imp->mk_root(p, i, r);
     }
         
     void manager::root(numeral const & a, unsigned k, numeral & b) {
-        set_cancel(false);
         m_imp->root(const_cast<numeral&>(a), k, b);
     }
 
     void manager::power(numeral const & a, unsigned k, numeral & b) {
         TRACE("anum_detail", display_root(tout, a); tout << "^" << k << "\n";);
-        set_cancel(false);
         m_imp->power(const_cast<numeral&>(a), k, b);
         TRACE("anum_detail", tout << "^ result: "; display_root(tout, b); tout << "\n";);
     }
 
     void manager::add(numeral const & a, numeral const & b, numeral & c) {
         TRACE("anum_detail", display_root(tout, a); tout << " + "; display_root(tout, b); tout << "\n";);
-        set_cancel(false);
         m_imp->add(const_cast<numeral&>(a), const_cast<numeral&>(b), c);
         TRACE("anum_detail", tout << "+ result: "; display_root(tout, c); tout << "\n";);
     }
@@ -2939,45 +2915,37 @@ namespace algebraic_numbers {
 
     void manager::sub(numeral const & a, numeral const & b, numeral & c) {
         TRACE("anum_detail", display_root(tout, a); tout << " - "; display_root(tout, b); tout << "\n";);
-        set_cancel(false);
         m_imp->sub(const_cast<numeral&>(a), const_cast<numeral&>(b), c);
         TRACE("anum_detail", tout << "- result: "; display_root(tout, c); tout << "\n";);
     }
 
     void manager::mul(numeral const & a, numeral const & b, numeral & c) {
         TRACE("anum_detail", display_root(tout, a); tout << " * "; display_root(tout, b); tout << "\n";);
-        set_cancel(false);
         m_imp->mul(const_cast<numeral&>(a), const_cast<numeral&>(b), c);
         TRACE("anum_detail", tout << "* result: "; display_root(tout, c); tout << "\n";);
     }
 
     void manager::div(numeral const & a, numeral const & b, numeral & c) {
-        set_cancel(false);
         m_imp->div(const_cast<numeral&>(a), const_cast<numeral&>(b), c);
     }
 
     void manager::neg(numeral & a) {
-        set_cancel(false);
         m_imp->neg(a);
     }
 
     void manager::inv(numeral & a) {
-        set_cancel(false);
         m_imp->inv(a);
     }
 
     int manager::compare(numeral const & a, numeral const & b) {
-        set_cancel(false);
         return m_imp->compare(const_cast<numeral&>(a), const_cast<numeral&>(b));
     }
 
     bool manager::eq(numeral const & a, numeral const & b) {
-        set_cancel(false);
         return m_imp->eq(const_cast<numeral&>(a), const_cast<numeral&>(b));
     }
     
     bool manager::eq(numeral const & a, mpq const & b) {
-        set_cancel(false);
         return m_imp->eq(const_cast<numeral&>(a), b);
     }
 
@@ -2988,12 +2956,10 @@ namespace algebraic_numbers {
     }
 
     bool manager::lt(numeral const & a, numeral const & b) {
-        set_cancel(false);
         return m_imp->lt(const_cast<numeral&>(a), const_cast<numeral&>(b));
     }
     
     bool manager::lt(numeral const & a, mpq const & b) {
-        set_cancel(false);
         return m_imp->lt(const_cast<numeral&>(a), b);
     }
 
@@ -3004,7 +2970,6 @@ namespace algebraic_numbers {
     }
 
     bool manager::gt(numeral const & a, mpq const & b) {
-        set_cancel(false);
         return m_imp->gt(const_cast<numeral&>(a), b);
     }
 
@@ -3073,38 +3038,31 @@ namespace algebraic_numbers {
     }
 
     int manager::eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v) {
-        set_cancel(false);
         SASSERT(&(x2v.m()) == this);
         return m_imp->eval_sign_at(p, x2v);
     }
 
     void manager::display_interval(std::ostream & out, numeral const & a) const {
-        const_cast<manager*>(this)->set_cancel(false);
         m_imp->display_interval(out, a);
     }
 
     void manager::display_decimal(std::ostream & out, numeral const & a, unsigned precision) const {
-        const_cast<manager*>(this)->set_cancel(false);
         m_imp->display_decimal(out, a, precision);
     }
 
     void manager::display_root(std::ostream & out, numeral const & a) const {
-        const_cast<manager*>(this)->set_cancel(false);
         m_imp->display_root(out, a);
     }
 
     void manager::display_mathematica(std::ostream & out, numeral const & a) const {
-        const_cast<manager*>(this)->set_cancel(false);
         m_imp->display_mathematica(out, a);
     }
 
     void manager::display_root_smt2(std::ostream & out, numeral const & a) const {
-        const_cast<manager*>(this)->set_cancel(false);
         m_imp->display_root_smt2(out, a);
     }
 
     void manager::reset_statistics() {
-        set_cancel(false);
         m_imp->reset_statistics();
     }
         
diff --git a/src/math/polynomial/algebraic_numbers.h b/src/math/polynomial/algebraic_numbers.h
index a4669eae6..d11237b86 100644
--- a/src/math/polynomial/algebraic_numbers.h
+++ b/src/math/polynomial/algebraic_numbers.h
@@ -64,8 +64,8 @@ namespace algebraic_numbers {
         static void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
 
         void set_cancel(bool f);
-        
         void cancel() { set_cancel(true); }
+        void reset_cancel() { set_cancel(false); }
 
         void updt_params(params_ref const & p);
 
diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp
index 4e14c5661..f5d96e740 100644
--- a/src/math/polynomial/polynomial.cpp
+++ b/src/math/polynomial/polynomial.cpp
@@ -2368,7 +2368,6 @@ namespace polynomial {
 
         void checkpoint() {
             if (m_cancel) {
-                set_cancel(false);
                 throw polynomial_exception("canceled");
             }
             cooperate("polynomial");
diff --git a/src/math/polynomial/polynomial.h b/src/math/polynomial/polynomial.h
index d17d2ac5a..e52dd4fee 100644
--- a/src/math/polynomial/polynomial.h
+++ b/src/math/polynomial/polynomial.h
@@ -220,6 +220,7 @@ namespace polynomial {
 
         void set_cancel(bool f);
         void cancel() { set_cancel(true); }
+        void reset_cancel() { set_cancel(false); }
 
         /**
            \brief Abstract event handler.
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index beed0061e..dc4c20aa8 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -244,10 +244,10 @@ unsigned model_evaluator::get_num_steps() const {
     return m_imp->get_num_steps();
 }
 
-void model_evaluator::cancel() {
+void model_evaluator::set_cancel(bool f) {
     #pragma omp critical (model_evaluator)
     {
-        m_imp->cancel();
+        m_imp->set_cancel(f);
     }
 }
 
diff --git a/src/model/model_evaluator.h b/src/model/model_evaluator.h
index aad06739b..1a7469c6c 100644
--- a/src/model/model_evaluator.h
+++ b/src/model/model_evaluator.h
@@ -41,7 +41,9 @@ public:
 
     void operator()(expr * t, expr_ref & r);
 
-    void cancel();
+    void set_cancel(bool f);
+    void cancel() { set_cancel(true); }
+    void reset_cancel() { set_cancel(false); }
     void cleanup(params_ref const & p = params_ref());
     void reset(params_ref const & p = params_ref());
     
diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h
index f84050e68..d3309beb5 100644
--- a/src/muz_qe/dl_context.h
+++ b/src/muz_qe/dl_context.h
@@ -349,6 +349,7 @@ namespace datalog {
         void cancel();
 
         void cleanup();
+        void reset_cancel() { cleanup(); }
 
         /**
            \brief check if query 'q' is satisfied under asserted rules and background.
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index c99c362bd..0698f4eaf 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -390,6 +390,7 @@ namespace smt2 {
         void check_float(char const * msg) { if (!curr_is_float()) throw parser_exception(msg); }
 
         void error(unsigned line, unsigned pos, char const * msg) {
+            m_ctx.reset_cancel();
             if (use_vs_format()) {
                 m_ctx.diagnostic_stream() << "Z3(" << line << ", " << pos << "): ERROR: " << msg;
                 if (msg[strlen(msg)-1] != '\n')
diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp
index 779c68625..8ecd079bf 100644
--- a/src/smt/smt_kernel.cpp
+++ b/src/smt/smt_kernel.cpp
@@ -253,12 +253,10 @@ namespace smt {
     }
 
     lbool kernel::setup_and_check() {
-        set_cancel(false);
         return m_imp->setup_and_check();
     }
 
     lbool kernel::check(unsigned num_assumptions, expr * const * assumptions) {
-        set_cancel(false);
         lbool r = m_imp->check(num_assumptions, assumptions);
         TRACE("smt_kernel", tout << "check result: " << r << "\n";);
         return r;
diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index 4bf9e48f4..198872cf5 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -175,7 +175,6 @@ tactic * mk_fail_if_undecided_tactic() {
 
 void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) {
     t.reset_statistics();
-    t.reset_cancel();
     try {
         t(in, result, mc, pc, core);
         t.cleanup();
diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
index 785a9d82e..ca66b7a14 100644
--- a/src/tactic/tactical.cpp
+++ b/src/tactic/tactical.cpp
@@ -116,7 +116,6 @@ protected:
         m_t2->set_cancel(f);
     }
 
-
     template<typename T>
     tactic * translate_core(ast_manager & m) { 
         tactic * new_t1 = m_t1->translate(m);
diff --git a/src/util/cancel_eh.h b/src/util/cancel_eh.h
index 74c5040a2..0401e6f03 100644
--- a/src/util/cancel_eh.h
+++ b/src/util/cancel_eh.h
@@ -29,6 +29,7 @@ class cancel_eh : public event_handler {
     T & m_obj;
 public:
     cancel_eh(T & o):m_obj(o) {}
+    ~cancel_eh() { m_obj.reset_cancel(); }
     virtual void operator()() { 
         m_obj.cancel(); 
     }