diff --git a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp
index f79e62277..06fcd57bb 100644
--- a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp
+++ b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp
@@ -1,127 +1,148 @@
-#include "src/storage/dd/sylvan/InternalSylvanDdManager.h"
-
-#include <cmath>
-
-#include "src/settings/SettingsManager.h"
-#include "src/settings/modules/SylvanSettings.h"
-
-#include "src/utility/constants.h"
-#include "src/utility/macros.h"
-#include "src/exceptions/NotSupportedException.h"
-
-namespace storm {
-    namespace dd {
-        uint_fast64_t InternalDdManager<DdType::Sylvan>::numberOfInstances = 0;
-        
-        // It is important that the variable pairs start at an even offset, because sylvan assumes this to be true for
-        // some operations.
-        uint_fast64_t InternalDdManager<DdType::Sylvan>::nextFreeVariableIndex = 0;
-        
-        uint_fast64_t findLargestPowerOfTwoFitting(uint_fast64_t number) {
-            for (uint_fast64_t index = 0; index < 64; ++index) {
-                if ((number & (1ull << (63 - index))) != 0) {
-                    return 63 - index;
-                }
-            }
-            return 0;
-        }
-        
-        InternalDdManager<DdType::Sylvan>::InternalDdManager() {
-            if (numberOfInstances == 0) {
-                // Initialize lace: auto-detect number of workers.
-                lace_init(storm::settings::getModule<storm::settings::modules::SylvanSettings>().getNumberOfThreads(), 1000000);
-                lace_startup(0, 0, 0);
-                
-                // Each node takes 24 bytes and the maximal memory is specified in megabytes.
-                uint_fast64_t totalNodesToStore = storm::settings::getModule<storm::settings::modules::SylvanSettings>().getMaximalMemory() * 1024 * 1024 / 24;
-                
-                // Compute the power of two that still fits within the total numbers to store.
-                uint_fast64_t powerOfTwo = findLargestPowerOfTwoFitting(totalNodesToStore);
-                
-                sylvan::Sylvan::initPackage(1ull << std::max(16ull, powerOfTwo > 24 ? powerOfTwo - 8 : 0ull), 1ull << (powerOfTwo - 1), 1ull << std::max(16ull, powerOfTwo > 24 ? powerOfTwo - 12 : 0ull), 1ull << (powerOfTwo - 1));
-                sylvan::Sylvan::initBdd(1);
-                sylvan::Sylvan::initMtbdd();
-            }
-            ++numberOfInstances;
-        }
-        
-        InternalDdManager<DdType::Sylvan>::~InternalDdManager() {
-            --numberOfInstances;
-            if (numberOfInstances == 0) {
-                // Enable this to print the sylvan statistics to a file.
-//                FILE* filePointer = fopen("sylvan.stats", "w");
-//                sylvan_stats_report(filePointer, 0);
-//                fclose(filePointer);
-                
-                sylvan::Sylvan::quitPackage();
-                lace_exit();
-            }
-        }
-        
-        InternalBdd<DdType::Sylvan> InternalDdManager<DdType::Sylvan>::getBddOne() const {
-            return InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddOne());
-        }
-        
-        template<>
-        InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddOne() const {
-            return InternalAdd<DdType::Sylvan, double>(this, sylvan::Mtbdd::doubleTerminal(storm::utility::one<double>()));
-        }
-
-        template<>
-        InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddOne() const {
-            return InternalAdd<DdType::Sylvan, uint_fast64_t>(this, sylvan::Mtbdd::int64Terminal(storm::utility::one<uint_fast64_t>()));
-        }
-        
-        InternalBdd<DdType::Sylvan> InternalDdManager<DdType::Sylvan>::getBddZero() const {
-            return InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddZero());
-        }
-        
-        template<>
-        InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddZero() const {
-            return InternalAdd<DdType::Sylvan, double>(this, sylvan::Mtbdd::doubleTerminal(storm::utility::zero<double>()));
-        }
-
-        template<>
-        InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddZero() const {
-            return InternalAdd<DdType::Sylvan, uint_fast64_t>(this, sylvan::Mtbdd::int64Terminal(storm::utility::zero<uint_fast64_t>()));
-        }
-        
-        template<>
-        InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getConstant(double const& value) const {
-            return InternalAdd<DdType::Sylvan, double>(this, sylvan::Mtbdd::doubleTerminal(value));
-        }
-
-        template<>
-        InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getConstant(uint_fast64_t const& value) const {
-            return InternalAdd<DdType::Sylvan, uint_fast64_t>(this, sylvan::Mtbdd::int64Terminal(value));
-        }
-        
-        std::pair<InternalBdd<DdType::Sylvan>, InternalBdd<DdType::Sylvan>> InternalDdManager<DdType::Sylvan>::createNewDdVariablePair() {
-            InternalBdd<DdType::Sylvan> first = InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddVar(nextFreeVariableIndex));
-            InternalBdd<DdType::Sylvan> second = InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddVar(nextFreeVariableIndex + 1));
-            nextFreeVariableIndex += 2;
-            return std::make_pair(first, second);
-        }
-        
-        void InternalDdManager<DdType::Sylvan>::allowDynamicReordering(bool value) {
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan.");
-        }
-        
-        bool InternalDdManager<DdType::Sylvan>::isDynamicReorderingAllowed() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan.");
-        }
-        
-        void InternalDdManager<DdType::Sylvan>::triggerReordering() {
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan.");
-        }
-                
-        template InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddOne() const;
-        template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddOne() const;
-        
-        template InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddZero() const;
-        template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddZero() const;
-        
-        template InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getConstant(double const& value) const;
-        template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getConstant(uint_fast64_t const& value) const;
-    }
+#include "src/storage/dd/sylvan/InternalSylvanDdManager.h"
+
+#include <cmath>
+
+#include "src/settings/SettingsManager.h"
+#include "src/settings/modules/SylvanSettings.h"
+
+#include "src/utility/constants.h"
+#include "src/utility/macros.h"
+#include "src/exceptions/NotSupportedException.h"
+
+namespace storm {
+    namespace dd {
+        uint_fast64_t InternalDdManager<DdType::Sylvan>::numberOfInstances = 0;
+        
+        // It is important that the variable pairs start at an even offset, because sylvan assumes this to be true for
+        // some operations.
+        uint_fast64_t InternalDdManager<DdType::Sylvan>::nextFreeVariableIndex = 0;
+        
+        uint_fast64_t findLargestPowerOfTwoFitting(uint_fast64_t number) {
+            for (uint_fast64_t index = 0; index < 64; ++index) {
+                if ((number & (1ull << (63 - index))) != 0) {
+                    return 63 - index;
+                }
+            }
+            return 0;
+        }
+        
+        InternalDdManager<DdType::Sylvan>::InternalDdManager() {
+            if (numberOfInstances == 0) {
+                // Initialize lace: auto-detect number of workers.
+                lace_init(storm::settings::getModule<storm::settings::modules::SylvanSettings>().getNumberOfThreads(), 1000000);
+                lace_startup(0, 0, 0);
+                
+                // Each node takes 24 bytes and the maximal memory is specified in megabytes.
+                uint_fast64_t totalNodesToStore = storm::settings::getModule<storm::settings::modules::SylvanSettings>().getMaximalMemory() * 1024 * 1024 / 24;
+                
+                // Compute the power of two that still fits within the total numbers to store.
+                uint_fast64_t powerOfTwo = findLargestPowerOfTwoFitting(totalNodesToStore);
+                
+                sylvan::Sylvan::initPackage(1ull << std::max(16ull, powerOfTwo > 24 ? powerOfTwo - 8 : 0ull), 1ull << (powerOfTwo - 1), 1ull << std::max(16ull, powerOfTwo > 24 ? powerOfTwo - 12 : 0ull), 1ull << (powerOfTwo - 1));
+                sylvan::Sylvan::initBdd(1);
+                sylvan::Sylvan::initMtbdd();
+            }
+            ++numberOfInstances;
+        }
+        
+        InternalDdManager<DdType::Sylvan>::~InternalDdManager() {
+            --numberOfInstances;
+            if (numberOfInstances == 0) {
+                // Enable this to print the sylvan statistics to a file.
+//                FILE* filePointer = fopen("sylvan.stats", "w");
+//                sylvan_stats_report(filePointer, 0);
+//                fclose(filePointer);
+                
+                sylvan::Sylvan::quitPackage();
+                lace_exit();
+            }
+        }
+        
+        InternalBdd<DdType::Sylvan> InternalDdManager<DdType::Sylvan>::getBddOne() const {
+            return InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddOne());
+        }
+        
+        template<>
+        InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddOne() const {
+            return InternalAdd<DdType::Sylvan, double>(this, sylvan::Mtbdd::doubleTerminal(storm::utility::one<double>()));
+        }
+
+        template<>
+        InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddOne() const {
+            return InternalAdd<DdType::Sylvan, uint_fast64_t>(this, sylvan::Mtbdd::int64Terminal(storm::utility::one<uint_fast64_t>()));
+        }
+
+#ifdef STORM_HAVE_CARL
+		template<>
+		InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getAddOne() const {
+			return InternalAdd<DdType::Sylvan, storm::RationalFunction>(this, sylvan::Mtbdd::terminal(sylvan_storm_rational_function_get_type(), storm::utility::one<storm::RationalFunction>()));
+		}
+#endif
+        
+        InternalBdd<DdType::Sylvan> InternalDdManager<DdType::Sylvan>::getBddZero() const {
+            return InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddZero());
+        }
+        
+        template<>
+        InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddZero() const {
+            return InternalAdd<DdType::Sylvan, double>(this, sylvan::Mtbdd::doubleTerminal(storm::utility::zero<double>()));
+        }
+
+        template<>
+        InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddZero() const {
+            return InternalAdd<DdType::Sylvan, uint_fast64_t>(this, sylvan::Mtbdd::int64Terminal(storm::utility::zero<uint_fast64_t>()));
+        }
+
+#ifdef STORM_HAVE_CARL
+		template<>
+		InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getAddZero() const {
+			return InternalAdd<DdType::Sylvan, storm::RationalFunction>(this, sylvan::Mtbdd::terminal(sylvan_storm_rational_function_get_type(), storm::utility::zero<storm::RationalFunction>()));
+		}
+#endif
+        
+        template<>
+        InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getConstant(double const& value) const {
+            return InternalAdd<DdType::Sylvan, double>(this, sylvan::Mtbdd::doubleTerminal(value));
+        }
+
+        template<>
+        InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getConstant(uint_fast64_t const& value) const {
+            return InternalAdd<DdType::Sylvan, uint_fast64_t>(this, sylvan::Mtbdd::int64Terminal(value));
+        }
+        
+#ifdef STORM_HAVE_CARL
+		template<>
+		InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getConstant(storm::RationalFunction const& value) const {
+			return InternalAdd<DdType::Sylvan, storm::RationalFunction>(this, sylvan::Mtbdd::terminal(sylvan_storm_rational_function_get_type(), storm::utility::zero<storm::RationalFunction>()));
+		}
+#endif
+
+        std::pair<InternalBdd<DdType::Sylvan>, InternalBdd<DdType::Sylvan>> InternalDdManager<DdType::Sylvan>::createNewDdVariablePair() {
+            InternalBdd<DdType::Sylvan> first = InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddVar(nextFreeVariableIndex));
+            InternalBdd<DdType::Sylvan> second = InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddVar(nextFreeVariableIndex + 1));
+            nextFreeVariableIndex += 2;
+            return std::make_pair(first, second);
+        }
+        
+        void InternalDdManager<DdType::Sylvan>::allowDynamicReordering(bool value) {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan.");
+        }
+        
+        bool InternalDdManager<DdType::Sylvan>::isDynamicReorderingAllowed() const {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan.");
+        }
+        
+        void InternalDdManager<DdType::Sylvan>::triggerReordering() {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan.");
+        }
+                
+        template InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddOne() const;
+        template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddOne() const;
+        
+        template InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddZero() const;
+        template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddZero() const;
+        
+        template InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getConstant(double const& value) const;
+        template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getConstant(uint_fast64_t const& value) const;
+    }
 }
