model: remove useless special case
authorBrian Norris <banorris@uci.edu>
Thu, 15 Nov 2012 00:30:39 +0000 (16:30 -0800)
committerBrian Norris <banorris@uci.edu>
Thu, 15 Nov 2012 00:30:39 +0000 (16:30 -0800)
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

index 3f200ed..922a0d6 100644 (file)
--- 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();
        }