diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp
index 1e07ccd3e..9dc6de4d6 100644
--- a/src/storm/abstraction/MenuGameRefiner.cpp
+++ b/src/storm/abstraction/MenuGameRefiner.cpp
@@ -120,7 +120,7 @@ namespace storm {
         }
                 
         template<storm::dd::DdType Type, typename ValueType>
-        PivotStateResult<Type, ValueType> pickPivotState(AbstractionSettings::PivotSelectionHeuristic const& heuristic, storm::abstraction::MenuGame<Type, ValueType> const& game, PivotStateCandidatesResult<Type> const& pivotStateCandidateResult, boost::optional<QualitativeResultMinMax<Type>> const& qualitativeResult, boost::optional<QuantitativeResultMinMax<Type, ValueType>> const& quantitativeResult) {
+        PivotStateResult<Type, ValueType> pickPivotState(AbstractionSettings::PivotSelectionHeuristic const& heuristic, storm::abstraction::MenuGame<Type, ValueType> const& game, PivotStateCandidatesResult<Type> const& pivotStateCandidateResult, boost::optional<QualitativeGameResultMinMax<Type>> const& qualitativeResult, boost::optional<QuantitativeGameResultMinMax<Type, ValueType>> const& quantitativeResult) {
             
             // Get easy access to strategies.
             storm::dd::Bdd<Type> minPlayer1Strategy;
@@ -571,7 +571,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType Type, typename ValueType>
-        bool MenuGameRefiner<Type, ValueType>::refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QualitativeResultMinMax<Type> const& qualitativeResult) const {
+        bool MenuGameRefiner<Type, ValueType>::refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QualitativeGameResultMinMax<Type> const& qualitativeResult) const {
             STORM_LOG_TRACE("Trying refinement after qualitative check.");
             // Get all relevant strategies.
             storm::dd::Bdd<Type> minPlayer1Strategy = qualitativeResult.prob0Min.getPlayer1Strategy();
@@ -616,7 +616,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType Type, typename ValueType>
-        bool MenuGameRefiner<Type, ValueType>::refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QuantitativeResultMinMax<Type, ValueType> const& quantitativeResult) const {
+        bool MenuGameRefiner<Type, ValueType>::refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QuantitativeGameResultMinMax<Type, ValueType> const& quantitativeResult) const {
             STORM_LOG_TRACE("Refining after quantitative check.");
             // Get all relevant strategies.
             storm::dd::Bdd<Type> minPlayer1Strategy = quantitativeResult.min.player1Strategy;
diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h
index d5681ff2f..c0a4b8f8a 100644
--- a/src/storm/abstraction/MenuGameRefiner.h
+++ b/src/storm/abstraction/MenuGameRefiner.h
@@ -7,8 +7,8 @@
 #include <boost/optional.hpp>
 
 #include "storm/abstraction/RefinementCommand.h"
-#include "storm/abstraction/QualitativeResultMinMax.h"
-#include "storm/abstraction/QuantitativeResultMinMax.h"
+#include "storm/abstraction/QualitativeGameResultMinMax.h"
+#include "storm/abstraction/QuantitativeGameResultMinMax.h"
 
 #include "storm/storage/expressions/Expression.h"
 #include "storm/storage/expressions/FullPredicateSplitter.h"
@@ -85,14 +85,14 @@ namespace storm {
              *
              * @param True if predicates for refinement could be derived, false otherwise.
              */
-            bool refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QualitativeResultMinMax<Type> const& qualitativeResult) const;
+            bool refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QualitativeGameResultMinMax<Type> const& qualitativeResult) const;
             
             /*!
              * Refines the abstractor based on the quantitative result by trying to derive suitable predicates.
              *
              * @param True if predicates for refinement could be derived, false otherwise.
              */
-            bool refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QuantitativeResultMinMax<Type, ValueType> const& quantitativeResult) const;
+            bool refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QuantitativeGameResultMinMax<Type, ValueType> const& quantitativeResult) const;
             
             /*!
              * Retrieves whether all guards were added.
diff --git a/src/storm/abstraction/QualitativeResult.h b/src/storm/abstraction/QualitativeGameResult.h
similarity index 65%
rename from src/storm/abstraction/QualitativeResult.h
rename to src/storm/abstraction/QualitativeGameResult.h
index 66386e72a..2de6ef0ef 100644
--- a/src/storm/abstraction/QualitativeResult.h
+++ b/src/storm/abstraction/QualitativeGameResult.h
@@ -6,7 +6,7 @@ namespace storm {
     namespace abstraction {
         
         template <storm::dd::DdType Type>
-        using QualitativeResult = storm::utility::graph::GameProb01Result<Type>;
+        using QualitativeGameResult = storm::utility::graph::GameProb01Result<Type>;
         
     }
 }
diff --git a/src/storm/abstraction/QualitativeResultMinMax.h b/src/storm/abstraction/QualitativeGameResultMinMax.h
similarity index 83%
rename from src/storm/abstraction/QualitativeResultMinMax.h
rename to src/storm/abstraction/QualitativeGameResultMinMax.h
index b013c8acb..c028b9ddb 100644
--- a/src/storm/abstraction/QualitativeResultMinMax.h
+++ b/src/storm/abstraction/QualitativeGameResultMinMax.h
@@ -8,9 +8,9 @@ namespace storm {
     namespace abstraction {
 
         template<storm::dd::DdType Type>
-        struct QualitativeResultMinMax {
+        struct QualitativeGameResultMinMax {
         public:
-            QualitativeResultMinMax() = default;
+            QualitativeGameResultMinMax() = default;
             
             storm::utility::graph::GameProb01Result<Type> prob0Min;
             storm::utility::graph::GameProb01Result<Type> prob1Min;
diff --git a/src/storm/abstraction/QualitativeMdpResult.h b/src/storm/abstraction/QualitativeMdpResult.h
new file mode 100644
index 000000000..ce97bd1e2
--- /dev/null
+++ b/src/storm/abstraction/QualitativeMdpResult.h
@@ -0,0 +1,13 @@
+#pragma once
+
+#include "storm/utility/graph.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        template <storm::dd::DdType Type>
+        using QualitativeMdpResult = std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>>;
+        
+    }
+}
+
diff --git a/src/storm/abstraction/QualitativeMdpResultMinMax.h b/src/storm/abstraction/QualitativeMdpResultMinMax.h
new file mode 100644
index 000000000..b701167b2
--- /dev/null
+++ b/src/storm/abstraction/QualitativeMdpResultMinMax.h
@@ -0,0 +1,21 @@
+#pragma once
+
+#include "storm/storage/dd/DdType.h"
+
+#include "storm/abstraction/QualitativeMdpResult.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        template<storm::dd::DdType Type>
+        struct QualitativeMdpResultMinMax {
+        public:
+            QualitativeMdpResultMinMax() = default;
+            
+            QualitativeMdpResult<Type> min;
+            QualitativeMdpResult<Type> max;
+        };
+        
+    }
+}
+
diff --git a/src/storm/abstraction/QuantitativeResult.h b/src/storm/abstraction/QuantitativeGameResult.h
similarity index 55%
rename from src/storm/abstraction/QuantitativeResult.h
rename to src/storm/abstraction/QuantitativeGameResult.h
index f2975067a..accfcb499 100644
--- a/src/storm/abstraction/QuantitativeResult.h
+++ b/src/storm/abstraction/QuantitativeGameResult.h
@@ -8,10 +8,10 @@ namespace storm {
     namespace abstraction {
 
         template<storm::dd::DdType Type, typename ValueType>
-        struct QuantitativeResult {
-            QuantitativeResult() = default;
+        struct QuantitativeGameResult {
+            QuantitativeGameResult() = default;
             
-            QuantitativeResult(std::pair<ValueType, ValueType> initialStatesRange, storm::dd::Add<Type, ValueType> const& values, storm::dd::Bdd<Type> const& player1Strategy, storm::dd::Bdd<Type> const& player2Strategy) : initialStatesRange(initialStatesRange), values(values), player1Strategy(player1Strategy), player2Strategy(player2Strategy) {
+            QuantitativeGameResult(std::pair<ValueType, ValueType> initialStatesRange, storm::dd::Add<Type, ValueType> const& values, storm::dd::Bdd<Type> const& player1Strategy, storm::dd::Bdd<Type> const& player2Strategy) : initialStatesRange(initialStatesRange), values(values), player1Strategy(player1Strategy), player2Strategy(player2Strategy) {
                 // Intentionally left empty.
             }
             
diff --git a/src/storm/abstraction/QuantitativeGameResultMinMax.h b/src/storm/abstraction/QuantitativeGameResultMinMax.h
new file mode 100644
index 000000000..3b13b6927
--- /dev/null
+++ b/src/storm/abstraction/QuantitativeGameResultMinMax.h
@@ -0,0 +1,21 @@
+#pragma once
+
+#include "storm/abstraction/QuantitativeGameResult.h"
+
+namespace storm {
+    namespace abstraction {
+     
+        template<storm::dd::DdType Type, typename ValueType>
+        struct QuantitativeGameResultMinMax {
+            QuantitativeGameResultMinMax() = default;
+            
+            QuantitativeGameResultMinMax(QuantitativeGameResult<Type, ValueType> const& min, QuantitativeGameResult<Type, ValueType> const& max) : min(min), max(max) {
+                // Intentionally left empty.
+            }
+            
+            QuantitativeGameResult<Type, ValueType> min;
+            QuantitativeGameResult<Type, ValueType> max;
+        };
+        
+    }
+}
diff --git a/src/storm/abstraction/QuantitativeResultMinMax.h b/src/storm/abstraction/QuantitativeResultMinMax.h
deleted file mode 100644
index f0bdab86d..000000000
--- a/src/storm/abstraction/QuantitativeResultMinMax.h
+++ /dev/null
@@ -1,21 +0,0 @@
-#pragma once
-
-#include "storm/abstraction/QuantitativeResult.h"
-
-namespace storm {
-    namespace abstraction {
-     
-        template<storm::dd::DdType Type, typename ValueType>
-        struct QuantitativeResultMinMax {
-            QuantitativeResultMinMax() = default;
-            
-            QuantitativeResultMinMax(QuantitativeResult<Type, ValueType> const& min, QuantitativeResult<Type, ValueType> const& max) : min(min), max(max) {
-                // Intentionally left empty.
-            }
-            
-            QuantitativeResult<Type, ValueType> min;
-            QuantitativeResult<Type, ValueType> max;
-        };
-        
-    }
-}
diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
index 5444cf732..7574aea14 100644
--- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
+++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
@@ -47,8 +47,8 @@
 namespace storm {
     namespace modelchecker {
         
-        using storm::abstraction::QuantitativeResult;
-        using storm::abstraction::QuantitativeResultMinMax;
+        using storm::abstraction::QuantitativeGameResult;
+        using storm::abstraction::QuantitativeGameResultMinMax;
         
         template<storm::dd::DdType Type, typename ModelType>
         GameBasedMdpModelChecker<Type, ModelType>::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPrecision()), reuseQualitativeResults(false), reuseQuantitativeResults(false) {
@@ -161,7 +161,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType Type, typename ValueType>
-        std::unique_ptr<CheckResult> checkForResultAfterQualitativeCheck(CheckTask<storm::logic::Formula> const& checkTask, storm::dd::Bdd<Type> const& initialStates, QualitativeResultMinMax<Type> const& qualitativeResult) {
+        std::unique_ptr<CheckResult> checkForResultAfterQualitativeCheck(CheckTask<storm::logic::Formula> const& checkTask, storm::dd::Bdd<Type> const& initialStates, QualitativeGameResultMinMax<Type> const& qualitativeResult) {
             // Check whether we can already give the answer based on the current information.
             std::unique_ptr<CheckResult> result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, storm::OptimizationDirection::Minimize, initialStates, qualitativeResult.prob0Min.getPlayer1States(), qualitativeResult.prob1Min.getPlayer1States());
             if (result) {
@@ -234,7 +234,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType Type, typename ValueType>
-        QuantitativeResult<Type, ValueType> solveMaybeStates(storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& maybeStates, storm::dd::Bdd<Type> const& prob1States, boost::optional<QuantitativeResult<Type, ValueType>> const& startInfo = boost::none) {
+        QuantitativeGameResult<Type, ValueType> solveMaybeStates(storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& maybeStates, storm::dd::Bdd<Type> const& prob1States, boost::optional<QuantitativeGameResult<Type, ValueType>> const& startInfo = boost::none) {
             
             STORM_LOG_TRACE("Performing quantative solution step. Player 1: " << player1Direction << ", player 2: " << player2Direction << ".");
             
@@ -261,14 +261,14 @@ namespace storm {
             std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>> solver = solverFactory.create(submatrix, maybeStates, game.getIllegalPlayer1Mask(), game.getIllegalPlayer2Mask(), game.getRowVariables(), game.getColumnVariables(), game.getRowColumnMetaVariablePairs(), game.getPlayer1Variables(), game.getPlayer2Variables());
             solver->setGeneratePlayersStrategies(true);
             auto values = solver->solveGame(player1Direction, player2Direction, startVector, subvector, startInfo ? boost::make_optional(startInfo.get().player1Strategy) : boost::none, startInfo ? boost::make_optional(startInfo.get().player2Strategy) : boost::none);
-            return QuantitativeResult<Type, ValueType>(std::make_pair(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>()), values, solver->getPlayer1Strategy(), solver->getPlayer2Strategy());
+            return QuantitativeGameResult<Type, ValueType>(std::make_pair(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>()), values, solver->getPlayer1Strategy(), solver->getPlayer2Strategy());
         }
         
         template<storm::dd::DdType Type, typename ValueType>
-        QuantitativeResult<Type, ValueType> computeQuantitativeResult(storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, QualitativeResultMinMax<Type> const& qualitativeResult, storm::dd::Add<Type, ValueType> const& initialStatesAdd, storm::dd::Bdd<Type> const& maybeStates, boost::optional<QuantitativeResult<Type, ValueType>> const& startInfo = boost::none) {
+        QuantitativeGameResult<Type, ValueType> computeQuantitativeResult(storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, QualitativeGameResultMinMax<Type> const& qualitativeResult, storm::dd::Add<Type, ValueType> const& initialStatesAdd, storm::dd::Bdd<Type> const& maybeStates, boost::optional<QuantitativeGameResult<Type, ValueType>> const& startInfo = boost::none) {
             
             bool min = player2Direction == storm::OptimizationDirection::Minimize;
-            QuantitativeResult<Type, ValueType> result;
+            QuantitativeGameResult<Type, ValueType> result;
             
             // We fix the strategies. That is, we take the decisions of the strategies obtained in the qualitiative
             // preprocessing if possible.
@@ -352,8 +352,8 @@ namespace storm {
             storm::dd::Bdd<Type> globalTargetStates = abstractor->getStates(targetStateExpression);
             
             // Enter the main-loop of abstraction refinement.
-            boost::optional<QualitativeResultMinMax<Type>> previousQualitativeResult = boost::none;
-            boost::optional<QuantitativeResult<Type, ValueType>> previousMinQuantitativeResult = boost::none;
+            boost::optional<QualitativeGameResultMinMax<Type>> previousQualitativeResult = boost::none;
+            boost::optional<QuantitativeGameResult<Type, ValueType>> previousMinQuantitativeResult = boost::none;
             for (uint_fast64_t iterations = 0; iterations < 10000; ++iterations) {
                 auto iterationStart = std::chrono::high_resolution_clock::now();
                 STORM_LOG_TRACE("Starting iteration " << iterations << ".");
@@ -382,7 +382,7 @@ namespace storm {
                 
                 // (3) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max).
                 auto qualitativeStart = std::chrono::high_resolution_clock::now();
-                QualitativeResultMinMax<Type> qualitativeResult = computeProb01States(previousQualitativeResult, game, player1Direction, transitionMatrixBdd, constraintStates, targetStates);
+                QualitativeGameResultMinMax<Type> qualitativeResult = computeProb01States(previousQualitativeResult, game, player1Direction, transitionMatrixBdd, constraintStates, targetStates);
                 std::unique_ptr<CheckResult> result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, initialStates, qualitativeResult);
                 if (result) {
                     printStatistics(*abstractor, game);
@@ -426,7 +426,7 @@ namespace storm {
                     STORM_LOG_TRACE("Starting numerical solution step.");
                     auto quantitativeStart = std::chrono::high_resolution_clock::now();
 
-                    QuantitativeResultMinMax<Type, ValueType> quantitativeResult;
+                    QuantitativeGameResultMinMax<Type, ValueType> quantitativeResult;
                     
                     // (7) Solve the min values and check whether we can give the answer already.
                     quantitativeResult.min = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin, reuseQuantitativeResults ? previousMinQuantitativeResult : boost::none);
@@ -513,7 +513,7 @@ namespace storm {
         }
 
         template<storm::dd::DdType Type>
-        bool checkQualitativeStrategies(bool prob0, QualitativeResult<Type> const& result, storm::dd::Bdd<Type> const& targetStates) {
+        bool checkQualitativeStrategies(bool prob0, QualitativeGameResult<Type> const& result, storm::dd::Bdd<Type> const& targetStates) {
             if (prob0) {
                 STORM_LOG_ASSERT(result.hasPlayer1Strategy() && (result.getPlayer1States().isZero() || !result.getPlayer1Strategy().isZero()), "Unable to proceed without strategy.");
             } else {
@@ -526,7 +526,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType Type>
-        bool checkQualitativeStrategies(QualitativeResultMinMax<Type> const& qualitativeResult, storm::dd::Bdd<Type> const& targetStates) {
+        bool checkQualitativeStrategies(QualitativeGameResultMinMax<Type> const& qualitativeResult, storm::dd::Bdd<Type> const& targetStates) {
             bool result = true;
             result &= checkQualitativeStrategies(true, qualitativeResult.prob0Min, targetStates);
             result &= checkQualitativeStrategies(false, qualitativeResult.prob1Min, targetStates);
@@ -536,9 +536,9 @@ namespace storm {
         }
         
         template<storm::dd::DdType Type, typename ModelType>
-        QualitativeResultMinMax<Type> GameBasedMdpModelChecker<Type, ModelType>::computeProb01States(boost::optional<QualitativeResultMinMax<Type>> const& previousQualitativeResult, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates) {
+        QualitativeGameResultMinMax<Type> GameBasedMdpModelChecker<Type, ModelType>::computeProb01States(boost::optional<QualitativeGameResultMinMax<Type>> const& previousQualitativeResult, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates) {
             
-            QualitativeResultMinMax<Type> result;
+            QualitativeGameResultMinMax<Type> result;
             
             if (reuseQualitativeResults) {
                 // Depending on the player 1 direction, we choose a different order of operations.
diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h
index ae63f96df..b42fde67f 100644
--- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h
+++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h
@@ -10,7 +10,7 @@
 #include "storm/storage/SymbolicModelDescription.h"
 
 #include "storm/abstraction/QualitativeResult.h"
-#include "storm/abstraction/QualitativeResultMinMax.h"
+#include "storm/abstraction/QualitativeGameResultMinMax.h"
 
 #include "storm/logic/Bound.h"
 
@@ -29,8 +29,8 @@ namespace storm {
     
     namespace modelchecker {
         
-        using storm::abstraction::QualitativeResult;
-        using storm::abstraction::QualitativeResultMinMax;
+        using storm::abstraction::QualitativeGameResult;
+        using storm::abstraction::QualitativeGameResultMinMax;
         
         template<storm::dd::DdType Type, typename ModelType>
         class GameBasedMdpModelChecker : public AbstractModelChecker<ModelType> {
@@ -71,7 +71,7 @@ namespace storm {
              * Performs a qualitative check on the the given game to compute the (player 1) states that have probability
              * 0 or 1, respectively, to reach a target state and only visiting constraint states before.
              */