\ No newline at end of file
diff --git a/src/storage/dd/sylvan/InternalSylvanDdManager.h b/src/storage/dd/sylvan/InternalSylvanDdManager.h
index 55be0581f..0618b0dbe 100644
--- a/src/storage/dd/sylvan/InternalSylvanDdManager.h
+++ b/src/storage/dd/sylvan/InternalSylvanDdManager.h
@@ -1,132 +1,148 @@
-#ifndef STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_
-#define STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_
-
-#include "src/storage/dd/DdType.h"
-#include "src/storage/dd/InternalDdManager.h"
-
-#include "src/storage/dd/sylvan/InternalSylvanBdd.h"
-#include "src/storage/dd/sylvan/InternalSylvanAdd.h"
-
-namespace storm {
-    namespace dd {
-        template<DdType LibraryType, typename ValueType>
-        class InternalAdd;
-        
-        template<DdType LibraryType>
-        class InternalBdd;
-        
-        template<>
-        class InternalDdManager<DdType::Sylvan> {
-        public:
-            friend class InternalBdd<DdType::Sylvan>;
-            
-            template<DdType LibraryType, typename ValueType>
-            friend class InternalAdd;
-            
-            /*!
-             * Creates a new internal manager for Sylvan DDs.
-             */
-            InternalDdManager();
-
-            /*!
-             * Destroys the internal manager.
-             */
-            ~InternalDdManager();
-            
-            /*!
-             * Retrieves a BDD representing the constant one function.
-             *
-             * @return A BDD representing the constant one function.
-             */
-            InternalBdd<DdType::Sylvan> getBddOne() const;
-            
-            /*!
-             * Retrieves an ADD representing the constant one function.
-             *
-             * @return An ADD representing the constant one function.
-             */
-            template<typename ValueType>
-            InternalAdd<DdType::Sylvan, ValueType> getAddOne() const;
-            
-            /*!
-             * Retrieves a BDD representing the constant zero function.
-             *
-             * @return A BDD representing the constant zero function.
-             */
-            InternalBdd<DdType::Sylvan> getBddZero() const;
-            
-            /*!
-             * Retrieves an ADD representing the constant zero function.
-             *
-             * @return An ADD representing the constant zero function.
-             */
-            template<typename ValueType>
-            InternalAdd<DdType::Sylvan, ValueType> getAddZero() const;
-            
-            /*!
-             * Retrieves an ADD representing the constant function with the given value.
-             *
-             * @return An ADD representing the constant function with the given value.
-             */
-            template<typename ValueType>
-            InternalAdd<DdType::Sylvan, ValueType> getConstant(ValueType const& value) const;
-            
-            /*!
-             * Creates a new pair of DD variables and returns the two cubes as a result.
-             *
-             * @return The two cubes belonging to the DD variables.
-             */
-            std::pair<InternalBdd<DdType::Sylvan>, InternalBdd<DdType::Sylvan>> createNewDdVariablePair();
-            
-            /*!
-             * Sets whether or not dynamic reordering is allowed for the DDs managed by this manager.
-             *
-             * @param value If set to true, dynamic reordering is allowed and forbidden otherwise.
-             */
-            void allowDynamicReordering(bool value);
-            
-            /*!
-             * Retrieves whether dynamic reordering is currently allowed.
-             *
-             * @return True iff dynamic reordering is currently allowed.
-             */
-            bool isDynamicReorderingAllowed() const;
-            
-            /*!
-             * Triggers a reordering of the DDs managed by this manager.
-             */
-            void triggerReordering();
-            
-        private:
-            // A counter for the number of instances of this class. This is used to determine when to initialize and
-            // quit the sylvan. This is because Sylvan does not know the concept of managers but implicitly has a
-            // 'global' manager.
-            static uint_fast64_t numberOfInstances;
-            
-            // The index of the next free variable index. This needs to be shared across all instances since the sylvan
-            // manager is implicitly 'global'.
-            static uint_fast64_t nextFreeVariableIndex;
-        };
-        
-        template<>
-        InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddOne() const;
-        
-        template<>
-        InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddOne() const;
-
-        template<>
-        InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddZero() const;
-        
-        template<>
-        InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddZero() const;
-
-        template<>
-        InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getConstant(double const& value) const;
-        
-        template<>
-        InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getConstant(uint_fast64_t const& value) const;
-
-    }
-}
-
+#ifndef STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_
+#define STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_
+
+#include "src/storage/dd/DdType.h"
+#include "src/storage/dd/InternalDdManager.h"
+
+#include "src/storage/dd/sylvan/InternalSylvanBdd.h"
+#include "src/storage/dd/sylvan/InternalSylvanAdd.h"
+
+#include "src/adapters/CarlAdapter.h"
+
+namespace storm {
+    namespace dd {
+        template<DdType LibraryType, typename ValueType>
+        class InternalAdd;
+        
+        template<DdType LibraryType>
+        class InternalBdd;
+        
+        template<>
+        class InternalDdManager<DdType::Sylvan> {
+        public:
+            friend class InternalBdd<DdType::Sylvan>;
+            
+            template<DdType LibraryType, typename ValueType>
+            friend class InternalAdd;
+            
+            /*!
+             * Creates a new internal manager for Sylvan DDs.
+             */
+            InternalDdManager();
+
+            /*!
+             * Destroys the internal manager.
+             */
+            ~InternalDdManager();
+            
+            /*!
+             * Retrieves a BDD representing the constant one function.
+             *
+             * @return A BDD representing the constant one function.
+             */
+            InternalBdd<DdType::Sylvan> getBddOne() const;
+            
+            /*!
+             * Retrieves an ADD representing the constant one function.
+             *
+             * @return An ADD representing the constant one function.
+             */
+            template<typename ValueType>
+            InternalAdd<DdType::Sylvan, ValueType> getAddOne() const;
+            
+            /*!
+             * Retrieves a BDD representing the constant zero function.
+             *
+             * @return A BDD representing the constant zero function.
+             */
+            InternalBdd<DdType::Sylvan> getBddZero() const;
+            
+            /*!
+             * Retrieves an ADD representing the constant zero function.
+             *
+             * @return An ADD representing the constant zero function.
+             */
+            template<typename ValueType>
+            InternalAdd<DdType::Sylvan, ValueType> getAddZero() const;
+            
+            /*!
+             * Retrieves an ADD representing the constant function with the given value.
+             *
+             * @return An ADD representing the constant function with the given value.
+             */
+            template<typename ValueType>
+            InternalAdd<DdType::Sylvan, ValueType> getConstant(ValueType const& value) const;
+            
+            /*!
+             * Creates a new pair of DD variables and returns the two cubes as a result.
+             *
+             * @return The two cubes belonging to the DD variables.
+             */
+            std::pair<InternalBdd<DdType::Sylvan>, InternalBdd<DdType::Sylvan>> createNewDdVariablePair();
+            
+            /*!
+             * Sets whether or not dynamic reordering is allowed for the DDs managed by this manager.
+             *
+             * @param value If set to true, dynamic reordering is allowed and forbidden otherwise.
+             */
+            void allowDynamicReordering(bool value);
+            
+            /*!
+             * Retrieves whether dynamic reordering is currently allowed.
+             *
+             * @return True iff dynamic reordering is currently allowed.
+             */
+            bool isDynamicReorderingAllowed() const;
+            
+            /*!
+             * Triggers a reordering of the DDs managed by this manager.
+             */
+            void triggerReordering();
+            
+        private:
+            // A counter for the number of instances of this class. This is used to determine when to initialize and
+            // quit the sylvan. This is because Sylvan does not know the concept of managers but implicitly has a
+            // 'global' manager.
+            static uint_fast64_t numberOfInstances;
+            
+            // The index of the next free variable index. This needs to be shared across all instances since the sylvan
+            // manager is implicitly 'global'.
+            static uint_fast64_t nextFreeVariableIndex;
+        };
+        
+        template<>
+        InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddOne() const;
+        
+        template<>
+        InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddOne() const;
+
+#ifdef STORM_HAVE_CARL
+		template<>
+		InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getAddOne() const;
+#endif
+
+        template<>
+        InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddZero() const;
+        
+        template<>
+        InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddZero() const;
+
+#ifdef STORM_HAVE_CARL
+		template<>
+		InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getAddZero() const;
+#endif
+
+        template<>
+        InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getConstant(double const& value) const;
+        
+        template<>
+        InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getConstant(uint_fast64_t const& value) const;
+
+#ifdef STORM_HAVE_CARL
+		template<>
+		InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getConstant(storm::RationalNumber const& value) const;
+#endif
+    }
+}
+
 #endif /* STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ */
