diff --git a/resources/3rdparty/cudd-3.0.0/configure b/resources/3rdparty/cudd-3.0.0/configure
index f0e0e742e..1494802d5 100755
--- a/resources/3rdparty/cudd-3.0.0/configure
+++ b/resources/3rdparty/cudd-3.0.0/configure
@@ -4419,6 +4419,7 @@ else
 fi
 
 
+
 ac_ext=cpp
 ac_cpp='$CXXCPP $CPPFLAGS'
 ac_compile='$CXX -c $CXXFLAGS $CPPFLAGS conftest.$ac_ext >&5'
diff --git a/resources/3rdparty/sylvan/CMakeLists.txt b/resources/3rdparty/sylvan/CMakeLists.txt
index 27762655b..d9999a0f3 100644
--- a/resources/3rdparty/sylvan/CMakeLists.txt
+++ b/resources/3rdparty/sylvan/CMakeLists.txt
@@ -2,8 +2,8 @@ cmake_minimum_required(VERSION 2.6)
 project(sylvan C CXX)
 enable_testing()
 
-set(CMAKE_C_FLAGS "-O3 -Wextra -Wall -Werror -fno-strict-aliasing -std=gnu11")
-set(CMAKE_CXX_FLAGS "-O3 -Wextra -Wall -Werror -fno-strict-aliasing -Wno-deprecated-register -std=gnu++11")
+set(CMAKE_C_FLAGS "-O3 -Wextra -Wall -Werror -fno-strict-aliasing -std=gnu11 -fPIC")
+set(CMAKE_CXX_FLAGS "-O3 -Wextra -Wall -Werror -fno-strict-aliasing -Wno-deprecated-register -std=gnu++11 -fPIC")
 
 option(WITH_COVERAGE "Add generation of test coverage" OFF)
 if(WITH_COVERAGE)
diff --git a/src/adapters/EigenAdapter.cpp b/src/adapters/EigenAdapter.cpp
index 15be8c6ac..350ca8e20 100644
--- a/src/adapters/EigenAdapter.cpp
+++ b/src/adapters/EigenAdapter.cpp
@@ -24,4 +24,4 @@ namespace storm {
         template std::unique_ptr<Eigen::SparseMatrix<storm::RationalNumber>> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix<storm::RationalNumber> const& matrix);
         template std::unique_ptr<Eigen::SparseMatrix<storm::RationalFunction>> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix<storm::RationalFunction> const& matrix);
     }
-}
\ No newline at end of file
+}
diff --git a/src/generator/VariableInformation.cpp b/src/generator/VariableInformation.cpp
index b009f849f..b329cd42f 100644
--- a/src/generator/VariableInformation.cpp
+++ b/src/generator/VariableInformation.cpp
@@ -6,6 +6,8 @@
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidArgumentException.h"
 
+#include <cmath>
+
 namespace storm {
     namespace generator {
         
@@ -97,4 +99,4 @@ namespace storm {
             std::sort(integerVariables.begin(), integerVariables.end(), [] (IntegerVariableInformation const& a, IntegerVariableInformation const& b) { return a.variable < b.variable; });
         }
     }
-}
\ No newline at end of file
+}
diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
index f5a057d6f..1dbe8fcde 100644
--- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
+++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
@@ -189,18 +189,12 @@ namespace storm {
                 
                 return result;
             }
-
+            
             template <typename ValueType>
             std::vector<ValueType> SparseCtmcCslHelper<ValueType>::computeUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
                 return SparseDtmcPrctlHelper<ValueType>::computeUntilProbabilities(computeProbabilityMatrix(rateMatrix, exitRateVector), backwardTransitions, phiStates, psiStates, qualitative, linearEquationSolverFactory);
             }
             
