diff --git a/src/storm-gamebased-ar/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp b/src/storm-gamebased-ar/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp
index 7464b38491..d049727ffe 100644
--- a/src/storm-gamebased-ar/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp
+++ b/src/storm-gamebased-ar/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp
@@ -7,7 +7,7 @@
 
 #include "storm-gamebased-ar/abstraction/SymbolicStateSet.h"
 
-#include "storm/storage/dd/BisimulationDecomposition.h"
+#include "storm/storage/dd/bisimulation/BisimulationDecomposition.h"
 
 #include "storm/modelchecker/propositional/SymbolicPropositionalModelChecker.h"
 #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
diff --git a/src/storm/api/bisimulation.h b/src/storm/api/bisimulation.h
index 1b4ae14af9..102612054a 100644
--- a/src/storm/api/bisimulation.h
+++ b/src/storm/api/bisimulation.h
@@ -1,16 +1,13 @@
 #pragma once
 
+#include "storm/exceptions/NotSupportedException.h"
 #include "storm/models/sparse/Ctmc.h"
 #include "storm/models/sparse/Dtmc.h"
 #include "storm/models/sparse/Mdp.h"
-
 #include "storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h"
 #include "storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h"
-
-#include "storm/storage/dd/BisimulationDecomposition.h"
 #include "storm/storage/dd/DdType.h"
-
-#include "storm/exceptions/NotSupportedException.h"
+#include "storm/storage/dd/bisimulation/BisimulationDecomposition.h"
 #include "storm/utility/macros.h"
 
 namespace storm {
diff --git a/src/storm/storage/bisimulation/BisimulationDecomposition.cpp b/src/storm/storage/bisimulation/BisimulationDecomposition.cpp
index 4828c13ef7..bbb9a21878 100644
--- a/src/storm/storage/bisimulation/BisimulationDecomposition.cpp
+++ b/src/storm/storage/bisimulation/BisimulationDecomposition.cpp
@@ -6,23 +6,16 @@
 #include "storm/exceptions/AbortException.h"
 #include "storm/exceptions/IllegalFunctionCallException.h"
 #include "storm/exceptions/InvalidOptionException.h"
-
 #include "storm/logic/FormulaInformation.h"
 #include "storm/logic/FragmentSpecification.h"
-
+#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
+#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "storm/models/sparse/Ctmc.h"
 #include "storm/models/sparse/Dtmc.h"
 #include "storm/models/sparse/Mdp.h"
-#include "storm/models/sparse/StandardRewardModel.h"
-
-#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
-#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
-
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/CoreSettings.h"
-
 #include "storm/storage/bisimulation/DeterministicBlockData.h"
-
 #include "storm/utility/SignalHandler.h"
 #include "storm/utility/macros.h"
 
@@ -71,8 +64,8 @@ template<typename ModelType, typename BlockDataType>
 void BisimulationDecomposition<ModelType, BlockDataType>::Options::preserveFormula(storm::logic::Formula const& formula) {
     // Disable the measure driven initial partition.
     measureDrivenInitialPartition = false;
-    phiStates = boost::none;
-    psiStates = boost::none;
+    phiStates.reset();
+    psiStates.reset();
 
     // Retrieve information about formula.
     storm::logic::FormulaInformation info = formula.info();
@@ -163,7 +156,7 @@ void BisimulationDecomposition<ModelType, BlockDataType>::Options::checkAndSetMe
         phiStates = phiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector();
         psiStates = psiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector();
     } else {
-        optimalityType = boost::none;
+        optimalityType.reset();
     }
 }
 
@@ -181,7 +174,7 @@ void BisimulationDecomposition<ModelType, BlockDataType>::Options::addToRespecte
     if (!respectedAtomicPropositions) {
         respectedAtomicPropositions = labelsToRespect;
     } else {
-        respectedAtomicPropositions.get().insert(labelsToRespect.begin(), labelsToRespect.end());
+        respectedAtomicPropositions.value().insert(labelsToRespect.begin(), labelsToRespect.end());
     }
 }
 