\ No newline at end of file
diff --git a/src/utility/sylvan.h b/src/utility/sylvan.h
index ccaffe097..1dd236609 100644
--- a/src/utility/sylvan.h
+++ b/src/utility/sylvan.h
@@ -1,15 +1,16 @@
-#ifndef STORM_STORAGE_DD_SYLVAN_SYLVAN_H_
-#define STORM_STORAGE_DD_SYLVAN_SYLVAN_H_
-
-#pragma clang diagnostic push
-#pragma clang diagnostic ignored "-Wextra-semi"
-#pragma clang diagnostic ignored "-Wzero-length-array"
-#pragma clang diagnostic ignored "-Wgnu-zero-variadic-macro-arguments"
-#pragma clang diagnostic ignored "-Wdeprecated-register"
-#pragma clang diagnostic ignored "-Wc99-extensions"
-
-#include "sylvan_obj.hpp"
-
-#pragma clang diagnostic pop
-
+#ifndef STORM_STORAGE_DD_SYLVAN_SYLVAN_H_
+#define STORM_STORAGE_DD_SYLVAN_SYLVAN_H_
+
+#pragma clang diagnostic push
+#pragma clang diagnostic ignored "-Wextra-semi"
+#pragma clang diagnostic ignored "-Wzero-length-array"
+#pragma clang diagnostic ignored "-Wgnu-zero-variadic-macro-arguments"
+#pragma clang diagnostic ignored "-Wdeprecated-register"
+#pragma clang diagnostic ignored "-Wc99-extensions"
+
+#include "sylvan_obj.hpp"
+#include "sylvan_storm_rational_function.h"
+
+#pragma clang diagnostic pop
+
 #endif /* STORM_STORAGE_DD_SYLVAN_SYLVAN_H_ */
\ No newline at end of file