} else if (_sg_mc_liveness) {
nb_processes = ((mc_visited_pair_t) ref)->nb_processes;
heap_bytes_used = ((mc_visited_pair_t) ref)->heap_bytes_used;
+ } else {
+ xbt_die("Both liveness and safety are disabled.");
}
int start = 0;
(mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
+ } else {
+ nb_processes_test = 0;
+ heap_bytes_used_test = 0;
+ xbt_die("Both liveness and safety are disabled.");
}
if (nb_processes_test < nb_processes) {
start = cursor + 1;
int min2 = mc_stats->expanded_states;
unsigned int cursor2 = 0;
unsigned int index2 = 0;
- xbt_dynar_foreach(visited_states, cursor2, state_test) {
- if (state_test->num < min2) {
+ xbt_dynar_foreach(visited_states, cursor2, state_test){
+ if (!mc_important_snapshot(state_test->system_state) && state_test->num < min2) {
index2 = cursor2;
min2 = state_test->num;
}
unsigned int cursor2 = 0;
unsigned int index2 = 0;
xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
- if (pair_test->num < min2) {
+ if (!mc_important_snapshot(pair_test->graph_state->system_state) && pair_test->num < min2) {
index2 = cursor2;
min2 = pair_test->num;
}