diff --git a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
index b7b7bf385..fcbe3c018 100644
--- a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
+++ b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
@@ -242,6 +242,11 @@ namespace storm {
                         // 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);
+                        
                         // Before cutting the non-maybe columns, we need to compute the sizes of the row groups.
                         storm::dd::Add<DdType, uint_fast64_t> stateActionAdd = (submatrix.notZero().existsAbstract(model.getColumnVariables()) || subvector.notZero()).template toAdd<uint_fast64_t>();
                         std::vector<uint_fast64_t> rowGroupSizes = stateActionAdd.sumAbstract(model.getNondeterminismVariables()).toVector(odd);
@@ -254,7 +259,7 @@ namespace storm {
                         
                         // Translate the symbolic matrix/vector to their explicit representations.
                         std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd);
-                        
+                                                
                         // Now solve the resulting equation system.
                         std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(explicitRepresentation.first);
                         solver->solveEquationSystem(dir, x, explicitRepresentation.second);
diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
index 09cac3521..a9ca1fe2d 100644
--- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
+++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
@@ -275,15 +275,15 @@ namespace storm {
             template<typename ValueType>
             std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeReachabilityRewardsHelper(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
                 
-                std::vector<uint_fast64_t> nondeterminsticChoiceIndices = transitionMatrix.getRowGroupIndices();
+                std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices();
                 
                 // Determine which states have a reward of infinity by definition.
                 storm::storage::BitVector infinityStates;
                 storm::storage::BitVector trueStates(transitionMatrix.getRowGroupCount(), true);
                 if (dir == OptimizationDirection::Minimize) {
-                    infinityStates = storm::utility::graph::performProb1E(transitionMatrix, nondeterminsticChoiceIndices, backwardTransitions, trueStates, targetStates);
+                    infinityStates = storm::utility::graph::performProb1E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, trueStates, targetStates);
                 } else {
-                    infinityStates = storm::utility::graph::performProb1A(transitionMatrix, nondeterminsticChoiceIndices, backwardTransitions, trueStates, targetStates);
+                    infinityStates = storm::utility::graph::performProb1A(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, trueStates, targetStates);
                 }
                 infinityStates.complement();
                 storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates;
@@ -310,13 +310,12 @@ namespace storm {
                         
                         // Prepare the right-hand side of the equation system.
                         std::vector<ValueType> b = totalStateRewardVectorGetter(submatrix.getRowCount(), transitionMatrix, maybeStates);
-                        
-                        // This also means that -- when minimizing -- we have to set the entries to infinity that have
-                        // any successor that is an "infinity state". This prevents the action from "being taken" and
-                        // forces the choice that leads to a reward less than infinity.
+
+                        // 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.
                         uint_fast64_t currentRow = 0;
                         for (auto state : maybeStates) {
-                            for (uint_fast64_t row = nondeterminsticChoiceIndices[state]; row < nondeterminsticChoiceIndices[state + 1]; ++row, ++currentRow) {
+                            for (uint_fast64_t row = nondeterministicChoiceIndices[state]; row < nondeterministicChoiceIndices[state + 1]; ++row, ++currentRow) {
                                 for (auto const& element : transitionMatrix.getRow(row)) {
                                     if (infinityStates.get(element.getColumn())) {
                                         b[currentRow] = storm::utility::infinity<ValueType>();
@@ -327,7 +326,7 @@ namespace storm {
                         }
                         
                         // Create vector for results for maybe states.
-                        std::vector<ValueType> x(maybeStates.getNumberOfSetBits());
+                        std::vector<ValueType> x(maybeStates.getNumberOfSetBits(), storm::utility::zero<ValueType>());
                         
                         // Solve the corresponding system of equations.
                         std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(submatrix);
diff --git a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
index 52447c289..329591bf1 100644
--- a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
+++ b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
@@ -192,6 +192,11 @@ namespace storm {
                         // 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());
                         
diff --git a/src/storage/dd/DdManager.cpp b/src/storage/dd/DdManager.cpp
index 17e237986..9281a0a33 100644
--- a/src/storage/dd/DdManager.cpp
+++ b/src/storage/dd/DdManager.cpp
@@ -3,6 +3,7 @@
 #include "src/storage/expressions/ExpressionManager.h"
 
 #include "src/utility/macros.h"
+#include "src/utility/constants.h"
 #include "src/exceptions/InvalidArgumentException.h"
 
 namespace storm {
@@ -34,6 +35,12 @@ namespace storm {
             return Add<LibraryType, ValueType>(*this, internalDdManager.template getAddZero<ValueType>());
         }
         
+        template<DdType LibraryType>
+        template<typename ValueType>
+        Add<LibraryType, ValueType> DdManager<LibraryType>::getInfinity() const {
+            return getConstant(storm::utility::infinity<ValueType>());
+        }
+        
         template<DdType LibraryType>
         template<typename ValueType>
         Add<LibraryType, ValueType> DdManager<LibraryType>::getConstant(ValueType const& value) const {
@@ -315,6 +322,9 @@ namespace storm {
         template Add<DdType::CUDD, double> DdManager<DdType::CUDD>::getAddOne() const;
         template Add<DdType::CUDD, uint_fast64_t> DdManager<DdType::CUDD>::getAddOne() const;
 
+        template Add<DdType::CUDD, double> DdManager<DdType::CUDD>::getInfinity<double>() const;
+        template Add<DdType::CUDD, uint_fast64_t> DdManager<DdType::CUDD>::getInfinity<uint_fast64_t>() const;
+
         template Add<DdType::CUDD, double> DdManager<DdType::CUDD>::getConstant(double const& value) const;
         template Add<DdType::CUDD, uint_fast64_t> DdManager<DdType::CUDD>::getConstant(uint_fast64_t const& value) const;
         
@@ -330,6 +340,9 @@ namespace storm {
         template Add<DdType::Sylvan, double> DdManager<DdType::Sylvan>::getAddOne() const;
         template Add<DdType::Sylvan, uint_fast64_t> DdManager<DdType::Sylvan>::getAddOne() const;
         
+        template Add<DdType::Sylvan, double> DdManager<DdType::Sylvan>::getInfinity<double>() const;
+        template Add<DdType::Sylvan, uint_fast64_t> DdManager<DdType::Sylvan>::getInfinity<uint_fast64_t>() const;
+        
         template Add<DdType::Sylvan, double> DdManager<DdType::Sylvan>::getConstant(double const& value) const;
         template Add<DdType::Sylvan, uint_fast64_t> DdManager<DdType::Sylvan>::getConstant(uint_fast64_t const& value) const;
         
diff --git a/src/storage/dd/DdManager.h b/src/storage/dd/DdManager.h
index ca7fd4ca0..7f8df8c92 100644
--- a/src/storage/dd/DdManager.h
+++ b/src/storage/dd/DdManager.h
@@ -69,6 +69,14 @@ namespace storm {
              */
             template<typename ValueType>
             Add<LibraryType, ValueType> getAddZero() const;
+
+            /*!
+             * Retrieves an ADD representing the constant infinity function.
+             *
+             * @return An ADD representing the constant infinity function.
+             */
+            template<typename ValueType>
+            Add<LibraryType, ValueType> getInfinity() const;
             
             /*!
              * Retrieves an ADD representing the constant function with the given value.