-            QualitativeResultMinMax<Type> computeProb01States(boost::optional<QualitativeResultMinMax<Type>> const& previousQualitativeResult, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates);
+            QualitativeGameResultMinMax<Type> computeProb01States(boost::optional<QualitativeGameResultMinMax<Type>> const& previousQualitativeResult, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates);
             
             void printStatistics(storm::abstraction::MenuGameAbstractor<Type, ValueType> const& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game) const;
             
diff --git a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp
index 976006cf6..108b57686 100644
--- a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp
+++ b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp
@@ -6,6 +6,7 @@
 
 #include "storm/modelchecker/results/CheckResult.h"
 #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
+#include "storm/modelchecker/results/QuantitativeCheckResult.h"
 #include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h"
 #include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
 #include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
@@ -15,6 +16,8 @@
 #include "storm/storage/dd/Bdd.h"
 #include "storm/storage/dd/BisimulationDecomposition.h"
 
+#include "storm/abstraction/QualitativeMdpResultMinMax.h"
+
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/AbstractionSettings.h"
 
@@ -41,28 +44,28 @@ namespace storm {
         
         template<typename ModelType>
         std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) {
-            return computeValuesAbstractionRefinement(false, checkTask.substituteFormula<storm::logic::Formula>(checkTask.getFormula()));
+            return computeValuesAbstractionRefinement(checkTask.substituteFormula<storm::logic::Formula>(checkTask.getFormula()));
         }
         
         template<typename ModelType>
         std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
