diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp
index 690264623..b8cd7ca4e 100644
--- a/src/api/api_opt.cpp
+++ b/src/api/api_opt.cpp
@@ -166,7 +166,7 @@ extern "C" {
                     mk_c(c)->handle_exception(ex);
                 }
                 r = l_undef;
-                if (ex.msg() == std::string("canceled") && !mk_c(c)->m().inc()) {
+                if (!mk_c(c)->m().inc()) {
                     to_optimize_ptr(o)->set_reason_unknown(ex.msg());
                 }
                 else {
diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index ce7b9c9b7..940cf6750 100644
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@@ -155,6 +155,9 @@ lia_move int_solver::check(lp::explanation * e) {
 
     check_return_helper pc(lra);
 
+    if (settings().get_cancel_flag())
+        return lia_move::undef;
+    
     ++m_number_of_calls;
     if (r == lia_move::undef && m_patcher.should_apply()) r = m_patcher();
     if (r == lia_move::undef && should_find_cube()) r = int_cube(*this)();
@@ -536,11 +539,14 @@ std::ostream& int_solver::display_row_info(std::ostream & out, unsigned row_inde
 bool int_solver::shift_var(unsigned j, unsigned range) {
     if (is_fixed(j) || is_base(j))
         return false;
-       
+    if (settings().get_cancel_flag())
+        return false;       
     bool inf_l = false, inf_u = false;
     impq l, u;
     mpq m;
-    VERIFY(get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m));
+    VERIFY(get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m) || settings().get_cancel_flag());
+    if (settings().get_cancel_flag())
+        return false;
     const impq & x = get_value(j);
     // x, the value of j column, might be shifted on a multiple of m
     if (inf_l && inf_u) {