diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h
index 3667d0af2..c279dc742 100644
--- a/src/storm-cli-utilities/model-handling.h
+++ b/src/storm-cli-utilities/model-handling.h
@@ -322,43 +322,47 @@ namespace storm {
             }
         }
         
-        template <storm::dd::DdType DdType, typename ValueType>
-        std::shared_ptr<storm::models::Model<ValueType>> preprocessDdModelBisimulation(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input, storm::settings::modules::BisimulationSettings const& bisimulationSettings) {
+        template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
+        std::shared_ptr<storm::models::Model<ExportValueType>> preprocessDdModelBisimulation(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input, storm::settings::modules::BisimulationSettings const& bisimulationSettings) {
             STORM_LOG_WARN_COND(!bisimulationSettings.isWeakBisimulationSet(), "Weak bisimulation is currently not supported on DDs. Falling back to strong bisimulation.");
             
             STORM_LOG_INFO("Performing bisimulation minimization...");
-            return storm::api::performBisimulationMinimization<DdType, ValueType>(model, createFormulasToRespect(input.properties), storm::storage::BisimulationType::Strong, bisimulationSettings.getSignatureMode());
+            return storm::api::performBisimulationMinimization<DdType, ValueType, ExportValueType>(model, createFormulasToRespect(input.properties), storm::storage::BisimulationType::Strong, bisimulationSettings.getSignatureMode());
         }
         
-        template <storm::dd::DdType DdType, typename ValueType>
+        template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
         std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessDdModel(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input) {
             auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
             auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
-            std::pair<std::shared_ptr<storm::models::Model<ValueType>>, bool> result = std::make_pair(model, false);
+            std::pair<std::shared_ptr<storm::models::Model<ValueType>>, bool> intermediateResult = std::make_pair(model, false);
             
             if (model->isOfType(storm::models::ModelType::MarkovAutomaton)) {
-                result.first = preprocessDdMarkovAutomaton(result.first->template as<storm::models::symbolic::Model<DdType, ValueType>>());
-                result.second = true;
+                intermediateResult.first = preprocessDdMarkovAutomaton(intermediateResult.first->template as<storm::models::symbolic::Model<DdType, ValueType>>());
+                intermediateResult.second = true;
             }
             
+            std::unique_ptr<std::pair<std::shared_ptr<storm::models::Model<ExportValueType>>, bool>> result;
+            auto symbolicModel = intermediateResult.first->template as<storm::models::symbolic::Model<DdType, ValueType>>();
             if (generalSettings.isBisimulationSet()) {
-                result.first = preprocessDdModelBisimulation(model, input, bisimulationSettings);
-                result.second = true;
+                std::shared_ptr<storm::models::Model<ExportValueType>> newModel = preprocessDdModelBisimulation<DdType, ValueType, ExportValueType>(symbolicModel, input, bisimulationSettings);
+                result = std::make_unique<std::pair<std::shared_ptr<storm::models::Model<ExportValueType>>, bool>>(newModel, true);
+            } else {
+                result = std::make_unique<std::pair<std::shared_ptr<storm::models::Model<ExportValueType>>, bool>>(symbolicModel->template toValueType<ExportValueType>(), !std::is_same<ValueType, ExportValueType>::value);
             }
             
-            return result;
+            return *result;
         }
         
-        template <storm::dd::DdType DdType, typename ValueType>
+        template <storm::dd::DdType DdType, typename BuildValueType, typename ExportValueType = BuildValueType>
         std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
             storm::utility::Stopwatch preprocessingWatch(true);
             
             std::pair<std::shared_ptr<storm::models::ModelBase>, bool> result = std::make_pair(model, false);
             if (model->isSparseModel()) {
-                result = preprocessSparseModel<ValueType>(result.first->as<storm::models::sparse::Model<ValueType>>(), input);
+                result = preprocessSparseModel<BuildValueType>(result.first->as<storm::models::sparse::Model<BuildValueType>>(), input);
             } else {
                 STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type.");
-                result = preprocessDdModel<DdType, ValueType>(result.first->as<storm::models::symbolic::Model<DdType, ValueType>>(), input);
+                result = preprocessDdModel<DdType, BuildValueType, ExportValueType>(result.first->as<storm::models::symbolic::Model<DdType, BuildValueType>>(), input);
             }
             
             preprocessingWatch.stop();
@@ -639,13 +643,13 @@ namespace storm {
             }
         }
         
