X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=3b83b569baf5c12f356aaf596023ca4fe3b3cde2;hp=417252c3f92ceb3a4bb7948612ca3592f1be49de;hb=029af23cb3196ffdd986497d2c45a938af526362;hpb=1798c510e77f37e3d79cba6a1fdad3b13ccc9674

diff --git a/model.cc b/model.cc
index 417252c3..3b83b569 100644
--- a/model.cc
+++ b/model.cc
@@ -1037,7 +1037,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 
 	/* Initialize work_queue with the "current action" work */
 	work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
-	while (!work_queue.empty()) {
+	while (!work_queue.empty() && !has_asserted()) {
 		WorkQueueEntry work = work_queue.front();
 		work_queue.pop_front();
 
@@ -2179,11 +2179,8 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 		}
 	}
 
-	if (!initialized) {
-		/** @todo Need a more informative way of reporting errors. */
-		printf("ERROR: may read from uninitialized atomic\n");
-		set_assert();
-	}
+	if (!initialized)
+		assert_bug("May read from uninitialized atomic");
 
 	if (DBG_ENABLED() || !initialized) {
 		printf("Reached read action:\n");