From f816b895e4b1219c3dcd0443a55ef90690a849ef Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Wed, 13 Jun 2012 10:12:08 +0200 Subject: [PATCH 1/1] model-checker : print statistics in all cases (property satisfied or not) --- src/mc/mc_global.c | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index dcf9b8bcc5..c0b7acddda 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -527,14 +527,19 @@ void MC_print_statistics_pairs(mc_stats_pair_t stats) void MC_assert(int prop) { - if (MC_IS_ENABLED && !prop) { - XBT_INFO("**************************"); - XBT_INFO("*** PROPERTY NOT VALID ***"); - XBT_INFO("**************************"); - XBT_INFO("Counter-example execution trace:"); - MC_dump_stack_safety_stateless(mc_stack_safety_stateless); - MC_print_statistics(mc_stats); - xbt_abort(); + if (MC_IS_ENABLED ){ + if(!prop) { + XBT_INFO("**************************"); + XBT_INFO("*** PROPERTY NOT VALID ***"); + XBT_INFO("**************************"); + XBT_INFO("Counter-example execution trace:"); + MC_dump_stack_safety_stateless(mc_stack_safety_stateless); + MC_print_statistics(mc_stats); + xbt_abort(); + }else{ + MC_print_statistics(mc_stats); + xbt_abort(); + } } } -- 2.20.1