-        template <storm::dd::DdType DdType, typename ValueType>
+        template <storm::dd::DdType DdType, typename BuildValueType, typename VerificationValueType = BuildValueType>
         std::shared_ptr<storm::models::ModelBase> buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput const& input, storm::settings::modules::CoreSettings::Engine engine) {
             auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
             auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
             std::shared_ptr<storm::models::ModelBase> model;
             if (!buildSettings.isNoBuildModelSet()) {
-                model = buildModel<DdType, ValueType>(engine, input, ioSettings);
+                model = buildModel<DdType, BuildValueType>(engine, input, ioSettings);
             }
             
             if (model) {
@@ -655,12 +659,12 @@ namespace storm {
             STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model.");
             
             if (model) {
-                auto preprocessingResult = preprocessModel<DdType, ValueType>(model, input);
+                auto preprocessingResult = preprocessModel<DdType, BuildValueType, VerificationValueType>(model, input);
                 if (preprocessingResult.second) {
                     model = preprocessingResult.first;
                     model->printModelInformationToStream(std::cout);
                 }
-                exportModel<DdType, ValueType>(model, input);
+                exportModel<DdType, BuildValueType>(model, input);
             }
             return model;
         }
@@ -678,17 +682,9 @@ namespace storm {
             } else if (engine == storm::settings::modules::CoreSettings::Engine::Exploration) {
                 verifyWithExplorationEngine<VerificationValueType>(input);
             } else {
-                std::shared_ptr<storm::models::ModelBase> model = buildPreprocessExportModelWithValueTypeAndDdlib<DdType, BuildValueType>(input, engine);
+                std::shared_ptr<storm::models::ModelBase> model = buildPreprocessExportModelWithValueTypeAndDdlib<DdType, BuildValueType, VerificationValueType>(input, engine);
 
                 if (model) {
-                    if (!std::is_same<BuildValueType, VerificationValueType>::value) {
-                        if (model->isSymbolicModel()) {
-                            STORM_LOG_INFO("Converting symbolic model value type to fit the verification value type.");
-                            auto symbolicModel = model->as<storm::models::symbolic::Model<DdType, BuildValueType>>();
-                            model = symbolicModel->template toValueType<VerificationValueType>();
-                        }
-                    }
-                    
                     if (coreSettings.isCounterexampleSet()) {
                         auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
                         generateCounterexamples<VerificationValueType>(model, input);
@@ -713,7 +709,7 @@ namespace storm {
                 STORM_LOG_INFO("Switching to DD library sylvan to allow for rational arithmetic.");
                 processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalNumber, double>(input);
             } else if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD) {
-                processInputWithValueTypeAndDdlib<storm::dd::DdType::CUDD, ValueType>(input);
+                processInputWithValueTypeAndDdlib<storm::dd::DdType::CUDD, double>(input);
             } else {
                 STORM_LOG_ASSERT(coreSettings.getDdLibraryType() == storm::dd::DdType::Sylvan, "Unknown DD library.");
                 processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, ValueType>(input);
diff --git a/src/storm/api/bisimulation.h b/src/storm/api/bisimulation.h
index 9ad43f9bd..dc7181e87 100644
--- a/src/storm/api/bisimulation.h
+++ b/src/storm/api/bisimulation.h
@@ -55,8 +55,8 @@ namespace storm {
             }
         }
         
-        template <storm::dd::DdType DdType, typename ValueType>
-        typename std::enable_if<DdType == storm::dd::DdType::Sylvan || std::is_same<ValueType, double>::value, std::shared_ptr<storm::models::Model<ValueType>>>::type performBisimulationMinimization(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType = storm::storage::BisimulationType::Strong, storm::dd::bisimulation::SignatureMode const& mode = storm::dd::bisimulation::SignatureMode::Eager) {
+        template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
+        typename std::enable_if<DdType == storm::dd::DdType::Sylvan || std::is_same<ValueType, double>::value, std::shared_ptr<storm::models::Model<ExportValueType>>>::type performBisimulationMinimization(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType = storm::storage::BisimulationType::Strong, storm::dd::bisimulation::SignatureMode const& mode = storm::dd::bisimulation::SignatureMode::Eager) {
             
             STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::Mdp) || model->isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::NotSupportedException, "Symbolic bisimulation minimization is currently only available for DTMCs, CTMCs, MDPs and MAs.");
             STORM_LOG_THROW(bisimulationType == storm::storage::BisimulationType::Strong, storm::exceptions::NotSupportedException, "Currently only strong bisimulation is supported.");
@@ -64,13 +64,13 @@ namespace storm {
             // Try to get rid of non state-rewards to easy bisimulation computation.
             model->reduceToStateBasedRewards();
             
-            storm::dd::BisimulationDecomposition<DdType, ValueType> decomposition(*model, formulas, bisimulationType);
+            storm::dd::BisimulationDecomposition<DdType, ValueType, ExportValueType> decomposition(*model, formulas, bisimulationType);
             decomposition.compute(mode);
             return decomposition.getQuotient();
         }
         
-        template <storm::dd::DdType DdType, typename ValueType>
-        typename std::enable_if<DdType != storm::dd::DdType::Sylvan && !std::is_same<ValueType, double>::value, std::shared_ptr<storm::models::Model<ValueType>>>::type performBisimulationMinimization(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType = storm::storage::BisimulationType::Strong, storm::dd::bisimulation::SignatureMode const& mode = storm::dd::bisimulation::SignatureMode::Eager) {
+        template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
+        typename std::enable_if<DdType != storm::dd::DdType::Sylvan && !std::is_same<ValueType, double>::value, std::shared_ptr<storm::models::Model<ExportValueType>>>::type performBisimulationMinimization(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType = storm::storage::BisimulationType::Strong, storm::dd::bisimulation::SignatureMode const& mode = storm::dd::bisimulation::SignatureMode::Eager) {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Symbolic bisimulation minimization is not supported for this combination of DD library and value type.");
             return nullptr;
         }
diff --git a/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h b/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h
index 9af7c3a8b..4fe5af95f 100644
--- a/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h
+++ b/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h
@@ -11,7 +11,7 @@ namespace storm {
     }
     
     namespace dd {
-        template<storm::dd::DdType DdType, typename ValueType>
+        template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
         class BisimulationDecomposition;
     }
     
@@ -47,7 +47,7 @@ namespace storm {
             ModelType const& model;
 
             /// The bisimulation object that maintains and refines the model.
-            std::unique_ptr<storm::dd::BisimulationDecomposition<DdType, ValueType>> bisimulation;
+            std::unique_ptr<storm::dd::BisimulationDecomposition<DdType, ValueType, ValueType>> bisimulation;
 
             /// Maintains the last abstract model that was returned.
             std::shared_ptr<storm::models::Model<ValueType>> lastAbstractModel;
diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp
index 71897fded..ee90118cb 100644
--- a/src/storm/models/symbolic/Model.cpp
+++ b/src/storm/models/symbolic/Model.cpp
@@ -6,6 +6,7 @@
 #include "storm/models/symbolic/Ctmc.h"
 #include "storm/models/symbolic/Mdp.h"
 #include "storm/models/symbolic/MarkovAutomaton.h"
+#include "storm/models/symbolic/StochasticTwoPlayerGame.h"
 
 #include "storm/exceptions/IllegalArgumentException.h"
 #include "storm/exceptions/InvalidOperationException.h"
@@ -384,7 +385,9 @@ namespace storm {
             
             template<storm::dd::DdType Type, typename ValueType>
             template<typename NewValueType>
-            std::shared_ptr<Model<Type, NewValueType>> Model<Type, ValueType>::toValueType() const {
+            typename std::enable_if<!std::is_same<ValueType, NewValueType>::value, std::shared_ptr<Model<Type, NewValueType>>>::type Model<Type, ValueType>::toValueType() const {
+                STORM_LOG_TRACE("Converting value type of symbolic model from " << typeid(ValueType).name() << " to " << typeid(NewValueType).name() << ".");
+                
                 // Make a huge branching here as we cannot make a templated function virtual.
                 if (this->getType() == storm::models::ModelType::Dtmc) {
                     return this->template as<storm::models::symbolic::Dtmc<Type, ValueType>>()->template toValueType<NewValueType>();
@@ -394,6 +397,28 @@ namespace storm {
                     return this->template as<storm::models::symbolic::Mdp<Type, ValueType>>()->template toValueType<NewValueType>();
                 } else if (this->getType() == storm::models::ModelType::MarkovAutomaton) {
                     return this->template as<storm::models::symbolic::MarkovAutomaton<Type, ValueType>>()->template toValueType<NewValueType>();
+                } else if (this->getType() == storm::models::ModelType::S2pg) {
+                    return this->template as<storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType>>()->template toValueType<NewValueType>();
+                }
+                
+                STORM_LOG_WARN("Could not convert value type of model.");
+                return nullptr;
+            }
+            
+            template<storm::dd::DdType Type, typename ValueType>
+            template<typename NewValueType>
+            typename std::enable_if<std::is_same<ValueType, NewValueType>::value, std::shared_ptr<Model<Type, NewValueType>>>::type Model<Type, ValueType>::toValueType() const {
+                // Make a huge branching here as we cannot make a templated function virtual.
+                if (this->getType() == storm::models::ModelType::Dtmc) {
+                    return std::make_shared<storm::models::symbolic::Dtmc<Type, ValueType>>(*this->template as<storm::models::symbolic::Dtmc<Type, ValueType>>());
+                } else if (this->getType() == storm::models::ModelType::Ctmc) {
+                    return std::make_shared<storm::models::symbolic::Ctmc<Type, ValueType>>(*this->template as<storm::models::symbolic::Ctmc<Type, ValueType>>());
+                } else if (this->getType() == storm::models::ModelType::Mdp) {
+                    return std::make_shared<storm::models::symbolic::Mdp<Type, ValueType>>(*this->template as<storm::models::symbolic::Mdp<Type, ValueType>>());
+                } else if (this->getType() == storm::models::ModelType::MarkovAutomaton) {
+                    return std::make_shared<storm::models::symbolic::MarkovAutomaton<Type, ValueType>>(*this->template as<storm::models::symbolic::MarkovAutomaton<Type, ValueType>>());
+                } else if (this->getType() == storm::models::ModelType::S2pg) {
+                    return std::make_shared<storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType>>(*this->template as<storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType>>());
                 }
                 
                 STORM_LOG_WARN("Could not convert value type of model.");
@@ -403,9 +428,14 @@ namespace storm {
             // Explicitly instantiate the template class.
             template class Model<storm::dd::DdType::CUDD, double>;
             template class Model<storm::dd::DdType::Sylvan, double>;
-            
+ 
+            template typename std::enable_if<std::is_same<double, double>::value, std::shared_ptr<Model<storm::dd::DdType::CUDD, double>>>::type Model<storm::dd::DdType::CUDD, double>::toValueType<double>() const;
+
             template class Model<storm::dd::DdType::Sylvan, storm::RationalNumber>;
-            template std::shared_ptr<Model<storm::dd::DdType::Sylvan, double>> Model<storm::dd::DdType::Sylvan, storm::RationalNumber>::toValueType() const;
+            template typename std::enable_if<std::is_same<double, double>::value, std::shared_ptr<Model<storm::dd::DdType::Sylvan, double>>>::type Model<storm::dd::DdType::Sylvan, double>::toValueType<double>() const;
+            template typename std::enable_if<std::is_same<storm::RationalNumber, storm::RationalNumber>::value, std::shared_ptr<Model<storm::dd::DdType::Sylvan, storm::RationalNumber>>>::type Model<storm::dd::DdType::Sylvan, storm::RationalNumber>::toValueType<storm::RationalNumber>() const;
+            template typename std::enable_if<std::is_same<storm::RationalFunction, storm::RationalFunction>::value, std::shared_ptr<Model<storm::dd::DdType::Sylvan, storm::RationalFunction>>>::type Model<storm::dd::DdType::Sylvan, storm::RationalFunction>::toValueType<storm::RationalFunction>() const;
+            template typename std::enable_if<!std::is_same<storm::RationalNumber, double>::value, std::shared_ptr<Model<storm::dd::DdType::Sylvan, double>>>::type Model<storm::dd::DdType::Sylvan, storm::RationalNumber>::toValueType<double>() const;
             template class Model<storm::dd::DdType::Sylvan, storm::RationalFunction>;
         } // namespace symbolic
     } // namespace models
diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h
index e194dfabc..1dca3dc6d 100644
--- a/src/storm/models/symbolic/Model.h
+++ b/src/storm/models/symbolic/Model.h
@@ -328,8 +328,11 @@ namespace storm {
                 std::set<storm::RationalFunctionVariable> const& getParameters() const;
                 
                 template<typename NewValueType>
-                std::shared_ptr<Model<Type, NewValueType>> toValueType() const;
+                typename std::enable_if<!std::is_same<ValueType, NewValueType>::value, std::shared_ptr<Model<Type, NewValueType>>>::type toValueType() const;
                 
+                template<typename NewValueType>
+                typename std::enable_if<std::is_same<ValueType, NewValueType>::value, std::shared_ptr<Model<Type, NewValueType>>>::type toValueType() const;
+
             protected:
                 /*!
                  * Sets the transition matrix of the model.
diff --git a/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp b/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp
index b4b59e934..677d80912 100644
--- a/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp
+++ b/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp
@@ -82,11 +82,30 @@ namespace storm {
                 return player2Variables;
             }
             
+            template<storm::dd::DdType Type, typename ValueType>
+            template<typename NewValueType>
+            std::shared_ptr<StochasticTwoPlayerGame<Type, NewValueType>> StochasticTwoPlayerGame<Type, ValueType>::toValueType() const {
+                typedef typename NondeterministicModel<Type, NewValueType>::RewardModelType NewRewardModelType;
+                std::unordered_map<std::string, NewRewardModelType> newRewardModels;
+                
+                for (auto const& e : this->getRewardModels()) {
+                    newRewardModels.emplace(e.first, e.second.template toValueType<NewValueType>());
+                }
+                
+                auto newLabelToBddMap = this->getLabelToBddMap();
+                newLabelToBddMap.erase("init");
+                newLabelToBddMap.erase("deadlock");
+                
+                return std::make_shared<StochasticTwoPlayerGame<Type, NewValueType>>(this->getManagerAsSharedPointer(), this->getReachableStates(), this->getInitialStates(), this->getDeadlockStates(), this->getTransitionMatrix().template toValueType<NewValueType>(), this->getRowVariables(), this->getColumnVariables(), this->getRowColumnMetaVariablePairs(), this->getPlayer1Variables(), this->getPlayer2Variables(), this->getNondeterminismVariables(), newLabelToBddMap, newRewardModels);
+
+            }
+            
             // Explicitly instantiate the template class.
 			template class StochasticTwoPlayerGame<storm::dd::DdType::CUDD, double>;
 			template class StochasticTwoPlayerGame<storm::dd::DdType::Sylvan, double>;
 #ifdef STORM_HAVE_CARL
             template class StochasticTwoPlayerGame<storm::dd::DdType::Sylvan, storm::RationalNumber>;
+            template std::shared_ptr<StochasticTwoPlayerGame<storm::dd::DdType::Sylvan, double>> StochasticTwoPlayerGame<storm::dd::DdType::Sylvan, storm::RationalNumber>::toValueType<double>() const;
 			template class StochasticTwoPlayerGame<storm::dd::DdType::Sylvan, storm::RationalFunction>;
 #endif
             
diff --git a/src/storm/models/symbolic/StochasticTwoPlayerGame.h b/src/storm/models/symbolic/StochasticTwoPlayerGame.h
index d3f009593..569d258dd 100644
--- a/src/storm/models/symbolic/StochasticTwoPlayerGame.h
+++ b/src/storm/models/symbolic/StochasticTwoPlayerGame.h
@@ -117,6 +117,9 @@ namespace storm {
                  */
                 storm::dd::Bdd<Type> getIllegalPlayer2Mask() const;
                 
+                template<typename NewValueType>
+                std::shared_ptr<StochasticTwoPlayerGame<Type, NewValueType>> toValueType() const;
+                
             private:
                 /*!
                  * Prepare all illegal masks.
diff --git a/src/storm/storage/dd/BisimulationDecomposition.cpp b/src/storm/storage/dd/BisimulationDecomposition.cpp
index 682f5602d..d43dd9c65 100644
--- a/src/storm/storage/dd/BisimulationDecomposition.cpp
+++ b/src/storm/storage/dd/BisimulationDecomposition.cpp
@@ -31,31 +31,31 @@ namespace storm {
             }
         }
         
-        template <storm::dd::DdType DdType, typename ValueType>
-        BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, preservationInformation))) {
+        template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
+        BisimulationDecomposition<DdType, ValueType, ExportValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, preservationInformation))) {
             this->initialize();
         }
       
-        template <storm::dd::DdType DdType, typename ValueType>
-        BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType, bisimulation::PreservationInformation<DdType, ValueType> const& preservationInformation) : model(model), preservationInformation(preservationInformation), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, preservationInformation))) {
+        template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
+        BisimulationDecomposition<DdType, ValueType, ExportValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType, bisimulation::PreservationInformation<DdType, ValueType> const& preservationInformation) : model(model), preservationInformation(preservationInformation), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, preservationInformation))) {
             this->initialize();
         }
   
-        template <storm::dd::DdType DdType, typename ValueType>
-        BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, formulas), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, formulas))) {
+        template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
+        BisimulationDecomposition<DdType, ValueType, ExportValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, formulas), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, formulas))) {
             this->initialize();
         }
         
-        template <storm::dd::DdType DdType, typename ValueType>
-        BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& initialPartition, bisimulation::PreservationInformation<DdType, ValueType> const& preservationInformation) : model(model), preservationInformation(preservationInformation), refiner(createRefiner(model, initialPartition)) {
+        template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
+        BisimulationDecomposition<DdType, ValueType, ExportValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& initialPartition, bisimulation::PreservationInformation<DdType, ValueType> const& preservationInformation) : model(model), preservationInformation(preservationInformation), refiner(createRefiner(model, initialPartition)) {
             this->initialize();
         }
         
-        template <storm::dd::DdType DdType, typename ValueType>
-        BisimulationDecomposition<DdType, ValueType>::~BisimulationDecomposition() = default;
+        template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
+        BisimulationDecomposition<DdType, ValueType, ExportValueType>::~BisimulationDecomposition() = default;
         
-        template <storm::dd::DdType DdType, typename ValueType>
-        void BisimulationDecomposition<DdType, ValueType>::initialize() {
+        template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
+        void BisimulationDecomposition<DdType, ValueType, ExportValueType>::initialize() {
             auto const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
             verboseProgress = generalSettings.isVerboseSet();
             showProgressDelay = generalSettings.getShowProgressDelay();
@@ -69,8 +69,8 @@ namespace storm {
             STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNodeCount() << " nodes.");
         }
         
-        template <storm::dd::DdType DdType, typename ValueType>
-        void BisimulationDecomposition<DdType, ValueType>::compute(bisimulation::SignatureMode const& mode) {
+        template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
+        void BisimulationDecomposition<DdType, ValueType, ExportValueType>::compute(bisimulation::SignatureMode const& mode) {
             STORM_LOG_ASSERT(refiner, "No suitable refiner.");
             STORM_LOG_ASSERT(this->refiner->getStatus() != Status::FixedPoint, "Can only proceed if no fixpoint has been reached yet.");
 
@@ -96,8 +96,8 @@ namespace storm {
             STORM_LOG_INFO("Partition refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms (" << iterations << " iterations, signature: " << std::chrono::duration_cast<std::chrono::milliseconds>(refiner->getTotalSignatureTime()).count() << "ms, refinement: " << std::chrono::duration_cast<std::chrono::milliseconds>(refiner->getTotalRefinementTime()).count() << "ms).");
         }
 
-        template <storm::dd::DdType DdType, typename ValueType>
-        bool BisimulationDecomposition<DdType, ValueType>::compute(uint64_t steps, bisimulation::SignatureMode const& mode) {
+        template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
+        bool BisimulationDecomposition<DdType, ValueType, ExportValueType>::compute(uint64_t steps, bisimulation::SignatureMode const& mode) {
             STORM_LOG_ASSERT(refiner, "No suitable refiner.");
             STORM_LOG_ASSERT(this->refiner->getStatus() != Status::FixedPoint, "Can only proceed if no fixpoint has been reached yet.");
             STORM_LOG_ASSERT(steps > 0, "Can only perform positive number of steps.");
@@ -123,24 +123,24 @@ namespace storm {
             return !refined;
         }
         
-        template <storm::dd::DdType DdType, typename ValueType>
-        bool BisimulationDecomposition<DdType, ValueType>::getReachedFixedPoint() const {
+        template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
+        bool BisimulationDecomposition<DdType, ValueType, ExportValueType>::getReachedFixedPoint() const {
             return this->refiner->getStatus() == Status::FixedPoint;
         }
         
-        template <storm::dd::DdType DdType, typename ValueType>
-        std::shared_ptr<storm::models::Model<ValueType>> BisimulationDecomposition<DdType, ValueType>::getQuotient() const {
-            std::shared_ptr<storm::models::Model<ValueType>> quotient;
+        template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
+        std::shared_ptr<storm::models::Model<ExportValueType>> BisimulationDecomposition<DdType, ValueType, ExportValueType>::getQuotient() const {
+            std::shared_ptr<storm::models::Model<ExportValueType>> quotient;
             if (this->refiner->getStatus() == Status::FixedPoint) {
                 STORM_LOG_INFO("Starting full quotient extraction.");
-                QuotientExtractor<DdType, ValueType> extractor;
+                QuotientExtractor<DdType, ValueType, ExportValueType> extractor;
                 quotient = extractor.extract(model, refiner->getStatePartition(), preservationInformation);
             } else {
                 STORM_LOG_THROW(model.getType() == storm::models::ModelType::Dtmc || model.getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidOperationException, "Can only extract partial quotient for discrete-time models.");
                 
                 STORM_LOG_INFO("Starting partial quotient extraction.");
                 if (!partialQuotientExtractor) {
-                    partialQuotientExtractor = std::make_unique<bisimulation::PartialQuotientExtractor<DdType, ValueType>>(model);
+                    partialQuotientExtractor = std::make_unique<bisimulation::PartialQuotientExtractor<DdType, ValueType, ExportValueType>>(model);
                 }
 
                 quotient = partialQuotientExtractor->extract(refiner->getStatePartition(), preservationInformation);
@@ -150,8 +150,8 @@ namespace storm {
             return quotient;
         }
         
-        template <storm::dd::DdType DdType, typename ValueType>
-        void BisimulationDecomposition<DdType, ValueType>::refineWrtRewardModels() {
+        template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
+        void BisimulationDecomposition<DdType, ValueType, ExportValueType>::refineWrtRewardModels() {
             for (auto const& rewardModelName : this->preservationInformation.getRewardModelNames()) {
                 auto const& rewardModel = this->model.getRewardModel(rewardModelName);
                 refiner->refineWrtRewardModel(rewardModel);
@@ -162,6 +162,7 @@ namespace storm {
 
         template class BisimulationDecomposition<storm::dd::DdType::Sylvan, double>;
         template class BisimulationDecomposition<storm::dd::DdType::Sylvan, storm::RationalNumber>;
+        template class BisimulationDecomposition<storm::dd::DdType::Sylvan, storm::RationalNumber, double>;
         template class BisimulationDecomposition<storm::dd::DdType::Sylvan, storm::RationalFunction>;
         
     }
diff --git a/src/storm/storage/dd/BisimulationDecomposition.h b/src/storm/storage/dd/BisimulationDecomposition.h
index b5a088ca2..1a552c497 100644
--- a/src/storm/storage/dd/BisimulationDecomposition.h
+++ b/src/storm/storage/dd/BisimulationDecomposition.h
@@ -29,11 +29,11 @@ namespace storm {
             template <storm::dd::DdType DdType, typename ValueType>
             class PartitionRefiner;
             
-            template <storm::dd::DdType DdType, typename ValueType>
+            template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
             class PartialQuotientExtractor;
         }
         
-        template <storm::dd::DdType DdType, typename ValueType>
+        template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
         class BisimulationDecomposition {
         public:
             BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType);
@@ -64,7 +64,7 @@ namespace storm {
             /*!
              * Retrieves the quotient model after the bisimulation decomposition was computed.
              */
-            std::shared_ptr<storm::models::Model<ValueType>> getQuotient() const;
+            std::shared_ptr<storm::models::Model<ExportValueType>> getQuotient() const;
             
         private:
             void initialize();
@@ -80,7 +80,7 @@ namespace storm {
             std::unique_ptr<bisimulation::PartitionRefiner<DdType, ValueType>> refiner;
             
             // A quotient extractor that is used when the fixpoint has not been reached yet.
-            mutable std::unique_ptr<bisimulation::PartialQuotientExtractor<DdType, ValueType>> partialQuotientExtractor;
+            mutable std::unique_ptr<bisimulation::PartialQuotientExtractor<DdType, ValueType, ExportValueType>> partialQuotientExtractor;
             
             // A flag indicating whether progress is reported.
             bool verboseProgress;
diff --git a/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.cpp
index 9e5e34b54..fea92c755 100644
--- a/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.cpp
+++ b/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.cpp
@@ -15,18 +15,18 @@ namespace storm {
     namespace dd {
         namespace bisimulation {
             
-            template<storm::dd::DdType DdType, typename ValueType>
-            PartialQuotientExtractor<DdType, ValueType>::PartialQuotientExtractor(storm::models::symbolic::Model<DdType, ValueType> const& model) : model(model) {
+            template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
+            PartialQuotientExtractor<DdType, ValueType, ExportValueType>::PartialQuotientExtractor(storm::models::symbolic::Model<DdType, ValueType> const& model) : model(model) {
                 auto const& settings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
                 this->quotientFormat = settings.getQuotientFormat();
                 
                 STORM_LOG_THROW(this->quotientFormat == storm::settings::modules::BisimulationSettings::QuotientFormat::Dd, storm::exceptions::NotSupportedException, "Only DD-based partial quotient extraction is currently supported.");
             }
             
-            template<storm::dd::DdType DdType, typename ValueType>
-            std::shared_ptr<storm::models::Model<ValueType>> PartialQuotientExtractor<DdType, ValueType>::extract(Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
+            template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
+            std::shared_ptr<storm::models::Model<ExportValueType>> PartialQuotientExtractor<DdType, ValueType, ExportValueType>::extract(Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
                 auto start = std::chrono::high_resolution_clock::now();
-                std::shared_ptr<storm::models::Model<ValueType>> result;
+                std::shared_ptr<storm::models::Model<ExportValueType>> result;
                 
                 STORM_LOG_THROW(this->quotientFormat == storm::settings::modules::BisimulationSettings::QuotientFormat::Dd, storm::exceptions::NotSupportedException, "Only DD-based partial quotient extraction is currently supported.");
                 result = extractDdQuotient(partition, preservationInformation);
@@ -38,8 +38,8 @@ namespace storm {
                 return result;
             }
             
-            template<storm::dd::DdType DdType, typename ValueType>
-            std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> PartialQuotientExtractor<DdType, ValueType>::extractDdQuotient(Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
+            template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
+            std::shared_ptr<storm::models::symbolic::Model<DdType, ExportValueType>> PartialQuotientExtractor<DdType, ValueType, ExportValueType>::extractDdQuotient(Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
                 
                 auto modelType = model.getType();
                 if (modelType == storm::models::ModelType::Dtmc || modelType == storm::models::ModelType::Mdp) {
@@ -122,16 +122,19 @@ namespace storm {
                     end = std::chrono::high_resolution_clock::now();
                     STORM_LOG_TRACE("Reward models extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
                     
+                    std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> result;
                     if (modelType == storm::models::ModelType::Dtmc) {
-                        return std::make_shared<storm::models::symbolic::Mdp<DdType, ValueType>>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getRowVariables(), preservedLabelBdds, quotientRewardModels);
+                        result = std::make_shared<storm::models::symbolic::Mdp<DdType, ValueType>>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getRowVariables(), preservedLabelBdds, quotientRewardModels);
                     } else if (modelType == storm::models::ModelType::Mdp) {
                         std::set<storm::expressions::Variable> allNondeterminismVariables;
                         std::set_union(model.getRowVariables().begin(), model.getRowVariables().end(), model.getNondeterminismVariables().begin(), model.getNondeterminismVariables().end(), std::inserter(allNondeterminismVariables, allNondeterminismVariables.begin()));
                         
-                        return std::make_shared<storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType>>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getRowVariables(), model.getNondeterminismVariables(), allNondeterminismVariables, preservedLabelBdds, quotientRewardModels);
+                        result = std::make_shared<storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType>>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getRowVariables(), model.getNondeterminismVariables(), allNondeterminismVariables, preservedLabelBdds, quotientRewardModels);
                     } else {
                         STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unsupported quotient type.");
                     }
+                    
+                    return result->template toValueType<ExportValueType>();
                 } else {
                     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot extract partial quotient for this model type.");
                 }
@@ -142,6 +145,7 @@ namespace storm {
             
 #ifdef STORM_HAVE_CARL
             template class PartialQuotientExtractor<storm::dd::DdType::Sylvan, storm::RationalNumber>;
+            template class PartialQuotientExtractor<storm::dd::DdType::Sylvan, storm::RationalNumber, double>;
             template class PartialQuotientExtractor<storm::dd::DdType::Sylvan, storm::RationalFunction>;
 #endif
             
diff --git a/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.h b/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.h
index 26ae033e6..d5c638c2a 100644
--- a/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.h
+++ b/src/storm/storage/dd/bisimulation/PartialQuotientExtractor.h
@@ -16,15 +16,15 @@ namespace storm {
     namespace dd {
         namespace bisimulation {
             
-            template<storm::dd::DdType DdType, typename ValueType>
+            template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
             class PartialQuotientExtractor {
             public:
                 PartialQuotientExtractor(storm::models::symbolic::Model<DdType, ValueType> const& model);
                 
-                std::shared_ptr<storm::models::Model<ValueType>> extract(Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
+                std::shared_ptr<storm::models::Model<ExportValueType>> extract(Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
                 
             private:
-                std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> extractDdQuotient(Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
+                std::shared_ptr<storm::models::symbolic::Model<DdType, ExportValueType>> extractDdQuotient(Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
                 
                 // The model for which to compute the partial quotient.
                 storm::models::symbolic::Model<DdType, ValueType> const& model;
diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
index 108164a2a..25075a0e9 100644
--- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
+++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
@@ -222,10 +222,10 @@ namespace storm {
                 spp::sparse_hash_map<BDD, bool> visitedNodes;
             };
 
-            template<storm::dd::DdType DdType, typename ValueType>
+            template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
             class InternalSparseQuotientExtractor;
 
-            template<storm::dd::DdType DdType, typename ValueType>
+            template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
             class InternalSparseQuotientExtractorBase {
             public:
                 InternalSparseQuotientExtractorBase(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Bdd<DdType> const& partitionBdd, storm::expressions::Variable const& blockVariable, uint64_t numberOfBlocks, storm::dd::Bdd<DdType> const& representatives) : model(model), manager(model.getManager()), isNondeterministic(false), partitionBdd(partitionBdd), numberOfBlocks(numberOfBlocks), blockVariable(blockVariable), representatives(representatives), matrixEntriesCreated(false) {
@@ -259,23 +259,23 @@ namespace storm {
 
                 virtual ~InternalSparseQuotientExtractorBase() = default;
 
-                storm::storage::SparseMatrix<ValueType> extractTransitionMatrix(storm::dd::Add<DdType, ValueType> const& transitionMatrix) {
+                storm::storage::SparseMatrix<ExportValueType> extractTransitionMatrix(storm::dd::Add<DdType, ValueType> const& transitionMatrix) {
                     return extractMatrixInternal(transitionMatrix);
                 }
                 
-                std::vector<ValueType> extractStateVector(storm::dd::Add<DdType, ValueType> const& vector) {
+                std::vector<ExportValueType> extractStateVector(storm::dd::Add<DdType, ValueType> const& vector) {
                     return extractVectorInternal(vector, this->rowVariablesCube, this->odd);
                 }
 
-                std::vector<ValueType> extractStateActionVector(storm::dd::Add<DdType, ValueType> const& vector) {
+                std::vector<ExportValueType> extractStateActionVector(storm::dd::Add<DdType, ValueType> const& vector) {
                     if (!this->isNondeterministic) {
                         return extractStateVector(vector);
                     } else {
                         STORM_LOG_ASSERT(!this->rowPermutation.empty(), "Expected proper row permutation.");
-                        std::vector<ValueType> valueVector = extractVectorInternal(vector, this->allSourceVariablesCube, this->nondeterminismOdd);
+                        std::vector<ExportValueType> valueVector = extractVectorInternal(vector, this->allSourceVariablesCube, this->nondeterminismOdd);
 
                         // Reorder the values according to the known row permutation.
-                        std::vector<ValueType> reorderedValues(valueVector.size());
+                        std::vector<ExportValueType> reorderedValues(valueVector.size());
                         for (uint64_t pos = 0; pos < valueVector.size(); ++pos) {
                             reorderedValues[pos] = valueVector[rowPermutation[pos]];
                         }
@@ -292,14 +292,14 @@ namespace storm {
                 }
 
             protected:
-                virtual storm::storage::SparseMatrix<ValueType> extractMatrixInternal(storm::dd::Add<DdType, ValueType> const& matrix) = 0;
+                virtual storm::storage::SparseMatrix<ExportValueType> extractMatrixInternal(storm::dd::Add<DdType, ValueType> const& matrix) = 0;
                 
-                virtual std::vector<ValueType> extractVectorInternal(storm::dd::Add<DdType, ValueType> const& vector, storm::dd::Bdd<DdType> const& variablesCube, storm::dd::Odd const& odd) = 0;
+                virtual std::vector<ExportValueType> extractVectorInternal(storm::dd::Add<DdType, ValueType> const& vector, storm::dd::Bdd<DdType> const& variablesCube, storm::dd::Odd const& odd) = 0;
                 
-                storm::storage::SparseMatrix<ValueType> createMatrixFromEntries() {
+                storm::storage::SparseMatrix<ExportValueType> createMatrixFromEntries() {
                     for (auto& row : matrixEntries) {
                         std::sort(row.begin(), row.end(),
-                                  [] (storm::storage::MatrixEntry<uint_fast64_t, ValueType> const& a, storm::storage::MatrixEntry<uint_fast64_t, ValueType> const& b) {
+                                  [] (storm::storage::MatrixEntry<uint_fast64_t, ExportValueType> const& a, storm::storage::MatrixEntry<uint_fast64_t, ExportValueType> const& b) {
                                       return a.getColumn() < b.getColumn();
                                   });
                     }
@@ -312,7 +312,7 @@ namespace storm {
                     
                     uint64_t rowCounter = 0;
                     uint64_t lastState = this->isNondeterministic ? rowToState[rowPermutation.front()] : 0;
-                    storm::storage::SparseMatrixBuilder<ValueType> builder(matrixEntries.size(), this->numberOfBlocks, 0, true, this->isNondeterministic);
+                    storm::storage::SparseMatrixBuilder<ExportValueType> builder(matrixEntries.size(), this->numberOfBlocks, 0, true, this->isNondeterministic);
                     if (this->isNondeterministic) {
                         builder.newRowGroup(0);
                     }
@@ -343,7 +343,7 @@ namespace storm {
                     return builder.build();
                 }
 
-                void addMatrixEntry(uint64_t row, uint64_t column, ValueType const& value) {
+                void addMatrixEntry(uint64_t row, uint64_t column, ExportValueType const& value) {
                     this->matrixEntries[row].emplace_back(column, value);
                 }
                 
@@ -390,7 +390,7 @@ namespace storm {
                 bool matrixEntriesCreated;
                 
                 // The entries of the quotient matrix that is built.
-                std::vector<std::vector<storm::storage::MatrixEntry<uint_fast64_t, ValueType>>> matrixEntries;
+                std::vector<std::vector<storm::storage::MatrixEntry<uint_fast64_t, ExportValueType>>> matrixEntries;
                 
                 // A vector storing for each row which state it belongs to.
                 std::vector<uint64_t> rowToState;
@@ -621,33 +621,33 @@ namespace storm {
                 spp::sparse_hash_map<DdNode const*, uint64_t> blockToOffset;
             };
 
-            template<typename ValueType>
-            class InternalSparseQuotientExtractor<storm::dd::DdType::Sylvan, ValueType> : public InternalSparseQuotientExtractorBase<storm::dd::DdType::Sylvan, ValueType> {
+            template<typename ValueType, typename ExportValueType>
+            class InternalSparseQuotientExtractor<storm::dd::DdType::Sylvan, ValueType, ExportValueType> : public InternalSparseQuotientExtractorBase<storm::dd::DdType::Sylvan, ValueType, ExportValueType> {
             public:
-                InternalSparseQuotientExtractor(storm::models::symbolic::Model<storm::dd::DdType::Sylvan, ValueType> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& partitionBdd, storm::expressions::Variable const& blockVariable, uint64_t numberOfBlocks, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& representatives) : InternalSparseQuotientExtractorBase<storm::dd::DdType::Sylvan, ValueType>(model, partitionBdd, blockVariable, numberOfBlocks, representatives) {
+                InternalSparseQuotientExtractor(storm::models::symbolic::Model<storm::dd::DdType::Sylvan, ValueType> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& partitionBdd, storm::expressions::Variable const& blockVariable, uint64_t numberOfBlocks, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& representatives) : InternalSparseQuotientExtractorBase<storm::dd::DdType::Sylvan, ValueType, ExportValueType>(model, partitionBdd, blockVariable, numberOfBlocks, representatives) {
                     this->createBlockToOffsetMapping();
                 }
                 
             private:
-                virtual storm::storage::SparseMatrix<ValueType> extractMatrixInternal(storm::dd::Add<storm::dd::DdType::Sylvan, ValueType> const& matrix) override {
+                virtual storm::storage::SparseMatrix<ExportValueType> extractMatrixInternal(storm::dd::Add<storm::dd::DdType::Sylvan, ValueType> const& matrix) override {
                     this->createMatrixEntryStorage();
                     extractTransitionMatrixRec(matrix.getInternalAdd().getSylvanMtbdd().GetMTBDD(), this->isNondeterministic ? this->nondeterminismOdd : this->odd, 0, this->partitionBdd.getInternalBdd().getSylvanBdd().GetBDD(), this->representatives.getInternalBdd().getSylvanBdd().GetBDD(), this->allSourceVariablesCube.getInternalBdd().getSylvanBdd().GetBDD(), this->nondeterminismVariablesCube.getInternalBdd().getSylvanBdd().GetBDD(), this->isNondeterministic ? &this->odd : nullptr, 0);
                     return this->createMatrixFromEntries();
                 }
                 
-                virtual std::vector<ValueType> extractVectorInternal(storm::dd::Add<storm::dd::DdType::Sylvan, ValueType> const& vector, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& variablesCube, storm::dd::Odd const& odd) override {
-                    std::vector<ValueType> result(odd.getTotalOffset());
+                virtual std::vector<ExportValueType> extractVectorInternal(storm::dd::Add<storm::dd::DdType::Sylvan, ValueType> const& vector, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& variablesCube, storm::dd::Odd const& odd) override {
+                    std::vector<ExportValueType> result(odd.getTotalOffset());
                     extractVectorRec(vector.getInternalAdd().getSylvanMtbdd().GetMTBDD(), this->representatives.getInternalBdd().getSylvanBdd().GetBDD(), variablesCube.getInternalBdd().getSylvanBdd().GetBDD(), odd, 0, result);
                     return result;
                 }
                 
-                void extractVectorRec(MTBDD vector, BDD representativesNode, BDD variables, storm::dd::Odd const& odd, uint64_t offset, std::vector<ValueType>& result) {
+                void extractVectorRec(MTBDD vector, BDD representativesNode, BDD variables, storm::dd::Odd const& odd, uint64_t offset, std::vector<ExportValueType>& result) {
                     if (representativesNode == sylvan_false || mtbdd_iszero(vector)) {
                         return;
                     }
                     
                     if (sylvan_isconst(variables)) {
-                        result[offset] = storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::getValue(vector);
+                        result[offset] = storm::utility::convertNumber<ExportValueType>(storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::getValue(vector));
                     } else {
                         MTBDD vectorT;
                         MTBDD vectorE;
@@ -723,7 +723,7 @@ namespace storm {
                     // If we have moved through all source variables, we must have arrived at a target block encoding.
                     if (sylvan_isconst(variables)) {
                         STORM_LOG_ASSERT(mtbdd_isleaf(transitionMatrixNode), "Expected constant node.");
-                        this->addMatrixEntry(sourceOffset, blockToOffset.at(targetPartitionNode), storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::getValue(transitionMatrixNode));
+                        this->addMatrixEntry(sourceOffset, blockToOffset.at(targetPartitionNode), storm::utility::convertNumber<ExportValueType>(storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::getValue(transitionMatrixNode)));
                         if (stateOdd) {
                             this->assignRowToState(sourceOffset, stateOffset);
                         }
@@ -817,18 +817,18 @@ namespace storm {
                 spp::sparse_hash_map<BDD, uint64_t> blockToOffset;
             };
 
-            template<storm::dd::DdType DdType, typename ValueType>
-            QuotientExtractor<DdType, ValueType>::QuotientExtractor() : useRepresentatives(false) {
+            template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
+            QuotientExtractor<DdType, ValueType, ExportValueType>::QuotientExtractor() : useRepresentatives(false) {
                 auto const& settings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
                 this->useRepresentatives = settings.isUseRepresentativesSet();
                 this->useOriginalVariables = settings.isUseOriginalVariablesSet();
                 this->quotientFormat = settings.getQuotientFormat();
             }
             
-            template<storm::dd::DdType DdType, typename ValueType>
-            std::shared_ptr<storm::models::Model<ValueType>> QuotientExtractor<DdType, ValueType>::extract(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
+            template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
+            std::shared_ptr<storm::models::Model<ExportValueType>> QuotientExtractor<DdType, ValueType, ExportValueType>::extract(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
                 auto start = std::chrono::high_resolution_clock::now();
-                std::shared_ptr<storm::models::Model<ValueType>> result;
+                std::shared_ptr<storm::models::Model<ExportValueType>> result;
                 if (quotientFormat == storm::settings::modules::BisimulationSettings::QuotientFormat::Sparse) {
                     result = extractSparseQuotient(model, partition, preservationInformation);
                 } else {
@@ -842,8 +842,8 @@ namespace storm {
                 return result;
             }
             
-            template<storm::dd::DdType DdType, typename ValueType>
-            std::shared_ptr<storm::models::sparse::Model<ValueType>> QuotientExtractor<DdType, ValueType>::extractSparseQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
+            template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
+            std::shared_ptr<storm::models::sparse::Model<ExportValueType>> QuotientExtractor<DdType, ValueType, ExportValueType>::extractSparseQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
                 auto states = partition.getStates().swapVariables(model.getRowColumnMetaVariablePairs());
                 
                 storm::dd::Bdd<DdType> partitionAsBdd = partition.storedAsAdd() ? partition.asAdd().toBdd() : partition.asBdd();
@@ -853,8 +853,8 @@ namespace storm {
                 auto representatives = InternalRepresentativeComputer<DdType>(partitionAsBdd, model.getRowVariables()).getRepresentatives();
                 STORM_LOG_ASSERT(representatives.getNonZeroCount() == partition.getNumberOfBlocks(), "Representatives size does not match that of the partition: " << representatives.getNonZeroCount() << " vs. " << partition.getNumberOfBlocks() << ".");
                 STORM_LOG_ASSERT((representatives && partitionAsBdd).existsAbstract(model.getRowVariables()) == partitionAsBdd.existsAbstract(model.getRowVariables()), "Representatives do not cover all blocks.");
-                InternalSparseQuotientExtractor<DdType, ValueType> sparseExtractor(model, partitionAsBdd, partition.getBlockVariable(), partition.getNumberOfBlocks(), representatives);
-                storm::storage::SparseMatrix<ValueType> quotientTransitionMatrix = sparseExtractor.extractTransitionMatrix(model.getTransitionMatrix());
+                InternalSparseQuotientExtractor<DdType, ValueType, ExportValueType> sparseExtractor(model, partitionAsBdd, partition.getBlockVariable(), partition.getNumberOfBlocks(), representatives);
+                storm::storage::SparseMatrix<ExportValueType> quotientTransitionMatrix = sparseExtractor.extractTransitionMatrix(model.getTransitionMatrix());
                 auto end = std::chrono::high_resolution_clock::now();
                 STORM_LOG_INFO("Quotient transition matrix extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
 
@@ -881,47 +881,47 @@ namespace storm {
                 STORM_LOG_INFO("Quotient labels extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
 
                 start = std::chrono::high_resolution_clock::now();
-                std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> quotientRewardModels;
+                std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ExportValueType>> quotientRewardModels;
                 for (auto const& rewardModelName : preservationInformation.getRewardModelNames()) {
                     auto const& rewardModel = model.getRewardModel(rewardModelName);
                     
-                    boost::optional<std::vector<ValueType>> quotientStateRewards;
+                    boost::optional<std::vector<ExportValueType>> quotientStateRewards;
                     if (rewardModel.hasStateRewards()) {
                         quotientStateRewards = sparseExtractor.extractStateVector(rewardModel.getStateRewardVector());
                     }
                     
-                    boost::optional<std::vector<ValueType>> quotientStateActionRewards;
+                    boost::optional<std::vector<ExportValueType>> quotientStateActionRewards;
                     if (rewardModel.hasStateActionRewards()) {
                         quotientStateActionRewards = sparseExtractor.extractStateActionVector(rewardModel.getStateActionRewardVector());
                     }
                     
-                    quotientRewardModels.emplace(rewardModelName, storm::models::sparse::StandardRewardModel<ValueType>(std::move(quotientStateRewards), std::move(quotientStateActionRewards), boost::none));
+                    quotientRewardModels.emplace(rewardModelName, storm::models::sparse::StandardRewardModel<ExportValueType>(std::move(quotientStateRewards), std::move(quotientStateActionRewards), boost::none));
                 }
                 end = std::chrono::high_resolution_clock::now();
                 STORM_LOG_INFO("Reward models extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
 
-                std::shared_ptr<storm::models::sparse::Model<ValueType>> result;
+                std::shared_ptr<storm::models::sparse::Model<ExportValueType>> result;
                 if (model.getType() == storm::models::ModelType::Dtmc) {
-                    result = std::make_shared<storm::models::sparse::Dtmc<ValueType>>(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling), std::move(quotientRewardModels));
+                    result = std::make_shared<storm::models::sparse::Dtmc<ExportValueType>>(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling), std::move(quotientRewardModels));
                 } else if (model.getType() == storm::models::ModelType::Ctmc) {
-                    result = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling), std::move(quotientRewardModels));
+                    result = std::make_shared<storm::models::sparse::Ctmc<ExportValueType>>(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling), std::move(quotientRewardModels));
                 } else if (model.getType() == storm::models::ModelType::Mdp) {
-                    result = std::make_shared<storm::models::sparse::Mdp<ValueType>>(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling), std::move(quotientRewardModels));
+                    result = std::make_shared<storm::models::sparse::Mdp<ExportValueType>>(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling), std::move(quotientRewardModels));
                 } else if (model.getType() == storm::models::ModelType::MarkovAutomaton) {
                     storm::models::symbolic::MarkovAutomaton<DdType, ValueType> const& markovAutomaton = *model.template as<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>();
                     
                     boost::optional<storm::storage::BitVector> markovianStates = sparseExtractor.extractSetExists(markovAutomaton.getMarkovianStates());
-                    storm::storage::sparse::ModelComponents<ValueType> modelComponents(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling), std::move(quotientRewardModels), false, std::move(markovianStates));
+                    storm::storage::sparse::ModelComponents<ExportValueType> modelComponents(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling), std::move(quotientRewardModels), false, std::move(markovianStates));
                     modelComponents.exitRates = sparseExtractor.extractStateVector(markovAutomaton.getExitRateVector());
                     
-                    result = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(modelComponents));
+                    result = std::make_shared<storm::models::sparse::MarkovAutomaton<ExportValueType>>(std::move(modelComponents));
                 }
                 
                 return result;
             }
 
-            template<storm::dd::DdType DdType, typename ValueType>
-            std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> QuotientExtractor<DdType, ValueType>::extractDdQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
+            template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
+            std::shared_ptr<storm::models::symbolic::Model<DdType, ExportValueType>> QuotientExtractor<DdType, ValueType, ExportValueType>::extractDdQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
                 
                 if (this->useOriginalVariables) {
                     return extractQuotientUsingOriginalVariables(model, partition, preservationInformation);
@@ -930,8 +930,8 @@ namespace storm {
                 }
             }
 
-            template<storm::dd::DdType DdType, typename ValueType>
-            std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> QuotientExtractor<DdType, ValueType>::extractQuotientUsingBlockVariables(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
+            template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
+            std::shared_ptr<storm::models::symbolic::Model<DdType, ExportValueType>> QuotientExtractor<DdType, ValueType, ExportValueType>::extractQuotientUsingBlockVariables(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
                 auto modelType = model.getType();
                 
                 bool useRepresentativesForThisExtraction = this->useRepresentatives;
@@ -1028,22 +1028,25 @@ namespace storm {
                     end = std::chrono::high_resolution_clock::now();
                     STORM_LOG_INFO("Reward models extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
 
+                    std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> result;
                     if (modelType == storm::models::ModelType::Dtmc) {
-                        return std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>>(new storm::models::symbolic::Dtmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, quotientRewardModels));
+                        result = std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>>(new storm::models::symbolic::Dtmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, quotientRewardModels));
                     } else if (modelType == storm::models::ModelType::Ctmc) {
-                        return std::shared_ptr<storm::models::symbolic::Ctmc<DdType, ValueType>>(new storm::models::symbolic::Ctmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, quotientRewardModels));
+                        result = std::shared_ptr<storm::models::symbolic::Ctmc<DdType, ValueType>>(new storm::models::symbolic::Ctmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, quotientRewardModels));
                     } else if (modelType == storm::models::ModelType::Mdp) {
-                        return std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>>(new storm::models::symbolic::Mdp<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
+                        result = std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>>(new storm::models::symbolic::Mdp<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
                     } else {
-                        return std::shared_ptr<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>(new storm::models::symbolic::MarkovAutomaton<DdType, ValueType>(model.getManager().asSharedPointer(), model. template as<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>()->getMarkovianMarker(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
+                        result = std::shared_ptr<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>(new storm::models::symbolic::MarkovAutomaton<DdType, ValueType>(model.getManager().asSharedPointer(), model. template as<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>()->getMarkovianMarker(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
                     }
+                    
+                    return result->template toValueType<ExportValueType>();
                 } else {
                     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot extract quotient for this model type.");
                 }
             }
             
-            template<storm::dd::DdType DdType, typename ValueType>
-            std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> QuotientExtractor<DdType, ValueType>::extractQuotientUsingOriginalVariables(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
+            template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
+            std::shared_ptr<storm::models::symbolic::Model<DdType, ExportValueType>> QuotientExtractor<DdType, ValueType, ExportValueType>::extractQuotientUsingOriginalVariables(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
                 auto modelType = model.getType();
                 
                 bool useRepresentativesForThisExtraction = this->useRepresentatives;
@@ -1146,15 +1149,18 @@ namespace storm {
                     end = std::chrono::high_resolution_clock::now();
                     STORM_LOG_INFO("Reward models extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
                     
+                    std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> result;
                     if (modelType == storm::models::ModelType::Dtmc) {
-                        return std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>>(new storm::models::symbolic::Dtmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), preservedLabelBdds, quotientRewardModels));
+                        result = std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>>(new storm::models::symbolic::Dtmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), preservedLabelBdds, quotientRewardModels));
                     } else if (modelType == storm::models::ModelType::Ctmc) {
-                        return std::shared_ptr<storm::models::symbolic::Ctmc<DdType, ValueType>>(new storm::models::symbolic::Ctmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), preservedLabelBdds, quotientRewardModels));
+                        result = std::shared_ptr<storm::models::symbolic::Ctmc<DdType, ValueType>>(new storm::models::symbolic::Ctmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), preservedLabelBdds, quotientRewardModels));
                     } else if (modelType == storm::models::ModelType::Mdp) {
-                        return std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>>(new storm::models::symbolic::Mdp<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
+                        result = std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>>(new storm::models::symbolic::Mdp<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
                     } else {
-                        return std::shared_ptr<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>(new storm::models::symbolic::MarkovAutomaton<DdType, ValueType>(model.getManager().asSharedPointer(), model. template as<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>()->getMarkovianMarker(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
+                        result = std::shared_ptr<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>(new storm::models::symbolic::MarkovAutomaton<DdType, ValueType>(model.getManager().asSharedPointer(), model. template as<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>()->getMarkovianMarker(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
                     }
+                    
+                    return result->template toValueType<ExportValueType>();
                 } else {
                     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot extract quotient for this model type.");
                 }
@@ -1164,6 +1170,7 @@ namespace storm {
             
             template class QuotientExtractor<storm::dd::DdType::Sylvan, double>;
             template class QuotientExtractor<storm::dd::DdType::Sylvan, storm::RationalNumber>;
+            template class QuotientExtractor<storm::dd::DdType::Sylvan, storm::RationalNumber, double>;
             template class QuotientExtractor<storm::dd::DdType::Sylvan, storm::RationalFunction>;
             
         }
diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.h b/src/storm/storage/dd/bisimulation/QuotientExtractor.h
index b75b27b08..422453bf7 100644
--- a/src/storm/storage/dd/bisimulation/QuotientExtractor.h
+++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.h
@@ -16,19 +16,19 @@ namespace storm {
     namespace dd {
         namespace bisimulation {
             
-            template<storm::dd::DdType DdType, typename ValueType>
+            template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
             class QuotientExtractor {
             public:
                 QuotientExtractor();
                 
-                std::shared_ptr<storm::models::Model<ValueType>> extract(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
+                std::shared_ptr<storm::models::Model<ExportValueType>> extract(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
                 
             private:
-                std::shared_ptr<storm::models::sparse::Model<ValueType>> extractSparseQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
+                std::shared_ptr<storm::models::sparse::Model<ExportValueType>> extractSparseQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
                 
-                std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> extractDdQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
-                std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> extractQuotientUsingBlockVariables(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
-                std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> extractQuotientUsingOriginalVariables(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
+                std::shared_ptr<storm::models::symbolic::Model<DdType, ExportValueType>> extractDdQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
+                std::shared_ptr<storm::models::symbolic::Model<DdType, ExportValueType>> extractQuotientUsingBlockVariables(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
+                std::shared_ptr<storm::models::symbolic::Model<DdType, ExportValueType>> extractQuotientUsingOriginalVariables(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
 
                 bool useRepresentatives;
                 bool useOriginalVariables;