diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp
index 842580ef6..41cff1408 100644
--- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp
+++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp
@@ -1,12 +1,61 @@
 #include "storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h"
+
+#include "storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h"
+
 #include "storm/models/sparse/MarkovAutomaton.h"
 #include "storm/models/sparse/Mdp.h"
 #include "storm/models/sparse/StandardRewardModel.h"
 #include "storm/utility/solver.h"
+#include "storm/utility/graph.h"
+#include "storm/storage/SparseMatrix.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/MultiObjectiveSettings.h"
+
+#include "storm/exceptions/InvalidOperationException.h"
 
 namespace storm {
     namespace modelchecker {
         namespace multiobjective {
+
+            
+            storm::storage::BitVector encodingSettings() {
+                storm::storage::BitVector res(64, false);
+                if (storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().isMaxStepsSet()) {
+                    res.setFromInt(0, 64, storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getMaxSteps());
+                }
+                return res;
+            }
+            
+            bool isMinNegativeEncoding() {
+                return encodingSettings().get(63);
+            }
+            
+            bool isMaxDiffEncoding() {
+                bool result = encodingSettings().get(62);
+                STORM_LOG_ERROR_COND(!result || !isMinNegativeEncoding(), "maxDiffEncoding only works without minnegative encoding.");
+                return result;
+            }
+            
+            bool choiceVarReduction() {
+                return encodingSettings().get(61);
+            }
+            
+            bool inOutEncoding() {
+                return encodingSettings().get(60);
+            }
+            
+            bool assertBottomStateSum() {
+                bool result = encodingSettings().get(59);
+                STORM_LOG_ERROR_COND(!result || inOutEncoding(), "Asserting bottom state sum is only relevant for in-out encoding.");
+                return result;
+            }
+            
+            bool useNonOptimalSolutions() {
+                bool result = encodingSettings().get(58);
+                STORM_LOG_ERROR_COND(!result || inOutEncoding(), "Asserting bottom state sum is only relevant for in-out encoding.");
+                return result;
+            }
             
             template <typename ModelType, typename GeometryValueType>
             DeterministicSchedsLpChecker<ModelType, GeometryValueType>::DeterministicSchedsLpChecker(Environment const& env, ModelType const& model, std::vector<DeterministicSchedsObjectiveHelper<ModelType>> const& objectiveHelper) : model(model) , objectiveHelper(objectiveHelper) {
@@ -43,7 +92,7 @@ namespace storm {
                 // set up objective function for the given weight vector
                 for (uint64_t objIndex = 0; objIndex < initialStateResults.size(); ++objIndex) {
                     currentObjectiveVariables.push_back(lpModel->addUnboundedContinuousVariable("w_" + std::to_string(objIndex), storm::utility::convertNumber<ValueType>(weightVector[objIndex])));
-                    if (objectiveHelper[objIndex].minimizing()) {
+                    if (objectiveHelper[objIndex].minimizing() && !isMinNegativeEncoding()) {
                         lpModel->addConstraint("", currentObjectiveVariables.back().getExpression() == -initialStateResults[objIndex]);
                     } else {
                         lpModel->addConstraint("", currentObjectiveVariables.back().getExpression() == initialStateResults[objIndex]);
@@ -105,7 +154,7 @@ namespace storm {
                 
                 std::vector<Point> foundPoints;
                 std::vector<Polytope> infeasableAreas;
-                checkRecursive(polytopeTree, eps, foundPoints, infeasableAreas);
+                checkRecursive(polytopeTree, eps, foundPoints, infeasableAreas, 0);
                 
                 swCheck.stop();
                 std::cout << " done!" << std::endl;
@@ -114,13 +163,17 @@ namespace storm {
             
             template <typename ModelType, typename GeometryValueType>
             void DeterministicSchedsLpChecker<ModelType, GeometryValueType>::initializeLpModel(Environment const& env) {
+                STORM_LOG_INFO("Initializing LP model with " << model.getNumberOfStates() << " states.");
                 uint64_t numStates = model.getNumberOfStates();
+                uint64_t initialState = *model.getInitialStates().begin();
+
                 lpModel = storm::utility::solver::getLpSolver<ValueType>("model");
                 gurobiLpModel = dynamic_cast<storm::solver::GurobiLpSolver<ValueType>*>(lpModel.get());
                 
                 lpModel->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
                 initialStateResults.clear();
                 
+                auto zero = lpModel->getConstant(storm::utility::zero<ValueType>());
                 auto one = lpModel->getConstant(storm::utility::one<ValueType>());
                 
                 // Create choice variables and assert that at least one choice is taken at each state.
@@ -132,98 +185,233 @@ namespace storm {
                         choiceVars.emplace_back();
                     } else {
                         std::vector<storm::expressions::Expression> localChoices;
+                        if (choiceVarReduction()) {
+                            --numChoices;
+                        }
                         for (uint64_t choice = 0; choice < numChoices; ++choice) {
                             localChoices.push_back(lpModel->addBoundedIntegerVariable("c" + std::to_string(state) + "_" + std::to_string(choice), 0, 1).getExpression());
+                            choiceVars.push_back(localChoices.back());
+                        }
+                        storm::expressions::Expression localChoicesSum = storm::expressions::sum(localChoices).reduceNesting();
+                        if (choiceVarReduction()) {
+                            lpModel->addConstraint("", localChoicesSum <= one);
+                            choiceVars.push_back(one - localChoicesSum);
+                        } else {
+                            lpModel->addConstraint("", localChoicesSum == one);
                         }
-                        lpModel->addConstraint("", storm::expressions::sum(localChoices).reduceNesting() == one);
-                        choiceVars.insert(choiceVars.end(), localChoices.begin(), localChoices.end());
                     }
                 }
                 
-                for (uint64_t objIndex = 0; objIndex < objectiveHelper.size(); ++objIndex) {
-                    auto const& schedulerIndependentStates = objectiveHelper[objIndex].getSchedulerIndependentStateValues();
-                    // Create state variables
-                    std::vector<storm::expressions::Expression> stateVars;
-                    stateVars.reserve(numStates);
-                    for (uint64_t state = 0; state < numStates; ++state) {
-                        auto valIt = schedulerIndependentStates.find(state);
-                        if (valIt == schedulerIndependentStates.end()) {
-                            stateVars.push_back(lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex) + "_" + std::to_string(state), objectiveHelper[objIndex].getLowerValueBoundAtState(env, state), objectiveHelper[objIndex].getUpperValueBoundAtState(env, state)).getExpression());
-                        } else {
-                            stateVars.push_back(lpModel->getConstant(valIt->second));
-                        }
-                        if (state == *model.getInitialStates().begin()) {
-                            initialStateResults.push_back(stateVars.back());
+                if (inOutEncoding()) {
+                    storm::storage::BitVector bottomStates(model.getNumberOfStates(), true);
+                    for (auto const& helper : objectiveHelper) {
+                        STORM_LOG_THROW(helper.isTotalRewardObjective(), storm::exceptions::InvalidOperationException, "The given type of encoding is only supported if the objectives can be reduced to total reward objectives.");
+                        storm::storage::BitVector objBottomStates(model.getNumberOfStates(), false);
+                        for (auto const& stateVal : helper.getSchedulerIndependentStateValues()) {
+                            STORM_LOG_THROW(storm::utility::isZero(stateVal.second), storm::exceptions::InvalidOperationException, "Non-zero constant state-values not allowed for this type of encoding.");
+                            objBottomStates.set(stateVal.first, true);
                         }
+                        bottomStates &= objBottomStates;
                     }
+                    storm::storage::BitVector nonBottomStates = ~bottomStates;
+                    STORM_LOG_TRACE("Found " << bottomStates.getNumberOfSetBits() << " bottom states.");
+                    STORM_LOG_ERROR_COND(storm::utility::graph::performProb1A(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), model.getBackwardTransitions(), nonBottomStates, bottomStates).full(), "End components not yet treated correctly.");
                     
-                    // Create and assert choice values
-                    auto const& choiceValueOffsets = objectiveHelper[objIndex].getChoiceValueOffsets();
-                    for (uint64_t state = 0; state < numStates; ++state) {
-                        if (schedulerIndependentStates.find(state) != schedulerIndependentStates.end()) {
-                            continue;
+                    // Compute upper bounds for each state
+                    std::vector<ValueType> visitingTimesUpperBounds;
+                    {
+                        // TODO: this doesn't work if there are end components.
+                        storm::storage::SparseMatrix<ValueType> transitions = model.getTransitionMatrix().getSubmatrix(true, nonBottomStates, nonBottomStates);
+                        std::vector<ValueType> probabilitiesToBottomStates = model.getTransitionMatrix().getConstrainedRowGroupSumVector(nonBottomStates, bottomStates);
+                        auto subsystemBounds = storm::modelchecker::helper::BaierUpperRewardBoundsComputer<ValueType>::computeUpperBoundOnExpectedVisitingTimes(transitions, probabilitiesToBottomStates);
+                        uint64_t subsystemState = 0;
+                        visitingTimesUpperBounds.reserve(bottomStates.size());
+                        for (uint64_t state = 0; state < bottomStates.size(); ++state) {
+                            if (bottomStates.get(state)) {
+                                visitingTimesUpperBounds.push_back(storm::utility::zero<ValueType>());
+                            } else {
+                                visitingTimesUpperBounds.push_back(subsystemBounds[subsystemState]);
+                                ++subsystemState;
+                            }
                         }
-                        storm::expressions::Expression stateValue;
-                        uint64_t numChoices = model.getNumberOfChoices(state);
-                        uint64_t choiceOffset = model.getTransitionMatrix().getRowGroupIndices()[state];
-                        for (uint64_t choice = 0; choice < numChoices; ++choice) {
-                            storm::expressions::Expression choiceValue;
-                            auto valIt = choiceValueOffsets.find(choiceOffset + choice);
-                            if (valIt != choiceValueOffsets.end()) {
-                                choiceValue = lpModel->getConstant(valIt->second);
+                        assert(subsystemState == subsystemBounds.size());
+                    }
+                    // create choiceValue variables and assert deterministic ones.
+                    std::vector<storm::expressions::Expression> choiceValVars(model.getNumberOfChoices());
+                    for (auto const& state : nonBottomStates) {
+                        for (uint64_t globalChoice = model.getTransitionMatrix().getRowGroupIndices()[state]; globalChoice < model.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++globalChoice) {
+                            choiceValVars[globalChoice] = lpModel->addBoundedContinuousVariable("y" + std::to_string(globalChoice), storm::utility::zero<ValueType>(), visitingTimesUpperBounds[state]).getExpression();
+                            if (model.getNumberOfChoices(state) > 1) {;
+                                lpModel->addConstraint("", choiceValVars[globalChoice] <= lpModel->getConstant(visitingTimesUpperBounds[state]) * choiceVars[globalChoice]);
                             }
-                            for (auto const& transition : model.getTransitionMatrix().getRow(state, choice)) {
-                                storm::expressions::Expression transitionValue = lpModel->getConstant(transition.getValue()) * stateVars[transition.getColumn()];
-                                if (choiceValue.isInitialized()) {
-                                    choiceValue = choiceValue + transitionValue;
+                        }
+                    }
+                    // Get 'in' and 'out' expressions
+                    std::vector<storm::expressions::Expression> bottomStatesIn;
+                    std::vector<std::vector<storm::expressions::Expression>> ins(numStates), outs(numStates);
+                    ins[initialState].push_back(one);
+                    for (auto const& state : nonBottomStates) {
+                        for (uint64_t globalChoice = model.getTransitionMatrix().getRowGroupIndices()[state]; globalChoice < model.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++globalChoice) {
+                            for (auto const& transition : model.getTransitionMatrix().getRow(globalChoice)) {
+                                uint64_t successor = transition.getColumn();
+                                storm::expressions::Expression exp = lpModel->getConstant(transition.getValue()) * choiceValVars[globalChoice];
+                                if (bottomStates.get(successor)) {
+                                    bottomStatesIn.push_back(exp);
                                 } else {
-                                    choiceValue = transitionValue;
+                                    ins[successor].push_back(exp);
                                 }
                             }
-                            choiceValue = choiceValue.simplify().reduceNesting();
-                            if (numChoices == 1) {
-                                stateValue = choiceValue;
-                            } else {
-                                auto choiceValVar = lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex) + "_" + std::to_string(state) + "_" + std::to_string(choice), storm::utility::zero<ValueType>(), objectiveHelper[objIndex].getUpperValueBoundAtState(env, state)).getExpression();
-                                uint64_t globalChoiceIndex = model.getTransitionMatrix().getRowGroupIndices()[state] + choice;
-                                storm::expressions::Expression upperValueBoundAtChoice = lpModel->getConstant(objectiveHelper[objIndex].getUpperValueBoundAtState(env, state));
-                                if (objectiveHelper[objIndex].minimizing()) {
-                                    lpModel->addConstraint("", choiceValVar + (upperValueBoundAtChoice * (one - choiceVars[globalChoiceIndex])) >= choiceValue);
-                                    // Optional: lpModel->addConstraint("", choiceValVar <= choiceValue);
+                            outs[state].push_back(choiceValVars[globalChoice]);
+                        }
+                    }
+                    
+                    // Assert 'in == out' at each state
+                    for (auto const& state : nonBottomStates) {
+                        lpModel->addConstraint("", storm::expressions::sum(ins[state]) == storm::expressions::sum(outs[state]));
+                        
+                    }
+                    if (assertBottomStateSum()) {
+                        lpModel->addConstraint("", storm::expressions::sum(bottomStatesIn) == one);
+                    }
+                    
+                    
+                    // create initial state results for each objective
+                    for (uint64_t objIndex = 0; objIndex < objectiveHelper.size(); ++objIndex) {
+                        auto choiceValueOffsets = objectiveHelper[objIndex].getChoiceValueOffsets();
+                        std::vector<storm::expressions::Expression> objValue;
+                        for (auto const& state : nonBottomStates) {
+                            for (uint64_t globalChoice = model.getTransitionMatrix().getRowGroupIndices()[state]; globalChoice < model.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++globalChoice) {
+                                auto choiceValueIt = choiceValueOffsets.find(globalChoice);
+                                if (choiceValueIt != choiceValueOffsets.end()) {
+                                    assert(!storm::utility::isZero(choiceValueIt->second));
+                                    objValue.push_back(lpModel->getConstant(choiceValueIt->second) * choiceValVars[globalChoice]);
+                                }
+                            }
+                        }
+                        auto objValueVariable = lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex), objectiveHelper[objIndex].getLowerValueBoundAtState(env, initialState), objectiveHelper[objIndex].getUpperValueBoundAtState(env, initialState));
+                        lpModel->addConstraint("", objValueVariable == storm::expressions::sum(objValue));
+                        initialStateResults.push_back(objValueVariable);
+                    }
+                    
+                } else {
+                    // 'classic' backward encoding.
+                    for (uint64_t objIndex = 0; objIndex < objectiveHelper.size(); ++objIndex) {
+                        auto const& schedulerIndependentStates = objectiveHelper[objIndex].getSchedulerIndependentStateValues();
+                        // Create state variables
+                        std::vector<storm::expressions::Expression> stateVars;
+                        stateVars.reserve(numStates);
+                        for (uint64_t state = 0; state < numStates; ++state) {
+                            auto valIt = schedulerIndependentStates.find(state);
+                            if (valIt == schedulerIndependentStates.end()) {
+                                if (objectiveHelper[objIndex].minimizing() && isMinNegativeEncoding()) {
+                                    stateVars.push_back(lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex) + "_" + std::to_string(state), -objectiveHelper[objIndex].getUpperValueBoundAtState(env, state), -objectiveHelper[objIndex].getLowerValueBoundAtState(env, state)).getExpression());
                                 } else {
-                                    lpModel->addConstraint("", choiceValVar <= choiceValue);
-                                    lpModel->addConstraint("", choiceValVar <= upperValueBoundAtChoice * choiceVars[globalChoiceIndex]);
+                                    stateVars.push_back(lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex) + "_" + std::to_string(state), objectiveHelper[objIndex].getLowerValueBoundAtState(env, state), objectiveHelper[objIndex].getUpperValueBoundAtState(env, state)).getExpression());
                                 }
-                                if (choice == 0) {
-                                    stateValue = choiceValVar;
+                            } else {
+                                if (objectiveHelper[objIndex].minimizing() && isMinNegativeEncoding()) {
+                                    stateVars.push_back(lpModel->getConstant(-valIt->second));
                                 } else {
-                                    stateValue = stateValue + choiceValVar;
+                                    stateVars.push_back(lpModel->getConstant(valIt->second));
                                 }
-                                // Alternative encoding: (Then the sum of the choiceVars also has to be >= one (instead of == one)
-                                //storm::expressions::Expression maxDiff = lpModel->getConstant(objectiveHelper[objIndex].getUpperValueBoundAtState(env, state) - objectiveHelper[objIndex].getLowerValueBoundAtState(env, state)) * (one - choiceVars[globalChoiceIndex]);
-                                //lpModel->addConstraint("", stateVars[state] - choiceValVar <= maxDiff);
-                                //lpModel->addConstraint("", choiceValVar - stateVars[state] <= maxDiff);
+                            }
+                            if (state == initialState) {
+                                initialStateResults.push_back(stateVars.back());
                             }
                         }
-                        if (objectiveHelper[objIndex].minimizing()) {
-                            lpModel->addConstraint("", stateVars[state] >= stateValue);
-                        } else {
-                            lpModel->addConstraint("", stateVars[state] <= stateValue);
+                        
+                        // Create and assert choice values
+                        auto const& choiceValueOffsets = objectiveHelper[objIndex].getChoiceValueOffsets();
+                        for (uint64_t state = 0; state < numStates; ++state) {
+                            if (schedulerIndependentStates.find(state) != schedulerIndependentStates.end()) {
+                                continue;
+                            }
+                            storm::expressions::Expression stateValue;
+                            uint64_t numChoices = model.getNumberOfChoices(state);
+                            uint64_t choiceOffset = model.getTransitionMatrix().getRowGroupIndices()[state];
+                            storm::expressions::Expression upperValueBoundAtState = lpModel->getConstant(objectiveHelper[objIndex].getUpperValueBoundAtState(env, state));
+                            for (uint64_t choice = 0; choice < numChoices; ++choice) {
+                                storm::expressions::Expression choiceValue;
+                                auto valIt = choiceValueOffsets.find(choiceOffset + choice);
+                                if (valIt != choiceValueOffsets.end()) {
+                                    if (objectiveHelper[objIndex].minimizing() && isMinNegativeEncoding()) {
+                                        choiceValue = lpModel->getConstant(-valIt->second);
+                                    } else {
+                                        choiceValue = lpModel->getConstant(valIt->second);
+                                    }
+                                }
+                                for (auto const& transition : model.getTransitionMatrix().getRow(state, choice)) {
+                                    storm::expressions::Expression transitionValue = lpModel->getConstant(transition.getValue()) * stateVars[transition.getColumn()];
+                                    if (choiceValue.isInitialized()) {
+                                        choiceValue = choiceValue + transitionValue;
+                                    } else {
+                                        choiceValue = transitionValue;
+                                    }
+                                }
+                                choiceValue = choiceValue.simplify().reduceNesting();
+                                if (numChoices == 1) {
+                                    stateValue = choiceValue;
+                                } else {
+                                    uint64_t globalChoiceIndex = model.getTransitionMatrix().getRowGroupIndices()[state] + choice;
+                                    if (isMaxDiffEncoding()) {
+                                        storm::expressions::Expression maxDiff = upperValueBoundAtState * (one - choiceVars[globalChoiceIndex]);
+                                        if (objectiveHelper[objIndex].minimizing()) {
+                                            lpModel->addConstraint("", stateVars[state] >= choiceValue - maxDiff);
+                                        } else {
+                                            lpModel->addConstraint("", stateVars[state] <= choiceValue + maxDiff);
+                                        }
+                                    }
+                                    
+                                    storm::expressions::Expression choiceValVar;
+                                    if (objectiveHelper[objIndex].minimizing() && isMinNegativeEncoding()) {
+                                        choiceValVar = lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex) + "_" + std::to_string(state) + "_" + std::to_string(choice), -objectiveHelper[objIndex].getUpperValueBoundAtState(env, state), storm::utility::zero<ValueType>()).getExpression();
+                                    } else {
+                                        choiceValVar = lpModel->addBoundedContinuousVariable("x" + std::to_string(objIndex) + "_" + std::to_string(state) + "_" + std::to_string(choice), storm::utility::zero<ValueType>(), objectiveHelper[objIndex].getUpperValueBoundAtState(env, state)).getExpression();
+                                    }
+                                    if (objectiveHelper[objIndex].minimizing()) {
+                                        if (isMinNegativeEncoding()) {
+                                            lpModel->addConstraint("", choiceValVar <= choiceValue);
+                                            lpModel->addConstraint("", choiceValVar <= -upperValueBoundAtState * (one - choiceVars[globalChoiceIndex]));
+                                        } else {
+                                            lpModel->addConstraint("", choiceValVar + (upperValueBoundAtState * (one - choiceVars[globalChoiceIndex])) >= choiceValue);
+                                            // Optional: lpModel->addConstraint("", choiceValVar <= choiceValue);
+                                        }
+                                    } else {
+                                        lpModel->addConstraint("", choiceValVar <= choiceValue);
+                                        lpModel->addConstraint("", choiceValVar <= upperValueBoundAtState * choiceVars[globalChoiceIndex]);
+                                    }
+                                    if (choice == 0) {
+                                        stateValue = choiceValVar;
+                                    } else {
+                                        stateValue = stateValue + choiceValVar;
+                                    }
+                                }
+                            }
+                            if (objectiveHelper[objIndex].minimizing()) {
+                                if (isMinNegativeEncoding()) {
+                                    lpModel->addConstraint("", stateVars[state] <= stateValue + (lpModel->getConstant(storm::utility::convertNumber<ValueType>(numChoices - 1)) * upperValueBoundAtState));
+                                } else {
+                                    lpModel->addConstraint("", stateVars[state] >= stateValue);
+                                }
+                            } else {
+                                lpModel->addConstraint("", stateVars[state] <= stateValue);
+                            }
                         }
                     }
                 }
                 swAux.start();
                 lpModel->update();
                 swAux.stop();
+                STORM_LOG_INFO("Done initializing LP model.");
             }
             
             template <typename ModelType, typename GeometryValueType>
-            void DeterministicSchedsLpChecker<ModelType, GeometryValueType>::checkRecursive(storm::storage::geometry::PolytopeTree <GeometryValueType>& polytopeTree, GeometryValueType const& eps, std::vector<Point>& foundPoints, std::vector<Polytope>& infeasableAreas) {
+            void DeterministicSchedsLpChecker<ModelType, GeometryValueType>::checkRecursive(storm::storage::geometry::PolytopeTree <GeometryValueType>& polytopeTree, GeometryValueType const& eps, std::vector<Point>& foundPoints, std::vector<Polytope>& infeasableAreas, uint64_t const& depth) {
                 std::cout << ".";
                 std::cout.flush();
                 STORM_LOG_ASSERT(!polytopeTree.isEmpty(), "Tree node is empty");
                 STORM_LOG_ASSERT(!polytopeTree.getPolytope()->isEmpty(), "Tree node is empty.");
-                STORM_LOG_TRACE("Checking " << polytopeTree.toString());
+                STORM_LOG_TRACE("Checking at depth " << depth << ": " << polytopeTree.toString());
                 
                 swLpBuild.start();
                 lpModel->push();
@@ -245,6 +433,7 @@ namespace storm {
                     
                     if (lpModel->isInfeasible()) {
                         infeasableAreas.push_back(polytopeTree.getPolytope());
+                        lpModel->writeModelToFile("out.lp");
                         polytopeTree.clear();
                     } else {
                         STORM_LOG_ASSERT(!lpModel->isUnbounded(), "LP result is unbounded.");
@@ -253,7 +442,7 @@ namespace storm {
                             newPoint.push_back(storm::utility::convertNumber<GeometryValueType>(lpModel->getContinuousValue(objVar)));
                         }
                         std::vector<Point> newPoints = {newPoint};
-                        if (gurobiLpModel) {
+                        if (gurobiLpModel && useNonOptimalSolutions()) {
                             // gurobi might have other good solutions.
                             for (uint64_t solutionIndex = 0; solutionIndex < gurobiLpModel->getSolutionCount(); ++ solutionIndex) {
                                 Point p;
@@ -269,7 +458,6 @@ namespace storm {
                                     newPoints.push_back(std::move(p));
                                 }
                             }
-                            std::cout << "found " << (newPoints.size() - 1) << " useful points" << std::endl;
                         }
                         GeometryValueType offset = storm::utility::convertNumber<GeometryValueType>(lpModel->getObjectiveValue());
                         if (gurobiLpModel) {
@@ -289,14 +477,14 @@ namespace storm {
                         }
                         swAux.stop();
                         if (!polytopeTree.isEmpty()) {
-                            checkRecursive(polytopeTree, eps, foundPoints, infeasableAreas);
+                            checkRecursive(polytopeTree, eps, foundPoints, infeasableAreas, depth);
                         }
                     }
                 } else {
                     // Traverse all the children.
                     for (uint64_t childId = 0; childId < polytopeTree.getChildren().size(); ++childId) {
                         uint64_t newPointIndex = foundPoints.size();
-                        checkRecursive(polytopeTree.getChildren()[childId], eps, foundPoints, infeasableAreas);
+                        checkRecursive(polytopeTree.getChildren()[childId], eps, foundPoints, infeasableAreas, depth + 1);
                         STORM_LOG_ASSERT(polytopeTree.getChildren()[childId].isEmpty(), "expected empty children.");
                         // Make the new points known to the right siblings
                         for (; newPointIndex < foundPoints.size(); ++newPointIndex) {
@@ -308,8 +496,11 @@ namespace storm {
                     // All children are empty now, so this node becomes empty.
                     polytopeTree.clear();
                 }
+                STORM_LOG_TRACE("Checking DONE at depth " << depth << " with node " << polytopeTree.toString());
+
                 swLpBuild.start();
                 lpModel->pop();
+                lpModel->update();
                 swLpBuild.stop();
             }
             
diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h
index e22b6d7a8..7c9f7978f 100644
--- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h
+++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h
@@ -48,7 +48,7 @@ namespace storm {
             private:
                 void initializeLpModel(Environment const& env);
                 
-                void checkRecursive(storm::storage::geometry::PolytopeTree<GeometryValueType>& polytopeTree, GeometryValueType const& eps, std::vector<Point>& foundPoints, std::vector<Polytope>& infeasableAreas);
+                void checkRecursive(storm::storage::geometry::PolytopeTree<GeometryValueType>& polytopeTree, GeometryValueType const& eps, std::vector<Point>& foundPoints, std::vector<Polytope>& infeasableAreas, uint64_t const& depth);
                 
                 ModelType const& model;
                 std::vector<DeterministicSchedsObjectiveHelper<ModelType>> const& objectiveHelper;
diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp
index 734a016d0..b1f9ece62 100644
--- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp
+++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp
@@ -219,6 +219,11 @@ namespace storm {
             bool DeterministicSchedsObjectiveHelper<ModelType>::minimizing() const {
                 return storm::solver::minimize(objective.formula->getOptimalityType());
             }
+            
+            template <typename ModelType>
+            bool DeterministicSchedsObjectiveHelper<ModelType>::isTotalRewardObjective() const {
+                return objective.formula->isRewardOperatorFormula() && objective.formula->getSubformula().isTotalRewardFormula();
+            }
 
             template class DeterministicSchedsObjectiveHelper<storm::models::sparse::Mdp<double>>;
             template class DeterministicSchedsObjectiveHelper<storm::models::sparse::Mdp<storm::RationalNumber>>;
diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.h b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.h
index 9cf85f030..c93ef6086 100644
--- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.h
+++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.h
@@ -36,6 +36,11 @@ namespace storm {
                 
                 bool minimizing() const;
                 
+                /*!
+                 * Returns true if this is a total reward objective
+                 */
+                bool isTotalRewardObjective() const;
+                
             private:
                 
                 mutable boost::optional<std::map<uint64_t, ValueType>> schedulerIndependentStateValues;