diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index b03de70a2..7f5f6872e 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -21,6 +21,7 @@ Notes:
 #include"solver.h"
 #include"scoped_timer.h"
 #include"combined_solver_params.hpp"
+#include"common_msgs.h"
 #define PS_VB_LVL 15
 
 /**
@@ -201,7 +202,12 @@ public:
             return m_solver2->get_consequences(asms, vars, consequences);
         }
         catch (z3_exception& ex) {
-            set_reason_unknown(ex.msg());
+            if (get_manager().canceled()) {
+                set_reason_unknown(Z3_CANCELED_MSG);
+            }
+            else {
+                set_reason_unknown(ex.msg());
+            }
         }
         return l_undef;
     }
diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index 8f32019d5..441ece429 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -21,6 +21,8 @@ Notes:
 #include"ast_util.h"
 #include"ast_pp.h"
 #include"ast_pp_util.h"
+#include "common_msgs.h"
+
 
 unsigned solver::get_num_assertions() const {
     NOT_IMPLEMENTED_YET();
@@ -56,7 +58,19 @@ struct scoped_assumption_push {
 };
 
 lbool solver::get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
-    return get_consequences_core(asms, vars, consequences);
+    try {
+        return get_consequences_core(asms, vars, consequences);
+    }
+    catch (z3_exception& ex) {
+        if (asms.get_manager().canceled()) {
+            set_reason_unknown(Z3_CANCELED_MSG);
+            return l_undef;
+        }
+        else {
+            set_reason_unknown(ex.msg());
+        }
+        throw;
+    }
 }
 
 lbool solver::get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {