Since stats won't be printed regularly, we still want a measure of
"how many executions have run" when we print a summary trace.
if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
model_print("Earliest divergence point since last feasible execution:\n");
if (earliest_diverge)
if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
model_print("Earliest divergence point since last feasible execution:\n");
if (earliest_diverge)
if ((diverge = get_next_backtrack()) == NULL)
return false;
if ((diverge = get_next_backtrack()) == NULL)
return false;
-static void print_list(action_list_t *list)
+static void print_list(action_list_t *list, int exec_num = -1)
{
action_list_t::iterator it;
model_print("---------------------------------------------------------------------\n");
{
action_list_t::iterator it;
model_print("---------------------------------------------------------------------\n");
- model_print("Trace:\n");
+ if (exec_num >= 0)
+ model_print("Execution %d:\n", exec_num);
+
unsigned int hash=0;
for (it = list->begin(); it != list->end(); it++) {
unsigned int hash=0;
for (it = list->begin(); it != list->end(); it++) {
if (!isfinalfeasible())
model_print("INFEASIBLE EXECUTION!\n");
if (!isfinalfeasible())
model_print("INFEASIBLE EXECUTION!\n");
- print_list(action_trace);
+ print_list(action_trace, stats.num_total);