@@ -347,7 +340,7 @@ template<typename ModelType, typename BlockDataType>
 void BisimulationDecomposition<ModelType, BlockDataType>::initializeLabelBasedPartition() {
     partition = storm::storage::bisimulation::Partition<BlockDataType>(model.getNumberOfStates());
 
-    for (auto const& label : options.respectedAtomicPropositions.get()) {
+    for (auto const& label : options.respectedAtomicPropositions.value()) {
         if (label == "init") {
             continue;
         }
@@ -365,14 +358,14 @@ template<typename ModelType, typename BlockDataType>
 void BisimulationDecomposition<ModelType, BlockDataType>::initializeMeasureDrivenPartition() {
     std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = this->getStatesWithProbability01();
 
-    boost::optional<storm::storage::sparse::state_type> representativePsiState;
-    if (!options.psiStates.get().empty()) {
-        representativePsiState = *options.psiStates.get().begin();
+    std::optional<storm::storage::sparse::state_type> representativePsiState;
+    if (!options.psiStates.value().empty()) {
+        representativePsiState = *options.psiStates.value().begin();
     }
 
     partition = storm::storage::bisimulation::Partition<BlockDataType>(
         model.getNumberOfStates(), statesWithProbability01.first,
-        options.getBounded() || options.getKeepRewards() ? options.psiStates.get() : statesWithProbability01.second, representativePsiState);
+        options.getBounded() || options.getKeepRewards() ? options.psiStates.value() : statesWithProbability01.second, representativePsiState);
 
     // If the model has state rewards, we need to consider them, because otherwise reward properties are not
     // preserved.
@@ -404,7 +397,6 @@ template class BisimulationDecomposition<storm::models::sparse::Dtmc<double>, bi
 template class BisimulationDecomposition<storm::models::sparse::Ctmc<double>, bisimulation::DeterministicBlockData>;
 template class BisimulationDecomposition<storm::models::sparse::Mdp<double>, bisimulation::DeterministicBlockData>;
 
-#ifdef STORM_HAVE_CARL
 template class BisimulationDecomposition<storm::models::sparse::Dtmc<storm::RationalNumber>, bisimulation::DeterministicBlockData>;
 template class BisimulationDecomposition<storm::models::sparse::Ctmc<storm::RationalNumber>, bisimulation::DeterministicBlockData>;
 template class BisimulationDecomposition<storm::models::sparse::Mdp<storm::RationalNumber>, bisimulation::DeterministicBlockData>;
@@ -412,6 +404,5 @@ template class BisimulationDecomposition<storm::models::sparse::Mdp<storm::Ratio
 template class BisimulationDecomposition<storm::models::sparse::Dtmc<storm::RationalFunction>, bisimulation::DeterministicBlockData>;
 template class BisimulationDecomposition<storm::models::sparse::Ctmc<storm::RationalFunction>, bisimulation::DeterministicBlockData>;
 template class BisimulationDecomposition<storm::models::sparse::Mdp<storm::RationalFunction>, bisimulation::DeterministicBlockData>;
-#endif
 }  // namespace storage
 }  // namespace storm
diff --git a/src/storm/storage/bisimulation/BisimulationDecomposition.h b/src/storm/storage/bisimulation/BisimulationDecomposition.h
index e284003f61..8d8181f07d 100644
--- a/src/storm/storage/bisimulation/BisimulationDecomposition.h
+++ b/src/storm/storage/bisimulation/BisimulationDecomposition.h
@@ -1,6 +1,6 @@
-#ifndef STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_
-#define STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_
+#pragma once
 
+#include "storm/logic/Formulas.h"
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/BisimulationSettings.h"
 #include "storm/solver/OptimizationDirection.h"
@@ -8,12 +8,7 @@
 #include "storm/storage/StateBlock.h"
 #include "storm/storage/bisimulation/BisimulationType.h"
 #include "storm/storage/bisimulation/Partition.h"
-#include "storm/storage/sparse/StateType.h"
-
-#include "storm/logic/Formulas.h"
-
 #include "storm/utility/ConstantsComparator.h"
-#include "storm/utility/constants.h"
 
 namespace storm {
 namespace logic {
@@ -56,7 +51,7 @@ class BisimulationDecomposition : public Decomposition<StateBlock> {
          * Creates an object representing the options necessary to obtain the quotient while still preserving
          * the given formula.
          *
-         * @param The model for which the quotient model shall be computed. This needs to be given in order to
+         * @param model The model for which the quotient model shall be computed. This needs to be given in order to
          * derive a suitable initial partition.
          * @param formula The formula that is to be preserved.
          */
@@ -66,7 +61,7 @@ class BisimulationDecomposition : public Decomposition<StateBlock> {
          * Creates an object representing the options necessary to obtain the smallest quotient while still
          * preserving the given formulas.
          *
-         * @param The model for which the quotient model shall be computed. This needs to be given in order to
+         * @param model The model for which the quotient model shall be computed. This needs to be given in order to
          * derive a suitable initial partition.
          * @param formulas The formulas that need to be preserved.
          */
@@ -120,27 +115,27 @@ class BisimulationDecomposition : public Decomposition<StateBlock> {
 
         OptimizationDirection getOptimizationDirection() const {
             STORM_LOG_ASSERT(optimalityType, "Optimality type not set.");
-            return optimalityType.get();
+            return optimalityType.value();
         }
 
         // A flag that indicates whether a measure driven initial partition is to be used. If this flag is set
         // to true, the two optional pairs phiStatesAndLabel and psiStatesAndLabel must be set. Then, the
         // measure driven initial partition wrt. to the states phi and psi is taken.
         bool measureDrivenInitialPartition;
-        boost::optional<storm::storage::BitVector> phiStates;
-        boost::optional<storm::storage::BitVector> psiStates;
+        std::optional<storm::storage::BitVector> phiStates;
+        std::optional<storm::storage::BitVector> psiStates;
 
         /// An optional set of strings that indicate which of the atomic propositions of the model are to be
         /// respected and which may be ignored. If not given, all atomic propositions of the model are respected.
-        boost::optional<std::set<std::string>> respectedAtomicPropositions;
+        std::optional<std::set<std::string>> respectedAtomicPropositions;
 
         /// A flag that governs whether the quotient model is actually built or only the decomposition is computed.
         bool buildQuotient;
 
        private:
-        boost::optional<OptimizationDirection> optimalityType;
+        std::optional<OptimizationDirection> optimalityType;
 
-        /// A flag that indicates whether or not the state-rewards of the model are to be respected (and should
+        /// A flag that indicates whether the state-rewards of the model are to be respected (and should
         /// be kept in the quotient model, if one is built).
         bool keepRewards;
 
@@ -184,7 +179,7 @@ class BisimulationDecomposition : public Decomposition<StateBlock> {
     };
 
     /*!
-     * Decomposes the given model into equivalance classes of a bisimulation.
+     * Decomposes the given model into equivalence classes of a bisimulation.
      *
      * @param model The model to decompose.
      * @param options The options to use during for the decomposition.
@@ -208,10 +203,10 @@ class BisimulationDecomposition : public Decomposition<StateBlock> {
 
    protected:
     /*!
-     * Decomposes the given model into equivalance classes of a bisimulation.
+     * Decomposes the given model into equivalence classes of a bisimulation.
      *
      * @param model The model to decompose.
-     * @param backwardTransition The backward transitions of the model.
+     * @param backwardTransitions The backward transitions of the model.
      * @param options The options to use during for the decomposition.
      */
     BisimulationDecomposition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Options const& options);
@@ -231,11 +226,10 @@ class BisimulationDecomposition : public Decomposition<StateBlock> {
      * @param splitterVector The vector into which to insert the newly discovered potential splitters.
      */
     virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter,
-                                                std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) = 0;
+                                                std::vector<bisimulation::Block<BlockDataType>*>& splitterVector) = 0;
 
     /*!
-     * Builds the quotient model based on the previously computed equivalence classes (stored in the blocks
-     * of the decomposition.
+     * Builds the quotient model based on the previously computed equivalence classes (stored in the blocks of the decomposition).
      */
     virtual void buildQuotient() = 0;
 
@@ -297,10 +291,8 @@ class BisimulationDecomposition : public Decomposition<StateBlock> {
     // A comparator used for comparing the distances of constants.
     storm::utility::ConstantsComparator<ValueType> comparator;
 
-    // The quotient, if it was build. Otherwhise a null pointer.
+    // The quotient, if it was build. Otherwise a null pointer.
     std::shared_ptr<ModelType> quotient;
 };
 }  // namespace storage
 }  // namespace storm
-
-#endif /* STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ */
diff --git a/src/storm/storage/bisimulation/Block.cpp b/src/storm/storage/bisimulation/Block.cpp
index 6720fd5dd7..b9382178d5 100644
--- a/src/storm/storage/bisimulation/Block.cpp
+++ b/src/storm/storage/bisimulation/Block.cpp
@@ -1,11 +1,9 @@
 #include "storm/storage/bisimulation/Block.h"
 
-#include <iomanip>
 #include <iostream>
 
 #include "storm/storage/bisimulation/DeterministicBlockData.h"
 #include "storm/storage/bisimulation/Partition.h"
-
 #include "storm/utility/macros.h"
 
 namespace storm {
diff --git a/src/storm/storage/bisimulation/Block.h b/src/storm/storage/bisimulation/Block.h
index fb279cb903..db412e739b 100644
--- a/src/storm/storage/bisimulation/Block.h
+++ b/src/storm/storage/bisimulation/Block.h
@@ -1,8 +1,4 @@
-#ifndef STORM_STORAGE_BISIMULATION_BLOCK_H_
-#define STORM_STORAGE_BISIMULATION_BLOCK_H_
-
-#include <boost/optional.hpp>
-#include <list>
+#pragma once
 
 #include "storm/storage/sparse/StateType.h"
 
@@ -105,5 +101,3 @@ class Block {
 }  // namespace bisimulation
 }  // namespace storage
 }  // namespace storm
-
-#endif /* STORM_STORAGE_BISIMULATION_BLOCK_H_ */
diff --git a/src/storm/storage/bisimulation/DeterministicBlockData.cpp b/src/storm/storage/bisimulation/DeterministicBlockData.cpp
index 8aac6162b5..b7e2a8e2b2 100644
--- a/src/storm/storage/bisimulation/DeterministicBlockData.cpp
+++ b/src/storm/storage/bisimulation/DeterministicBlockData.cpp
@@ -89,8 +89,8 @@ bool DeterministicBlockData::hasRepresentativeState() const {
 }
 
 storm::storage::sparse::state_type DeterministicBlockData::representativeState() const {
-    STORM_LOG_THROW(valRepresentativeState, storm::exceptions::InvalidOperationException, "Unable to retrieve representative state for block.");
-    return valRepresentativeState.get();
+    STORM_LOG_THROW(hasRepresentativeState(), storm::exceptions::InvalidOperationException, "Unable to retrieve representative state for block.");
+    return valRepresentativeState.value();
 }
 
 bool DeterministicBlockData::needsRefinement() const {
diff --git a/src/storm/storage/bisimulation/DeterministicBlockData.h b/src/storm/storage/bisimulation/DeterministicBlockData.h
index f5bde43a5c..e0f345813b 100644
--- a/src/storm/storage/bisimulation/DeterministicBlockData.h
+++ b/src/storm/storage/bisimulation/DeterministicBlockData.h
@@ -1,7 +1,4 @@
-#ifndef STORM_STORAGE_BISIMULATION_DETERMINISTICBLOCKDATA_H_
-#define STORM_STORAGE_BISIMULATION_DETERMINISTICBLOCKDATA_H_
-
-#include <cstdint>
+#pragma once
 
 #include "storm/storage/bisimulation/Block.h"
 
@@ -43,7 +40,7 @@ class DeterministicBlockData {
     // Marks the block as needing refinement (or not).
     void setNeedsRefinement(bool value = true);
 
-    // Sets whether or not the block is to be interpreted as absorbing.
+    // Sets whether the block is to be interpreted as absorbing.
     void setAbsorbing(bool absorbing);
 
     // Retrieves whether the block is to be interpreted as absorbing.
@@ -77,20 +74,18 @@ class DeterministicBlockData {
     uint_fast64_t valMarker2;
 
     // Some bits to store flags: splitter flag, refinement flag, absorbing flag.
-    static const uint64_t SPLITTER_FLAG = 1ull;
-    static const uint64_t REFINEMENT_FLAG = 1ull << 1;
-    static const uint64_t ABSORBING_FLAG = 1ull << 2;
-    static const uint64_t REWARD_FLAG = 1ull << 3;
+    static constexpr uint64_t SPLITTER_FLAG = 1ull;
+    static constexpr uint64_t REFINEMENT_FLAG = 1ull << 1;
+    static constexpr uint64_t ABSORBING_FLAG = 1ull << 2;
+    static constexpr uint64_t REWARD_FLAG = 1ull << 3;
     uint8_t flags;
 
     // An optional representative state for the block. If this is set, this state is used to derive the
     // atomic propositions of the meta state in the quotient model.
-    boost::optional<storm::storage::sparse::state_type> valRepresentativeState;
+    std::optional<storm::storage::sparse::state_type> valRepresentativeState;
 };
 
 std::ostream& operator<<(std::ostream& out, DeterministicBlockData const& data);
 }  // namespace bisimulation
 }  // namespace storage
 }  // namespace storm
-
-#endif /* STORM_STORAGE_BISIMULATION_DETERMINISTICBLOCKDATA_H_ */
diff --git a/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp b/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
index df742566a1..ad29713e8d 100644
--- a/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
+++ b/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
@@ -1,27 +1,20 @@
 #include "storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h"
 
 #include <algorithm>
-#include <boost/iterator/zip_iterator.hpp>
 #include <chrono>
-#include <iomanip>
 #include <unordered_map>
 
 #include "storm/adapters/RationalFunctionAdapter.h"
+#include "storm/exceptions/IllegalFunctionCallException.h"
 #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
-
 #include "storm/models/sparse/Ctmc.h"
 #include "storm/models/sparse/Dtmc.h"
-#include "storm/models/sparse/StandardRewardModel.h"
-
-#include "storm/exceptions/IllegalFunctionCallException.h"
-#include "storm/exceptions/InvalidArgumentException.h"
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/GeneralSettings.h"
 #include "storm/utility/ConstantsComparator.h"
 #include "storm/utility/constants.h"
 #include "storm/utility/graph.h"
 
-#include "storm/settings/SettingsManager.h"
-#include "storm/settings/modules/GeneralSettings.h"
-
 namespace storm {
 namespace storage {
 
@@ -37,7 +30,7 @@ DeterministicModelBisimulationDecomposition<ModelType>::DeterministicModelBisimu
 
 template<typename ModelType>
 std::pair<storm::storage::BitVector, storm::storage::BitVector> DeterministicModelBisimulationDecomposition<ModelType>::getStatesWithProbability01() {
-    return storm::utility::graph::performProb01(this->backwardTransitions, this->options.phiStates.get(), this->options.psiStates.get());
+    return storm::utility::graph::performProb01(this->backwardTransitions, this->options.phiStates.value(), this->options.psiStates.value());
 }
 
 template<typename ModelType>
@@ -107,7 +100,7 @@ void DeterministicModelBisimulationDecomposition<ModelType>::initializeSilentPro
         Block<BlockDataType> const* currentBlockPtr = &this->partition.getBlock(state);
         for (auto const& successorEntry : this->model.getTransitionMatrix().getRowGroup(state)) {
             if (&this->partition.getBlock(successorEntry.getColumn()) == currentBlockPtr) {
-                silentProbabilities[state] += successorEntry.getValue();
+                silentProbabilities[state] += getTransitionValue(successorEntry, state);
             }
         }
     }
@@ -322,7 +315,7 @@ void DeterministicModelBisimulationDecomposition<ModelType>::exploreRemainingSta
             }
 
             // We keep track of the probability of the predecessor moving to the splitter.
-            increaseProbabilityToSplitter(predecessor, predecessorBlock, predecessorEntry.getValue());
+            increaseProbabilityToSplitter(predecessor, predecessorBlock, getTransitionValue(predecessorEntry, predecessor));
 
             // Only move the state if it has not been seen as a predecessor before.
             storm::storage::sparse::state_type predecessorPosition = this->partition.getPosition(predecessor);
@@ -330,7 +323,7 @@ void DeterministicModelBisimulationDecomposition<ModelType>::exploreRemainingSta
                 moveStateToMarker1(predecessor, predecessorBlock);
             }
 
