From 6df0efcd3e0c52be97a8f36abd9cba4e89b4d3ee Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 9 Mar 2021 13:03:17 +0100 Subject: [PATCH] Set result correctly for reachability rewards in MdpInstantiationChecker --- .../instantiation/SparseMdpInstantiationModelChecker.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp index eac3df86a..ddeb32cb3 100644 --- a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp +++ b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp @@ -140,7 +140,7 @@ namespace storm { // Check the formula and store the result as a hint for the next call. // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { - std::unique_ptr result = modelChecker.check(env, *this->currentCheckTask); + result = modelChecker.check(env, *this->currentCheckTask); storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); hint.setResultHint(result->template asExplicitQuantitativeCheckResult().getValueVector()); hint.setSchedulerHint(dynamic_cast const&>(scheduler));