model-checker : fix bugged mutual exclusion example in SMPI

diff --git a/examples/smpi/mc/bugged1_liveness.c b/examples/smpi/mc/bugged1_liveness.c
index f7dab1b..4b5b067 100644 (file)
--- a/examples/smpi/mc/bugged1_liveness.c
+++ b/examples/smpi/mc/bugged1_liveness.c
@@ -71,6 +71,7 @@ int main(int argc, char **argv){
             CS_used = 1;
           }else{
             xbt_dynar_push(requests, &recv_buff);
             CS_used = 1;
           }else{
             xbt_dynar_push(requests, &recv_buff);

+            CS_used = 0;

           }
         }else{
           printf("CS release. Resource now idle.\n");
           }
         }else{
           printf("CS release. Resource now idle.\n");