-            // We must not insert the the splitter itself if we are not computing a weak bisimulation on CTMCs.
+            // We must not insert the splitter itself if we are not computing a weak bisimulation on CTMCs.
             if (this->options.getType() != BisimulationType::Weak || this->model.getType() != storm::models::ModelType::Ctmc || predecessorBlock != splitter) {
                 insertIntoPredecessorList(predecessorBlock, predecessorBlocks);
             }
@@ -361,7 +354,7 @@ void DeterministicModelBisimulationDecomposition<ModelType>::updateSilentProbabi
             ValueType newSilentProbability = storm::utility::zero<ValueType>();
             for (auto const& successorEntry : this->model.getTransitionMatrix().getRow(*stateIt)) {
                 if (this->partition.getBlock(successorEntry.getColumn()) == block) {
-                    newSilentProbability += successorEntry.getValue();
+                    newSilentProbability += getTransitionValue(successorEntry, *stateIt);
                 }
             }
             silentProbabilities[*stateIt] = newSilentProbability;
@@ -475,7 +468,7 @@ void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBl
 
 template<typename ModelType>
 void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlocksOfSplitterWeak(
-    bisimulation::Block<BlockDataType>& splitter, std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks,
+    bisimulation::Block<BlockDataType> const& splitter, std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks,
     std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) {
     for (auto block : predecessorBlocks) {
         if (block->data().hasRewards()) {
@@ -548,9 +541,9 @@ void DeterministicModelBisimulationDecomposition<ModelType>::refinePartitionBase
             }
 
             // We keep track of the probability of the predecessor moving to the splitter.
-            increaseProbabilityToSplitter(predecessor, predecessorBlock, predecessorEntry.getValue());
+            increaseProbabilityToSplitter(predecessor, predecessorBlock, getTransitionValue(predecessorEntry, predecessor));
 
-            // We only need to move the predecessor if its not already known as a predecessor already.
+            // We only need to move the predecessor if it is not already known as a predecessor already.
             if (predecessorPosition >= predecessorBlock.data().marker1()) {
                 // If the predecessor block is not the splitter, we can move the state easily.
                 if (predecessorBlock != splitter) {
@@ -604,7 +597,7 @@ void DeterministicModelBisimulationDecomposition<ModelType>::buildQuotient() {
 
     // Prepare the new state labeling for (b).
     storm::models::sparse::StateLabeling newLabeling(this->size());
-    std::set<std::string> atomicPropositionsSet = this->options.respectedAtomicPropositions.get();
+    std::set<std::string> atomicPropositionsSet = this->options.respectedAtomicPropositions.value();
     atomicPropositionsSet.insert("init");
     std::vector<std::string> atomicPropositions = std::vector<std::string>(atomicPropositionsSet.begin(), atomicPropositionsSet.end());
     for (auto const& ap : atomicPropositions) {
@@ -667,9 +660,10 @@ void DeterministicModelBisimulationDecomposition<ModelType>::buildQuotient() {
 
                 auto probIterator = blockProbability.find(targetBlock);
                 if (probIterator != blockProbability.end()) {
-                    probIterator->second += entry.getValue();
+                    probIterator->second += getTransitionValue(entry, representativeState);
                 } else {
-                    blockProbability[targetBlock] = entry.getValue();
+                    blockProbability[targetBlock] = getTransitionValue(entry, representativeState);
+                    ;
                 }
             }
 
@@ -722,18 +716,54 @@ void DeterministicModelBisimulationDecomposition<ModelType>::buildQuotient() {
     }
 
     // Finally construct the quotient model.
-    this->quotient = std::shared_ptr<ModelType>(new ModelType(builder.build(), std::move(newLabeling), std::move(rewardModels)));
+    this->quotient = std::make_shared<ModelType>(builder.build(), std::move(newLabeling), std::move(rewardModels));
+}
+
+template<typename ModelType>
+DeterministicModelBisimulationDecomposition<ModelType>::ValueType DeterministicModelBisimulationDecomposition<ModelType>::getTransitionValue(
+    storm::storage::MatrixEntry<storm::storage::sparse::state_type, ValueType> const& matrixEntry, storm::storage::sparse::state_type state) const {
+    return matrixEntry.getValue();
+}
+
+// Need to specialize for all ValueType
+template<>
+double DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<double>>::getTransitionValue(
+    storm::storage::MatrixEntry<storm::storage::sparse::state_type, double> const& matrixEntry, storm::storage::sparse::state_type state) const {
+    double transitionValue = matrixEntry.getValue();
+    // Currently not needed as CTMCs are stored as rate matrix
+    // TODO: enable when removing CTMC rate matrix
+    // transitionValue *= this->model.getExitRateVector().at(state);
+    return transitionValue;
+}
+
+template<>
+storm::RationalNumber DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<storm::RationalNumber>>::getTransitionValue(
+    storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber> const& matrixEntry, storm::storage::sparse::state_type state) const {
+    storm::RationalNumber transitionValue = matrixEntry.getValue();
+    // Currently not needed as CTMCs are stored as rate matrix
+    // TODO: enable when removing CTMC rate matrix
+    // transitionValue *= this->model.getExitRateVector().at(state);
+    return transitionValue;
+}
+
+template<>
+storm::RationalFunction DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<storm::RationalFunction>>::getTransitionValue(
+    storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalFunction> const& matrixEntry,
+    storm::storage::sparse::state_type state) const {
+    storm::RationalFunction transitionValue = matrixEntry.getValue();
+    // Currently not needed as CTMCs are stored as rate matrix
+    // TODO: enable when removing CTMC rate matrix
+    // transitionValue *= this->model.getExitRateVector().at(state);
+    return transitionValue;
 }
 
 template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>;
 template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<double>>;
 
-#ifdef STORM_HAVE_CARL
 template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<storm::RationalNumber>>;
 template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<storm::RationalNumber>>;
 
 template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<storm::RationalFunction>>;
 template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<storm::RationalFunction>>;
-#endif
 }  // namespace storage
 }  // namespace storm
diff --git a/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h b/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h
index fa3f68f269..2a6176fa62 100644
--- a/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h
+++ b/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h
@@ -1,5 +1,4 @@
-#ifndef STORM_STORAGE_BISIMULATION_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_
-#define STORM_STORAGE_BISIMULATION_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_
+#pragma once
 
 #include "storm/storage/bisimulation/BisimulationDecomposition.h"
 #include "storm/storage/bisimulation/DeterministicBlockData.h"
@@ -109,7 +108,7 @@ class DeterministicModelBisimulationDecomposition : public BisimulationDecomposi
     void refinePredecessorBlockOfSplitterWeak(bisimulation::Block<BlockDataType>& block, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue);
 
     // Refines the predecessor blocks of the splitter wrt. weak bisimulation in DTMCs.
-    void refinePredecessorBlocksOfSplitterWeak(bisimulation::Block<BlockDataType>& splitter,
+    void refinePredecessorBlocksOfSplitterWeak(bisimulation::Block<BlockDataType> const& splitter,
                                                std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks,
                                                std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue);
 
@@ -127,6 +126,9 @@ class DeterministicModelBisimulationDecomposition : public BisimulationDecomposi
     // Inserts the block into the list of predecessors if it is not already contained.
     void insertIntoPredecessorList(bisimulation::Block<BlockDataType>& predecessorBlock, std::list<bisimulation::Block<BlockDataType>*>& predecessorBlocks);
 
+    ValueType getTransitionValue(storm::storage::MatrixEntry<storm::storage::sparse::state_type, ValueType> const& matrixEntry,
+                                 [[maybe_unused]] storm::storage::sparse::state_type state) const;
+
     // A vector that holds the probabilities of states going into the splitter. This is used by the method that
     // refines a block based on probabilities.
     std::vector<ValueType> probabilitiesToCurrentSplitter;
@@ -136,5 +138,3 @@ class DeterministicModelBisimulationDecomposition : public BisimulationDecomposi
 };
 }  // namespace storage
 }  // namespace storm
-
-#endif /* STORM_STORAGE_BISIMULATION_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */
diff --git a/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp b/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp
index 307d476481..982167c9ed 100644
--- a/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp
+++ b/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp
@@ -1,15 +1,11 @@
 #include "storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h"
 
+#include "storm/adapters/RationalFunctionAdapter.h"
+#include "storm/exceptions/IllegalFunctionCallException.h"
 #include "storm/models/sparse/Mdp.h"
-#include "storm/models/sparse/StandardRewardModel.h"
-
 #include "storm/utility/graph.h"
-
-#include "storm/exceptions/IllegalFunctionCallException.h"
 #include "storm/utility/macros.h"
 
-#include "storm/adapters/RationalFunctionAdapter.h"
-
 namespace storm {
 namespace storage {
 
@@ -34,10 +30,10 @@ std::pair<storm::storage::BitVector, storm::storage::BitVector> Nondeterministic
                     "Can only compute states with probability 0/1 with an optimization direction (min/max).");
     if (this->options.getOptimizationDirection() == OptimizationDirection::Minimize) {
         return storm::utility::graph::performProb01Min(this->model.getTransitionMatrix(), this->model.getTransitionMatrix().getRowGroupIndices(),
-                                                       this->model.getBackwardTransitions(), this->options.phiStates.get(), this->options.psiStates.get());
+                                                       this->model.getBackwardTransitions(), this->options.phiStates.value(), this->options.psiStates.value());
     } else {
         return storm::utility::graph::performProb01Max(this->model.getTransitionMatrix(), this->model.getTransitionMatrix().getRowGroupIndices(),
-                                                       this->model.getBackwardTransitions(), this->options.phiStates.get(), this->options.psiStates.get());
+                                                       this->model.getBackwardTransitions(), this->options.phiStates.value(), this->options.psiStates.value());
     }
 }
 
