From 8d9a43be3bc794d7c9096dbda88640eb2fa99ee6 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 15 Feb 2013 18:09:03 -0800 Subject: [PATCH] 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: ... ... 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: --------------------------------------------------------------------- ... ... --------------------------------------------------------------------- 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 | 1 + 1 file changed, 1 insertion(+) diff --git a/model.cc b/model.cc index 655c511..0bccd83 100644 --- a/model.cc +++ b/model.cc @@ -2807,5 +2807,6 @@ void ModelChecker::run() }; } while (next_execution()); + model_print("******* Model-checking complete: *******\n"); print_stats(); } -- 2.34.1