From: Brian Norris <banorris@uci.edu>
Date: Thu, 15 Nov 2012 00:30:39 +0000 (-0800)
Subject: model: remove useless special case
X-Git-Tag: oopsla2013~539^2^2
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=4bb070b43345c8617c6c627e2b9b24039affb6b7;p=model-checker.git

model: remove useless special case

Why do we want to print races, etc., when exiting due to execution
length bound? If you want that, just enable debug prints.
---

diff --git a/model.cc b/model.cc
index 3f200ed..922a0d6 100644
--- a/model.cc
+++ b/model.cc
@@ -306,7 +306,7 @@ bool ModelChecker::next_execution()
 			pending_rel_seqs->size());
 
 
-	if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() ) {
+	if (isfinalfeasible() || DBG_ENABLED()) {
 		checkDataRaces();
 		print_summary();
 	}