@@ -118,7 +114,7 @@ void NondeterministicModelBisimulationDecomposition<ModelType>::buildQuotient()
 
     // Prepare the new state labeling for (b).
     storm::models::sparse::StateLabeling newLabeling(this->size());
-    std::set<std::string> atomicPropositionsSet = this->options.respectedAtomicPropositions.get();
+    std::set<std::string> atomicPropositionsSet = this->options.respectedAtomicPropositions.value();
     atomicPropositionsSet.insert("init");
     std::vector<std::string> atomicPropositions = std::vector<std::string>(atomicPropositionsSet.begin(), atomicPropositionsSet.end());
     for (auto const& ap : atomicPropositions) {
@@ -444,10 +440,7 @@ void NondeterministicModelBisimulationDecomposition<ModelType>::refinePartitionB
 }
 
 template class NondeterministicModelBisimulationDecomposition<storm::models::sparse::Mdp<double>>;
-
-#ifdef STORM_HAVE_CARL
 template class NondeterministicModelBisimulationDecomposition<storm::models::sparse::Mdp<storm::RationalNumber>>;
 template class NondeterministicModelBisimulationDecomposition<storm::models::sparse::Mdp<storm::RationalFunction>>;
-#endif
 }  // namespace storage
 }  // namespace storm
diff --git a/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h b/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h
index 3617be8c21..089265f353 100644
--- a/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h
+++ b/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h
@@ -1,11 +1,9 @@
-#ifndef STORM_STORAGE_BISIMULATION_NONDETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_
-#define STORM_STORAGE_BISIMULATION_NONDETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_
+#pragma once
 
