From 4bb070b43345c8617c6c627e2b9b24039affb6b7 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Wed, 14 Nov 2012 16:30:39 -0800
Subject: [PATCH] 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.
---
 model.cc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/model.cc b/model.cc
index 3f200ed8..922a0d60 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();
 	}
-- 
2.34.1