diff --git a/src/library/mt_task_queue.cpp b/src/library/mt_task_queue.cpp
index 5ffa006f5f..8253cca81a 100644
--- a/src/library/mt_task_queue.cpp
+++ b/src/library/mt_task_queue.cpp
@@ -61,7 +61,7 @@ void mt_task_queue::notify_queue_changed() {
 constexpr chrono::milliseconds g_worker_max_idle_time = chrono::milliseconds(1000);
 
 void mt_task_queue::spawn_worker() {
-    lean_assert(!m_shutting_down);
+    lean_always_assert(!m_shutting_down);
     auto this_worker = std::make_shared<worker_info>();
     m_workers.push_back(this_worker);
     m_required_workers--;
@@ -120,8 +120,8 @@ void mt_task_queue::spawn_worker() {
 }
 
 void mt_task_queue::handle_finished(gtask const & t) {
-    lean_assert(get_state(t).load() > task_state::Running);
-    lean_assert(get_data(t));
+    lean_always_assert(get_state(t).load() > task_state::Running);
+    lean_always_assert(get_data(t));
 
     if (!get_data(t)->m_sched_info)
         return;  // task has never been submitted
@@ -135,7 +135,7 @@ void mt_task_queue::handle_finished(gtask const & t) {
                 if (check_deps(rdep)) {
                     m_waiting.erase(rdep);
                     if (get_state(rdep).load() < task_state::Running) {
-                        lean_assert(get_data(rdep));
+                        lean_always_assert(get_data(rdep));
                         if (get_data(rdep)->m_flags.m_eager_execution) {
                             get_state(rdep) = task_state::Running;
                             execute(rdep);
@@ -189,7 +189,7 @@ void mt_task_queue::submit_core(gtask const & t, unsigned prio) {
         case task_state::Running: case task_state::Failed: case task_state::Success:
             break;
     }
-    lean_assert(get_state(t).load() >= task_state::Waiting);
+    lean_always_assert(get_state(t).load() >= task_state::Waiting);
 }
 
 void mt_task_queue::bump_prio(gtask const & t, unsigned new_prio) {
@@ -199,7 +199,7 @@ void mt_task_queue::bump_prio(gtask const & t, unsigned new_prio) {
                 auto prio = get_prio(t);
                 auto &q = m_queue[prio];
                 auto it = std::find(q.begin(), q.end(), t);
-                lean_assert(it != q.end());
+                lean_always_assert(it != q.end());
                 q.erase(it);
                 if (q.empty()) m_queue.erase(prio);
 
@@ -222,7 +222,7 @@ void mt_task_queue::bump_prio(gtask const & t, unsigned new_prio) {
 
 bool mt_task_queue::check_deps(gtask const & t) {
     check_stack("mt_task_queue::check_deps");
-    lean_assert(get_data(t));
+    lean_always_assert(get_data(t));
 
     buffer<gtask> deps;
     try {
@@ -241,7 +241,7 @@ bool mt_task_queue::check_deps(gtask const & t) {
         if (!dep) continue;
         switch (get_state(dep).load()) {
             case task_state::Waiting: case task_state::Queued: case task_state::Running:
-                lean_assert(get_imp(dep));
+                lean_always_assert(get_imp(dep));
                 get_sched_info(dep).m_reverse_deps.push_back(t);
                 return false;
             case task_state::Success:
@@ -301,10 +301,10 @@ void mt_task_queue::join() {
 }
 
 gtask mt_task_queue::dequeue() {
-    lean_assert(!m_queue.empty());
+    lean_always_assert(!m_queue.empty());
     auto it = m_queue.begin();
     auto & highest_prio = it->second;
-    lean_assert(!highest_prio.empty());
+    lean_always_assert(!highest_prio.empty());
     auto result = std::move(highest_prio.front());
     highest_prio.pop_front();
     if (highest_prio.empty()) {
@@ -314,8 +314,8 @@ gtask mt_task_queue::dequeue() {
 }
 
 void mt_task_queue::enqueue(gtask const & t) {
-    lean_assert(get_state(t).load() < task_state::Running);
-    lean_assert(get_imp(t));
+    lean_always_assert(get_state(t).load() < task_state::Running);
+    lean_always_assert(get_imp(t));
     get_state(t) = task_state::Queued;
     m_queue[get_prio(t)].push_back(t);
     if (m_required_workers > 0) {
diff --git a/src/util/debug.h b/src/util/debug.h
index 607e507749..3e526fe3e0 100644
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -84,6 +84,7 @@ Author: Leonardo de Moura
 
 #define lean_assert(COND, ARGS...) DEBUG_CODE({if (!(COND)) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); LEAN_DISPLAY(ARGS); lean::invoke_debugger(); }})
 #define lean_cond_assert(TAG, COND, ARGS...) DEBUG_CODE({if (lean::is_debug_enabled(TAG) && !(COND)) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); LEAN_DISPLAY(ARGS); lean::invoke_debugger(); }})
+#define lean_always_assert(COND, ARGS...) { if (!(COND)) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); LEAN_DISPLAY(ARGS); lean_unreachable(); } }
 
 #define lean_assert_eq(A, B) lean_assert(A == B, A, B)
 #define lean_assert_ne(A, B) lean_assert(A != B, A, B)
diff --git a/src/util/task.cpp b/src/util/task.cpp
index 07a6ad22a4..fa131a166c 100644
--- a/src/util/task.cpp
+++ b/src/util/task.cpp
@@ -36,10 +36,10 @@ void task_queue::wait_for_success(gtask const & t) {
 }
 
 void task_queue::execute(gtask const & t) {
-    lean_assert(t);
-    lean_assert(t->m_state.load() == task_state::Running);
-    lean_assert(t->m_data);
-    lean_assert(t->m_data->m_imp);
+    lean_always_assert(t);
+    lean_always_assert(t->m_state.load() == task_state::Running);
+    lean_always_assert(t->m_data);
+    lean_always_assert(t->m_data->m_imp);
 
     try {
         {
@@ -57,14 +57,14 @@ void task_queue::execute(gtask const & t) {
 }
 
 void task_queue::fail(gtask const & t, std::exception_ptr const & ex) {
-    lean_assert(t->m_state.load() < task_state::Running);
+    lean_always_assert(t->m_state.load() < task_state::Running);
 
     t->m_exception = ex;
     t->m_state = task_state::Failed;
 }
 
 void task_queue::fail(gtask const & t, gtask const & failed) {
-    lean_assert(failed->m_state.load() == task_state::Failed);
+    lean_always_assert(failed->m_state.load() == task_state::Failed);
 
     fail(t, failed->m_exception);
 }