+#include "storm/storage/DistributionWithReward.h"
 #include "storm/storage/bisimulation/BisimulationDecomposition.h"
 #include "storm/storage/bisimulation/DeterministicBlockData.h"
 
-#include "storm/storage/DistributionWithReward.h"
-
 namespace storm {
 namespace storage {
 
@@ -70,7 +68,7 @@ class NondeterministicModelBisimulationDecomposition : public BisimulationDecomp
     bool printDistributions(storm::storage::sparse::state_type state) const;
     bool checkDistributionsDifferent(bisimulation::Block<BlockDataType> const& block, storm::storage::sparse::state_type end) const;
 
-    // A mapping from choice indices to the state state that has this choice.
+    // A mapping from choice indices to the state that has this choice.
     std::vector<storm::storage::sparse::state_type> choiceToStateMapping;
 
     // A vector that holds the quotient distributions for all nondeterministic choices of all states.
@@ -81,5 +79,3 @@ class NondeterministicModelBisimulationDecomposition : public BisimulationDecomp
 };
 }  // namespace storage
 }  // namespace storm
-
-#endif /* STORM_STORAGE_BISIMULATION_NONDETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */
diff --git a/src/storm/storage/bisimulation/Partition.cpp b/src/storm/storage/bisimulation/Partition.cpp
index 93cd0081cd..798168562c 100644
--- a/src/storm/storage/bisimulation/Partition.cpp
+++ b/src/storm/storage/bisimulation/Partition.cpp
@@ -2,9 +2,8 @@
 
 #include <iostream>
 
