From 99c0d85ef14259735fdd84cb7b3e578f64434314 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 31 Jul 2012 16:32:59 -0700 Subject: [PATCH] model: refactor "infeasible" printing --- model.cc | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/model.cc b/model.cc index 0e24f1b0..cf845ecd 100644 --- a/model.cc +++ b/model.cc @@ -162,7 +162,10 @@ bool ModelChecker::next_execution() DBG(); num_executions++; - print_summary(); + + if (isfeasible() || DBG_ENABLED()) + print_summary(); + if ((diverge = model->get_next_backtrack()) == NULL) return false; @@ -516,20 +519,14 @@ static void print_list(action_list_t *list) void ModelChecker::print_summary(void) { - if (!isfeasible()) { - if (DBG_ENABLED()) - printf("INFEASIBLE EXECUTION!\n"); - else - return; - } - printf("\n"); printf("Number of executions: %d\n", num_executions); printf("Total nodes created: %d\n", node_stack->get_total_nodes()); - scheduler->print(); + if (!isfeasible()) + printf("INFEASIBLE EXECUTION!\n"); print_list(action_trace); printf("\n"); } -- 2.34.1