model: reformat execution trace prints

Bring the "INFEASIBLE" message together with the "Execution #" message,
to make the log more compact and readable (e.g., grep for "Execution"
will give you some regularly-patterned, useful information).

diff --git a/model.cc b/model.cc
index c63d9d9ced8db0b57100028540f3d4930e9bbf0e..9c3488435e02d0ec592b7381b9e207448c494ce1 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -2576,13 +2576,11 @@ ModelAction * ModelChecker::new_uninitialized_action(void *location) const
        return act;
 }
 
-static void print_list(action_list_t *list, int exec_num = -1)
+static void print_list(action_list_t *list)
 {
        action_list_t::iterator it;
 
        model_print("---------------------------------------------------------------------\n");
-       if (exec_num >= 0)
-               model_print("Execution %d:\n", exec_num);
 
        unsigned int hash = 0;
 
@@ -2635,9 +2633,12 @@ void ModelChecker::print_summary() const
        dumpGraph(buffername);
 #endif
 
-       if (!isfeasibleprefix())
-               print_infeasibility("INFEASIBLE EXECUTION");
-       print_list(action_trace, stats.num_total);
+       model_print("Execution %d:", stats.num_total);
+       if (isfeasibleprefix())
+               model_print("\n");
+       else
+               print_infeasibility(" INFEASIBLE");
+       print_list(action_trace);
        model_print("\n");
 }