-#include "storm/storage/bisimulation/DeterministicBlockData.h"
-
 #include "storm/exceptions/InvalidArgumentException.h"
+#include "storm/storage/bisimulation/DeterministicBlockData.h"
 #include "storm/utility/macros.h"
 
 namespace storm {
@@ -24,7 +23,7 @@ Partition<DataType>::Partition(std::size_t numberOfStates) : stateToBlockMapping
 
 template<typename DataType>
 Partition<DataType>::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States,
-                               boost::optional<storm::storage::sparse::state_type> representativeProb1State)
+                               std::optional<storm::storage::sparse::state_type> representativeProb1State)
     : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates) {
     storm::storage::sparse::state_type position = 0;
     Block<DataType>* firstBlock = nullptr;
@@ -54,7 +53,7 @@ Partition<DataType>::Partition(std::size_t numberOfStates, storm::storage::BitVe
             ++position;
         }
         secondBlock->data().setAbsorbing(true);
-        secondBlock->data().setRepresentativeState(representativeProb1State.get());
+        secondBlock->data().setRepresentativeState(representativeProb1State.value());
     }
 
     storm::storage::BitVector otherStates = ~(prob0States | prob1States);
@@ -180,10 +179,7 @@ template<typename DataType>
 void Partition<DataType>::sortRange(storm::storage::sparse::state_type beginIndex, storm::storage::sparse::state_type endIndex,
                                     std::function<bool(storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const& less,
                                     bool updatePositions) {
-    // FIXME, TODO: Wrapping less argument in a lambda here, as clang and the GCC stdlib do not play nicely
-    // Pass 'less' directly to std::sort when this has been resolved (problem with clang 3.7, gcc 5.1)
-    std::sort(this->states.begin() + beginIndex, this->states.begin() + endIndex,
-              [&](const storm::storage::sparse::state_type& a, storm::storage::sparse::state_type& b) { return less(a, b); });
+    std::sort(this->states.begin() + beginIndex, this->states.begin() + endIndex, less);
 
     if (updatePositions) {
         mapStatesToPositions(this->states.begin() + beginIndex, this->states.begin() + endIndex);
diff --git a/src/storm/storage/bisimulation/Partition.h b/src/storm/storage/bisimulation/Partition.h
index 0e8b2338ac..954d7d5f76 100644
--- a/src/storm/storage/bisimulation/Partition.h
+++ b/src/storm/storage/bisimulation/Partition.h
@@ -1,13 +1,10 @@
-#ifndef STORM_STORAGE_BISIMULATION_PARTITION_H_
-#define STORM_STORAGE_BISIMULATION_PARTITION_H_
+#pragma once
 
 #include <cstddef>
-#include <list>
 #include <memory>
 
-#include "storm/storage/bisimulation/Block.h"
-
 #include "storm/storage/BitVector.h"
+#include "storm/storage/bisimulation/Block.h"
 
 namespace storm {
 namespace storage {
@@ -36,7 +33,7 @@ class Partition {
      * model will receive exactly the atomic propositions of the representative state.
      */
     Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States,
-              boost::optional<storm::storage::sparse::state_type> representativeProb1State);
+              std::optional<storm::storage::sparse::state_type> representativeProb1State);
 
     Partition() = default;
     Partition(Partition const& other) = default;
@@ -55,7 +52,7 @@ class Partition {
     std::pair<typename std::vector<std::unique_ptr<Block<DataType>>>::iterator, bool> splitBlock(Block<DataType>& block,
                                                                                                  storm::storage::sparse::state_type position);
 
-    // Sorts the given range of the partitition according to the given order.
+    // Sorts the given range of the partition according to the given order.
     void sortRange(storm::storage::sparse::state_type beginIndex, storm::storage::sparse::state_type endIndex,
                    std::function<bool(storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const& less, bool updatePositions = true);
 
@@ -178,5 +175,3 @@ class Partition {
 }  // namespace bisimulation
 }  // namespace storage
 }  // namespace storm
-
-#endif /* STORM_STORAGE_BISIMULATION_PARTITION_H_ */
diff --git a/src/storm/storage/dd/BisimulationDecomposition.cpp b/src/storm/storage/dd/bisimulation/BisimulationDecomposition.cpp
similarity index 99%
rename from src/storm/storage/dd/BisimulationDecomposition.cpp
rename to src/storm/storage/dd/bisimulation/BisimulationDecomposition.cpp
index f21994c892..a0b23ef222 100644
--- a/src/storm/storage/dd/BisimulationDecomposition.cpp
+++ b/src/storm/storage/dd/bisimulation/BisimulationDecomposition.cpp
@@ -1,20 +1,17 @@
-#include "storm/storage/dd/BisimulationDecomposition.h"
-
-#include "storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.h"
-#include "storm/storage/dd/bisimulation/PartialQuotientExtractor.h"
-#include "storm/storage/dd/bisimulation/Partition.h"
-#include "storm/storage/dd/bisimulation/PartitionRefiner.h"
-#include "storm/storage/dd/bisimulation/QuotientExtractor.h"
+#include "storm/storage/dd/bisimulation/BisimulationDecomposition.h"
 
+#include "storm/exceptions/InvalidOperationException.h"
+#include "storm/exceptions/NotSupportedException.h"
 #include "storm/models/symbolic/Mdp.h"
 #include "storm/models/symbolic/Model.h"
 #include "storm/models/symbolic/StandardRewardModel.h"
-
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/GeneralSettings.h"
-
-#include "storm/exceptions/InvalidOperationException.h"
-#include "storm/exceptions/NotSupportedException.h"
+#include "storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.h"
+#include "storm/storage/dd/bisimulation/PartialQuotientExtractor.h"
+#include "storm/storage/dd/bisimulation/Partition.h"
+#include "storm/storage/dd/bisimulation/PartitionRefiner.h"
+#include "storm/storage/dd/bisimulation/QuotientExtractor.h"
 #include "storm/utility/macros.h"
 
 namespace storm {
diff --git a/src/storm/storage/dd/BisimulationDecomposition.h b/src/storm/storage/dd/bisimulation/BisimulationDecomposition.h
similarity index 99%
rename from src/storm/storage/dd/BisimulationDecomposition.h
rename to src/storm/storage/dd/bisimulation/BisimulationDecomposition.h
index cbd4b79186..b64117c43c 100644
--- a/src/storm/storage/dd/BisimulationDecomposition.h
+++ b/src/storm/storage/dd/bisimulation/BisimulationDecomposition.h
@@ -3,14 +3,13 @@
 #include <memory>
 #include <vector>
 
+#include "storm/logic/Formula.h"
 #include "storm/storage/bisimulation/BisimulationType.h"
 #include "storm/storage/dd/DdType.h"
 #include "storm/storage/dd/bisimulation/PreservationInformation.h"
 #include "storm/storage/dd/bisimulation/QuotientFormat.h"
 #include "storm/storage/dd/bisimulation/SignatureMode.h"
 
-#include "storm/logic/Formula.h"
-
 namespace storm {
 namespace models {
 template<typename ValueType>
diff --git a/src/test/storm/storage/DeterministicModelBisimulationDecompositionTest.cpp b/src/test/storm/storage/DeterministicModelBisimulationDecompositionTest.cpp
index 9922d1f579..ebdbe05739 100644
--- a/src/test/storm/storage/DeterministicModelBisimulationDecompositionTest.cpp
+++ b/src/test/storm/storage/DeterministicModelBisimulationDecompositionTest.cpp
@@ -3,8 +3,10 @@
 
 #include "storm-parsers/parser/AutoParser.h"
 #include "storm-parsers/parser/FormulaParser.h"
+#include "storm-parsers/parser/PrismParser.h"
+#include "storm/builder/ExplicitModelBuilder.h"
+#include "storm/models/sparse/Ctmc.h"
 #include "storm/models/sparse/Dtmc.h"
-#include "storm/models/sparse/StandardRewardModel.h"
 #include "storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h"
 
 TEST(DeterministicModelBisimulationDecomposition, Die) {
@@ -119,3 +121,58 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) {
     EXPECT_EQ(65ul, result->getNumberOfStates());
     EXPECT_EQ(105ul, result->getNumberOfTransitions());
 }
+
+TEST(DeterministicModelBisimulationDecomposition, Cluster) {
+    // TODO FIXME
+    GTEST_SKIP() << "CTMC bisimulation currently yields unstable results.";
+#ifndef STORM_HAVE_Z3
+    GTEST_SKIP() << "Z3 not available.";
+#endif
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true);
+    std::shared_ptr<storm::models::sparse::Model<double>> model =
+        storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
+
+    ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc);
+    std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
+    ASSERT_EQ(3478ul, ctmc->getNumberOfStates());
+    ASSERT_EQ(14639ul, ctmc->getNumberOfTransitions());
+
+    storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<double>> bisim(*ctmc);
+    std::shared_ptr<storm::models::sparse::Model<double>> result;
+    ASSERT_NO_THROW(bisim.computeBisimulationDecomposition());
+    ASSERT_NO_THROW(result = bisim.getQuotient());
+
+    EXPECT_EQ(storm::models::ModelType::Ctmc, result->getType());
+    EXPECT_EQ(1731ul, result->getNumberOfStates());
+    EXPECT_EQ(8619ul, result->getNumberOfTransitions());
+
+    typename storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<double>>::Options options;
+    options.respectedAtomicPropositions = std::set<std::string>({"down"});
+    storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<double>> bisim2(*ctmc, options);
+    ASSERT_NO_THROW(bisim2.computeBisimulationDecomposition());
+    ASSERT_NO_THROW(result = bisim2.getQuotient());
+
+    EXPECT_EQ(storm::models::ModelType::Ctmc, result->getType());
+    EXPECT_EQ(1618ul, result->getNumberOfStates());
+    EXPECT_EQ(8816ul, result->getNumberOfTransitions());
+
+    options.setType(storm::storage::BisimulationType::Weak);
+    storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<double>> bisim3(*ctmc, options);
+    ASSERT_NO_THROW(bisim3.computeBisimulationDecomposition());
+    ASSERT_NO_THROW(result = bisim3.getQuotient());
+
+    EXPECT_EQ(storm::models::ModelType::Ctmc, result->getType());
+    EXPECT_EQ(41ul, result->getNumberOfStates());
+    EXPECT_EQ(159ul, result->getNumberOfTransitions());
+
+    storm::parser::FormulaParser formulaParser;
+    std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10000 \"down\"]");
+    typename storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<double>>::Options options3(*ctmc, *formula);
+    storm::storage::DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<double>> bisim5(*ctmc, options3);
+    ASSERT_NO_THROW(bisim5.computeBisimulationDecomposition());
+    ASSERT_NO_THROW(result = bisim5.getQuotient());
+
+    EXPECT_EQ(storm::models::ModelType::Ctmc, result->getType());
+    EXPECT_EQ(1618ul, result->getNumberOfStates());
+    EXPECT_EQ(8816ul, result->getNumberOfTransitions());
+}
\ No newline at end of file
diff --git a/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp b/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp
index 1844491704..41b69a9d61 100644
--- a/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp
+++ b/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp
@@ -4,21 +4,18 @@
 #include "storm-parsers/parser/FormulaParser.h"
 #include "storm-parsers/parser/PrismParser.h"
 #include "storm/builder/DdPrismModelBuilder.h"
-#include "storm/logic/Formulas.h"
 #include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
 #include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
 #include "storm/modelchecker/results/CheckResult.h"
 #include "storm/modelchecker/results/QuantitativeCheckResult.h"
 #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
 #include "storm/models/sparse/Mdp.h"
-#include "storm/models/sparse/StandardRewardModel.h"
 #include "storm/models/symbolic/Dtmc.h"
 #include "storm/models/symbolic/Mdp.h"
 #include "storm/models/symbolic/StandardRewardModel.h"
 #include "storm/solver/SymbolicLinearEquationSolver.h"
-#include "storm/solver/SymbolicMinMaxLinearEquationSolver.h"
 #include "storm/storage/SymbolicModelDescription.h"
-#include "storm/storage/dd/BisimulationDecomposition.h"
+#include "storm/storage/dd/bisimulation/BisimulationDecomposition.h"
 
 class Cudd {
    public: