From 22efc98d95682e33aa85fd85f5e79d887875734b Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Fri, 1 Mar 2013 15:01:47 -0800
Subject: [PATCH] model: fix ASSERT()

Apparently this ASSERT() is still not good. ASSERT() was triggered, for
example, with:

  $ ./run.sh test/linuxrwlocks.o -f 4 -m 1
---
 model.cc | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/model.cc b/model.cc
index 7048096..9135e5c 100644
--- 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 */
-- 
2.34.1