diff --git a/src/solver/EliminationLinearEquationSolver.cpp b/src/solver/EliminationLinearEquationSolver.cpp
index 8cf773c16..e35402e95 100644
--- a/src/solver/EliminationLinearEquationSolver.cpp
+++ b/src/solver/EliminationLinearEquationSolver.cpp
@@ -56,7 +56,7 @@ namespace storm {
         }
         
         template<typename ValueType>
-        void EliminationLinearEquationSolver<ValueType>::solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
+        bool EliminationLinearEquationSolver<ValueType>::solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
             // FIXME: This solver will not work for all input systems. More concretely, the current implementation will
             // not work for systems that have a 0 on the diagonal. This is not a restriction of this technique in general
             // but arbitrary matrices require pivoting, which is not currently implemented.
@@ -108,6 +108,8 @@ namespace storm {
             if (localA) {
                 localA->convertToEquationSystem();
             };
+
+            return true;
         }
         
         template<typename ValueType>
diff --git a/src/solver/EliminationLinearEquationSolver.h b/src/solver/EliminationLinearEquationSolver.h
index 5963c5763..93cb20346 100644
--- a/src/solver/EliminationLinearEquationSolver.h
+++ b/src/solver/EliminationLinearEquationSolver.h
@@ -32,7 +32,7 @@ namespace storm {
             virtual void setMatrix(storm::storage::SparseMatrix<ValueType> const& A) override;
             virtual void setMatrix(storm::storage::SparseMatrix<ValueType>&& A) override;
             
-            virtual void solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
+            virtual bool solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
             virtual void multiply(std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const override;
 
             EliminationLinearEquationSolverSettings<ValueType>& getSettings();
diff --git a/src/solver/GmmxxLinearEquationSolver.h b/src/solver/GmmxxLinearEquationSolver.h
index 61027f456..6247723c8 100644
--- a/src/solver/GmmxxLinearEquationSolver.h
+++ b/src/solver/GmmxxLinearEquationSolver.h
@@ -102,18 +102,7 @@ namespace storm {
             virtual bool deallocateAuxMemory(LinearEquationSolverOperation operation) const override;
             virtual bool reallocateAuxMemory(LinearEquationSolverOperation operation) const override;
             virtual bool hasAuxMemory(LinearEquationSolverOperation operation) const override;
-            
-            virtual void setPrecision(double precision) override{
-                this->precision = precision;
-            }
-            
-            virtual void setIterations(uint_fast64_t maximalNumberOfIterations) override{
-                this->maximalNumberOfIterations = maximalNumberOfIterations;
-            }
-            
-            virtual void setRelative(bool relative) override{
-                this->relative = relative;
-            }
+
             
         private:
             /*!
diff --git a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp
deleted file mode 100644
index f89f32a94..000000000
--- a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp
+++ /dev/null
@@ -1,214 +0,0 @@
-#include "src/solver/GmmxxMinMaxLinearEquationSolver.h"
-
-#include <utility>
-
-#include "src/settings/SettingsManager.h"
-#include "src/adapters/GmmxxAdapter.h"
-#include "src/solver/GmmxxLinearEquationSolver.h"
-#include "src/storage/TotalScheduler.h"
-#include "src/utility/vector.h"
-
-#include "src/settings/modules/GeneralSettings.h"
-#include "src/settings/modules/GmmxxEquationSolverSettings.h"
-
-namespace storm {
-    namespace solver {
-        
-        template<typename ValueType>
-        GmmxxMinMaxLinearEquationSolver<ValueType>::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, MinMaxTechniqueSelection preferredTechnique, bool trackScheduler) :
-        MinMaxLinearEquationSolver<ValueType>(A, storm::settings::gmmxxEquationSolverSettings().getPrecision(), storm::settings::gmmxxEquationSolverSettings().getConvergenceCriterion() == storm::settings::modules::GmmxxEquationSolverSettings::ConvergenceCriterion::Relative, storm::settings::gmmxxEquationSolverSettings().getMaximalIterationCount(), trackScheduler, preferredTechnique), gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<ValueType>(A)), rowGroupIndices(A.getRowGroupIndices()) {
-                // Intentionally left empty.
-        }
-        
-        template<typename ValueType>
-		GmmxxMinMaxLinearEquationSolver<ValueType>::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative, bool trackScheduler) : MinMaxLinearEquationSolver<ValueType>(A, precision, relative, maximalNumberOfIterations, trackScheduler, tech), gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<ValueType>(A)),  rowGroupIndices(A.getRowGroupIndices())  {
-            // Intentionally left empty.
-        }
-
-        template<typename ValueType>
-        void GmmxxMinMaxLinearEquationSolver<ValueType>::solveEquationSystem(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const {
-			if (this->useValueIteration) {
-                // Set up the environment for the power method. If scratch memory was not provided, we need to create it.
-				bool multiplyResultMemoryProvided = true;
-				if (multiplyResult == nullptr) {
-					multiplyResult = new std::vector<ValueType>(b.size());
-					multiplyResultMemoryProvided = false;
-				}
-
-				std::vector<ValueType>* currentX = &x;
-				bool xMemoryProvided = true;
-				if (newX == nullptr) {
-					newX = new std::vector<ValueType>(x.size());
-					xMemoryProvided = false;
-				}
-				uint_fast64_t iterations = 0;
-				bool converged = false;
-
-				// Keep track of which of the vectors for x is the auxiliary copy.
-				std::vector<ValueType>* copyX = newX;
-
-				// Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number
-				// of iterations.
-				while (!converged && iterations < this->maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) {
-					// Compute x' = A*x + b.
-					gmm::mult(*gmmxxMatrix, *currentX, *multiplyResult);
-					gmm::add(b, *multiplyResult);
-
-					// Reduce the vector x by applying min/max over all nondeterministic choices.
-					storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, rowGroupIndices);
-					
-					// Determine whether the method converged.
-					converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, this->precision, this->relative);
-
-					// Update environment variables.
-					std::swap(currentX, newX);
-					++iterations;
-				}
-
-				// Check if the solver converged and issue a warning otherwise.
-				if (converged) {
-					STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations.");
-				} else {
-					STORM_LOG_WARN("Iterative solver did not converge after " << iterations << " iterations.");
-				}
-
-				// If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result
-				// is currently stored in currentX, but x is the output vector.
-				if (currentX == copyX) {
-					std::swap(x, *currentX);
-				}
-                                
-                if(this->trackScheduler){
-                    if(iterations==0){ //may happen due to early termination. Then we need to compute x'= A*x+b
-					    gmm::mult(*gmmxxMatrix, x, *multiplyResult);
-					    gmm::add(b, *multiplyResult);
-                    }
-                    std::vector<uint_fast64_t> choices(x.size());
-                    storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, x, rowGroupIndices, &(choices));
-                    this->scheduler = std::make_unique<storm::storage::TotalScheduler>(std::move(choices));
-                }
-
-				if (!xMemoryProvided) {
-					delete copyX;
-				}
-
-				if (!multiplyResultMemoryProvided) {
-					delete multiplyResult;
-				}
-			} else {
-				// We will use Policy Iteration to solve the given system.
-				// We first guess an initial choice resolution which will be refined after each iteration.
-				std::vector<storm::storage::sparse::state_type> scheduler(this->A.getRowGroupIndices().size() - 1);
-
-				// Create our own multiplyResult for solving the deterministic sub-instances.
-				std::vector<ValueType> deterministicMultiplyResult(rowGroupIndices.size() - 1);
-				std::vector<ValueType> subB(rowGroupIndices.size() - 1);
-
-				bool multiplyResultMemoryProvided = true;
-				if (multiplyResult == nullptr) {
-					multiplyResult = new std::vector<ValueType>(b.size());
-					multiplyResultMemoryProvided = false;
-				}
-
-				std::vector<ValueType>* currentX = &x;
-				bool xMemoryProvided = true;
-				if (newX == nullptr) {
-					newX = new std::vector<ValueType>(x.size());
-					xMemoryProvided = false;
-				}
-
-				uint_fast64_t iterations = 0;
-				bool converged = false;
-
-				// Keep track of which of the vectors for x is the auxiliary copy.
-				std::vector<ValueType>* copyX = newX;
-
-				// Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number
-				// of iterations.
-				while (!converged && iterations < this->maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) {
-					// Take the sub-matrix according to the current choices
-					storm::storage::SparseMatrix<ValueType> submatrix = this->A.selectRowsFromRowGroups(scheduler, true);
-					submatrix.convertToEquationSystem();
-					
-					GmmxxLinearEquationSolver<ValueType> gmmLinearEquationSolver(submatrix, storm::solver::GmmxxLinearEquationSolver<double>::SolutionMethod::Gmres, this->precision, this->maximalNumberOfIterations, storm::solver::GmmxxLinearEquationSolver<double>::Preconditioner::Ilu, this->relative, 50);
-					storm::utility::vector::selectVectorValues<ValueType>(subB, scheduler, rowGroupIndices, b);
-
-					// Copy X since we will overwrite it
-					std::copy(currentX->begin(), currentX->end(), newX->begin());
-
-					// Solve the resulting linear equation system
-					gmmLinearEquationSolver.solveEquationSystem(*newX, subB, &deterministicMultiplyResult);
-
-					// Compute x' = A*x + b. This step is necessary to allow the choosing of the optimal policy for the next iteration.
-					gmm::mult(*gmmxxMatrix, *newX, *multiplyResult);
-					gmm::add(b, *multiplyResult);
-
-					// Reduce the vector x by applying min/max over all nondeterministic choices.
-					// Here, we capture which choice was taken in each state, thereby refining our initial guess.
-					storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, rowGroupIndices, &(scheduler));
-
-					// Determine whether the method converged.
-					converged = storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *newX, static_cast<ValueType>(this->precision), this->relative);
-
-					// Update environment variables.
-					std::swap(currentX, newX);
-					++iterations;
-				}
-
-				// Check if the solver converged and issue a warning otherwise.
-				if (converged) {
-					STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations.");
-				} else {
-					STORM_LOG_WARN("Iterative solver did not converge after " << iterations << " iterations.");
-				}
-                
-                // If requested, we store the scheduler for retrieval.
-                if (this->isTrackSchedulerSet()) {
-                    this->scheduler = std::make_unique<storm::storage::TotalScheduler>(std::move(scheduler));
-                }
-
-				// If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result
-				// is currently stored in currentX, but x is the output vector.
-				if (currentX == copyX) {
-					std::swap(x, *currentX);
-				}
-
-				if (!xMemoryProvided) {
-					delete copyX;
-				}
-
-				if (!multiplyResultMemoryProvided) {
-					delete multiplyResult;
-				}
-			}
-        }
-        
-        template<typename ValueType>
-        void GmmxxMinMaxLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
-            bool multiplyResultMemoryProvided = true;
-            if (multiplyResult == nullptr) {
-                multiplyResult = new std::vector<ValueType>(gmmxxMatrix->nr);
-                multiplyResultMemoryProvided = false;
-            }
-            
-            // Now perform matrix-vector multiplication as long as we meet the bound of the formula.
-            for (uint_fast64_t i = 0; i < n; ++i) {
-                gmm::mult(*gmmxxMatrix, x, *multiplyResult);
-                
-                if (b != nullptr) {
-                    gmm::add(*b, *multiplyResult);
-                }
-                
-                storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, x, rowGroupIndices);
-                
-            }
-            
-            if (!multiplyResultMemoryProvided) {
-                delete multiplyResult;
-            }
-        }
-
-        // Explicitly instantiate the solver.
-        template class GmmxxMinMaxLinearEquationSolver<double>;
-    } // namespace solver
-} // namespace storm
diff --git a/src/solver/NativeLinearEquationSolver.cpp b/src/solver/NativeLinearEquationSolver.cpp
index c1f0b9315..97d09b06d 100644
--- a/src/solver/NativeLinearEquationSolver.cpp
+++ b/src/solver/NativeLinearEquationSolver.cpp
@@ -102,7 +102,7 @@ namespace storm {
 
         
         template<typename ValueType>
-        void NativeLinearEquationSolver<ValueType>::solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
+        bool NativeLinearEquationSolver<ValueType>::solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
             bool allocatedAuxStorage = !this->hasAuxMemory(LinearEquationSolverOperation::SolveEquations);
             if (allocatedAuxStorage) {
                 this->allocateAuxMemory(LinearEquationSolverOperation::SolveEquations);
@@ -174,7 +174,7 @@ namespace storm {
                 if (allocatedAuxStorage) {
                     this->deallocateAuxMemory(LinearEquationSolverOperation::SolveEquations);
                 }
-                return converged;
+                return iterationCount < this->getSettings().getMaximalNumberOfIterations();
             }
 
 
diff --git a/src/solver/NativeMinMaxLinearEquationSolver.cpp b/src/solver/NativeMinMaxLinearEquationSolver.cpp
deleted file mode 100644
index ad3512d27..000000000
--- a/src/solver/NativeMinMaxLinearEquationSolver.cpp
+++ /dev/null
@@ -1,222 +0,0 @@
-#include "src/solver/NativeMinMaxLinearEquationSolver.h"
-
-#include <utility>
-
-#include "src/storage/TotalScheduler.h"
-
-#include "src/settings/SettingsManager.h"
-#include "src/settings/modules/NativeEquationSolverSettings.h"
-#include "src/settings/modules/GeneralSettings.h"
-#include "src/utility/vector.h"
-#include "src/solver/NativeLinearEquationSolver.h"
-
-namespace storm {
-    namespace solver {
-        
-        template<typename ValueType>
-        NativeMinMaxLinearEquationSolver<ValueType>::NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, MinMaxTechniqueSelection preferredTechnique, bool trackScheduler) :  MinMaxLinearEquationSolver<ValueType>(A, storm::settings::nativeEquationSolverSettings().getPrecision(), storm::settings::nativeEquationSolverSettings().getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative, storm::settings::nativeEquationSolverSettings().getMaximalIterationCount(), trackScheduler, preferredTechnique) {
-            // Intentionally left empty.
-        }
-        
-        template<typename ValueType>
-		NativeMinMaxLinearEquationSolver<ValueType>::NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative, bool trackScheduler) : MinMaxLinearEquationSolver<ValueType>(A, precision, relative, maximalNumberOfIterations, trackScheduler, tech) {
-            // Intentionally left empty.
-        }
-        
-        template<typename ValueType>
-        void NativeMinMaxLinearEquationSolver<ValueType>::solveEquationSystem(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const {
-			if (this->useValueIteration) {
-				// Set up the environment for the power method. If scratch memory was not provided, we need to create it.
-				bool multiplyResultMemoryProvided = true;
-				if (multiplyResult == nullptr) {
-					multiplyResult = new std::vector<ValueType>(this->A.getRowCount());
-					multiplyResultMemoryProvided = false;
-				}
-				std::vector<ValueType>* currentX = &x;
-				bool xMemoryProvided = true;
-				if (newX == nullptr) {
-					newX = new std::vector<ValueType>(x.size());
-					xMemoryProvided = false;
-				}
-                                
-				uint_fast64_t iterations = 0;
-				bool converged = false;
-
-				// Keep track of which of the vectors for x is the auxiliary copy.
-				std::vector<ValueType>* copyX = newX;
-
-				// Proceed with the iterations as long as the method did not converge or reach the
-				// user-specified maximum number of iterations.
-				while (!converged && iterations < this->maximalNumberOfIterations && (!this->hasCustomTerminationCondition() || this->getTerminationCondition().terminateNow(*currentX))) {
-					// Compute x' = A*x + b.
-					this->A.multiplyWithVector(*currentX, *multiplyResult);
-					storm::utility::vector::addVectors(*multiplyResult, b, *multiplyResult);
-
-					// Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost
-					// element of the min/max operator stack.
-					storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, this->A.getRowGroupIndices());
-					
-					// Determine whether the method converged.
-					converged = storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *newX, static_cast<ValueType>(this->precision), this->relative);
-
-					// Update environment variables.
-					std::swap(currentX, newX);
-					++iterations;
-				}
-
-				// Check if the solver converged and issue a warning otherwise.
-				if (converged) {
-					STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations.");
-				} else {
-					STORM_LOG_WARN("Iterative solver did not converge after " << iterations << " iterations.");
-				}
-
-				// If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result
-				// is currently stored in currentX, but x is the output vector.
-				if (currentX == copyX) {
-					std::swap(x, *currentX);
-				}
-
-                if(this->trackScheduler){
-                    if(iterations==0){ //may happen due to early termination. Then we need to compute x'= A*x+b
-                        this->A.multiplyWithVector(x, *multiplyResult);
-                        storm::utility::vector::addVectors(*multiplyResult, b, *multiplyResult);
-                    }
-                    std::vector<uint_fast64_t> choices(x.size());
-                    storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, x, this->A.getRowGroupIndices(), &(choices));
-                    this->scheduler = std::make_unique<storm::storage::TotalScheduler>(std::move(choices));
-                }
-                
-				if (!xMemoryProvided) {
-					delete copyX;
-				}
-
-				if (!multiplyResultMemoryProvided) {
-					delete multiplyResult;
-				}
-                                
-			} else {
-				// We will use Policy Iteration to solve the given system.
-				// We first guess an initial choice resolution which will be refined after each iteration.
-				std::vector<storm::storage::sparse::state_type> scheduler(this->A.getRowGroupIndices().size() - 1);
-
-				// Create our own multiplyResult for solving the deterministic sub-instances.
-				std::vector<ValueType> deterministicMultiplyResult(this->A.getRowGroupIndices().size() - 1);
-				std::vector<ValueType> subB(this->A.getRowGroupIndices().size() - 1);
-
-				// Check whether intermediate storage was provided and create it otherwise.
-				bool multiplyResultMemoryProvided = true;
-				if (multiplyResult == nullptr) {
-					multiplyResult = new std::vector<ValueType>(b.size());
-					multiplyResultMemoryProvided = false;
-				}
-
-				std::vector<ValueType>* currentX = &x;
-				bool xMemoryProvided = true;
-				if (newX == nullptr) {
-					newX = new std::vector<ValueType>(x.size());
-					xMemoryProvided = false;
-				}
-
-				uint_fast64_t iterations = 0;
-				bool converged = false;
-
-				// Keep track of which of the vectors for x is the auxiliary copy.
-				std::vector<ValueType>* copyX = newX;
-
-				// Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number
-				// of iterations.
-				while (!converged && iterations < this->maximalNumberOfIterations && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) {
-					// Take the sub-matrix according to the current choices
-					storm::storage::SparseMatrix<ValueType> submatrix = this->A.selectRowsFromRowGroups(scheduler, true);
-					submatrix.convertToEquationSystem();
-
-					NativeLinearEquationSolver<ValueType> nativeLinearEquationSolver(submatrix);
-					storm::utility::vector::selectVectorValues<ValueType>(subB, scheduler, this->A.getRowGroupIndices(), b);
-
-					// Copy X since we will overwrite it
-					std::copy(currentX->begin(), currentX->end(), newX->begin());
-
-					// Solve the resulting linear equation system of the sub-instance for x under the current choices
-					nativeLinearEquationSolver.solveEquationSystem(*newX, subB, &deterministicMultiplyResult);
-
-					// Compute x' = A*x + b. This step is necessary to allow the choosing of the optimal policy for the next iteration.
-					this->A.multiplyWithVector(*newX, *multiplyResult);
-					storm::utility::vector::addVectors(*multiplyResult, b, *multiplyResult);
-
-					// Reduce the vector x by applying min/max over all nondeterministic choices.
-					// Here, we capture which choice was taken in each state, thereby refining our initial guess.
-					storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, this->A.getRowGroupIndices(), &(scheduler));
-					
-
-					// Determine whether the method converged.
-					converged = storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *newX, static_cast<ValueType>(this->precision), this->relative);
-
-					// Update environment variables.
-					std::swap(currentX, newX);
-					++iterations;
-				}
-
-				// Check if the solver converged and issue a warning otherwise.
-				if (converged) {
-					STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations.");
-				} else {
-					STORM_LOG_WARN("Iterative solver did not converge after " << iterations << " iterations.");
-				}
-
-                // If requested, we store the scheduler for retrieval.
-                if (this->isTrackSchedulerSet()) {
-                    this->scheduler = std::make_unique<storm::storage::TotalScheduler>(std::move(scheduler));
-                }
-                
-				// If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result
-				// is currently stored in currentX, but x is the output vector.
-				if (currentX == copyX) {
-					std::swap(x, *currentX);
-				}
-
-				if (!xMemoryProvided) {
-					delete copyX;
-				}
-
-				if (!multiplyResultMemoryProvided) {
-					delete multiplyResult;
-				}
-			}
-        }
-        
-        template<typename ValueType>
-        void NativeMinMaxLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
-            
-            // If scratch memory was not provided, we need to create it.
-            bool multiplyResultMemoryProvided = true;
-            if (multiplyResult == nullptr) {
-                multiplyResult = new std::vector<ValueType>(this->A.getRowCount());
-                multiplyResultMemoryProvided = false;
-            }
-
-            // Now perform matrix-vector multiplication as long as we meet the bound of the formula.
-            for (uint_fast64_t i = 0; i < n; ++i) {
-                this->A.multiplyWithVector(x, *multiplyResult);
-                
-                // Add b if it is non-null.
-                if (b != nullptr) {
-                    storm::utility::vector::addVectors(*multiplyResult, *b, *multiplyResult);
-                }
-                
-                // Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost
-                // element of the min/max operator stack.
-                storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, x, this->A.getRowGroupIndices());
-                
-            }
-            
-            if (!multiplyResultMemoryProvided) {
-                delete multiplyResult;
-            }
-        }
-        
-        // Explicitly instantiate the solver.
-        template class NativeMinMaxLinearEquationSolver<double>;
-		template class NativeMinMaxLinearEquationSolver<float>;
-    } // namespace solver
-} // namespace storm
diff --git a/src/solver/Smt2SmtSolver.cpp b/src/solver/Smt2SmtSolver.cpp
index a04e13148..229fcb351 100644
--- a/src/solver/Smt2SmtSolver.cpp
+++ b/src/solver/Smt2SmtSolver.cpp
@@ -91,7 +91,7 @@ namespace storm {
         void Smt2SmtSolver::add(storm::RationalFunction const& leftHandSide, storm::CompareRelation const& relation, storm::RationalFunction const& rightHandSide) {
             STORM_LOG_THROW(useCarlExpressions, storm::exceptions::IllegalFunctionCallException, "This solver was initialized without allowing carl expressions");
             //if some of the occurring variables are not declared yet, we will have to.
-            std::set<storm::Variable> variables;
+            std::set<storm::RationalFunctionVariable> variables;
             leftHandSide.gatherVariables(variables);
             rightHandSide.gatherVariables(variables);
             std::vector<std::string> const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables);
@@ -107,7 +107,7 @@ namespace storm {
         
         void Smt2SmtSolver::add(storm::ArithConstraint<storm::RawPolynomial> const& constraint) {
             //if some of the occurring variables are not declared yet, we will have to.
-            std::set<storm::Variable> variables = constraint.lhs().gatherVariables();
+            std::set<storm::RationalFunctionVariable> variables = constraint.lhs().gatherVariables();
             std::vector<std::string> const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables);
             for (auto declaration : varDeclarations){
                 writeCommand(declaration, true);
@@ -118,7 +118,7 @@ namespace storm {
         void Smt2SmtSolver::add(storm::RationalFunctionVariable const& guard, typename storm::ArithConstraint<storm::Polynomial> const& constraint){
             STORM_LOG_THROW((guard.getType()==carl::VariableType::VT_BOOL), storm::exceptions::IllegalArgumentException, "Tried to add a guarded constraint, but the guard is not of type bool.");
             //if some of the occurring variables are not declared yet, we will have to (including the guard!).
-            std::set<storm::Variable> variables = constraint.lhs().gatherVariables();
+            std::set<storm::RationalFunctionVariable> variables = constraint.lhs().gatherVariables();
             variables.insert(guard);
             std::vector<std::string> const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables);
             for (auto declaration : varDeclarations){
@@ -130,7 +130,7 @@ namespace storm {
         
         void Smt2SmtSolver::add(const storm::RationalFunctionVariable& variable, bool value){
             STORM_LOG_THROW((variable.getType()==carl::VariableType::VT_BOOL), storm::exceptions::IllegalArgumentException, "Tried to add a constraint that consists of a non-boolean variable.");
-            std::set<storm::Variable> variableSet;
+            std::set<storm::RationalFunctionVariable> variableSet;
             variableSet.insert(variable);
             std::vector<std::string> const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variableSet);
             for (auto declaration : varDeclarations){
@@ -184,7 +184,7 @@ namespace storm {
 #endif
 
         void Smt2SmtSolver::init() {
-            if (storm::settings::smt2SmtSolverSettings().isSolverCommandSet()){
+            if (storm::settings::getModule<storm::settings::modules::Smt2SmtSolverSettings>().isSolverCommandSet()){
 #ifdef WINDOWS
                 STORM_LOG_WARN("opening a thread for the smt solver is not implemented on Windows. Hence, no actual solving will be done")
 #else
@@ -193,7 +193,7 @@ namespace storm {
                 
                 //for executing the solver we will need the path to the executable file as well as the arguments as a char* array
                 //where the first argument is the path to the executable file and the last is NULL
-                const std::string cmdString = storm::settings::smt2SmtSolverSettings().getSolverCommand();
+                const std::string cmdString = storm::settings::getModule<storm::settings::modules::Smt2SmtSolverSettings>().getSolverCommand();
                 std::vector<std::string> solverCommandVec;
                 boost::split(solverCommandVec, cmdString, boost::is_any_of("\t "));
                 char** solverArgs = new char* [solverCommandVec.size()+1];
@@ -243,9 +243,9 @@ namespace storm {
                 STORM_LOG_WARN("No SMT-LIBv2 Solver Command specified, which means that no actual SMT solving can be done");
             }
 
-            if (storm::settings::smt2SmtSolverSettings().isExportSmtLibScriptSet()){
+            if (storm::settings::getModule<storm::settings::modules::Smt2SmtSolverSettings>().isExportSmtLibScriptSet()){
                 STORM_LOG_DEBUG("The SMT-LIBv2 commands are exportet to the given file");
-                commandFile.open(storm::settings::smt2SmtSolverSettings().getExportSmtLibScriptPath(), std::ios::trunc);
+                commandFile.open(storm::settings::getModule<storm::settings::modules::Smt2SmtSolverSettings>().getExportSmtLibScriptPath(), std::ios::trunc);
                 isCommandFileOpen=commandFile.is_open();
                 STORM_LOG_THROW(isCommandFileOpen, storm::exceptions::InvalidArgumentException, "The file where the smt2commands should be written to could not be opened");
             }
diff --git a/src/solver/StandardMinMaxLinearEquationSolver.cpp b/src/solver/StandardMinMaxLinearEquationSolver.cpp
index 1a1f1fcda..ba0bf43f9 100644
--- a/src/solver/StandardMinMaxLinearEquationSolver.cpp
+++ b/src/solver/StandardMinMaxLinearEquationSolver.cpp
@@ -84,15 +84,17 @@ namespace storm {
         }
         
         template<typename ValueType>
-        void StandardMinMaxLinearEquationSolver<ValueType>::solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
+        bool StandardMinMaxLinearEquationSolver<ValueType>::solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
             switch (this->getSettings().getSolutionMethod()) {
-                case StandardMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration: solveEquationsValueIteration(dir, x, b); break;
-                case StandardMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration: solveEquationsPolicyIteration(dir, x, b); break;
+                case StandardMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration:
+                    return solveEquationsValueIteration(dir, x, b);
+                case StandardMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration:
+                    return solveEquationsPolicyIteration(dir, x, b);
             }
         }
         
         template<typename ValueType>
-        void StandardMinMaxLinearEquationSolver<ValueType>::solveEquationsPolicyIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
+        bool StandardMinMaxLinearEquationSolver<ValueType>::solveEquationsPolicyIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
             // Create the initial scheduler.
             std::vector<storm::storage::sparse::state_type> scheduler(this->A.getRowGroupCount());
             
@@ -163,6 +165,12 @@ namespace storm {
             if (this->isTrackSchedulerSet()) {
                 this->scheduler = std::make_unique<storm::storage::TotalScheduler>(std::move(scheduler));
             }
+
+            if(status == Status::Converged || status == Status::TerminatedEarly) {
+                return true;
+            } else{
+                return false;
+            }
         }
         
         template<typename ValueType>
@@ -181,7 +189,7 @@ namespace storm {
         }
         
         template<typename ValueType>
-        void StandardMinMaxLinearEquationSolver<ValueType>::solveEquationsValueIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
+        bool StandardMinMaxLinearEquationSolver<ValueType>::solveEquationsValueIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
             std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory->create(A);
             bool allocatedAuxMemory = !this->hasAuxMemory(MinMaxLinearEquationSolverOperation::SolveEquations);
             if (allocatedAuxMemory) {
@@ -225,6 +233,12 @@ namespace storm {
             if (allocatedAuxMemory) {
                 this->deallocateAuxMemory(MinMaxLinearEquationSolverOperation::SolveEquations);
             }
+
+            if(status == Status::Converged || status == Status::TerminatedEarly) {
+                return true;
+            } else{
+                return false;
+            }
         }
         
         template<typename ValueType>
diff --git a/src/solver/StandardMinMaxLinearEquationSolver.h b/src/solver/StandardMinMaxLinearEquationSolver.h
index 0c0b37f79..5ad43347d 100644
--- a/src/solver/StandardMinMaxLinearEquationSolver.h
+++ b/src/solver/StandardMinMaxLinearEquationSolver.h
@@ -38,7 +38,7 @@ namespace storm {
             StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, StandardMinMaxLinearEquationSolverSettings<ValueType> const& settings = StandardMinMaxLinearEquationSolverSettings<ValueType>());
             StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, StandardMinMaxLinearEquationSolverSettings<ValueType> const& settings = StandardMinMaxLinearEquationSolverSettings<ValueType>());
             
-            virtual void solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
+            virtual bool solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
             virtual void repeatedMultiply(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n) const override;
 
             StandardMinMaxLinearEquationSolverSettings<ValueType> const& getSettings() const;
@@ -49,8 +49,8 @@ namespace storm {
             virtual bool hasAuxMemory(MinMaxLinearEquationSolverOperation operation) const override;
             
         private:
-            void solveEquationsPolicyIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
-            void solveEquationsValueIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
+            bool solveEquationsPolicyIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
+            bool solveEquationsValueIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
 
             bool valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const;
             
diff --git a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp
index 909c41c30..3b17ec77e 100644
--- a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp
+++ b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp
@@ -33,7 +33,7 @@ namespace storm {
         }
                 
         template<typename ValueType>
-		void TopologicalMinMaxLinearEquationSolver<ValueType>::solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
+		bool TopologicalMinMaxLinearEquationSolver<ValueType>::solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
 			
 #ifdef GPU_USE_FLOAT
 #define __FORCE_FLOAT_CALCULATION true
@@ -49,12 +49,12 @@ namespace storm {
 				std::vector<float> new_x = storm::utility::vector::toValueType<float>(x);
 				std::vector<float> const new_b = storm::utility::vector::toValueType<float>(b);
 
-				newSolver.solveEquations(dir, new_x, new_b);
+				bool callConverged = newSolver.solveEquations(dir, new_x, new_b);
 
 				for (size_t i = 0, size = new_x.size(); i < size; ++i) {
 					x.at(i) = new_x.at(i);
 				}
-				return;
+				return callConverged;
 			}
 			
 			// For testing only
@@ -280,6 +280,8 @@ namespace storm {
 				} else {
 					STORM_LOG_WARN("Iterative solver did not converged after " << currentMaxLocalIterations << " iterations.");
 				}
+
+				return converged;
 			}
         }
 
diff --git a/src/solver/TopologicalMinMaxLinearEquationSolver.h b/src/solver/TopologicalMinMaxLinearEquationSolver.h
index 5eac4a976..347675447 100644
--- a/src/solver/TopologicalMinMaxLinearEquationSolver.h
+++ b/src/solver/TopologicalMinMaxLinearEquationSolver.h
@@ -32,7 +32,7 @@ namespace storm {
              */
             TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, double precision = 1e-6, uint_fast64_t maximalNumberOfIterations = 20000, bool relative = true);
                         
-            virtual void solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
+            virtual bool solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
             
             virtual void repeatedMultiply(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n) const override;
 
diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp
index 3513c8f79..71d56cd63 100644
--- a/src/utility/constants.cpp
+++ b/src/utility/constants.cpp
@@ -50,12 +50,7 @@ namespace storm {
         bool isZero(storm::RationalNumber const& a) {
             return carl::isZero(a);
         }
-        
-        template<>
-        storm::RationalNumber infinity() {
-            // FIXME: this should be treated more properly.
-            return storm::RationalNumber(-1);
-        }
+
         
         template<>
         bool isOne(storm::RationalFunction const& a) {
@@ -277,7 +272,7 @@ namespace storm {
         template bool isOne(storm::RationalNumber const& value);
         template bool isZero(storm::RationalNumber const& value);
         template bool isConstant(storm::RationalNumber const& value);
-        
+
         template storm::RationalNumber one();
         template storm::RationalNumber zero();
         template storm::RationalNumber infinity();
@@ -308,10 +303,6 @@ namespace storm {
         template RationalFunction simplify(RationalFunction value);
         template RationalFunction& simplify(RationalFunction& value);
         template RationalFunction&& simplify(RationalFunction&& value);
-
-        template RationalNumber one();
-        template RationalNumber zero();
-        template RationalNumber infinity();
         
         template Polynomial one();
         template Polynomial zero();