-            return computeValuesAbstractionRefinement(false, checkTask.substituteFormula<storm::logic::Formula>(checkTask.getFormula()));
+            return computeValuesAbstractionRefinement(checkTask.substituteFormula<storm::logic::Formula>(checkTask.getFormula()));
         }
 
         template<typename ModelType>
         std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) {
             STORM_LOG_THROW(rewardMeasureType == storm::logic::RewardMeasureType::Expectation, storm::exceptions::InvalidPropertyException, "Can only compute reward expectations.");
-            return computeValuesAbstractionRefinement(true, checkTask.template substituteFormula<storm::logic::Formula>(checkTask.getFormula()));
+            return computeValuesAbstractionRefinement(checkTask.template substituteFormula<storm::logic::Formula>(checkTask.getFormula()));
         }
 
         template<typename ModelType>
-        std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeValuesAbstractionRefinement(bool rewards, CheckTask<storm::logic::Formula> const& checkTask) {
+        std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeValuesAbstractionRefinement(CheckTask<storm::logic::Formula> const& checkTask) {
 
             STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException, "The game-based abstraction refinement model checker can only compute the result for the initial states.");
             
             // Create the appropriate preservation information.
             storm::dd::bisimulation::PreservationInformation<DdType, ValueType> preservationInformation(model, {checkTask.getFormula().asSharedPointer()});
-            if (rewards) {
+            if (checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward) {
                 if (!checkTask.isRewardModelSet() || model.hasUniqueRewardModel()) {
                     preservationInformation.addRewardModel(model.getUniqueRewardModelName());
                 } else if (checkTask.isRewardModelSet()) {
@@ -85,10 +88,21 @@ namespace storm {
                 if (fullQuotient) {
                     STORM_LOG_TRACE("Reached final quotient.");
                     quotient->printModelInformationToStream(std::cout);
-                    result = computeResultFullQuotient(*quotient, rewards, checkTask);
+                    result = computeResultFullQuotient(*quotient, checkTask);
                 } else {
                     // Obtain lower and upper bounds from the partial quotient.
-                    std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> bounds = computeBoundsPartialQuotient(*quotient, rewards, checkTask);
+                    std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> bounds = computeBoundsPartialQuotient(*quotient, checkTask);
+                    
+                    // If either of the two bounds does not exist, the answer can be derived from the existing bounds.
+                    if (bounds.first == nullptr || bounds.second == nullptr) {
+                        STORM_LOG_ASSERT(bounds.first || bounds.second, "Expected at least one bound.");
+                        quotient->printModelInformationToStream(std::cout);
+                        if (bounds.first) {
+                            return std::move(bounds.first);
+                        } else {
+                            return std::move(bounds.second);
+                        }
+                    }
                     
                     // Check whether the bounds are sufficiently close.
                     bool converged = checkBoundsSufficientlyClose(bounds);
@@ -152,47 +166,151 @@ namespace storm {
             
             return std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(lowerBounds.getReachableStates(), lowerBounds.getStates(), (lowerBounds.getValueVector() + upperBounds.getValueVector()) / lowerBounds.getValueVector().getDdManager().getConstant(storm::utility::convertNumber<ValueType>(std::string("2.0"))));
         }
+
+        template<typename ModelType>
+        typename PartialBisimulationMdpModelChecker<ModelType>::ValueType PartialBisimulationMdpModelChecker<ModelType>::getExtremalBound(storm::OptimizationDirection dir, QuantitativeCheckResult<ValueType> const& result) {
+            if (dir == storm::OptimizationDirection::Minimize) {
+                return result.getMin();
+            } else {
+                return result.getMax();
+            }
+        }
         
-        static int i = 0;
+        template<typename ModelType>
+        bool PartialBisimulationMdpModelChecker<ModelType>::boundsSufficient(storm::models::Model<ValueType> const& quotient, bool lowerBounds, QuantitativeCheckResult<ValueType> const& result, storm::logic::ComparisonType comparisonType, ValueType const& threshold) {
+            if (lowerBounds) {
+                if (storm::logic::isLowerBound(comparisonType)) {
+                    ValueType minimalLowerBound = getExtremalBound(storm::OptimizationDirection::Minimize, result);
+                    return (storm::logic::isStrict(comparisonType) && minimalLowerBound > threshold) || (!storm::logic::isStrict(comparisonType) && minimalLowerBound >= threshold);
+                } else {
+                    ValueType maximalLowerBound = getExtremalBound(storm::OptimizationDirection::Maximize, result);
+                    return (storm::logic::isStrict(comparisonType) && maximalLowerBound >= threshold) || (!storm::logic::isStrict(comparisonType) && maximalLowerBound > threshold);
+                }
+            } else {
+                if (storm::logic::isLowerBound(comparisonType)) {
+                    ValueType minimalUpperBound = getExtremalBound(storm::OptimizationDirection::Minimize, result);
+                    return (storm::logic::isStrict(comparisonType) && minimalUpperBound <= threshold) || (!storm::logic::isStrict(comparisonType) && minimalUpperBound < threshold);
+                } else {
+                    ValueType maximalUpperBound = getExtremalBound(storm::OptimizationDirection::Maximize, result);
+                    return (storm::logic::isStrict(comparisonType) && maximalUpperBound < threshold) || (!storm::logic::isStrict(comparisonType) && maximalUpperBound <= threshold);
+                }
+            }
+        }
         
         template<typename ModelType>
-        std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> PartialBisimulationMdpModelChecker<ModelType>::computeBoundsPartialQuotient(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask) {
+        std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeBoundsPartialQuotient(SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>>& checker, storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, storm::OptimizationDirection const& dir, CheckTask<storm::logic::Formula>& checkTask) {
             
-            std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> result;
-            
-            CheckTask<storm::logic::Formula> newCheckTask(checkTask);
-            SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>> checker(quotient);
+            bool rewards = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward;
 
-            newCheckTask.setOptimizationDirection(storm::OptimizationDirection::Minimize);
+            std::unique_ptr<CheckResult> result;
+            checkTask.setOptimizationDirection(dir);
             if (rewards) {
-                result.first = checker.computeRewards(storm::logic::RewardMeasureType::Expectation,newCheckTask);
+                result = checker.computeRewards(storm::logic::RewardMeasureType::Expectation, checkTask);
             } else {
-                result.first = checker.computeProbabilities(newCheckTask);
+                result = checker.computeProbabilities(checkTask);
             }
-            STORM_LOG_ASSERT(result.first, "Expected result.");
-            result.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>().getValueVector().exportToDot("lower_values" + std::to_string(i) + ".dot");
-            result.first->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotient.getReachableStates(), quotient.getInitialStates()));
+            STORM_LOG_ASSERT(result, "Expected result.");
+            result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotient.getReachableStates(), quotient.getInitialStates()));
+            return result;
+        }
+        
+        template<typename ModelType>
+        std::pair<storm::dd::Bdd<PartialBisimulationMdpModelChecker<ModelType>::DdType>, storm::dd::Bdd<PartialBisimulationMdpModelChecker<ModelType>::DdType>> PartialBisimulationMdpModelChecker<ModelType>::getConstraintAndTargetStates(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask) {
+            std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> result;
             
-            newCheckTask.setOptimizationDirection(storm::OptimizationDirection::Maximize);
-            if (rewards) {
-                result.second = checker.computeRewards(storm::logic::RewardMeasureType::Expectation, newCheckTask);
+            SymbolicPropositionalModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>> checker(quotient);
+            if (checkTask.getFormula().isUntilFormula()) {
+                std::unique_ptr<CheckResult> subresult = checker.check(checkTask.getFormula().asUntilFormula().getLeftSubformula());
+                result.first = subresult->asSymbolicQualitativeCheckResult<DdType>().getTruthValuesVector();
+                subresult = checker.check(checkTask.getFormula().asUntilFormula().getRightSubformula());
+                result.second = subresult->asSymbolicQualitativeCheckResult<DdType>().getTruthValuesVector();
+            } else if (checkTask.getFormula().isEventuallyFormula()) {
+                storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula().asEventuallyFormula();
+                result.first = quotient.getReachableStates();
+                std::unique_ptr<CheckResult> subresult = checker.check(eventuallyFormula.getSubformula());
+                result.second = subresult->asSymbolicQualitativeCheckResult<DdType>().getTruthValuesVector();
             } else {
-                result.second = checker.computeProbabilities(newCheckTask);
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The given formula is not supported by this model checker.");
             }
-            STORM_LOG_ASSERT(result.second, "Expected result.");
-            result.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>().getValueVector().exportToDot("upper_values" + std::to_string(i++) + ".dot");
-            result.second->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotient.getReachableStates(), quotient.getInitialStates()));
+            
+            return result;
+        }
+        
+        template<typename ModelType>
+        std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> PartialBisimulationMdpModelChecker<ModelType>::computeBoundsPartialQuotient(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask) {
 
+            std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> result;
+
+            // We go through two phases. In phase (1) we are solving the qualitative part and in phase (2) the quantitative part.
+            
+            // Preparation: determine the constraint states and the target states of the reachability objective.
+            bool isRewardFormula = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward;
+            std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> constraintTargetStates = getConstraintAndTargetStates(quotient, checkTask);
+            
+            // Phase (1): solve qualitatively.
+            storm::abstraction::QualitativeMdpResultMinMax<DdType> qualitativeResults;
+            storm::dd::Bdd<DdType> transitionMatrixBdd = quotient.getTransitionMatrix().notZero();
+            if (isRewardFormula) {
+                qualitativeResults.min.second = storm::utility::graph::performProb1E(quotient, transitionMatrixBdd, constraintTargetStates.first, constraintTargetStates.second, storm::utility::graph::performProbGreater0E(quotient, transitionMatrixBdd, constraintTargetStates.first, constraintTargetStates.second));
+                qualitativeResults.max.second = storm::utility::graph::performProb1A(quotient, transitionMatrixBdd, constraintTargetStates.first, storm::utility::graph::performProbGreater0A(quotient, transitionMatrixBdd, constraintTargetStates.first, constraintTargetStates.second));
+            } else {
+                qualitativeResults.min = storm::utility::graph::performProb01Min(quotient, transitionMatrixBdd, constraintTargetStates.first, constraintTargetStates.second);
+                qualitativeResults.max = storm::utility::graph::performProb01Max(quotient, transitionMatrixBdd, constraintTargetStates.first, constraintTargetStates.second);
+            }
+            
+            
+//            CheckTask<storm::logic::Formula> newCheckTask(checkTask);
+//
+//            if (!checkTask.isBoundSet() || storm::logic::isLowerBound(checkTask.getBoundComparisonType())) {
+//                // Check whether we can answer the query (lower bound above bound).
+//                result.first = computeBoundsPartialQuotient(checker, quotient, rewards, storm::OptimizationDirection::Minimize, newCheckTask);
+//                if (checkTask.isBoundSet()) {
+//                    bool sufficient = boundsSufficient(quotient, true, result.first->asQuantitativeCheckResult<ValueType>(), checkTask.getBoundComparisonType(), checkTask.getBoundThreshold());
+//                    if (sufficient) {
+//                        return result;
+//                    }
+//                }
+//
+//                // Check whether we can answer the query (upper bound below bound).
+//                result.second = computeBoundsPartialQuotient(checker, quotient, rewards, storm::OptimizationDirection::Maximize, newCheckTask);
+//                if (checkTask.isBoundSet()) {
+//                    bool sufficient = boundsSufficient(quotient, false, result.second->asQuantitativeCheckResult<ValueType>(), checkTask.getBoundComparisonType(), checkTask.getBoundThreshold());
+//                    if (sufficient) {
+//                        result.first = nullptr;
+//                        return result;
+//                    }
+//                }
+//            } else {
+//                // Check whether we can answer the query (upper bound below bound).
+//                result.second = computeBoundsPartialQuotient(checker, quotient, rewards, storm::OptimizationDirection::Maximize, newCheckTask);
+//                if (checkTask.isBoundSet()) {
+//                    bool sufficient = boundsSufficient(quotient, false, result.second->asQuantitativeCheckResult<ValueType>(), checkTask.getBoundComparisonType(), checkTask.getBoundThreshold());
+//                    if (sufficient) {
+//                        return result;
+//                    }
+//                }
+//
+//                // Check whether we can answer the query (lower bound above bound).
+//                result.first = computeBoundsPartialQuotient(checker, quotient, rewards, storm::OptimizationDirection::Minimize, newCheckTask);
+//                if (checkTask.isBoundSet()) {
+//                    bool sufficient = boundsSufficient(quotient, true, result.first->asQuantitativeCheckResult<ValueType>(), checkTask.getBoundComparisonType(), checkTask.getBoundThreshold());
+//                    if (sufficient) {
+//                        result.second = nullptr;
+//                        return result;
+//                    }
+//                }
+//            }
+            
             return result;
         }
 
         template<typename ModelType>
-        std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> PartialBisimulationMdpModelChecker<ModelType>::computeBoundsPartialQuotient(storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask) {
+        std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> PartialBisimulationMdpModelChecker<ModelType>::computeBoundsPartialQuotient(storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask) {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Currently not implemented.");
         }
 
         template<typename ModelType>
-        std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> PartialBisimulationMdpModelChecker<ModelType>::computeBoundsPartialQuotient(storm::models::Model<ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask) {
+        std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> PartialBisimulationMdpModelChecker<ModelType>::computeBoundsPartialQuotient(storm::models::Model<ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask) {
             
             // Sanity checks.
             STORM_LOG_THROW(quotient.isSymbolicModel(), storm::exceptions::NotSupportedException, "Expecting symbolic quotient.");
@@ -200,14 +318,16 @@ namespace storm {
             STORM_LOG_THROW(modelType == storm::models::ModelType::Mdp || modelType == storm::models::ModelType::S2pg, storm::exceptions::NotSupportedException, "Only MDPs and stochastic games are supported as partial quotients.");
             
             if (modelType == storm::models::ModelType::Mdp) {
-                return computeBoundsPartialQuotient(*quotient.template as<storm::models::symbolic::Mdp<DdType, ValueType>>(), rewards, checkTask);
+                return computeBoundsPartialQuotient(static_cast<storm::models::symbolic::Mdp<DdType, ValueType> const&>(quotient), checkTask);
             } else {
-                return computeBoundsPartialQuotient(*quotient.template as<storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType>>(), rewards, checkTask);
+                return computeBoundsPartialQuotient(static_cast<storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType> const&>(quotient), checkTask);
             }
         }
         
         template<typename ModelType>
-        std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeResultFullQuotient(storm::models::symbolic::Dtmc<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask) {
+        std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeResultFullQuotient(storm::models::symbolic::Dtmc<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask) {
+            bool rewards = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward;
+            
             SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<DdType, ValueType>> checker(quotient);
             std::unique_ptr<CheckResult> result;
             if (rewards) {
@@ -220,7 +340,9 @@ namespace storm {
         }
 
         template<typename ModelType>
-        std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeResultFullQuotient(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask) {
+        std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeResultFullQuotient(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask) {
+            bool rewards = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward;
+
             SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>> checker(quotient);
             std::unique_ptr<CheckResult> result;
             if (rewards) {
@@ -233,7 +355,7 @@ namespace storm {
         }
 
         template<typename ModelType>
-        std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeResultFullQuotient(storm::models::Model<ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask) {
+        std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeResultFullQuotient(storm::models::Model<ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask) {
             
             // Sanity checks.
             STORM_LOG_THROW(quotient.isSymbolicModel(), storm::exceptions::NotSupportedException, "Expecting symbolic quotient.");
@@ -241,9 +363,9 @@ namespace storm {
             STORM_LOG_THROW(modelType == storm::models::ModelType::Dtmc || modelType == storm::models::ModelType::Mdp, storm::exceptions::NotSupportedException, "Only DTMCs and MDPs supported as full quotients.");
             
             if (modelType == storm::models::ModelType::Dtmc) {
-                return computeResultFullQuotient(*quotient.template as<storm::models::symbolic::Dtmc<DdType, ValueType>>(), rewards, checkTask);
+                return computeResultFullQuotient(static_cast<storm::models::symbolic::Dtmc<DdType, ValueType> const&>(quotient), checkTask);
             } else {
-                return computeResultFullQuotient(*quotient.template as<storm::models::symbolic::Mdp<DdType, ValueType>>(), rewards, checkTask);
+                return computeResultFullQuotient(static_cast<storm::models::symbolic::Mdp<DdType, ValueType> const&>(quotient), checkTask);
             }
         }
         
diff --git a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h
index 3fa6f0c03..e18c738be 100644
--- a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h
+++ b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h
@@ -4,6 +4,8 @@
 
 #include "storm/storage/dd/DdType.h"
 
+#include "storm/solver/OptimizationDirection.h"
+
 namespace storm {
     namespace dd {
         template <storm::dd::DdType DdType>
@@ -27,7 +29,12 @@ namespace storm {
     }
     
     namespace modelchecker {
+        template <typename ModelType>
+        class SymbolicMdpPrctlModelChecker;
         
+        template <typename ValueType>
+        class QuantitativeCheckResult;
+
         template<typename ModelType>
         class PartialBisimulationMdpModelChecker : public AbstractModelChecker<ModelType> {
         public:
@@ -46,22 +53,33 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
 
         private:
-            std::unique_ptr<CheckResult> computeValuesAbstractionRefinement(bool rewards, CheckTask<storm::logic::Formula> const& checkTask);
+            std::unique_ptr<CheckResult> computeValuesAbstractionRefinement(CheckTask<storm::logic::Formula> const& checkTask);
             
             // Methods to check for convergence and postprocessing the result.
             bool checkBoundsSufficientlyClose(std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> const& bounds);
             std::unique_ptr<CheckResult> getAverageOfBounds(std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> const& bounds);
             void printBoundsInformation(std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> const& bounds);
 
+            // Retrieves the constraint and target states of the quotient wrt. to the formula in the check task.
+            std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> getConstraintAndTargetStates(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask);
+            
+            // Retrieves the extremal bound (wrt. to the optimization direction) of the quantitative check result.
+            ValueType getExtremalBound(storm::OptimizationDirection dir, QuantitativeCheckResult<ValueType> const& result);
+            
+            // Retrieves whether the quantitative bounds are sufficient to answer the the query given by the bound (comparison
+            // type and threshold).
+            bool boundsSufficient(storm::models::Model<ValueType> const& quotient, bool lowerBounds, QuantitativeCheckResult<ValueType> const& result, storm::logic::ComparisonType comparisonType, ValueType const& threshold);
+            
             // Methods to compute bounds on the partial quotient.
-            std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> computeBoundsPartialQuotient(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask);
-            std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> computeBoundsPartialQuotient(storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask);
-            std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> computeBoundsPartialQuotient(storm::models::Model<ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask);
+            std::unique_ptr<CheckResult> computeBoundsPartialQuotient(SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>>& checker, storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, storm::OptimizationDirection const& dir, CheckTask<storm::logic::Formula>& checkTask);
+            std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> computeBoundsPartialQuotient(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask);
+            std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> computeBoundsPartialQuotient(storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask);
+            std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> computeBoundsPartialQuotient(storm::models::Model<ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask);
             
             // Methods to solve the query on the full quotient.
-            std::unique_ptr<CheckResult> computeResultFullQuotient(storm::models::symbolic::Dtmc<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask);
-            std::unique_ptr<CheckResult> computeResultFullQuotient(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask);
-            std::unique_ptr<CheckResult> computeResultFullQuotient(storm::models::Model<ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask);
+            std::unique_ptr<CheckResult> computeResultFullQuotient(storm::models::symbolic::Dtmc<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask);
+            std::unique_ptr<CheckResult> computeResultFullQuotient(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask);
+            std::unique_ptr<CheckResult> computeResultFullQuotient(storm::models::Model<ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask);
             
             // The non-abstracted model.
             ModelType const& model;
diff --git a/src/storm/modelchecker/hints/ModelCheckerHint.h b/src/storm/modelchecker/hints/ModelCheckerHint.h
index afa24484a..14dd4dcbb 100644
--- a/src/storm/modelchecker/hints/ModelCheckerHint.h
+++ b/src/storm/modelchecker/hints/ModelCheckerHint.h
@@ -1,12 +1,13 @@
-#ifndef STORM_MODELCHECKER_HINTS_MODELCHECKERHINT_H
-#define STORM_MODELCHECKER_HINTS_MODELCHECKERHINT_H
+#pragma once
+
+#include "storm/storage/dd/DdType.h"
 
 namespace storm {
     namespace modelchecker {
         
         template<typename ValueType>
         class ExplicitModelCheckerHint;
-        
+
         /*!
          * This class contains information that might accelerate the model checking process.
          * @note The model checker has to make sure whether a given hint is actually applicable and thus a hint might be ignored.
@@ -15,10 +16,10 @@ namespace storm {
         public:
             ModelCheckerHint() = default;
             
-            // Returns true iff this hint does not contain any information
+            // Returns true iff this hint does not contain any information.
             virtual bool isEmpty() const;
             
-            // Returns true iff this is an explicit model checker hint
+            // Returns true iff this is an explicit model checker hint.
             virtual bool isExplicitModelCheckerHint() const;
             
             template<typename ValueType>
@@ -26,10 +27,8 @@ namespace storm {
             
             template<typename ValueType>
             ExplicitModelCheckerHint<ValueType> const& asExplicitModelCheckerHint() const;
-            
         };
         
     }
 }
 
-#endif /* STORM_MODELCHECKER_HINTS_MODELCHECKERHINT_H */
diff --git a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp
index 436a55925..4f7d0cf34 100644
--- a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp
+++ b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp
@@ -101,7 +101,7 @@ namespace storm {
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
             SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();
-            return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory);
+            return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), *this->linearEquationSolverFactory);
         }
 
         template class SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>;
diff --git a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
index 59cb85256..f7311559c 100644
--- a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
@@ -37,7 +37,7 @@ namespace storm {
             }
             
             template<storm::dd::DdType DdType, typename ValueType>
-            std::unique_ptr<CheckResult> SymbolicMdpPrctlHelper<DdType, ValueType>::computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory) {
+            std::unique_ptr<CheckResult> SymbolicMdpPrctlHelper<DdType, ValueType>::computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory, boost::optional<storm::dd::Add<DdType, ValueType>> const& startValues) {
                 // We need to identify the states which have to be taken out of the matrix, i.e. all states that have
                 // probability 0 and 1 of satisfying the until-formula.
                 std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> statesWithProbability01;
@@ -96,7 +96,7 @@ namespace storm {
                         solver->setBounds(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>());
                         solver->setRequirementsChecked();
 
-                        storm::dd::Add<DdType, ValueType> result = solver->solveEquations(dir, model.getManager().template getAddZero<ValueType>(), subvector);
+                        storm::dd::Add<DdType, ValueType> result = solver->solveEquations(dir, startValues ? maybeStates.ite(startValues.get(), model.getManager().template getAddZero<ValueType>()) : model.getManager().template getAddZero<ValueType>(), subvector);
                         
                         return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), statesWithProbability01.second.template toAdd<ValueType>() + result));
                     } else {
@@ -189,7 +189,7 @@ namespace storm {
             }
             
             template<storm::dd::DdType DdType, typename ValueType>
-            std::unique_ptr<CheckResult> SymbolicMdpPrctlHelper<DdType, ValueType>::computeReachabilityRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd<DdType> const& targetStates, bool qualitative, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory) {
+            std::unique_ptr<CheckResult> SymbolicMdpPrctlHelper<DdType, ValueType>::computeReachabilityRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd<DdType> const& targetStates, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory, boost::optional<storm::dd::Add<DdType, ValueType>> const& startValues) {
                 
                 // Only compute the result if there is at least one reward model.
                 STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
@@ -208,59 +208,52 @@ namespace storm {
                 
                 STORM_LOG_INFO("Preprocessing: " << infinityStates.getNonZeroCount() << " states with reward infinity, " << targetStates.getNonZeroCount() << " target states (" << maybeStates.getNonZeroCount() << " states remaining).");
 
-                // Check whether we need to compute exact rewards for some states.
-                if (qualitative) {
-                    // Set the values for all maybe-states to 1 to indicate that their reward values
-                    // are neither 0 nor infinity.
-                    return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), infinityStates.ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), model.getManager().template getAddZero<ValueType>()) + maybeStates.template toAdd<ValueType>() * model.getManager().getConstant(storm::utility::one<ValueType>())));
-                } else {
-                    // If there are maybe states, we need to solve an equation system.
-                    if (!maybeStates.isZero()) {
-                        // Create the matrix and the vector for the equation system.
-                        storm::dd::Add<DdType, ValueType> maybeStatesAdd = maybeStates.template toAdd<ValueType>();
-                        
-                        // Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting
-                        // non-maybe states in the matrix.
-                        storm::dd::Add<DdType, ValueType> submatrix = transitionMatrix * maybeStatesAdd;
-                        
-                        // Then compute the state reward vector to use in the computation.
-                        storm::dd::Add<DdType, ValueType> subvector = rewardModel.getTotalRewardVector(maybeStatesAdd, submatrix, model.getColumnVariables());
-                        
-                        // Since we are cutting away target and infinity states, we need to account for this by giving
-                        // choices the value infinity that have some successor contained in the infinity states.
-                        storm::dd::Bdd<DdType> choicesWithInfinitySuccessor = (maybeStates && transitionMatrixBdd && infinityStates.swapVariables(model.getRowColumnMetaVariablePairs())).existsAbstract(model.getColumnVariables());
-                        subvector = choicesWithInfinitySuccessor.ite(model.getManager().template getInfinity<ValueType>(), subvector);
-                        
-                        // Finally cut away all columns targeting non-maybe states.
-                        submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs());
-                        
-                        // Now solve the resulting equation system.
-                        std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs());
-                        
-                        // Check requirements of solver.
-                        storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(storm::solver::EquationSystemType::ReachabilityRewards, dir);
-                        boost::optional<storm::dd::Bdd<DdType>> initialScheduler;
-                        if (!requirements.empty()) {
-                            if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) {
-                                STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it.");
-                                initialScheduler = computeValidSchedulerHint(storm::solver::EquationSystemType::ReachabilityRewards, model, transitionMatrix, maybeStates, targetStates);
-                                requirements.clearValidInitialScheduler();
-                            }
-                            requirements.clearLowerBounds();
-                            STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Could not establish requirements of solver.");
-                        }
-                        if (initialScheduler) {
-                            solver->setInitialScheduler(initialScheduler.get());
+                // If there are maybe states, we need to solve an equation system.
+                if (!maybeStates.isZero()) {
+                    // Create the matrix and the vector for the equation system.
+                    storm::dd::Add<DdType, ValueType> maybeStatesAdd = maybeStates.template toAdd<ValueType>();
+                    
+                    // Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting
+                    // non-maybe states in the matrix.
+                    storm::dd::Add<DdType, ValueType> submatrix = transitionMatrix * maybeStatesAdd;
+                    
+                    // Then compute the state reward vector to use in the computation.
+                    storm::dd::Add<DdType, ValueType> subvector = rewardModel.getTotalRewardVector(maybeStatesAdd, submatrix, model.getColumnVariables());
+                    
+                    // Since we are cutting away target and infinity states, we need to account for this by giving
+                    // choices the value infinity that have some successor contained in the infinity states.
+                    storm::dd::Bdd<DdType> choicesWithInfinitySuccessor = (maybeStates && transitionMatrixBdd && infinityStates.swapVariables(model.getRowColumnMetaVariablePairs())).existsAbstract(model.getColumnVariables());
+                    subvector = choicesWithInfinitySuccessor.ite(model.getManager().template getInfinity<ValueType>(), subvector);
+                    
+                    // Finally cut away all columns targeting non-maybe states.
+                    submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs());
+                    
+                    // Now solve the resulting equation system.
+                    std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs());
+                    
+                    // Check requirements of solver.
+                    storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(storm::solver::EquationSystemType::ReachabilityRewards, dir);
+                    boost::optional<storm::dd::Bdd<DdType>> initialScheduler;
+                    if (!requirements.empty()) {
+                        if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) {
+                            STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it.");
+                            initialScheduler = computeValidSchedulerHint(storm::solver::EquationSystemType::ReachabilityRewards, model, transitionMatrix, maybeStates, targetStates);
+                            requirements.clearValidInitialScheduler();
                         }
-                        solver->setLowerBound(storm::utility::zero<ValueType>());
-                        solver->setRequirementsChecked();
-
-                        storm::dd::Add<DdType, ValueType> result = solver->solveEquations(dir, model.getManager().template getAddZero<ValueType>(), subvector);
-
-                        return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), infinityStates.ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), result)));
-                    } else {
-                        return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), infinityStates.ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), model.getManager().template getAddZero<ValueType>())));
+                        requirements.clearLowerBounds();
+                        STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Could not establish requirements of solver.");
+                    }
+                    if (initialScheduler) {
+                        solver->setInitialScheduler(initialScheduler.get());
                     }
