diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
index ade41c728..cd2422f2b 100644
--- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
+++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
@@ -163,7 +163,7 @@ namespace storm {
                 dtmc.writeDotToStream(modelDot);
                 modelDot.close();
             }
-            
+
             storm::modelchecker::helper::SparseLTLHelper<ValueType, false> helper(dtmc.getTransitionMatrix(), this->getModel().getNumberOfStates());
             storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, dtmc);
 
diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
index 2bcc9478a..b9749ca55 100644
--- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
@@ -313,98 +313,6 @@ namespace storm {
                 multiplier->multiply(env, result, nullptr, result);
                 return result;
             }
-            
-            template<typename ValueType, typename RewardModelType>
-            std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeDAProductProbabilities(Environment const& env, typename storm::models::sparse::Dtmc<ValueType,RewardModelType> const& dtmc, storm::solver::SolveGoal<ValueType>&& goal, storm::automata::DeterministicAutomaton const& da, std::map<std::string, storm::storage::BitVector>& apSatSets, bool qualitative) {
-                const storm::automata::APSet& apSet = da.getAPSet();
-
-                std::vector<storm::storage::BitVector> apLabels;
-                for (const std::string& ap : apSet.getAPs()) {
-                    auto it = apSatSets.find(ap);
-                    STORM_LOG_THROW(it != apSatSets.end(), storm::exceptions::InvalidOperationException, "Deterministic automaton has AP " << ap << ", does not appear in formula");
-
-                    apLabels.push_back(std::move(it->second));
-                }
-
-                storm::storage::BitVector statesOfInterest;
-                if (goal.hasRelevantValues()) {
-                    statesOfInterest = goal.relevantValues();
-                } else {
-                    // product from all model states
-                    statesOfInterest = storm::storage::BitVector(dtmc.getNumberOfStates(), true);
-                }
-
-                STORM_LOG_INFO("Building DTMC-DA product with deterministic automaton, starting from " << statesOfInterest.getNumberOfSetBits() << " model states...");
-                storm::transformer::DAProductBuilder productBuilder(da, apLabels);
-                auto product = productBuilder.build(dtmc, statesOfInterest);
-                STORM_LOG_INFO("Product DTMC has " << product->getProductModel().getNumberOfStates() << " states and "
-                        << product->getProductModel().getNumberOfTransitions() << " transitions.");
-
-                if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isTraceSet()) {
-                    STORM_LOG_TRACE("Writing model to model.dot");
-                    std::ofstream modelDot("model.dot");
-                    dtmc.writeDotToStream(modelDot);
-                    modelDot.close();
-
-                    STORM_LOG_TRACE("Writing product model to product.dot");
-                    std::ofstream productDot("product.dot");
-                    product->getProductModel().writeDotToStream(productDot);
-                    productDot.close();
-
-                    STORM_LOG_TRACE("Product model mapping:");
-                    std::stringstream str;
-                    product->printMapping(str);
-                    STORM_LOG_TRACE(str.str());
-                }
-
-                STORM_LOG_INFO("Computing BSCCs and checking for acceptance...");
-                
-                storm::storage::StronglyConnectedComponentDecomposition<ValueType> bottomSccs(product->getProductModel().getTransitionMatrix(),
-                                                                                              storage::StronglyConnectedComponentDecompositionOptions().onlyBottomSccs().dropNaiveSccs());
-                storm::storage::BitVector acceptingBSCC(product->getProductModel().getNumberOfStates());
-                std::size_t checkedBSCCs = 0, acceptingBSCCs = 0, acceptingBSCCStates = 0;
-                for (auto& scc : bottomSccs) {
-                    checkedBSCCs++;
-                    if (product->getAcceptance()->isAccepting(scc)) {
-                        acceptingBSCCs++;
-                        for (auto& state : scc) {
-                            acceptingBSCC.set(state);
-                            acceptingBSCCStates++;
-                        }
-                    }
-                }
-
-                STORM_LOG_INFO("BSCC analysis: " << acceptingBSCCs << " of " << checkedBSCCs << " BSCCs were accepting (" << acceptingBSCCStates << " states in accepting BSCCs).");
-
-                if (acceptingBSCCs == 0) {
-                    STORM_LOG_INFO("No accepting BSCCs, skipping probability computation.");
-                    std::vector<ValueType> numericResult(dtmc.getNumberOfStates(), storm::utility::zero<ValueType>());
-                    return numericResult;
-                }
-
-                STORM_LOG_INFO("Computing probabilities for reaching accepting BSCCs...");
-
-                storm::storage::BitVector bvTrue(product->getProductModel().getNumberOfStates(), true);
-
-                storm::solver::SolveGoal<ValueType> solveGoalProduct(goal);
-                storm::storage::BitVector soiProduct(product->getStatesOfInterest());
-                solveGoalProduct.setRelevantValues(std::move(soiProduct));
-
-                std::vector<ValueType> prodNumericResult
-                    = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeUntilProbabilities(env,
-                                                                                                               std::move(solveGoalProduct),
-                                                                                                               product->getProductModel().getTransitionMatrix(),
-                                                                                                               product->getProductModel().getBackwardTransitions(),
-                                                                                                               bvTrue,
-                                                                                                               acceptingBSCC,
-                                                                                                               qualitative);
-
-                std::vector<ValueType> numericResult = product->projectToOriginalModel(dtmc, prodNumericResult);
-                return numericResult;
-            }
-
-
-
 
             template<typename ValueType, typename RewardModelType>
             std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeCumulativeRewards(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound) {
diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h
index 4af089f9b..aaea5b7c1 100644
--- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h
+++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h
@@ -48,8 +48,6 @@ namespace storm {
 
                 static std::vector<ValueType> computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative);
 
-                static std::vector<ValueType> computeDAProductProbabilities(Environment const& env, typename storm::models::sparse::Dtmc<ValueType,RewardModelType> const& dtmc, storm::solver::SolveGoal<ValueType>&& goal, storm::automata::DeterministicAutomaton const& da, std::map<std::string, storm::storage::BitVector>& apSatSets, bool qualitative);
-
                 static std::vector<ValueType> computeCumulativeRewards(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound);
                 
                 static std::vector<ValueType> computeInstantaneousRewards(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount);