model: fix ASSERT()

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 7048096ca25e0cbe0ad9928504802de4231c5a18..9135e5c85e6d4b03cc08e6fa462103e34c43cb8a 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -483,10 +483,16 @@ void ModelChecker::record_stats()
                stats.num_buggy_executions++;
        else if (is_complete_execution())
                stats.num_complete++;
-       else if (scheduler->all_threads_sleeping())
+       else {
                stats.num_redundant++;
-       else
-               ASSERT(false);
+
+               /**
+                * @todo We can violate this ASSERT() when fairness/sleep sets
+                * conflict to cause an execution to terminate, e.g. with:
+                * Scheduler: [0: disabled][1: disabled][2: sleep][3: current, enabled]
+                */
+               //ASSERT(scheduler->all_threads_sleeping());
+       }
 }
 
 /** @brief Print execution stats */