+                    solver->setLowerBound(storm::utility::zero<ValueType>());
+                    solver->setRequirementsChecked();
+                    
+                    storm::dd::Add<DdType, ValueType> result = solver->solveEquations(dir, startValues ? maybeStates.ite(startValues.get(), model.getManager().template getAddZero<ValueType>()) : model.getManager().template getAddZero<ValueType>(), subvector);
+                    
+                    return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), infinityStates.ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), result)));
+                } else {
+                    return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>(model.getReachableStates(), infinityStates.ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), model.getManager().template getAddZero<ValueType>())));
                 }
             }
             
diff --git a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h
index 0dd68f188..4bbbe11df 100644
--- a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h
+++ b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h
@@ -25,7 +25,7 @@ namespace storm {
                 
                 static std::unique_ptr<CheckResult> computeNextProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& nextStates);
                 
-                static std::unique_ptr<CheckResult> computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory);
+                static std::unique_ptr<CheckResult> computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory, boost::optional<storm::dd::Add<DdType, ValueType>> const& startValues = boost::none);
                 
                 static std::unique_ptr<CheckResult> computeGloballyProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory);
                 
@@ -33,7 +33,7 @@ namespace storm {
                 
                 static std::unique_ptr<CheckResult> computeInstantaneousRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory);
                 
-                static std::unique_ptr<CheckResult> computeReachabilityRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd<DdType> const& targetStates, bool qualitative, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory);
+                static std::unique_ptr<CheckResult> computeReachabilityRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd<DdType> const& targetStates, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory, boost::optional<storm::dd::Add<DdType, ValueType>> const& startValues = boost::none);
             };
             
         }