diff --git a/spot/mc/ec.hh b/spot/mc/ec.hh
index 7cfdfdb70..86f799ceb 100644
--- a/spot/mc/ec.hh
+++ b/spot/mc/ec.hh
@@ -124,7 +124,7 @@ namespace spot
 
     std::string trace()
     {
-      assert(counterexample_found());
+      SPOT_ASSERT(counterexample_found());
       std::string res = "Prefix:\n";
 
        // Compute the prefix of the accepting run
diff --git a/spot/mc/intersect.hh b/spot/mc/intersect.hh
index 2a927e291..b13187a97 100644
--- a/spot/mc/intersect.hh
+++ b/spot/mc/intersect.hh
@@ -62,7 +62,7 @@ namespace spot
               twacube_ptr twa):
       sys_(sys), twa_(twa)
     {
-      assert(is_a_kripkecube(sys));
+      SPOT_ASSERT(is_a_kripkecube(sys));
       map.reserve(2000000);
       todo.reserve(100000);
     }
@@ -178,8 +178,9 @@ namespace spot
     /// is slightly different.
     void forward_iterators(bool just_pushed)
     {
-      assert(!todo.empty());
-      assert(!(todo.back().it_prop->done() &&  todo.back().it_kripke->done()));
+      SPOT_ASSERT(!todo.empty());
+      SPOT_ASSERT(!(todo.back().it_prop->done() &&
+                    todo.back().it_kripke->done()));
 
       // Sometimes kripke state may have no successors.
       if (todo.back().it_kripke->done())
@@ -187,7 +188,7 @@ namespace spot
 
       // The state has just been push and the 2 iterators intersect.
       // There is no need to move iterators forward.
-      assert(!(todo.back().it_prop->done()));
+      SPOT_ASSERT(!(todo.back().it_prop->done()));
       if (just_pushed && twa_->get_cubeset()
           .intersect(twa_->trans_data(todo.back().it_prop).cube_,
                      todo.back().it_kripke->condition()))
diff --git a/spot/mc/reachability.hh b/spot/mc/reachability.hh
index 77648549b..3c52a75f2 100644
--- a/spot/mc/reachability.hh
+++ b/spot/mc/reachability.hh
@@ -35,7 +35,7 @@ namespace spot
     seq_reach_kripke(kripkecube<State, SuccIterator>& sys):
       sys_(sys)
     {
-      assert(is_a_kripkecube(sys));
+      SPOT_ASSERT(is_a_kripkecube(sys));
       visited.reserve(2000000);
       todo.reserve(100000);
     }
diff --git a/spot/mc/utils.hh b/spot/mc/utils.hh
index e51161fc2..1baa895fe 100644
--- a/spot/mc/utils.hh
+++ b/spot/mc/utils.hh
@@ -67,7 +67,7 @@ namespace spot
     {
       unsigned st = res_->new_state();
       names_->push_back(this->sys_.to_string(s));
-      assert(st == i);
+      SPOT_ASSERT(st == i);
     }
 
     void edge(unsigned src, unsigned dst)
@@ -167,7 +167,7 @@ namespace spot
       unsigned st = res_->new_state();
       names_->push_back(this->sys_.to_string(s.st_kripke) +
                         ('*' + std::to_string(s.st_prop)));
-      assert(st+1 == i);
+      SPOT_ASSERT(st+1 == i);
       return true;
     }