model: end-of-execution print

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

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