diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index 374f6c3b2..7bce00c6a 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp @@ -288,7 +288,7 @@ namespace storm { if (stepBound) { assert(*stepBound > 0); x = std::vector(maybeStates.getNumberOfSetBits(), storm::utility::zero()); - solver->repeatedMultiply(dirForParameters, x, ¶meterLifter->getVector(), *stepBound); + solver->repeatedMultiply(env, dirForParameters, x, ¶meterLifter->getVector(), *stepBound); } else { x.resize(maybeStates.getNumberOfSetBits(), storm::utility::zero()); solver->solveEquations(env, dirForParameters, x, parameterLifter->getVector()); diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp index 085c25a2c..04a5c41e1 100644 --- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp @@ -248,14 +248,7 @@ namespace storm { parameterLifter->specifyRegion(region, dirForParameters); // Set up the solver - auto solver = solverFactory->create(player1Matrix, parameterLifter->getMatrix()); - if (storm::NumberTraits::IsExact && dynamic_cast*>(solver.get())) { - STORM_LOG_INFO("Parameter Lifting: Setting solution method for exact Game Solver to policy iteration"); - auto* standardSolver = dynamic_cast*>(solver.get()); - auto settings = standardSolver->getSettings(); - settings.setSolutionMethod(storm::solver::StandardGameSolverSettings::SolutionMethod::PolicyIteration); - standardSolver->setSettings(settings); - } + auto solver = solverFactory->create(env, player1Matrix, parameterLifter->getMatrix()); if (lowerResultBound) solver->setLowerBound(lowerResultBound.get()); if (upperResultBound) solver->setUpperBound(upperResultBound.get()); if (applyPreviousResultAsHint) {