diff --git a/examples/python/CMakeLists.txt b/examples/python/CMakeLists.txt
index dc4b62279..deb51d2ab 100644
--- a/examples/python/CMakeLists.txt
+++ b/examples/python/CMakeLists.txt
@@ -13,17 +13,18 @@ set(z3py_bindings_build_dest "${PROJECT_BINARY_DIR}/python")
 
 set(build_z3_python_examples_target_depends "")
 foreach (example_file ${python_example_files})
-  add_custom_command(OUTPUT "${z3py_bindings_build_dest}/${example_file}"
+  get_filename_component(example_file_name "${example_file}" NAME)
+  add_custom_command(OUTPUT "${z3py_bindings_build_dest}/${example_file_name}"
     COMMAND "${CMAKE_COMMAND}" "-E" "copy"
       "${CMAKE_CURRENT_SOURCE_DIR}/${example_file}"
       # We flatten the hierarchy so that all python files have
       # the `z3` directory in their directory so that their import
       # statements "just work".
-      "${z3py_bindings_build_dest}/"
+      "${z3py_bindings_build_dest}/${example_file_name}"
     DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/${example_file}"
-    COMMENT "Copying \"${example_file}\" to ${z3py_bindings_build_dest}/${example_file}"
+    COMMENT "Copying \"${example_file}\" to ${z3py_bindings_build_dest}/${example_file_name}"
   )
-  list(APPEND build_z3_python_examples_target_depends "${z3py_bindings_build_dest}/${example_file}")
+  list(APPEND build_z3_python_examples_target_depends "${z3py_bindings_build_dest}/${example_file_name}")
 endforeach()
 
 add_custom_target(build_z3_python_examples
diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp
index 1a1e31f0a..7323cad8e 100644
--- a/examples/tptp/tptp5.cpp
+++ b/examples/tptp/tptp5.cpp
@@ -1338,9 +1338,10 @@ public:
         }
         else if (e.is_quantifier()) {
             bool is_forall = Z3_is_quantifier_forall(ctx, e);
+            bool is_lambda = Z3_is_lambda(ctx, e);
             unsigned nb = Z3_get_quantifier_num_bound(ctx, e);
 
-            out << (is_forall?"!":"?") << "[";
+            out << (is_lambda?"^":(is_forall?"!":"?")) << "[";
             for (unsigned i = 0; i < nb; ++i) {
                 Z3_symbol n = Z3_get_quantifier_bound_name(ctx, e, i);
                 names.push_back(upper_case_var(z3::symbol(ctx, n)));
@@ -1680,6 +1681,9 @@ public:
             case Z3_OP_PR_HYPER_RESOLVE:
                 display_inference(out, "hyper_resolve", "thm", p); 
                 break;
+            case Z3_OP_PR_BIND:
+                display_inference(out, "bind", "th", p);
+                break;
             default:
                 out << "TBD: " << m_node_number << "\n" << p << "\n";
                 throw failure_ex("rule not handled");
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 8bd125dd7..3e6646299 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -3064,13 +3064,7 @@ bool ast_manager::is_quant_inst(expr const* e, expr*& not_q_or_i, ptr_vector<exp
 }
 
 bool ast_manager::is_rewrite(expr const* e, expr*& r1, expr*& r2) const {
-    if (is_rewrite(e)) {
-        VERIFY (is_eq(to_app(e)->get_arg(0), r1, r2));
-        return true;
-    }
-    else {
-        return false;
-    }
+    return is_rewrite(e) && is_eq(to_app(e)->get_arg(0), r1, r2);
 }
 
 proof * ast_manager::mk_def_axiom(expr * ax) {
@@ -3081,9 +3075,7 @@ proof * ast_manager::mk_def_axiom(expr * ax) {
 
 proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * proofs) {
     SASSERT(num_proofs >= 2);
-    for (unsigned i = 0; i < num_proofs; i++) {
-        SASSERT(has_fact(proofs[i]));
-    }
+    DEBUG_CODE(for (unsigned i = 0; i < num_proofs; i++) SASSERT(has_fact(proofs[i])););
     ptr_buffer<expr> args;
     expr * fact;
     expr * f1 = get_fact(proofs[0]);
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index bd5f4ff4a..b026b6a47 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -802,6 +802,7 @@ void rewriter_tpl<Config>::operator()(expr * t, expr_ref & result, proof_ref & r
     if (!frame_stack().empty() || m_cache != m_cache_stack[0]) {
         frame_stack().reset();
         result_stack().reset();
+        result_pr_stack().reset();
         m_scopes.reset();
         reset_cache();
     }
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index e7a2f6795..0d36e976b 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -473,7 +473,6 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
     m_status(UNKNOWN),
     m_numeral_as_real(false),
     m_ignore_check(false),
-    m_processing_pareto(false),
     m_exit_on_error(false),
     m_manager(m),
     m_own_manager(m == nullptr),
@@ -1261,7 +1260,6 @@ void cmd_context::insert_aux_pdecl(pdecl * p) {
 }
 
 void cmd_context::reset(bool finalize) {    
-    m_processing_pareto = false;
     m_logic = symbol::null;
     m_check_sat_result = nullptr;
     m_numeral_as_real = false;
@@ -1307,7 +1305,6 @@ void cmd_context::reset(bool finalize) {
 
 void cmd_context::assert_expr(expr * t) {
     scoped_rlimit no_limit(m().limit(), 0);
-    m_processing_pareto = false;
     if (!m_check_logic(t))
         throw cmd_exception(m_check_logic.get_last_error());
     m_check_sat_result = nullptr;
@@ -1320,7 +1317,6 @@ void cmd_context::assert_expr(expr * t) {
 }
 
 void cmd_context::assert_expr(symbol const & name, expr * t) {
-    m_processing_pareto = false;
     if (!m_check_logic(t))
         throw cmd_exception(m_check_logic.get_last_error());
     if (!produce_unsat_cores() || name == symbol::null) {
@@ -1440,7 +1436,6 @@ static void restore(ast_manager & m, ptr_vector<expr> & c, unsigned old_sz) {
 }
 
 void cmd_context::restore_assertions(unsigned old_sz) {
-    m_processing_pareto = false;
     if (!has_manager()) {
         // restore_assertions invokes m(), so if cmd_context does not have a manager, it will try to create one.
         SASSERT(old_sz == m_assertions.size());
@@ -1460,7 +1455,6 @@ void cmd_context::restore_assertions(unsigned old_sz) {
 
 void cmd_context::pop(unsigned n) {
     m_check_sat_result = nullptr;
-    m_processing_pareto = false;
     if (n == 0)
         return;
     unsigned lvl     = m_scopes.size();
@@ -1507,7 +1501,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
         scoped_rlimit _rlimit(m().limit(), rlimit);
         expr_ref_vector asms(m());
         asms.append(num_assumptions, assumptions);
-        if (!m_processing_pareto) {
+        if (!get_opt()->is_pareto()) {
             expr_ref_vector assertions(m());
             unsigned sz = m_assertions.size();
             for (unsigned i = 0; i < sz; ++i) {
@@ -1523,9 +1517,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
         }
         try {
             r = get_opt()->optimize(asms);
-            if (r == l_true && get_opt()->is_pareto()) {
-                m_processing_pareto = true;
-            }
         }
         catch (z3_error & ex) {
             throw ex;
@@ -1533,9 +1524,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
         catch (z3_exception & ex) {
             throw cmd_exception(ex.msg());
         }
-        if (m_processing_pareto && r != l_true) {
-            m_processing_pareto = false;
-        }
         get_opt()->set_status(r);
     }
     else if (m_solver) {
@@ -1575,10 +1563,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
         validate_model();
     }
     validate_check_sat_result(r);
-    if (was_opt && r != l_false && !m_processing_pareto) {
-        // get_opt()->display_assignment(regular_stream());
-    }
-
     model_ref md;
     if (r == l_true && m_params.m_dump_models && is_model_available(md)) {
         display_model(md);
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 0f471179a..47818c273 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -192,7 +192,6 @@ protected:
     status                       m_status;
     bool                         m_numeral_as_real;
     bool                         m_ignore_check;      // used by the API to disable check-sat() commands when parsing SMT 2.0 files.
-    bool                         m_processing_pareto; // used when re-entering check-sat for pareto front.
     bool                         m_exit_on_error;
 
     static std::ostringstream    g_error_stream;
diff --git a/src/math/grobner/pdd_solver.cpp b/src/math/grobner/pdd_solver.cpp
index 337ce6b7c..78978ce4c 100644
--- a/src/math/grobner/pdd_solver.cpp
+++ b/src/math/grobner/pdd_solver.cpp
@@ -362,7 +362,7 @@ namespace dd {
     }   
     
     bool solver::canceled() {
-        return m_limit.get_cancel_flag();
+        return m_limit.is_canceled();
     }
     
     bool solver::done() {
diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index 97c8a0b3f..f741a04f7 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -78,7 +78,7 @@ struct solver::imp {
             r = m_nlsat->check(); 
         }
         catch (z3_exception&) {
-            if (m_limit.get_cancel_flag()) {
+            if (m_limit.is_canceled()) {
                 r = l_undef;
             }
             else {
diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 707167e17..54cc55bd7 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -21,15 +21,15 @@ Revision History:
 #include<limits>
 #include "ast/arith_decl_plugin.h"
 #include "ast/bv_decl_plugin.h"
-#include "muz/base/dl_context.h"
 #include "ast/for_each_expr.h"
 #include "ast/ast_smt_pp.h"
 #include "ast/ast_smt2_pp.h"
 #include "ast/datatype_decl_plugin.h"
 #include "ast/scoped_proof.h"
-#include "muz/base/fp_params.hpp"
 #include "ast/ast_pp_util.h"
-
+#include "ast/ast_util.h"
+#include "muz/base/dl_context.h"
+#include "muz/base/fp_params.hpp"
 
 namespace datalog {
 
@@ -354,10 +354,9 @@ namespace datalog {
 
     void context::restrict_predicates(func_decl_set const& preds) {
         m_preds.reset();
-        func_decl_set::iterator it = preds.begin(), end = preds.end();
-        for (; it != end; ++it) {
-            TRACE("dl", tout << mk_pp(*it, m) << "\n";);
-            m_preds.insert(*it);
+        for (func_decl* p : preds) {
+            TRACE("dl", tout << mk_pp(p, m) << "\n";);
+            m_preds.insert(p);
         }
     }
 
@@ -742,13 +741,7 @@ namespace datalog {
     }
 
     expr_ref context::get_background_assertion() {
-        expr_ref result(m);
-        switch (m_background.size()) {
-        case 0: result = m.mk_true(); break;
-        case 1: result = m_background[0].get(); break;
-        default: result = m.mk_and(m_background.size(), m_background.c_ptr()); break;
-        }
-        return result;
+        return mk_and(m_background);
     }
 
     void context::assert_expr(expr* e) {
@@ -967,18 +960,17 @@ namespace datalog {
         rule_ref_vector rv (rm);
         get_rules_along_trace (rv);
         expr_ref fml (m);
-        rule_ref_vector::iterator it = rv.begin (), end = rv.end ();
-        for (; it != end; it++) {
-            m_rule_manager.to_formula (**it, fml);
+        for (auto* r : rv) {
+            m_rule_manager.to_formula (*r, fml);
             rules.push_back (fml);
             // The concatenated names are already stored last-first, so do not need to be reversed here
-            const symbol& rule_name = (*it)->name();
+            const symbol& rule_name = r->name();
             names.push_back (rule_name);
 
             TRACE ("dl",
                    if (rule_name == symbol::null) {
                        tout << "Encountered unnamed rule: ";
-                       (*it)->display(*this, tout);
+                       r->display(*this, tout);
                        tout << "\n";
                    });
         }
@@ -1070,9 +1062,7 @@ namespace datalog {
                 --i;
             }
         }
-        rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end();
-        for (; it != end; ++it) {
-            rule* r = *it;
+        for (rule* r : m_rule_set) {
             rm.to_formula(*r, fml);
             func_decl* h = r->get_decl();
             if (m_rule_set.is_output_predicate(h)) {
diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp
index 68974fb56..09d712dff 100644
--- a/src/muz/spacer/spacer_util.cpp
+++ b/src/muz/spacer/spacer_util.cpp
@@ -383,7 +383,7 @@ namespace {
             expr_ref res(m), v(m);
             v = m_model(e);
             // the literal must have a value
-            SASSERT(m.is_true(v) || m.is_false(v));
+            SASSERT(m.limit().is_canceled() || m.is_true(v) || m.is_false(v));
 
             res = m.is_false(v) ? m.mk_not(e) : e;
 
diff --git a/src/muz/transforms/dl_mk_subsumption_checker.cpp b/src/muz/transforms/dl_mk_subsumption_checker.cpp
index d75ae0b46..447976cae 100644
--- a/src/muz/transforms/dl_mk_subsumption_checker.cpp
+++ b/src/muz/transforms/dl_mk_subsumption_checker.cpp
@@ -350,7 +350,6 @@ namespace datalog {
             return nullptr;
         }
 
-
         //During the construction of the new set we may discover new total relations
         //(by quantifier elimination on the uninterpreted tails).
         SASSERT(m_new_total_relation_discovery_during_transformation || !m_have_new_total_rule);
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 65c2a8795..d36d7b96b 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -1759,7 +1759,7 @@ namespace nlsat {
             if (assigned_value(antecedent) == l_undef) {
                 checkpoint();
                 // antecedent must be false in the current arith interpretation
-                SASSERT(value(antecedent) == l_false || m_rlimit.get_cancel_flag());
+                SASSERT(value(antecedent) == l_false || m_rlimit.is_canceled());
                 if (!is_marked(b)) {
                     SASSERT(is_arith_atom(b) && max_var(b) < m_xk); // must be in a previous stage
                     TRACE("nlsat_resolve", tout << "literal is unassigned, but it is false in arithmetic interpretation, adding it to lemma\n";); 
@@ -1837,10 +1837,10 @@ namespace nlsat {
                 for (unsigned i = 0; i < sz; i++) {
                     literal l = m_lazy_clause[i];
                     if (l.var() != b) {
-                        SASSERT(value(l) == l_false || m_rlimit.get_cancel_flag());
+                        SASSERT(value(l) == l_false || m_rlimit.is_canceled());
                     }
                     else {
-                        SASSERT(value(l) == l_true || m_rlimit.get_cancel_flag());
+                        SASSERT(value(l) == l_true || m_rlimit.is_canceled());
                         SASSERT(!l.sign() || m_bvalues[b] == l_false);
                         SASSERT(l.sign()  || m_bvalues[b] == l_true);
                     }
diff --git a/src/opt/maxlex.cpp b/src/opt/maxlex.cpp
index 4acd875ca..9b73df8ca 100644
--- a/src/opt/maxlex.cpp
+++ b/src/opt/maxlex.cpp
@@ -161,7 +161,7 @@ namespace opt {
                 case l_true:
                     if (!update_assignment())
                         return l_undef;
-                    SASSERT(soft.value == l_true || m.limit().get_cancel_flag());
+                    SASSERT(soft.value == l_true || m.limit().is_canceled());
                     break;
                 case l_false:
                     soft.set_value(l_false);
diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 15d7ee825..e2bb32b89 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -216,7 +216,7 @@ public:
                        tout << *m_model << "assumptions: ";
                        for (expr* a : m_asms) tout << mk_pp(a, m) << " -> " << (*m_model)(a) << " ";
                        tout << "\n";);
-                SASSERT(m_model->is_true(m_asms));
+                SASSERT(m_model->is_true(m_asms) || m.limit().is_canceled());
                 found_optimum();
                 return l_true;
             case l_false:
diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp
index 1fa65a1b4..4d46929a9 100644
--- a/src/qe/qe_arith.cpp
+++ b/src/qe/qe_arith.cpp
@@ -65,7 +65,7 @@ namespace qe {
             DEBUG_CODE(expr_ref val(m); 
                        eval(lit, val); 
                        CTRACE("qe", !m.is_true(val), tout << mk_pp(lit, m) << " := " << val << "\n";);
-                       SASSERT(m.limit().get_cancel_flag() || !m.is_false(val)););
+                       SASSERT(m.limit().is_canceled() || !m.is_false(val)););
 
             if (!m.inc()) 
                 return false;
@@ -345,6 +345,9 @@ namespace qe {
                 if (is_arith(v) && !tids.contains(v)) {
                     rational r;
                     expr_ref val = eval(v);
+                    if (!m.inc())
+                        return vector<def>();
+
                     VERIFY(a.is_numeral(val, r));
                     TRACE("qe", tout << mk_pp(v, m) << " " << val << "\n";);
                     tids.insert(v, mbo.add_var(r, a.is_int(v)));
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 8f78a9106..4f903e815 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -647,8 +647,10 @@ namespace qe {
                 switch (res) {
                 case l_true:
                     s.get_model(m_model);
+                    if (!m_model)
+                        return l_undef;
                     SASSERT(validate_defs("check_sat"));
-                    SASSERT(validate_assumptions(*m_model.get(), asms));
+                    SASSERT(!m_model.get() || validate_assumptions(*m_model.get(), asms));
                     SASSERT(validate_model(asms));
                     TRACE("qe", s.display(tout); display(tout << "\n", *m_model.get()); display(tout, asms); );
                     if (m_level == 0) {
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 6273e675d..9730334b9 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -963,6 +963,8 @@ private:
         for (expr * f : m_fmls) {
             expr_ref tmp(m);
             eval(f, tmp);
+            if (m.limit().is_canceled())
+                return;
             CTRACE("sat", !m.is_true(tmp),
                    tout << "Evaluation failed: " << mk_pp(f, m) << " to " << tmp << "\n";
                    model_smt2_pp(tout, m, *(mdl.get()), 0););
diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index 576a85a87..8da9c8fad 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -182,13 +182,13 @@ void asserted_formulas::get_assertions(ptr_vector<expr> & result) const {
 void asserted_formulas::push_scope() {
     reduce();
     commit();
-    SASSERT(inconsistent() || m_qhead == m_formulas.size() || m.limit().get_cancel_flag());
+    SASSERT(inconsistent() || m_qhead == m_formulas.size() || m.limit().is_canceled());
     TRACE("asserted_formulas_scopes", tout << "before push: " << m_scopes.size() << "\n";);
     m_scoped_substitution.push();
     m_scopes.push_back(scope());
     scope & s = m_scopes.back();
     s.m_formulas_lim = m_formulas.size();
-    SASSERT(inconsistent() || s.m_formulas_lim == m_qhead || m.limit().get_cancel_flag());
+    SASSERT(inconsistent() || s.m_formulas_lim == m_qhead || m.limit().is_canceled());
     s.m_inconsistent_old = m_inconsistent;
     m_defined_names.push();
     m_elim_term_ite.push();
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 801d0a3e3..5a620c232 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -554,7 +554,7 @@ namespace smt {
         catch (...) {
             // Restore trail size since procedure was interrupted in the middle.
             // If the add_eq_trail remains on the trail stack, then Z3 may crash when the destructor is invoked.
-            TRACE("add_eq", tout << "add_eq interrupted. This is unsafe " << m.limit().get_cancel_flag() << "\n";);
+            TRACE("add_eq", tout << "add_eq interrupted. This is unsafe " << m.limit().is_canceled() << "\n";);
             m_trail_stack.shrink(old_trail_size);
             throw;
         }
@@ -2845,12 +2845,13 @@ namespace smt {
         }
     }
 
-    void context::push() {
-        TRACE("unit_subsumption_bug", display(tout << "context::push()\n"););        
+    void context::push() {       
         pop_to_base_lvl();
         setup_context(false);
         bool was_consistent = !inconsistent();
         internalize_assertions(); // internalize assertions before invoking m_asserted_formulas.push_scope
+        if (!m.inc())
+            throw default_exception("push canceled");
         scoped_suspend_rlimit _suspend_cancel(m.limit());
         propagate();
         if (was_consistent && inconsistent() && !m_asserted_formulas.inconsistent()) {
@@ -3084,6 +3085,7 @@ namespace smt {
         TRACE("internalize_assertions", tout << "internalize_assertions()...\n";);
         timeit tt(get_verbosity_level() >= 100, "smt.preprocessing");
         reduce_assertions();
+        if (get_cancel_flag()) return;
         if (!m_asserted_formulas.inconsistent()) {
             unsigned sz    = m_asserted_formulas.get_num_formulas();
             unsigned qhead = m_asserted_formulas.get_qhead();
@@ -4483,9 +4485,9 @@ namespace smt {
         return false;
     }
 
-    void context::get_model(model_ref & m) {
-        if (inconsistent())
-            m = nullptr;       
+    void context::get_model(model_ref & mdl) {
+        if (inconsistent() || !m.inc())
+            mdl = nullptr;       
         else {
             mk_proto_model();
             if (!m_model && m_proto_model) {
@@ -4497,7 +4499,7 @@ namespace smt {
                     // no op
                 }                
             }
-            m = m_model.get();
+            mdl = m_model.get();
         }
     }
 
diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp
index 92a08df14..0fc8d5fff 100644
--- a/src/smt/smt_context_inv.cpp
+++ b/src/smt/smt_context_inv.cpp
@@ -264,7 +264,7 @@ namespace smt {
     bool context::check_th_diseq_propagation() const {
         TRACE("check_th_diseq_propagation", tout << "m_propagated_th_diseqs.size() " << m_propagated_th_diseqs.size() << "\n";);
         int num = get_num_bool_vars();
-        if (inconsistent() || get_manager().limit().get_cancel_flag()) { 
+        if (inconsistent() || get_manager().limit().is_canceled()) {
             return true;
         }
         for (bool_var v = 0; v < num; v++) {
diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp
index 1caeede92..c8ff45488 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic.cpp
@@ -231,6 +231,8 @@ public:
                     mc = concat(fmc.get(), mc.get());
                     in->add(mc.get());
                 }
+                if (m_ctx->canceled()) 
+                    throw tactic_exception(Z3_CANCELED_MSG);                
                 return;
             }
             case l_false: {
diff --git a/src/smt/theory_arith_inv.h b/src/smt/theory_arith_inv.h
index e569d221a..9517f558f 100644
--- a/src/smt/theory_arith_inv.h
+++ b/src/smt/theory_arith_inv.h
@@ -191,7 +191,7 @@ namespace smt {
 
     template<typename Ext>
     bool theory_arith<Ext>::satisfy_bounds() const {
-        if (get_manager().limit().get_cancel_flag())
+        if (get_manager().limit().is_canceled())
             return true;
         int num = get_num_vars();
         for (theory_var v = 0; v < num; v++) {
@@ -217,7 +217,7 @@ namespace smt {
 
     template<typename Ext>
     bool theory_arith<Ext>::valid_assignment() const {
-        if (get_manager().limit().get_cancel_flag())
+        if (get_manager().limit().is_canceled())
             return true;
         if (valid_row_assignment() &&
             satisfy_bounds() &&
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 853961912..e6c8b25e7 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -1811,7 +1811,7 @@ namespace smt {
     }
 
     bool theory_bv::check_invariant() {
-        if (m.limit().get_cancel_flag())
+        if (m.limit().is_canceled())
             return true;
         if (ctx.inconsistent())
             return true;
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 5a966a324..a545d7215 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3441,7 +3441,7 @@ public:
         else {
             rational r = get_value(v);
             TRACE("arith", tout << mk_pp(o, m) << " v" << v << " := " << r << "\n";);
-            SASSERT("integer variables should have integer values: " && (!a.is_int(o) || r.is_int() || m.limit().get_cancel_flag()));
+            SASSERT("integer variables should have integer values: " && (!a.is_int(o) || r.is_int() || m.limit().is_canceled()));
             if (a.is_int(o) && !r.is_int()) r = floor(r);
             return alloc(expr_wrapper_proc, m_factory->mk_value(r,  m.get_sort(o)));
         }
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index a537f2678..dac2f3070 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -507,8 +507,6 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero) {
         m_fixed.contains(e)) {
         return false;
     }
-
-
     
     m_trail_stack.push(insert_obj_trail<theory_seq, expr>(m_fixed, e));
     m_fixed.insert(e);
@@ -520,8 +518,7 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero) {
     }
     else if (!is_zero) {
         unsigned _lo = lo.get_unsigned();
-        expr_ref_vector elems(m);
-        
+        expr_ref_vector elems(m);        
         for (unsigned j = 0; j < _lo; ++j) {
             m_sk.decompose(seq, head, tail);
             elems.push_back(head);
@@ -2304,7 +2301,7 @@ void theory_seq::validate_fmls(enode_pair_vector const& eqs, literal_vector cons
         k.assert_expr(f);
     }
     lbool r = k.check();
-    if (r != l_false && !m.limit().get_cancel_flag()) {
+    if (r != l_false && !m.limit().is_canceled()) {
         model_ref mdl;
         k.get_model(mdl);
         IF_VERBOSE(0, 
diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp
index 80b561d08..bfb5da408 100644
--- a/src/tactic/core/reduce_invertible_tactic.cpp
+++ b/src/tactic/core/reduce_invertible_tactic.cpp
@@ -204,15 +204,15 @@ private:
             return true;
 
         case OP_BMUL:
+            model = rational::one();
+            return true;
+
         case OP_BSDIV:
         case OP_BSDIV0:
         case OP_BSDIV_I:
         case OP_BUDIV:
         case OP_BUDIV0:
         case OP_BUDIV_I:
-            model = rational::one();
-            return true;
-
         default:
             return false;
         }
diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index dd248bcca..66f58f71e 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -190,6 +190,10 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, p
             (*mc)(labels);
             model_converter2model(m, mc.get(), md);
         }
+        if (!m.inc()) {
+            reason_unknown = "canceled";
+            return l_undef;
+        }
         if (!md) {
             // create empty model.
             md = alloc(model, m);
diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp
index a38f0ebf2..c88505f83 100644
--- a/src/util/rlimit.cpp
+++ b/src/util/rlimit.cpp
@@ -44,14 +44,12 @@ uint64_t reslimit::count() const {
 
 bool reslimit::inc() {
     ++m_count;
-    bool r = (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend;
-    return r;
+    return not_canceled();
 }
 
 bool reslimit::inc(unsigned offset) {
     m_count += offset;
-    bool r = (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend;
-    return r;
+    return not_canceled();
 }
 
 void reslimit::push(unsigned delta_limit) {
diff --git a/src/util/rlimit.h b/src/util/rlimit.h
index 6502c0426..cd3599f6f 100644
--- a/src/util/rlimit.h
+++ b/src/util/rlimit.h
@@ -50,7 +50,8 @@ public:
     uint64_t count() const;
 
     bool suspended() const { return m_suspend;  }
-    bool get_cancel_flag() const { return m_cancel > 0 && !m_suspend; }
+    inline bool not_canceled() const { return (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend; }
+    inline bool is_canceled() const { return !not_canceled(); }
     char const* get_cancel_msg() const;
     void cancel();
     void reset_cancel();