diff --git a/src/builder/DftExplorationHeuristic.cpp b/src/builder/DftExplorationHeuristic.cpp
index e14c34dee..4bc72ccc1 100644
--- a/src/builder/DftExplorationHeuristic.cpp
+++ b/src/builder/DftExplorationHeuristic.cpp
@@ -3,7 +3,6 @@
 #include "src/utility/macros.h"
 #include "src/utility/constants.h"
 #include "src/exceptions/NotImplementedException.h"
-#include "src/storage/dft/DFTState.h"
 
 #include <limits>
 
@@ -11,74 +10,87 @@ namespace storm {
     namespace builder {
 
         template<typename ValueType>
-        DFTExplorationHeuristic<ValueType>::DFTExplorationHeuristic() : skip(true), depth(std::numeric_limits<std::size_t>::max()), rate(storm::utility::zero<ValueType>()), exitRate(storm::utility::zero<ValueType>()) {
+        DFTExplorationHeuristic<ValueType>::DFTExplorationHeuristic(size_t id) : id(id), expand(false), depth(std::numeric_limits<std::size_t>::max()), rate(storm::utility::zero<ValueType>()), exitRate(storm::utility::zero<ValueType>()) {
             // Intentionally left empty
         }
 
         template<typename ValueType>
-        void DFTExplorationHeuristic<ValueType>::setHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) {
+        void DFTExplorationHeuristic<ValueType>::updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) {
             this->depth = std::min(this->depth, depth);
             this->rate = std::max(this->rate, rate);
             this->exitRate = std::max(this->exitRate, exitRate);
         }
 
         template<typename ValueType>
-        bool DFTExplorationHeuristic<ValueType>::isSkip(double approximationThreshold, ApproximationHeuristic heuristic) const {
-            if (!skip) {
-                return false;
-            }
-            switch (heuristic) {
-                case ApproximationHeuristic::NONE:
-                    return false;
-                case ApproximationHeuristic::DEPTH:
-                    return depth > approximationThreshold;
-                case ApproximationHeuristic::RATERATIO:
-                    return getRateRatio() < approximationThreshold;
-                default:
-                    STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic not known.");
-            }
+        DFTExplorationHeuristicNone<ValueType>::DFTExplorationHeuristicNone(size_t id) : DFTExplorationHeuristic<ValueType>(id) {
+            // Intentionally left empty
+        }
+
+        template<typename ValueType>
+        bool DFTExplorationHeuristicNone<ValueType>::isSkip(double approximationThreshold) const {
+            return false;
+        }
+
+        template<typename ValueType>
+        bool DFTExplorationHeuristicNone<ValueType>::operator<(DFTExplorationHeuristicNone<ValueType> const& other) const {
+            // Just use memory address for comparing
+            // TODO Matthias: better idea?
+            return this > &other;
+        }
+
+        template<typename ValueType>
+        DFTExplorationHeuristicDepth<ValueType>::DFTExplorationHeuristicDepth(size_t id) : DFTExplorationHeuristic<ValueType>(id) {
+            // Intentionally left empty
+        }
+
+        template<typename ValueType>
+        bool DFTExplorationHeuristicDepth<ValueType>::isSkip(double approximationThreshold) const {
+            return !this->expand && this->depth > approximationThreshold;
+        }
+
+        template<typename ValueType>
+        bool DFTExplorationHeuristicDepth<ValueType>::operator<(DFTExplorationHeuristicDepth<ValueType> const& other) const {
+            return this->depth > other.depth;
         }
 
         template<typename ValueType>
-        void DFTExplorationHeuristic<ValueType>::setNotSkip() {
-            skip = false;
+        DFTExplorationHeuristicRateRatio<ValueType>::DFTExplorationHeuristicRateRatio(size_t id) : DFTExplorationHeuristic<ValueType>(id) {
+            // Intentionally left empty
         }
 
         template<typename ValueType>
-        size_t DFTExplorationHeuristic<ValueType>::getDepth() const {
-            return depth;
+        bool DFTExplorationHeuristicRateRatio<ValueType>::isSkip(double approximationThreshold) const {
+            return !this->expand && this->getRateRatio() < approximationThreshold;
         }
 
         template<typename ValueType>
-        bool DFTExplorationHeuristic<ValueType>::compare(DFTExplorationHeuristic<ValueType> other, ApproximationHeuristic heuristic) {
-            switch (heuristic) {
-                case ApproximationHeuristic::NONE:
-                    // Just use memory address for comparing
-                    // TODO Matthias: better idea?
-                    return this > &other;
-                case ApproximationHeuristic::DEPTH:
-                    return this->depth > other.depth;
-                case ApproximationHeuristic::RATERATIO:
-                    return this->getRateRatio() < other.getRateRatio();
-                default:
-                    STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic not known.");
-            }
+        bool DFTExplorationHeuristicRateRatio<ValueType>::operator<(DFTExplorationHeuristicRateRatio<ValueType> const& other) const {
+            return this->getRateRatio() < other.getRateRatio();
         }
 
+
         template<>
-        double DFTExplorationHeuristic<double>::getRateRatio() const {
+        double DFTExplorationHeuristicRateRatio<double>::getRateRatio() const {
             return rate/exitRate;
         }
 
         template<>
-        double DFTExplorationHeuristic<storm::RationalFunction>::getRateRatio() const {
+        double DFTExplorationHeuristicRateRatio<storm::RationalFunction>::getRateRatio() const {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic rate ration does not work.");
         }
 
+
+        // Instantiate templates.
         template class DFTExplorationHeuristic<double>;
+        template class DFTExplorationHeuristicNone<double>;
+        template class DFTExplorationHeuristicDepth<double>;
+        template class DFTExplorationHeuristicRateRatio<double>;
 
 #ifdef STORM_HAVE_CARL
         template class DFTExplorationHeuristic<storm::RationalFunction>;
+        template class DFTExplorationHeuristicNone<storm::RationalFunction>;
+        template class DFTExplorationHeuristicDepth<storm::RationalFunction>;
+        template class DFTExplorationHeuristicRateRatio<storm::RationalFunction>;
 #endif
     }
 }
diff --git a/src/builder/DftExplorationHeuristic.h b/src/builder/DftExplorationHeuristic.h
index 3fd3d72a8..8f12d2ec1 100644
--- a/src/builder/DftExplorationHeuristic.h
+++ b/src/builder/DftExplorationHeuristic.h
@@ -2,16 +2,9 @@
 #define STORM_BUILDER_DFTEXPLORATIONHEURISTIC_H_
 
 #include <memory>
-#include <algorithm>
 
 namespace storm {
 
-    // Forward declaration
-    namespace storage {
-        template<typename ValueType>
-        class DFTState;
-    }
-
     namespace builder {
 
         /*!
@@ -19,32 +12,74 @@ namespace storm {
          */
         enum class ApproximationHeuristic { NONE, DEPTH, RATERATIO };
 
+
+        /*!
+         * General super class for appoximation heuristics.
+         */
         template<typename ValueType>
         class DFTExplorationHeuristic {
 
         public:
-            DFTExplorationHeuristic();
-
-            void setHeuristicValues(size_t depth, ValueType rate, ValueType exitRate);
-
-            bool isSkip(double approximationThreshold, ApproximationHeuristic heuristic) const;
+            DFTExplorationHeuristic(size_t id);
 
-            void setNotSkip();
+            void updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate);
 
-            size_t getDepth() const;
+            virtual bool isSkip(double approximationThreshold) const = 0;
 
-            bool compare(DFTExplorationHeuristic<ValueType> other, ApproximationHeuristic heuristic);
+            void markExpand() {
+                expand = true;
+            }
 
-        private:
+            size_t getId() const {
+                return id;
+            }
 
-            double getRateRatio() const;
+            size_t getDepth() const {
+                return depth;
+            }
 
-            bool skip;
+        protected:
+            size_t id;
+            bool expand;
             size_t depth;
             ValueType rate;
             ValueType exitRate;
 
         };
+
+        template<typename ValueType>
+        class DFTExplorationHeuristicNone : public DFTExplorationHeuristic<ValueType> {
+        public:
+            DFTExplorationHeuristicNone(size_t id);
+
+            bool isSkip(double approximationThreshold) const override;
+
+            bool operator<(DFTExplorationHeuristicNone<ValueType> const& other) const;
+        };
+
+        template<typename ValueType>
+        class DFTExplorationHeuristicDepth : public DFTExplorationHeuristic<ValueType> {
+        public:
+            DFTExplorationHeuristicDepth(size_t id);
+
+            bool isSkip(double approximationThreshold) const override;
+
+            bool operator<(DFTExplorationHeuristicDepth<ValueType> const& other) const;
+        };
+
+        template<typename ValueType>
+        class DFTExplorationHeuristicRateRatio : public DFTExplorationHeuristic<ValueType> {
+        public:
+            DFTExplorationHeuristicRateRatio(size_t id);
+
+            bool isSkip(double approximationThreshold) const override;
+
+            bool operator<(DFTExplorationHeuristicRateRatio<ValueType> const& other) const;
+
+        private:
+            double getRateRatio() const;
+        };
+
     }
 }
 
diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp
index 268ec03dc..5595a5f49 100644
--- a/src/builder/ExplicitDFTModelBuilderApprox.cpp
+++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp
@@ -31,8 +31,8 @@ namespace storm {
                 generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates),
                 matrixBuilder(!generator.isDeterministicModel()),
                 stateStorage(((dft.stateVectorSize() / 64) + 1) * 64),
-                explorationQueue([this](StateType idA, StateType idB) {
-                        return isPriorityGreater(idA, idB);
+                explorationQueue([this](ExplorationHeuristicPointer a, ExplorationHeuristicPointer b) {
+                        return *a < *b;
                     })
         {
             // Intentionally left empty.
@@ -76,7 +76,7 @@ namespace storm {
                 initialStateIndex = stateStorage.initialStateIndices[0];
                 STORM_LOG_TRACE("Initial state: " << initialStateIndex);
                 // Initialize heuristic values for inital state
-                statesNotExplored.at(initialStateIndex)->setHeuristicValues(0, storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
+                statesNotExplored.at(initialStateIndex).second->updateHeuristicValues(0, storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
             } else {
                 initializeNextIteration();
             }
@@ -128,8 +128,8 @@ namespace storm {
             // Push skipped states to explore queue
             // TODO Matthias: remove
             for (auto const& skippedState : skippedStates) {
-                statesNotExplored[skippedState.second->getId()] = skippedState.second;
-                explorationQueue.push(skippedState.second->getId());
+                statesNotExplored[skippedState.second.first->getId()] = skippedState.second;
+                explorationQueue.push(skippedState.second.second);
             }
 
             // Initialize matrix builder again
@@ -157,7 +157,7 @@ namespace storm {
             matrixBuilder.mappingOffset = nrStates;
             STORM_LOG_TRACE("# expanded states: " << nrExpandedStates);
             StateType skippedIndex = nrExpandedStates;
-            std::map<StateType, DFTStatePointer> skippedStatesNew;
+            std::map<StateType, std::pair<DFTStatePointer, ExplorationHeuristicPointer>> skippedStatesNew;
             for (size_t id = 0; id < matrixBuilder.stateRemapping.size(); ++id) {
                 StateType index = matrixBuilder.stateRemapping[id];
                 auto itFind = skippedStates.find(index);
@@ -204,7 +204,7 @@ namespace storm {
                             auto itFind = skippedStates.find(itEntry->getColumn());
                             if (itFind != skippedStates.end()) {
                                 // Set id for skipped states as we remap it later
-                                matrixBuilder.addTransition(matrixBuilder.mappingOffset + itFind->second->getId(), itEntry->getValue());
+                                matrixBuilder.addTransition(matrixBuilder.mappingOffset + itFind->second.first->getId(), itEntry->getValue());
                             } else {
                                 // Set newly remapped index for expanded states
                                 matrixBuilder.addTransition(indexRemapping[itEntry->getColumn()], itEntry->getValue());
@@ -228,10 +228,12 @@ namespace storm {
             // TODO Matthias: do not empty queue every time but break before
             while (!explorationQueue.empty()) {
                 // Get the first state in the queue
-                StateType currentId = explorationQueue.popTop();
+                ExplorationHeuristicPointer currentExplorationHeuristic = explorationQueue.popTop();
+                StateType currentId = currentExplorationHeuristic->getId();
                 auto itFind = statesNotExplored.find(currentId);
                 STORM_LOG_ASSERT(itFind != statesNotExplored.end(), "Id " << currentId << " not found");
-                DFTStatePointer currentState = itFind->second;
+                DFTStatePointer currentState = itFind->second.first;
+                STORM_LOG_ASSERT(currentExplorationHeuristic == itFind->second.second, "Exploration heuristics do not match");
                 STORM_LOG_ASSERT(currentState->getId() == currentId, "Ids do not match");
                 // Remove it from the list of not explored states
                 statesNotExplored.erase(itFind);
@@ -254,7 +256,7 @@ namespace storm {
                 bool fixQueue = false;
                 generator.load(currentState);
 
-                if (currentState->isSkip(approximationThreshold, heuristic)) {
+                if (currentExplorationHeuristic->isSkip(approximationThreshold)) {
                     // Skip the current state
                     ++nrSkippedStates;
                     STORM_LOG_TRACE("Skip expansion of state: " << dft.getStateString(currentState));
@@ -263,7 +265,7 @@ namespace storm {
                     // TODO Matthias: what to do when there is no unique target state?
                     matrixBuilder.addTransition(failedStateId, storm::utility::zero<ValueType>());
                     // Remember skipped state
-                    skippedStates[matrixBuilder.getCurrentRowGroup() - 1] = currentState;
+                    skippedStates[matrixBuilder.getCurrentRowGroup() - 1] = std::make_pair(currentState, currentExplorationHeuristic);
                     matrixBuilder.finishRow();
                 } else {
                     // Explore the current state
@@ -282,7 +284,13 @@ namespace storm {
                             // Set heuristic values for reached states
                             auto iter = statesNotExplored.find(stateProbabilityPair.first);
                             if (iter != statesNotExplored.end()) {
-                                iter->second->setHeuristicValues(currentState, stateProbabilityPair.second, choice.getTotalMass());
+                                // Update heuristic values
+                                DFTStatePointer state = iter->second.first;
+                                if (state->hasFailed(dft.getTopLevelIndex()) || state->isFailsafe(dft.getTopLevelIndex()) || state->nrFailableDependencies() > 0 || (state->nrFailableDependencies() == 0 && state->nrFailableBEs() == 0)) {
+                                    // Do not skip absorbing state or if reached by dependencies
+                                    iter->second.second->markExpand();
+                                }
+                                iter->second.second->updateHeuristicValues(currentExplorationHeuristic->getDepth() + 1, stateProbabilityPair.second, choice.getTotalMass());
                                 fixQueue = true;
                             }
                         }
@@ -421,12 +429,13 @@ namespace storm {
                 auto matrixEntry = matrix.getRow(it->first, 0).begin();
                 STORM_LOG_ASSERT(matrixEntry->getColumn() == failedStateId, "Transition has wrong target state.");
                 // Get the lower bound by considering the failure of all possible BEs
+                DFTStatePointer state = it->second.first;
                 ValueType newRate = storm::utility::zero<ValueType>();
-                for (size_t index = 0; index < it->second->nrFailableBEs(); ++index) {
-                    newRate += it->second->getFailableBERate(index);
+                for (size_t index = 0; index < state->nrFailableBEs(); ++index) {
+                    newRate += state->getFailableBERate(index);
                 }
-                for (size_t index = 0; index < it->second->nrNotFailableBEs(); ++index) {
-                    newRate += it->second->getNotFailableBERate(index);
+                for (size_t index = 0; index < state->nrNotFailableBEs(); ++index) {
+                    newRate += state->getNotFailableBERate(index);
                 }
                 matrixEntry->setValue(newRate);
             }
@@ -441,12 +450,13 @@ namespace storm {
                 // Get the upper bound by considering the failure of all BEs
                 // The used formula for the rate is 1/( 1/a + 1/b + ...)
                 // TODO Matthias: improve by using closed formula for AND of all BEs
+                DFTStatePointer state = it->second.first;
                 ValueType newRate = storm::utility::zero<ValueType>();
-                for (size_t index = 0; index < it->second->nrFailableBEs(); ++index) {
-                    newRate += storm::utility::one<ValueType>() / it->second->getFailableBERate(index);
+                for (size_t index = 0; index < state->nrFailableBEs(); ++index) {
+                    newRate += storm::utility::one<ValueType>() / state->getFailableBERate(index);
                 }
-                for (size_t index = 0; index < it->second->nrNotFailableBEs(); ++index) {
-                    newRate += storm::utility::one<ValueType>() / it->second->getNotFailableBERate(index);
+                for (size_t index = 0; index < state->nrNotFailableBEs(); ++index) {
+                    newRate += storm::utility::one<ValueType>() / state->getNotFailableBERate(index);
                 }
                 newRate = storm::utility::one<ValueType>() / newRate;
                 matrixEntry->setValue(newRate);
@@ -473,14 +483,14 @@ namespace storm {
                     // Check if state is pseudo state
                     // If state is explored already the possible pseudo state was already constructed
                     auto iter = statesNotExplored.find(stateId);
-                    if (iter != statesNotExplored.end() && iter->second->isPseudoState()) {
+                    if (iter != statesNotExplored.end() && iter->second.first->isPseudoState()) {
                         // Create pseudo state now
-                        STORM_LOG_ASSERT(iter->second->getId() == stateId, "Ids do not match.");
-                        STORM_LOG_ASSERT(iter->second->status() == state->status(), "Pseudo states do not coincide.");
+                        STORM_LOG_ASSERT(iter->second.first->getId() == stateId, "Ids do not match.");
+                        STORM_LOG_ASSERT(iter->second.first->status() == state->status(), "Pseudo states do not coincide.");
                         state->setId(stateId);
                         // Update mapping to map to concrete state now
-                        statesNotExplored[stateId] = state;
-                        // TODO Matthias: copy explorationHeuristic
+                        // TODO Matthias: just change pointer?
+                        statesNotExplored[stateId] = std::make_pair(state, iter->second.second);
                         // We do not push the new state on the exploration queue as the pseudo state was already pushed
                         STORM_LOG_TRACE("Created pseudo state " << dft.getStateString(state));
                     }
@@ -493,8 +503,9 @@ namespace storm {
                 stateId = stateStorage.stateToId.findOrAdd(state->status(), state->getId());
                 STORM_LOG_ASSERT(stateId == state->getId(), "Ids do not match.");
                 // Insert state as not yet explored
-                statesNotExplored[stateId] = state;
-                explorationQueue.push(stateId);
+                ExplorationHeuristicPointer heuristic = std::make_shared<ExplorationHeuristic>(stateId);
+                statesNotExplored[stateId] = std::make_pair(state, heuristic);
+                explorationQueue.push(heuristic);
                 // Reserve one slot for the new state in the remapping
                 matrixBuilder.stateRemapping.push_back(0);
                 STORM_LOG_TRACE("New " << (state->isPseudoState() ? "pseudo" : "concrete") << " state: " << dft.getStateString(state));
@@ -511,12 +522,6 @@ namespace storm {
             modelComponents.markovianStates.set(matrixBuilder.getCurrentRowGroup() - 1, markovian);
         }
 
-        template<typename ValueType, typename StateType>
-        bool ExplicitDFTModelBuilderApprox<ValueType, StateType>::isPriorityGreater(StateType idA, StateType idB) const {
-            return statesNotExplored.at(idA)->comparePriority(statesNotExplored.at(idB), heuristic);
-        }
-
-
         // Explicitly instantiate the class.
         template class ExplicitDFTModelBuilderApprox<double>;
 
diff --git a/src/builder/ExplicitDFTModelBuilderApprox.h b/src/builder/ExplicitDFTModelBuilderApprox.h
index 74798e889..4238194eb 100644
--- a/src/builder/ExplicitDFTModelBuilderApprox.h
+++ b/src/builder/ExplicitDFTModelBuilderApprox.h
@@ -26,11 +26,10 @@ namespace storm {
         template<typename ValueType, typename StateType = uint32_t>
         class ExplicitDFTModelBuilderApprox {
 
-            using DFTElementPointer = std::shared_ptr<storm::storage::DFTElement<ValueType>>;
-            using DFTElementCPointer = std::shared_ptr<storm::storage::DFTElement<ValueType> const>;
-            using DFTGatePointer = std::shared_ptr<storm::storage::DFTGate<ValueType>>;
             using DFTStatePointer = std::shared_ptr<storm::storage::DFTState<ValueType>>;
-            using DFTRestrictionPointer = std::shared_ptr<storm::storage::DFTRestriction<ValueType>>;
+            // TODO Matthias: make choosable
+            using ExplorationHeuristic = DFTExplorationHeuristicNone<ValueType>;
+            using ExplorationHeuristicPointer = std::shared_ptr<ExplorationHeuristic>;
 
 
             // A structure holding the individual components of a model.
@@ -294,16 +293,16 @@ namespace storm {
             storm::storage::sparse::StateStorage<StateType> stateStorage;
 
             // A priority queue of states that still need to be explored.
-            storm::storage::DynamicPriorityQueue<StateType, std::vector<StateType>, std::function<bool(StateType, StateType)>> explorationQueue;
+            storm::storage::DynamicPriorityQueue<ExplorationHeuristicPointer, std::vector<ExplorationHeuristicPointer>, std::function<bool(ExplorationHeuristicPointer, ExplorationHeuristicPointer)>> explorationQueue;
 
-            // A mapping of not yet explored states from the id to the state object.
-            std::map<StateType, DFTStatePointer> statesNotExplored;
+            // A mapping of not yet explored states from the id to the tuple (state object, heuristic values).
+            std::map<StateType, std::pair<DFTStatePointer, ExplorationHeuristicPointer>> statesNotExplored;
 
             // Holds all skipped states which were not yet expanded. More concretely it is a mapping from matrix indices
             // to the corresponding skipped states.
             // Notice that we need an ordered map here to easily iterate in increasing order over state ids.
             // TODO remove again
-            std::map<StateType, DFTStatePointer> skippedStates;
+            std::map<StateType, std::pair<DFTStatePointer, ExplorationHeuristicPointer>> skippedStates;
         };
 
     }
diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp
index f6bb692a7..70ff18122 100644
--- a/src/storage/dft/DFTState.cpp
+++ b/src/storage/dft/DFTState.cpp
@@ -6,7 +6,7 @@ namespace storm {
     namespace storage {
 
         template<typename ValueType>
-        DFTState<ValueType>::DFTState(DFT<ValueType> const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateVectorSize()), mId(id), mPseudoState(false), mDft(dft), mStateGenerationInfo(stateGenerationInfo), exploreHeuristic()  {
+        DFTState<ValueType>::DFTState(DFT<ValueType> const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateVectorSize()), mId(id), mPseudoState(false), mDft(dft), mStateGenerationInfo(stateGenerationInfo) {
             // TODO Matthias: use construct()
             
             // Initialize uses
@@ -37,7 +37,7 @@ namespace storm {
         }
 
         template<typename ValueType>
-        DFTState<ValueType>::DFTState(storm::storage::BitVector const& status, DFT<ValueType> const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(status), mId(id), mPseudoState(true), mDft(dft), mStateGenerationInfo(stateGenerationInfo), exploreHeuristic() {
+        DFTState<ValueType>::DFTState(storm::storage::BitVector const& status, DFT<ValueType> const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(status), mId(id), mPseudoState(true), mDft(dft), mStateGenerationInfo(stateGenerationInfo) {
             // Intentionally left empty
         }
         
@@ -85,9 +85,7 @@ namespace storm {
 
         template<typename ValueType>
         std::shared_ptr<DFTState<ValueType>> DFTState<ValueType>::copy() const {
-            std::shared_ptr<DFTState<ValueType>> stateCopy = std::make_shared<storm::storage::DFTState<ValueType>>(*this);
-            stateCopy->exploreHeuristic = storm::builder::DFTExplorationHeuristic<ValueType>();
-            return stateCopy;
+            return std::make_shared<storm::storage::DFTState<ValueType>>(*this);
         }
 
         template<typename ValueType>
diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h
index eb3164516..207eecac3 100644
--- a/src/storage/dft/DFTState.h
+++ b/src/storage/dft/DFTState.h
@@ -34,8 +34,7 @@ namespace storm {
             bool mValid = true;
             const DFT<ValueType>& mDft;
             const DFTStateGenerationInfo& mStateGenerationInfo;
-            storm::builder::DFTExplorationHeuristic<ValueType> exploreHeuristic;
-            
+
         public:
             /**
              * Construct the initial state.
@@ -123,26 +122,6 @@ namespace storm {
                 return mPseudoState;
             }
 
-            void setHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) {
-                exploreHeuristic.setHeuristicValues(depth, rate, exitRate);
-            }
-
-            void setHeuristicValues(std::shared_ptr<storm::storage::DFTState<ValueType>> oldState, ValueType rate, ValueType exitRate) {
-                if (hasFailed(mDft.getTopLevelIndex()) || isFailsafe(mDft.getTopLevelIndex()) || nrFailableDependencies() > 0 || (nrFailableDependencies() == 0 && nrFailableBEs() == 0)) {
-                    // Do not skip absorbing state or if reached by dependencies
-                    exploreHeuristic.setNotSkip();
-                }
-                exploreHeuristic.setHeuristicValues(oldState->exploreHeuristic.getDepth() + 1, rate, exitRate);
-            }
-
-            bool isSkip(double approximationThreshold, storm::builder::ApproximationHeuristic heuristic) {
-                return exploreHeuristic.isSkip(approximationThreshold, heuristic);
-            }
-
-            bool comparePriority(std::shared_ptr<DFTState> const& other, storm::builder::ApproximationHeuristic heuristic) {
-                return this->exploreHeuristic.compare(other->exploreHeuristic, heuristic);
-            }
-
             storm::storage::BitVector const& status() const {
                 return mStatus;
             }