-            template <typename ValueType>
-            std::vector<ValueType> SparseCtmcCslHelper<ValueType>::computeUntilProbabilitiesElimination(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) {
-                // Use "normal" function again, if RationalFunction finally is supported.
-                return storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ValueType>>::computeUntilProbabilities(computeProbabilityMatrix(rateMatrix, exitRateVector), backwardTransitions, initialStates, phiStates, psiStates, false);
-            }
-
             template <typename ValueType>
             std::vector<ValueType> SparseCtmcCslHelper<ValueType>::computeNextProbabilities(storm::storage::SparseMatrix<ValueType> const& rateMatrix, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
                 return SparseDtmcPrctlHelper<ValueType>::computeNextProbabilities(computeProbabilityMatrix(rateMatrix, exitRateVector), nextStates, linearEquationSolverFactory);
@@ -322,7 +316,7 @@ namespace storm {
                 
                 // Initialize result to state rewards of the this->getModel().
                 std::vector<ValueType> result(rewardModel.getStateRewardVector());
-
+                
                 // If the time-bound is not zero, we need to perform a transient analysis.
                 if (timeBound > 0) {
                     ValueType uniformizationRate = 0;
@@ -344,7 +338,7 @@ namespace storm {
             std::vector<ValueType> SparseCtmcCslHelper<ValueType>::computeCumulativeRewards(storm::storage::SparseMatrix<ValueType> const& rateMatrix, std::vector<ValueType> const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
                 // Only compute the result if the model has a state-based reward this->getModel().
                 STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
-                                
+                
                 uint_fast64_t numberOfStates = rateMatrix.getRowCount();
                 
                 // If the time bound is zero, the result is the constant zero vector.
@@ -363,19 +357,19 @@ namespace storm {
                 STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive.");
                 
                 storm::storage::SparseMatrix<ValueType> uniformizedMatrix = computeUniformizedMatrix(rateMatrix, storm::storage::BitVector(numberOfStates, true), uniformizationRate, exitRateVector);
-
+                
                 // Compute the total state reward vector.
                 std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, exitRateVector);
                 
                 // Finally, compute the transient probabilities.
                 return computeTransientProbabilities<true>(uniformizedMatrix, nullptr, timeBound, uniformizationRate, totalRewardVector, linearEquationSolverFactory);
             }
-
+            
             template <typename ValueType>
             template <typename RewardModelType>
             std::vector<ValueType> SparseCtmcCslHelper<ValueType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
                 STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
-
+                
                 storm::storage::SparseMatrix<ValueType> probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector);
                 
                 std::vector<ValueType> totalRewardVector;
@@ -430,7 +424,7 @@ namespace storm {
                 
                 return generatorMatrix;
             }
-
+            
             template <typename ValueType>
             std::vector<ValueType> SparseCtmcCslHelper<ValueType>::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<ValueType> const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
                 // If there are no goal states, we avoid the computation and directly return zero.
@@ -654,12 +648,12 @@ namespace storm {
                 
                 return result;
             }
-
+            
             template <typename ValueType>
             std::vector<ValueType> SparseCtmcCslHelper<ValueType>::computeReachabilityTimes(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
                 // Compute expected time on CTMC by reduction to DTMC with rewards.
                 storm::storage::SparseMatrix<ValueType> probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector);
-
+                
                 // Initialize rewards.
                 std::vector<ValueType> totalRewardVector;
                 for (size_t i = 0; i < exitRateVector.size(); ++i) {
@@ -671,42 +665,17 @@ namespace storm {
                         totalRewardVector.push_back(storm::utility::one<ValueType>() / exitRateVector[i]);
                     }
                 }
-
+                
                 return storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeReachabilityRewards(probabilityMatrix, backwardTransitions, totalRewardVector, targetStates, qualitative, linearEquationSolverFactory);
             }
-
             
-            template <typename ValueType>
-            std::vector<ValueType> SparseCtmcCslHelper<ValueType>::computeReachabilityTimesElimination(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative) {
-                // Use "normal" function again, if RationalFunction finally is supported.
-                // Compute expected time on CTMC by reduction to DTMC with rewards.
-                storm::storage::SparseMatrix<ValueType> probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector);
-
-                // Initialize rewards.
-                std::vector<ValueType> totalRewardVector;
-                for (size_t i = 0; i < exitRateVector.size(); ++i) {
-                    if (targetStates[i] || storm::utility::isZero(exitRateVector[i])) {
-                        // Set reward for target states or states without outgoing transitions to 0.
-                        totalRewardVector.push_back(storm::utility::zero<ValueType>());
-                    } else {
-                        // Reward is (1 / exitRate).
-                        totalRewardVector.push_back(storm::utility::one<ValueType>() / exitRateVector[i]);
-                    }
-                }
-
-                return storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ValueType>>::computeReachabilityRewards(probabilityMatrix, backwardTransitions, initialStates, targetStates, totalRewardVector, false);
-            }
-
             template class SparseCtmcCslHelper<double>;
             template std::vector<double> SparseCtmcCslHelper<double>::computeInstantaneousRewards(storm::storage::SparseMatrix<double> const& rateMatrix, std::vector<double> const& exitRateVector, storm::models::sparse::StandardRewardModel<double> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
             template std::vector<double> SparseCtmcCslHelper<double>::computeCumulativeRewards(storm::storage::SparseMatrix<double> const& rateMatrix, std::vector<double> const& exitRateVector, storm::models::sparse::StandardRewardModel<double> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
             template std::vector<double> SparseCtmcCslHelper<double>::computeReachabilityRewards(storm::storage::SparseMatrix<double> const& rateMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, std::vector<double> const& exitRateVector, storm::models::sparse::StandardRewardModel<double> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
-
-            template std::vector<storm::RationalNumber> SparseCtmcCslHelper<storm::RationalNumber>::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<storm::RationalNumber> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<storm::RationalNumber> const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
-
             
-            template std::vector<storm::RationalFunction> SparseCtmcCslHelper<storm::RationalFunction>::computeUntilProbabilitiesElimination(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative);
-            template std::vector<storm::RationalFunction> SparseCtmcCslHelper<storm::RationalFunction>::computeReachabilityTimesElimination(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative);
+            
+            template std::vector<storm::RationalNumber> SparseCtmcCslHelper<storm::RationalNumber>::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<storm::RationalNumber> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<storm::RationalNumber> const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
             template std::vector<storm::RationalFunction> SparseCtmcCslHelper<storm::RationalFunction>::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<storm::RationalFunction> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<storm::RationalFunction> const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
         }
     }
diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.h b/src/modelchecker/csl/helper/SparseCtmcCslHelper.h
index 8485b2501..2bbb6a3c8 100644
--- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.h
+++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.h
@@ -16,7 +16,6 @@ namespace storm {
                 static std::vector<ValueType> computeNextProbabilities(storm::storage::SparseMatrix<ValueType> const& rateMatrix, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
                 
                 static std::vector<ValueType> computeUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
-                static std::vector<ValueType> computeUntilProbabilitiesElimination(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative);
                 
                 template <typename RewardModelType>
                 static std::vector<ValueType> computeInstantaneousRewards(storm::storage::SparseMatrix<ValueType> const& rateMatrix, std::vector<ValueType> const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
@@ -30,7 +29,6 @@ namespace storm {
                 static std::vector<ValueType> computeLongRunAverageProbabilities(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<ValueType> const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
                 
                 static std::vector<ValueType> computeReachabilityTimes(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
-                static std::vector<ValueType> computeReachabilityTimesElimination(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative);
 
                 /*!
                  * Computes the matrix representing the transitions of the uniformized CTMC.
diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
index 1f3067253..9d774a6ec 100644
--- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
+++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
@@ -432,15 +432,11 @@ namespace storm {
             storm::storage::BitVector const& phiStates = leftResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
             storm::storage::BitVector const& psiStates = rightResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
             
-            std::vector<ValueType> result = computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), phiStates, psiStates, checkTask.isOnlyInitialStatesRelevantSet());
-            
-            // Construct check result.
-            std::unique_ptr<CheckResult> checkResult(new ExplicitQuantitativeCheckResult<ValueType>(result));
-            return checkResult;
+            return computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), phiStates, psiStates, checkTask.isOnlyInitialStatesRelevantSet());
         }
         
         template<typename SparseDtmcModelType>
-        std::vector<typename SparseDtmcModelType::ValueType> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool computeForInitialStatesOnly) {
+        std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool computeForInitialStatesOnly) {
             
             // Then, compute the subset of states that has a probability of 0 or 1, respectively.
             std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates);
@@ -491,9 +487,13 @@ namespace storm {
             if (computeForInitialStatesOnly) {
                 // If we computed the results for the initial (and prob 0 and prob1) states only, we need to filter the
                 // result to only communicate these results.
-                result = storm::utility::vector::filterVector(result, ~maybeStates | initialStates);
+                std::unique_ptr<ExplicitQuantitativeCheckResult<ValueType>> checkResult = std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>();
+                for (auto state : ~maybeStates | initialStates) {
+                    (*checkResult)[state] = result[state];
+                }
+                return std::move(checkResult);
             }
-            return result;
+            return std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>(result);
         }
         
         template<typename SparseDtmcModelType>
@@ -509,19 +509,16 @@ namespace storm {
             RewardModelType const& rewardModel = this->getModel().getRewardModel(checkTask.isRewardModelSet() ? checkTask.getRewardModel() : "");
             
             STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::IllegalArgumentException, "Input model does not have a reward model.");
-            std::vector<ValueType> result = computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), targetStates,
-                                                                       [&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates) {
-                                                                           return rewardModel.getTotalRewardVector(numberOfRows, transitionMatrix, maybeStates);
-                                                                       },
-                                                                       checkTask.isOnlyInitialStatesRelevantSet());
+            return computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), targetStates,
+                                              [&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates) {
+                                                  return rewardModel.getTotalRewardVector(numberOfRows, transitionMatrix, maybeStates);
+                                              },
+                                              checkTask.isOnlyInitialStatesRelevantSet());
             
-            // Construct check result.
-            std::unique_ptr<CheckResult> checkResult(new ExplicitQuantitativeCheckResult<ValueType>(result));
-            return checkResult;
         }
         
         template<typename SparseDtmcModelType>
-        std::vector<typename SparseDtmcModelType::ValueType> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::vector<ValueType>& stateRewardValues, bool computeForInitialStatesOnly) {
+        std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::vector<ValueType>& stateRewardValues, bool computeForInitialStatesOnly) {
             return computeReachabilityRewards(probabilityMatrix, backwardTransitions, initialStates, targetStates,
                                               [&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates) {
                                                   std::vector<ValueType> result(numberOfRows);
@@ -532,7 +529,7 @@ namespace storm {
         }
         
         template<typename SparseDtmcModelType>
-        std::vector<typename SparseDtmcModelType::ValueType> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, bool computeForInitialStatesOnly) {
+        std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, bool computeForInitialStatesOnly) {
             
             uint_fast64_t numberOfStates = probabilityMatrix.getRowCount();
             
@@ -587,9 +584,13 @@ namespace storm {
             if (computeForInitialStatesOnly) {
                 // If we computed the results for the initial (and inf) states only, we need to filter the result to
                 // only communicate these results.
-                result = storm::utility::vector::filterVector(result, ~maybeStates | initialStates);
+                std::unique_ptr<ExplicitQuantitativeCheckResult<ValueType>> checkResult = std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>();
+                for (auto state : ~maybeStates | initialStates) {
+                    (*checkResult)[state] = result[state];
+                }
+                return std::move(checkResult);
             }
-            return result;
+            return std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>(result);
         }
         
         template<typename SparseDtmcModelType>
diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
index 8459d4bf3..e1ec35ffa 100644
--- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
+++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
@@ -39,14 +39,14 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
            
             // Static helper methods 
-            static std::vector<ValueType> computeUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool computeForInitialStatesOnly);
+            static std::unique_ptr<CheckResult> computeUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool computeForInitialStatesOnly);
 
-            static std::vector<ValueType> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::vector<ValueType>& stateRewardValues, bool computeForInitialStatesOnly);
+            static std::unique_ptr<CheckResult> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::vector<ValueType>& stateRewardValues, bool computeForInitialStatesOnly);
 
         private:
             static std::vector<ValueType> computeLongRunValues(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& maybeStates, bool computeResultsForInitialStatesOnly, std::vector<ValueType>& stateValues);
             
-            static std::vector<ValueType> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, bool computeForInitialStatesOnly);
+            static std::unique_ptr<CheckResult> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, bool computeForInitialStatesOnly);
 
             static std::vector<ValueType> computeReachabilityValues(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& values, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<ValueType> const& oneStepProbabilitiesToTarget);
             
diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
index 218af9179..d5385461c 100644
--- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
+++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
@@ -5,6 +5,7 @@
 #include "src/utility/macros.h"
 #include "src/utility/vector.h"
 #include "src/exceptions/InvalidOperationException.h"
+#include "src/exceptions/InvalidAccessException.h"
 #include "src/adapters/CarlAdapter.h"
 
 
@@ -59,7 +60,11 @@ namespace storm {
 
             if (this->isResultForAllStates()) {
                 map_type newMap;
+                std::cout << filterTruthValues << std::endl;
                 for (auto const& element : filterTruthValues) {
+                    std::cout << element << std::endl;
+                    std::cout << this->getValueVector().size() << std::endl;
+                    STORM_LOG_THROW(element < this->getValueVector().size(), storm::exceptions::InvalidAccessException, "Invalid index in results.");
                     newMap.emplace(element, this->getValueVector()[element]);
                 }
                 this->values = newMap;
@@ -251,4 +256,4 @@ namespace storm {
         template class ExplicitQuantitativeCheckResult<storm::RationalNumber>;
         template class ExplicitQuantitativeCheckResult<storm::RationalFunction>;
     }
-}
\ No newline at end of file
+}
diff --git a/src/solver/GlpkLpSolver.cpp b/src/solver/GlpkLpSolver.cpp
index bcf296865..bc7d72a00 100644
--- a/src/solver/GlpkLpSolver.cpp
+++ b/src/solver/GlpkLpSolver.cpp
@@ -17,6 +17,9 @@
 
 #include "src/settings/modules/DebugSettings.h"
 #include "src/settings/modules/GlpkSettings.h"
+
+#include <cmath>
+
 namespace storm {
     namespace solver {
         GlpkLpSolver::GlpkLpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver(optDir), lp(nullptr), variableToIndexMap(), nextVariableIndex(1), nextConstraintIndex(1), modelContainsIntegerVariables(false), isInfeasibleFlag(false), isUnboundedFlag(false), rowIndices(), columnIndices(), coefficientValues() {
@@ -298,7 +301,7 @@ namespace storm {
             }
 
             // Now check the desired precision was actually achieved.
-            STORM_LOG_THROW(std::abs(static_cast<int>(value) - value) <= storm::settings::getModule<storm::settings::modules::GlpkSettings>().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in glpk solution (" << value << ").");
+            STORM_LOG_THROW(std::fabs(static_cast<int>(value) - value) <= storm::settings::getModule<storm::settings::modules::GlpkSettings>().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in glpk solution (" << value << ").");
             
             return static_cast<int_fast64_t>(value);
         }
@@ -320,7 +323,7 @@ namespace storm {
                 value = glp_get_col_prim(this->lp, static_cast<int>(variableIndexPair->second));
             }
 
-            STORM_LOG_THROW(std::abs(static_cast<int>(value) - value) <= storm::settings::getModule<storm::settings::modules::GlpkSettings>().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for binary variable in glpk solution (" << value << ").");
+            STORM_LOG_THROW(std::fabs(static_cast<int>(value) - value) <= storm::settings::getModule<storm::settings::modules::GlpkSettings>().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for binary variable in glpk solution (" << value << ").");
             
             return static_cast<bool>(value);
         }
@@ -349,4 +352,4 @@ namespace storm {
     }
 }
 
-#endif
\ No newline at end of file
+#endif
diff --git a/src/storage/dd/DdManager.cpp b/src/storage/dd/DdManager.cpp
index 74112d393..195565e8f 100644
--- a/src/storage/dd/DdManager.cpp
+++ b/src/storage/dd/DdManager.cpp
@@ -6,6 +6,8 @@
 #include "src/utility/constants.h"
 #include "src/exceptions/InvalidArgumentException.h"
 
+#include <cmath>
+
 namespace storm {
     namespace dd {
         template<DdType LibraryType>
@@ -354,4 +356,4 @@ namespace storm {
         template Add<DdType::Sylvan, double> DdManager<DdType::Sylvan>::getIdentity(storm::expressions::Variable const& variable) const;
         template Add<DdType::Sylvan, uint_fast64_t> DdManager<DdType::Sylvan>::getIdentity(storm::expressions::Variable const& variable) const;
     }
-}
\ No newline at end of file
+}
diff --git a/src/storage/dd/cudd/CuddAddIterator.cpp b/src/storage/dd/cudd/CuddAddIterator.cpp
index e11b75aec..379a0ff22 100644
--- a/src/storage/dd/cudd/CuddAddIterator.cpp
+++ b/src/storage/dd/cudd/CuddAddIterator.cpp
@@ -4,6 +4,8 @@
 #include "src/utility/macros.h"
 #include "src/storage/expressions/ExpressionManager.h"
 
+#include <cmath>
+
 namespace storm {
     namespace dd {
         template<typename ValueType>
@@ -184,4 +186,4 @@ namespace storm {
         template class AddIterator<DdType::CUDD, double>;
         template class AddIterator<DdType::CUDD, uint_fast64_t>;
     }
-}
\ No newline at end of file
+}
diff --git a/src/storage/dd/sylvan/SylvanAddIterator.cpp b/src/storage/dd/sylvan/SylvanAddIterator.cpp
index 4322aa1b6..8c97941a3 100644
--- a/src/storage/dd/sylvan/SylvanAddIterator.cpp
+++ b/src/storage/dd/sylvan/SylvanAddIterator.cpp
@@ -8,6 +8,8 @@
 #include "src/utility/macros.h"
 #include "src/exceptions/NotImplementedException.h"
 
+#include <cmath>
+
 namespace storm {
     namespace dd {
         template<typename ValueType>
@@ -186,4 +188,4 @@ namespace storm {
         template class AddIterator<DdType::Sylvan, double>;
         template class AddIterator<DdType::Sylvan, uint_fast64_t>;
     }
-}
\ No newline at end of file
+}
diff --git a/src/utility/storm.h b/src/utility/storm.h
index 813fb33d4..a623e04b6 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -402,8 +402,8 @@ namespace storm {
                 std::unique_ptr<storm::modelchecker::CheckResult> subResultPointer = propositionalModelchecker.check(eventuallyFormula.getSubformula());
                 storm::storage::BitVector const& targetStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
 
-                std::vector<storm::RationalFunction> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper<storm::RationalFunction>::computeReachabilityTimesElimination(ctmc->getTransitionMatrix(), ctmc->getBackwardTransitions(), ctmc->getExitRateVector(), ctmc->getInitialStates(), targetStates, false);
-                result = std::unique_ptr<storm::modelchecker::CheckResult>(new storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>(std::move(numericResult)));
+//                std::vector<storm::RationalFunction> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper<storm::RationalFunction>::computeReachabilityTimesElimination(ctmc->getTransitionMatrix(), ctmc->getBackwardTransitions(), ctmc->getExitRateVector(), ctmc->getInitialStates(), targetStates, false);
+//                result = std::unique_ptr<storm::modelchecker::CheckResult>(new storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>(std::move(numericResult)));
 
             } else if (formula->isProbabilityOperatorFormula()) {
                 // Compute reachability probability for pCTMCs
@@ -433,8 +433,8 @@ namespace storm {
                     psiStates = resultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
                 }
 
-                std::vector<storm::RationalFunction> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper<storm::RationalFunction>::computeUntilProbabilitiesElimination(ctmc->getTransitionMatrix(), ctmc->getBackwardTransitions(), ctmc->getExitRateVector(), ctmc->getInitialStates(), phiStates, psiStates, false);
-                result = std::unique_ptr<storm::modelchecker::CheckResult>(new storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>(std::move(numericResult)));
+//                std::vector<storm::RationalFunction> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper<storm::RationalFunction>::computeUntilProbabilitiesElimination(ctmc->getTransitionMatrix(), ctmc->getBackwardTransitions(), ctmc->getExitRateVector(), ctmc->getInitialStates(), phiStates, psiStates, false);
+//                result = std::unique_ptr<storm::modelchecker::CheckResult>(new storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>(std::move(numericResult)));
 
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The parametric engine currently does not support this property on CTMCs.");
diff --git a/test/functional/solver/GlpkLpSolverTest.cpp b/test/functional/solver/GlpkLpSolverTest.cpp
index 4aea94cf7..737f8b56e 100644
--- a/test/functional/solver/GlpkLpSolverTest.cpp
+++ b/test/functional/solver/GlpkLpSolverTest.cpp
@@ -13,6 +13,8 @@
 #include "src/storage/expressions/Expressions.h"
 #include "src/solver/OptimizationDirection.h"
 
+#include <cmath>
+
 TEST(GlpkLpSolver, LPOptimizeMax) {
     storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize);
     storm::expressions::Variable x;
@@ -34,16 +36,16 @@ TEST(GlpkLpSolver, LPOptimizeMax) {
     ASSERT_FALSE(solver.isInfeasible());
     double xValue = 0;
     ASSERT_NO_THROW(xValue = solver.getContinuousValue(x));
-    ASSERT_LT(std::abs(xValue - 1), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    ASSERT_LT(std::fabs(xValue - 1), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     double yValue = 0;
     ASSERT_NO_THROW(yValue = solver.getContinuousValue(y));
-    ASSERT_LT(std::abs(yValue - 6.5), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    ASSERT_LT(std::fabs(yValue - 6.5), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     double zValue = 0;
     ASSERT_NO_THROW(zValue = solver.getContinuousValue(z));
-    ASSERT_LT(std::abs(zValue - 2.75), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    ASSERT_LT(std::fabs(zValue - 2.75), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     double objectiveValue = 0;
     ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
-    ASSERT_LT(std::abs(objectiveValue - 14.75), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    ASSERT_LT(std::fabs(objectiveValue - 14.75), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
 }
 
 TEST(GlpkLpSolver, LPOptimizeMin) {
@@ -67,16 +69,16 @@ TEST(GlpkLpSolver, LPOptimizeMin) {
     ASSERT_FALSE(solver.isInfeasible());
     double xValue = 0;
     ASSERT_NO_THROW(xValue = solver.getContinuousValue(x));
-    ASSERT_LT(std::abs(xValue - 1), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    ASSERT_LT(std::fabs(xValue - 1), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     double yValue = 0;
     ASSERT_NO_THROW(yValue = solver.getContinuousValue(y));
-    ASSERT_LT(std::abs(yValue - 0), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    ASSERT_LT(std::fabs(yValue - 0), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     double zValue = 0;
     ASSERT_NO_THROW(zValue = solver.getContinuousValue(z));
-    ASSERT_LT(std::abs(zValue - 5.7), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    ASSERT_LT(std::fabs(zValue - 5.7), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     double objectiveValue = 0;
     ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
-    ASSERT_LT(std::abs(objectiveValue - (-6.7)), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    ASSERT_LT(std::fabs(objectiveValue - (-6.7)), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
 }
 
 TEST(GlpkLpSolver, MILPOptimizeMax) {
@@ -106,10 +108,10 @@ TEST(GlpkLpSolver, MILPOptimizeMax) {
     ASSERT_EQ(6, yValue);
     double zValue = 0;
     ASSERT_NO_THROW(zValue = solver.getContinuousValue(z));
-    ASSERT_LT(std::abs(zValue - 3), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    ASSERT_LT(std::fabs(zValue - 3), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     double objectiveValue = 0;
     ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
-    ASSERT_LT(std::abs(objectiveValue - 14), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    ASSERT_LT(std::fabs(objectiveValue - 14), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
 }
 
 TEST(GlpkLpSolver, MILPOptimizeMin) {
@@ -139,10 +141,10 @@ TEST(GlpkLpSolver, MILPOptimizeMin) {
     ASSERT_EQ(0, yValue);
     double zValue = 0;
     ASSERT_NO_THROW(zValue = solver.getContinuousValue(z));
-    ASSERT_LT(std::abs(zValue - 5), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    ASSERT_LT(std::fabs(zValue - 5), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
     double objectiveValue = 0;
     ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
-    ASSERT_LT(std::abs(objectiveValue - (-6)), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    ASSERT_LT(std::fabs(objectiveValue - (-6)), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
 }
 
 TEST(GlpkLpSolver, LPInfeasible) {
@@ -244,4 +246,4 @@ TEST(GlpkLpSolver, MILPUnbounded) {
     ASSERT_THROW(solver.getContinuousValue(z), storm::exceptions::InvalidAccessException);
     ASSERT_THROW(solver.getObjectiveValue(), storm::exceptions::InvalidAccessException);
 }
-#endif
\ No newline at end of file
+#endif