X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=16d5db4ab280262d1c4439de6544a413f8ba794e;hb=fb6d374952284313141eaee75ecd322209d152db;hp=466bf613a905ece97aaba98c506e1bf9234109e7;hpb=251c63183adee7dbdceeabce5a706e8281bc2887;p=model-checker.git diff --git a/model.cc b/model.cc index 466bf61..16d5db4 100644 --- a/model.cc +++ b/model.cc @@ -197,15 +197,13 @@ void ModelChecker::assert_user_bug(const char *msg) /** @brief Print bug report listing for this execution (if any bugs exist) */ void ModelChecker::print_bugs() const { - if (execution->have_bug_reports()) { - SnapVector *bugs = execution->get_bugs(); - - model_print("Bug report: %zu bug%s detected\n", - bugs->size(), - bugs->size() > 1 ? "s" : ""); - for (unsigned int i = 0; i < bugs->size(); i++) - (*bugs)[i]->print(); - } + SnapVector *bugs = execution->get_bugs(); + + model_print("Bug report: %zu bug%s detected\n", + bugs->size(), + bugs->size() > 1 ? "s" : ""); + for (unsigned int i = 0; i < bugs->size(); i++) + (*bugs)[i]->print(); } /** @@ -252,10 +250,12 @@ void ModelChecker::print_stats() const */ void ModelChecker::print_execution(bool printbugs) const { + model_print("Program output from execution %d:\n", + get_execution_number()); print_program_output(); if (params.verbose >= 2) { - model_print("Earliest divergence point since last feasible execution:\n"); + model_print("\nEarliest divergence point since last feasible execution:\n"); if (earliest_diverge) earliest_diverge->print(); else @@ -266,8 +266,10 @@ void ModelChecker::print_execution(bool printbugs) const } /* Don't print invalid bugs */ - if (printbugs) + if (printbugs && execution->have_bug_reports()) { + model_print("\n"); print_bugs(); + } model_print("\n"); execution->print_summary();