- if (snapshot_compare(state->get(), current_state) == 0) {
- XBT_INFO("Non-progressive cycle: state %d -> state %d", (*state)->num, current_state->num);
- return true;
+ if (mcapi::get().snapshot_equal((*state)->system_state_.get(), current_state->system_state_.get())) {
+ XBT_INFO("Non-progressive cycle: state %d -> state %d", (*state)->num_, current_state->num_);
+ XBT_INFO("******************************************");
+ XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
+ XBT_INFO("******************************************");
+ XBT_INFO("Counter-example execution trace:");
+ auto checker = mcapi::get().mc_get_checker();
+ for (auto const& s : checker->get_textual_trace())
+ XBT_INFO(" %s", s.c_str());
+ mcapi::get().mc_dump_record_path();
+ mcapi::get().s_log_state();
+
+ throw TerminationError();