X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=33e8805078b546ac8d1b4f87dab3ea31e9be2651;hb=ecf16617a0c289981925fcd2437595f3a2fce8fe;hp=ab16bf82528ea5ebf30766970b37faca5a6ada1f;hpb=122aad1259a2df612ad39c640551be8da9cb26b9;p=model-checker.git diff --git a/model.cc b/model.cc index ab16bf8..33e8805 100644 --- a/model.cc +++ b/model.cc @@ -446,8 +446,8 @@ bool ModelChecker::next_execution() if (is_deadlocked()) assert_bug("Deadlock detected"); - print_bugs(); checkDataRaces(); + print_bugs(); printf("\n"); print_stats(); print_summary(); @@ -917,8 +917,7 @@ void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu } /* See if we have realized a data race */ - if (checkDataRaces()) - assert_bug("Data race"); + checkDataRaces(); } /** @@ -1849,8 +1848,7 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ } // If we resolved promises or data races, see if we have realized a data race. - if (checkDataRaces()) - assert_bug("Data race"); + checkDataRaces(); return updated; }