diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp index 0f64083ddda6..7722c4bfab69 100644 --- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp +++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp @@ -22,13 +22,23 @@ auto MiriGenmcShim::schedule_next( // a scheduling decision. threads_action_[curr_thread_id].kind = curr_thread_next_instr_kind; - if (const auto result = GenMCDriver::scheduleNext(threads_action_)) - return SchedulingResult { ExecutionState::Ok, static_cast(result.value()) }; - if (getExec().getGraph().isBlocked()) - return SchedulingResult { ExecutionState::Blocked, 0 }; - if (getResult().status.has_value()) // the "value" here is a `VerificationError` - return SchedulingResult { ExecutionState::Error, 0 }; - return SchedulingResult { ExecutionState::Finished, 0 }; + auto result = GenMCDriver::scheduleNext(threads_action_); + return std::visit( + [](auto&& arg) { + using T = std::decay_t; + if constexpr (std::is_same_v) + return SchedulingResult { ExecutionState::Ok, static_cast(arg) }; + else if constexpr (std::is_same_v) + return SchedulingResult { ExecutionState::Blocked, 0 }; + else if constexpr (std::is_same_v) + return SchedulingResult { ExecutionState::Error, 0 }; + else if constexpr (std::is_same_v) + return SchedulingResult { ExecutionState::Finished, 0 }; + else + static_assert(false, "non-exhaustive visitor!"); + }, + result + ); } /**** Execution start/end handling ****/