Fixed not always using the acyclic solver within LRA and multi-objective time-bounded reachability computations.

src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp

@@ -259,12 +259,8 @@ namespace storm {
                             bool isAcyclic = !storm::utility::graph::hasCycle(_IsTransitions);
                             if (isAcyclic) {
                                 STORM_LOG_INFO("Instant transitions are acyclic.");
-                                if (_IsSolverEnv->solver().minMax().isMethodSetFromDefault()) {
-                                    _IsSolverEnv->solver().minMax().setMethod(storm::solver::MinMaxMethod::Acyclic);
-                                }
-                                if (_IsSolverEnv->solver().isLinearEquationSolverTypeSetFromDefaultValue()) {
-                                   _IsSolverEnv->solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Acyclic);
-                                }
+                                _IsSolverEnv->solver().minMax().setMethod(storm::solver::MinMaxMethod::Acyclic);
+                                _IsSolverEnv->solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Acyclic);
                             }
                             if (nondetIs()) {
                                 storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> factory;

src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp

@@ -332,8 +332,7 @@ namespace storm {
                 std::unique_ptr<MinMaxSolverData> result(new MinMaxSolverData());
                 result->env = std::make_unique<storm::Environment>(env);
                 // For acyclic models we switch to the more efficient acyclic solver (Unless the solver / method was explicitly specified)
-                if (acyclic && result->env->solver().minMax().isMethodSetFromDefault() && result->env->solver().minMax().getMethod() != storm::solver::MinMaxMethod::Acyclic) {
-                    STORM_LOG_INFO("Switching to Acyclic linear equation solver method. To overwrite this, explicitly specify another solver.");
+                if (acyclic) {
                     result->env->solver().minMax().setMethod(storm::solver::MinMaxMethod::Acyclic);
                 }
                 storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxSolverFactory;
@@ -372,8 +371,7 @@ namespace storm {
                 result->env = std::make_unique<Environment>(env);
                 result->acyclic = acyclic;
                 // For acyclic models we switch to the more efficient acyclic solver (Unless the solver / method was explicitly specified)
-                if (acyclic && result->env->solver().isLinearEquationSolverTypeSetFromDefaultValue() && result->env->solver().getLinearEquationSolverType() != storm::solver::EquationSolverType::Acyclic) {
-                    STORM_LOG_INFO("Switching to Acyclic linear equation solver method. To overwrite this, explicitly specify another solver.");
+                if (acyclic) {
                     result->env->solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Acyclic);
                 }
                 result->factory = std::make_unique<storm::solver::GeneralLinearEquationSolverFactory<ValueType>>();