model: end-of-execution print
authorBrian Norris <banorris@uci.edu>
Sat, 16 Feb 2013 02:09:03 +0000 (18:09 -0800)
committerBrian Norris <banorris@uci.edu>
Sat, 16 Feb 2013 02:09:03 +0000 (18:09 -0800)
For readability of a "verbose" execution log (and even for the shorter,
non-verbose log), it helps to visually separate the final statistics
from any previously-printed statistics. For instance, in the following
verbose snippet from the end of an execution history, it's confusing why
there are two identical copies of the statistics:

... <other execution history> ...
Number of complete, bug-free executions: 4
Number of redundant executions: 0
Number of buggy executions: 0
Number of infeasible executions: 5
Total executions: 9
Total nodes created: 48

Execution 9:
---------------------------------------------------------------------
... <snipped trace info> ...
---------------------------------------------------------------------

Number of complete, bug-free executions: 4
Number of redundant executions: 0
Number of buggy executions: 0
Number of infeasible executions: 5
Total executions: 9
Total nodes created: 48

model.cc

index 655c511..0bccd83 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -2807,5 +2807,6 @@ void ModelChecker::run()
                };
        } while (next_execution());
 
                };
        } while (next_execution());
 
+       model_print("******* Model-checking complete: *******\n");
        print_stats();
 }
        print_stats();
 }