state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
bytes_used_test = state_test->heap_bytes_used;
nb_processes_test = state_test->nb_processes;
- if(nb_processes_test < current_nb_processes)
+ if(nb_processes_test < current_nb_processes){
start = cursor + 1;
- if(nb_processes_test > current_nb_processes)
- end = cursor - 1;
- if(nb_processes_test == current_nb_processes){
+ }else if(nb_processes_test > current_nb_processes){
+ end = cursor - 1;
+ }else if(nb_processes_test == current_nb_processes){
if(bytes_used_test < current_bytes_used)
start = cursor + 1;
if(bytes_used_test > current_bytes_used)
}
}
- max_depth_reached = 1;
+ if(MC_state_interleave_size(state) > 0){
+ max_depth_reached = 1;
+ }else{
+ /* Trash the current state, no longer needed */
+ MC_SET_RAW_MEM;
+ xbt_fifo_shift(mc_stack_safety);
+ MC_state_delete(state);
+ MC_UNSET_RAW_MEM;
+
+ max_depth_reached = 0;
+ }
+
}else{
XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
break;
} else {
+ XBT_DEBUG("Delete state at depth %d",xbt_fifo_size(mc_stack_safety) + 1);
MC_state_delete(state);
}
}