diff --git a/src/abstraction/AbstractionDdInformation.cpp b/src/abstraction/AbstractionDdInformation.cpp
index f3b8dbf15..598443df6 100644
--- a/src/abstraction/AbstractionDdInformation.cpp
+++ b/src/abstraction/AbstractionDdInformation.cpp
@@ -41,14 +41,7 @@ namespace storm {
         void AbstractionDdInformation<DdType, ValueType>::addPredicate(storm::expressions::Expression const& predicate) {
             std::stringstream stream;
             stream << predicate;
-            std::pair<storm::expressions::Variable, storm::expressions::Variable> newMetaVariable;
-            
-            // Create the new predicate variable below all other predicate variables.
-            if (predicateDdVariables.empty()) {
-                newMetaVariable = manager->addMetaVariable(stream.str());
-            } else {
-                newMetaVariable = manager->addMetaVariable(stream.str(), std::make_pair(storm::dd::MetaVariablePosition::Below, predicateDdVariables.back().second));
-            }
+            std::pair<storm::expressions::Variable, storm::expressions::Variable> newMetaVariable = manager->addMetaVariable(stream.str());
             
             predicateDdVariables.push_back(newMetaVariable);
             predicateBdds.emplace_back(manager->getEncoding(newMetaVariable.first, 1), manager->getEncoding(newMetaVariable.second, 1));
@@ -92,6 +85,7 @@ namespace storm {
         }
         
         template struct AbstractionDdInformation<storm::dd::DdType::CUDD, double>;
+        template struct AbstractionDdInformation<storm::dd::DdType::Sylvan, double>;
         
     }
 }
\ No newline at end of file
diff --git a/src/abstraction/MenuGame.cpp b/src/abstraction/MenuGame.cpp
index b84a735ae..d9ad05124 100644
--- a/src/abstraction/MenuGame.cpp
+++ b/src/abstraction/MenuGame.cpp
@@ -61,6 +61,7 @@ namespace storm {
         }
         
         template class MenuGame<storm::dd::DdType::CUDD, double>;
+        template class MenuGame<storm::dd::DdType::Sylvan, double>;
         
     }
 }
diff --git a/src/abstraction/StateSetAbstractor.cpp b/src/abstraction/StateSetAbstractor.cpp
index f104956ed..b3c7480e0 100644
--- a/src/abstraction/StateSetAbstractor.cpp
+++ b/src/abstraction/StateSetAbstractor.cpp
@@ -134,9 +134,9 @@ namespace storm {
             smtSolver->push();
             
             // Then add the constraint.
-            std::pair<std::vector<storm::expressions::Expression>, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>> result = constraint.toExpression(globalExpressionInformation.getManager(), ddInformation.bddVariableIndexToPredicateMap);
+            std::vector<storm::expressions::Expression> result = constraint.toExpression(globalExpressionInformation.getManager(), ddInformation.bddVariableIndexToPredicateMap);
             
-            for (auto const& expression : result.first) {
+            for (auto const& expression : result) {
                 smtSolver->add(expression);
             }
         }
@@ -150,5 +150,6 @@ namespace storm {
         }
         
         template class StateSetAbstractor<storm::dd::DdType::CUDD, double>;
+        template class StateSetAbstractor<storm::dd::DdType::Sylvan, double>;
     }
 }
diff --git a/src/abstraction/prism/AbstractCommand.cpp b/src/abstraction/prism/AbstractCommand.cpp
index a6b9c4599..e39bfd911 100644
--- a/src/abstraction/prism/AbstractCommand.cpp
+++ b/src/abstraction/prism/AbstractCommand.cpp
@@ -306,6 +306,7 @@ namespace storm {
             }
             
             template class AbstractCommand<storm::dd::DdType::CUDD, double>;
+            template class AbstractCommand<storm::dd::DdType::Sylvan, double>;
         }
     }
 }
\ No newline at end of file
diff --git a/src/abstraction/prism/AbstractModule.cpp b/src/abstraction/prism/AbstractModule.cpp
index feb7c7df3..069bbf0ef 100644
--- a/src/abstraction/prism/AbstractModule.cpp
+++ b/src/abstraction/prism/AbstractModule.cpp
@@ -57,6 +57,7 @@ namespace storm {
             }
             
             template class AbstractModule<storm::dd::DdType::CUDD, double>;
+            template class AbstractModule<storm::dd::DdType::Sylvan, double>;
         }
     }
 }
\ No newline at end of file
diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp
index 933f0ebc3..1e7d63b73 100644
--- a/src/abstraction/prism/AbstractProgram.cpp
+++ b/src/abstraction/prism/AbstractProgram.cpp
@@ -181,9 +181,9 @@ namespace storm {
             
             template <storm::dd::DdType DdType, typename ValueType>
             storm::dd::Bdd<DdType> AbstractProgram<DdType, ValueType>::getReachableStates(storm::dd::Bdd<DdType> const& initialStates, storm::dd::Bdd<DdType> const& transitionRelation) {
-                storm::dd::Bdd<storm::dd::DdType::CUDD> frontier = initialStates;
+                storm::dd::Bdd<DdType> frontier = initialStates;
 
-                storm::dd::Bdd<storm::dd::DdType::CUDD> reachableStates = initialStates;
+                storm::dd::Bdd<DdType> reachableStates = initialStates;
                 uint_fast64_t reachabilityIteration = 0;
                 while (!frontier.isZero()) {
                     ++reachabilityIteration;
@@ -199,6 +199,7 @@ namespace storm {
             
             // Explicitly instantiate the class.
             template class AbstractProgram<storm::dd::DdType::CUDD, double>;
+            template class AbstractProgram<storm::dd::DdType::Sylvan, double>;
             
         }
     }
diff --git a/src/storage/dd/Bdd.cpp b/src/storage/dd/Bdd.cpp
index 27d76dc44..7e767c044 100644
--- a/src/storage/dd/Bdd.cpp
+++ b/src/storage/dd/Bdd.cpp
@@ -269,7 +269,7 @@ namespace storm {
         }
         
         template<DdType LibraryType>
-        std::pair<std::vector<storm::expressions::Expression>, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>> Bdd<LibraryType>::toExpression(storm::expressions::ExpressionManager& manager, std::unordered_map<uint_fast64_t, storm::expressions::Expression> const& indexToExpressionMap) const {
+        std::vector<storm::expressions::Expression> Bdd<LibraryType>::toExpression(storm::expressions::ExpressionManager& manager, std::unordered_map<uint_fast64_t, storm::expressions::Expression> const& indexToExpressionMap) const {
             return internalBdd.toExpression(manager, indexToExpressionMap);
         }
         
diff --git a/src/storage/dd/Bdd.h b/src/storage/dd/Bdd.h
index 0c1563c7d..5d529890d 100644
--- a/src/storage/dd/Bdd.h
+++ b/src/storage/dd/Bdd.h
@@ -291,10 +291,9 @@ namespace storm {
              * @param manager The manager that is used to build the expression and, in particular, create new variables in.
              * @param indexToExpressionMap A mapping from indices (of DD variables) to expressions with which they are
              * to be replaced.
-             * @return A pair consisting of the created expressions and a mapping from pairs (i, j) to variables such
-             * that the i-th variable of level j is represented by the mapped-to variable.
+             * @return A list of expressions representing the function of the BDD.
              */
-            std::pair<std::vector<storm::expressions::Expression>, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>> toExpression(storm::expressions::ExpressionManager& manager, std::unordered_map<uint_fast64_t, storm::expressions::Expression> const& indexToExpressionMap) const;
+            std::vector<storm::expressions::Expression> toExpression(storm::expressions::ExpressionManager& manager, std::unordered_map<uint_fast64_t, storm::expressions::Expression> const& indexToExpressionMap) const;
             
             virtual Bdd<LibraryType> getSupport() const override;
             
diff --git a/src/storage/dd/cudd/InternalCuddBdd.cpp b/src/storage/dd/cudd/InternalCuddBdd.cpp
index 88a22bec2..3953c488e 100644
--- a/src/storage/dd/cudd/InternalCuddBdd.cpp
+++ b/src/storage/dd/cudd/InternalCuddBdd.cpp
@@ -416,35 +416,34 @@ namespace storm {
             }
         }
         
-        std::pair<std::vector<storm::expressions::Expression>, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>> InternalBdd<DdType::CUDD>::toExpression(storm::expressions::ExpressionManager& manager, std::unordered_map<uint_fast64_t, storm::expressions::Expression> const& indexToExpressionMap) const {
-            std::pair<std::vector<storm::expressions::Expression>, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>> result;
+        std::vector<storm::expressions::Expression> InternalBdd<DdType::CUDD>::toExpression(storm::expressions::ExpressionManager& manager, std::unordered_map<uint_fast64_t, storm::expressions::Expression> const& indexToExpressionMap) const {
+            std::vector<storm::expressions::Expression> result;
             
             // Create (and maintain) a mapping from the DD nodes to a counter that says the how-many-th node (within the
             // nodes of equal index) the node was.
             std::unordered_map<DdNode const*, uint_fast64_t> nodeToCounterMap;
             std::vector<uint_fast64_t> nextCounterForIndex(ddManager->getNumberOfDdVariables(), 0);
+            std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable> countIndexToVariablePair;
+
             bool negated = Cudd_Regular(this->getCuddDdNode()) != this->getCuddDdNode();
             
             // Translate from the top node downwards.
-            storm::expressions::Variable topVariable = this->toExpressionRec(Cudd_Regular(this->getCuddDdNode()), manager, result.first, result.second, nodeToCounterMap, nextCounterForIndex, indexToExpressionMap);
+            storm::expressions::Variable topVariable = this->toExpressionRec(Cudd_Regular(this->getCuddDdNode()), ddManager->getCuddManager(), manager, result, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex, indexToExpressionMap);
             
             // Create the final expression.
             if (negated) {
-                result.first.push_back(!topVariable);
+                result.push_back(!topVariable);
             } else {
-                result.first.push_back(topVariable);
+                result.push_back(topVariable);
             }
             
             return result;
         }
         
-        storm::expressions::Variable InternalBdd<DdType::CUDD>::toExpressionRec(DdNode const* dd, storm::expressions::ExpressionManager& manager, std::vector<storm::expressions::Expression>& expressions, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map<DdNode const*, uint_fast64_t>& nodeToCounterMap, std::vector<uint_fast64_t>& nextCounterForIndex, std::unordered_map<uint_fast64_t, storm::expressions::Expression> const& indexToExpressionMap) const {
+        storm::expressions::Variable InternalBdd<DdType::CUDD>::toExpressionRec(DdNode const* dd, cudd::Cudd const& ddManager, storm::expressions::ExpressionManager& manager, std::vector<storm::expressions::Expression>& expressions, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map<DdNode const*, uint_fast64_t>& nodeToCounterMap, std::vector<uint_fast64_t>& nextCounterForIndex, std::unordered_map<uint_fast64_t, storm::expressions::Expression> const& indexToExpressionMap) {
             STORM_LOG_ASSERT(dd == Cudd_Regular(dd), "Expected non-negated BDD node.");
             
-            // First, try to look up the current node if it's not a terminal node. The result of terminal nodes must not
-            // be reused, since we want to be able to incrementally refine the expression later and that requires
-            // different variables for the one-leaf.
-            //            if (!Cudd_IsConstant(dd)) {
+            // First, try to look up the current node if it's not a terminal node.
             auto nodeCounterIt = nodeToCounterMap.find(dd);
             if (nodeCounterIt != nodeToCounterMap.end()) {
                 // If we have found the node, this means we can look up the counter-index pair and get the corresponding variable.
@@ -452,7 +451,6 @@ namespace storm {
                 STORM_LOG_ASSERT(variableIt != countIndexToVariablePair.end(), "Unable to find node.");
                 return variableIt->second;
             }
-            //            }
             
             // If the node was not yet encountered, we create a variable and associate it with the appropriate expression.
             storm::expressions::Variable newVariable = manager.declareFreshBooleanVariable();
@@ -470,17 +468,17 @@ namespace storm {
             }
             
             // In the terminal case, we can only have a one since we are considering non-negated nodes only.
-            if (dd == Cudd_ReadOne(ddManager->getCuddManager().getManager())) {
+            if (dd == Cudd_ReadOne(ddManager.getManager())) {
                 // Push the expression that enforces that the new variable is true.
-                expressions.push_back(storm::expressions::implies(manager.boolean(true), newVariable));
+                expressions.push_back(storm::expressions::iff(manager.boolean(true), newVariable));
             } else {
                 // In the non-terminal case, we recursively translate the children nodes and then construct and appropriate ite-expression.
                 DdNode const* t = Cudd_T_const(dd);
                 DdNode const* e = Cudd_E_const(dd);
                 DdNode const* T = Cudd_Regular(t);
                 DdNode const* E = Cudd_Regular(e);
-                storm::expressions::Variable thenVariable = toExpressionRec(T, manager, expressions, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex, indexToExpressionMap);
-                storm::expressions::Variable elseVariable = toExpressionRec(E, manager, expressions, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex, indexToExpressionMap);
+                storm::expressions::Variable thenVariable = toExpressionRec(T, ddManager, manager, expressions, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex, indexToExpressionMap);
+                storm::expressions::Variable elseVariable = toExpressionRec(E, ddManager, manager, expressions, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex, indexToExpressionMap);
                 
                 // Create the appropriate expression.
                 auto expressionIt = indexToExpressionMap.find(Cudd_NodeReadIndex(dd));
diff --git a/src/storage/dd/cudd/InternalCuddBdd.h b/src/storage/dd/cudd/InternalCuddBdd.h
index 41ada0fe0..1556235ef 100644
--- a/src/storage/dd/cudd/InternalCuddBdd.h
+++ b/src/storage/dd/cudd/InternalCuddBdd.h
@@ -355,10 +355,9 @@ namespace storm {
              * @param manager The manager that is used to build the expression and, in particular, create new variables in.
              * @param indexToExpressionMap A mapping from indices (of DD variables) to expressions with which they are
              * to be replaced.
-             * @return A pair consisting of the created expressions and a mapping from pairs (i, j) to variables such
-             * that the i-th variable of level j is represented by the mapped-to variable.
+             * @return A list of expressions that is equivalent to the function represented by the BDD.
              */
-            std::pair<std::vector<storm::expressions::Expression>, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>> toExpression(storm::expressions::ExpressionManager& manager, std::unordered_map<uint_fast64_t, storm::expressions::Expression> const& indexToExpressionMap) const;
+            std::vector<storm::expressions::Expression> toExpression(storm::expressions::ExpressionManager& manager, std::unordered_map<uint_fast64_t, storm::expressions::Expression> const& indexToExpressionMap) const;
             
             /*!
              * Creates an ODD based on the current BDD.
@@ -465,8 +464,24 @@ namespace storm {
             template<typename ValueType>
             static void filterExplicitVectorRec(DdNode const* dd, cudd::Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd, std::vector<ValueType>& result, uint_fast64_t& currentIndex, std::vector<ValueType> const& values);
             
-            storm::expressions::Variable toExpressionRec(DdNode const* dd, storm::expressions::ExpressionManager& manager, std::vector<storm::expressions::Expression>& expressions, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map<DdNode const*, uint_fast64_t>& nodeToCounterMap, std::vector<uint_fast64_t>& nextCounterForIndex, std::unordered_map<uint_fast64_t, storm::expressions::Expression> const& indexToExpressionMap) const;
-            
+            /*!
+             * Creates a vector of expressions that represent the function of the given BDD node.
+             *
+             *
+             * @param dd The current node of the BDD.
+             * @param ddManager The manager responsible for the BDD.
+             * @param manager The expression manager over which to build the expressions.
+             * @param countIndexToVariablePair A mapping of (count, variable index) pairs to a pair of expression variables
+             * such that entry (i, j) is mapped to a variable that represents the i-th node labeled with variable j (counting
+             * from left to right).
+             * @param nodeToCounterMap A mapping from DD nodes to a number j such that the DD node was the j-th node
+             * visited with the same variable index as the given node.
+             * @param nextCounterForIndex A vector storing a mapping from variable indices to a counter that indicates
+             * how many nodes with the given variable index have been seen before.
+             * @param indexToExpressionMap A mapping of variable indices to the expressions they are to be replaced with.
+             */
+            static storm::expressions::Variable toExpressionRec(DdNode const* dd, cudd::Cudd const& ddManager, storm::expressions::ExpressionManager& manager, std::vector<storm::expressions::Expression>& expressions, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map<DdNode const*, uint_fast64_t>& nodeToCounterMap, std::vector<uint_fast64_t>& nextCounterForIndex, std::unordered_map<uint_fast64_t, storm::expressions::Expression> const& indexToExpressionMap);
+
             InternalDdManager<DdType::CUDD> const* ddManager;
             
             cudd::BDD cuddBdd;
diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storage/dd/sylvan/InternalSylvanBdd.cpp
index b3a981de7..421f6798e 100644
--- a/src/storage/dd/sylvan/InternalSylvanBdd.cpp
+++ b/src/storage/dd/sylvan/InternalSylvanBdd.cpp
@@ -389,8 +389,81 @@ namespace storm {
             }
         }
         
-        std::pair<std::vector<storm::expressions::Expression>, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>> InternalBdd<DdType::Sylvan>::toExpression(storm::expressions::ExpressionManager& manager, std::unordered_map<uint_fast64_t, storm::expressions::Expression> const& indexToExpressionMap) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Translating BDD to an expression is currently unsupported for sylvan.");
+        std::vector<storm::expressions::Expression> InternalBdd<DdType::Sylvan>::toExpression(storm::expressions::ExpressionManager& manager, std::unordered_map<uint_fast64_t, storm::expressions::Expression> const& indexToExpressionMap) const {
+            std::vector<storm::expressions::Expression> result;
+            
+            // Create (and maintain) a mapping from the DD nodes to a counter that says the how-many-th node (within the
+            // nodes of equal index) the node was.
+            std::unordered_map<BDD, uint_fast64_t> nodeToCounterMap;
+            std::vector<uint_fast64_t> nextCounterForIndex(ddManager->getNumberOfDdVariables(), 0);
+            std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable> countIndexToVariablePair;
+            
+            bool negated = bdd_isnegated(this->getSylvanBdd().GetBDD());
+            
+            // Translate from the top node downwards.
+            storm::expressions::Variable topVariable = this->toExpressionRec(bdd_regular(this->getSylvanBdd().GetBDD()), manager, result, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex, indexToExpressionMap);
+            
+            // Create the final expression.
+            if (negated) {
+                result.push_back(!topVariable);
+            } else {
+                result.push_back(topVariable);
+            }
+            
+            return result;
+        }
+        
+        storm::expressions::Variable InternalBdd<DdType::Sylvan>::toExpressionRec(BDD dd, storm::expressions::ExpressionManager& manager, std::vector<storm::expressions::Expression>& expressions, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map<BDD, uint_fast64_t>& nodeToCounterMap, std::vector<uint_fast64_t>& nextCounterForIndex, std::unordered_map<uint_fast64_t, storm::expressions::Expression> const& indexToExpressionMap) {
+            STORM_LOG_ASSERT(!bdd_isnegated(dd), "Expected non-negated BDD node.");
+            
+            // First, try to look up the current node if it's not a terminal node.
+            auto nodeCounterIt = nodeToCounterMap.find(dd);
+            if (nodeCounterIt != nodeToCounterMap.end()) {
+                // If we have found the node, this means we can look up the counter-index pair and get the corresponding variable.
+                auto variableIt = countIndexToVariablePair.find(std::make_pair(nodeCounterIt->second, sylvan_var(dd)));
+                STORM_LOG_ASSERT(variableIt != countIndexToVariablePair.end(), "Unable to find node.");
+                return variableIt->second;
+            }
+            
+            // If the node was not yet encountered, we create a variable and associate it with the appropriate expression.
+            storm::expressions::Variable newVariable = manager.declareFreshBooleanVariable();
+            
+            // Since we want to reuse the variable whenever possible, we insert the appropriate entries in the hash table.
+            if (!bdd_isterminal(dd)) {
+                // If we are dealing with a non-terminal node, we count it as a new node with this index.
+                nodeToCounterMap[dd] = nextCounterForIndex[sylvan_var(dd)];
+                countIndexToVariablePair[std::make_pair(nextCounterForIndex[sylvan_var(dd)], sylvan_var(dd))] = newVariable;
+                ++nextCounterForIndex[sylvan_var(dd)];
+            } else {
+                // If it's a terminal node, it is the one leaf and there's no need to keep track of a counter for this level.
+                nodeToCounterMap[dd] = 0;
+                countIndexToVariablePair[std::make_pair(0, sylvan_var(dd))] = newVariable;
+            }
+            
+            // In the terminal case, we can only have a one since we are considering non-negated nodes only.
+            if (bdd_isterminal(dd)) {
+                if (dd == sylvan_true) {
+                    expressions.push_back(storm::expressions::iff(manager.boolean(true), newVariable));
+                } else {
+                    expressions.push_back(storm::expressions::iff(manager.boolean(false), newVariable));
+                }
+            } else {
+                // In the non-terminal case, we recursively translate the children nodes and then construct and appropriate ite-expression.
+                BDD t = sylvan_high(dd);
+                BDD e = sylvan_low(dd);
+                BDD T = bdd_regular(t);
+                BDD E = bdd_regular(e);
+                storm::expressions::Variable thenVariable = toExpressionRec(T, manager, expressions, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex, indexToExpressionMap);
+                storm::expressions::Variable elseVariable = toExpressionRec(E, manager, expressions, countIndexToVariablePair, nodeToCounterMap, nextCounterForIndex, indexToExpressionMap);
+                
+                // Create the appropriate expression.
+                auto expressionIt = indexToExpressionMap.find(sylvan_var(dd));
+                STORM_LOG_ASSERT(expressionIt != indexToExpressionMap.end(), "Unable to find expression for variable index.");
+                expressions.push_back(storm::expressions::iff(newVariable, storm::expressions::ite(expressionIt->second, t == T ? thenVariable : !thenVariable, e == E ? elseVariable : !elseVariable)));
+            }
+            
+            // Return the variable for this node.
+            return newVariable;
         }
         
         template InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::fromVector(InternalDdManager<DdType::Sylvan> const* ddManager, std::vector<double> const& values, Odd const& odd, std::vector<uint_fast64_t> const& sortedDdVariableIndices, std::function<bool (double const&)> const& filter);
diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.h b/src/storage/dd/sylvan/InternalSylvanBdd.h
index 729cefd32..d0c781a1b 100644
--- a/src/storage/dd/sylvan/InternalSylvanBdd.h
+++ b/src/storage/dd/sylvan/InternalSylvanBdd.h
@@ -344,10 +344,9 @@ namespace storm {
              * @param manager The manager that is used to build the expression and, in particular, create new variables in.
              * @param indexToExpressionMap A mapping from indices (of DD variables) to expressions with which they are
              * to be replaced.
-             * @return A pair consisting of the created expressions and a mapping from pairs (i, j) to variables such
-             * that the i-th variable of level j is represented by the mapped-to variable.
+             * @return A list of expressions representing the function of the BDD.
              */
-            std::pair<std::vector<storm::expressions::Expression>, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>> toExpression(storm::expressions::ExpressionManager& manager, std::unordered_map<uint_fast64_t, storm::expressions::Expression> const& indexToExpressionMap) const;
+            std::vector<storm::expressions::Expression> toExpression(storm::expressions::ExpressionManager& manager, std::unordered_map<uint_fast64_t, storm::expressions::Expression> const& indexToExpressionMap) const;
             
             /*!
              * Creates an ODD based on the current BDD.
@@ -436,6 +435,23 @@ namespace storm {
             template<typename ValueType>
             static void filterExplicitVectorRec(BDD dd, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd, std::vector<ValueType>& result, uint_fast64_t& currentIndex, std::vector<ValueType> const& values);
             
+            /*!
+             * Creates a vector of expressions that represent the function of the given BDD node.
+             *
+             *
+             * @param dd The current node of the BDD.
+             * @param manager The expression manager over which to build the expressions.
+             * @param countIndexToVariablePair A mapping of (count, variable index) pairs to a pair of expression variables
+             * such that entry (i, j) is mapped to a variable that represents the i-th node labeled with variable j (counting
+             * from left to right).
+             * @param nodeToCounterMap A mapping from DD nodes to a number j such that the DD node was the j-th node
+             * visited with the same variable index as the given node.
+             * @param nextCounterForIndex A vector storing a mapping from variable indices to a counter that indicates
+             * how many nodes with the given variable index have been seen before.
+             * @param indexToExpressionMap A mapping of variable indices to the expressions they are to be replaced with.
+             */
+            static storm::expressions::Variable toExpressionRec(BDD dd, storm::expressions::ExpressionManager& manager, std::vector<storm::expressions::Expression>& expressions, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>& countIndexToVariablePair, std::unordered_map<BDD, uint_fast64_t>& nodeToCounterMap, std::vector<uint_fast64_t>& nextCounterForIndex, std::unordered_map<uint_fast64_t, storm::expressions::Expression> const& indexToExpressionMap);
+            
             /*!
              * Retrieves the sylvan BDD.
              *
diff --git a/test/functional/abstraction/PrismMenuGameTest.cpp b/test/functional/abstraction/PrismMenuGameTest.cpp
index f23949a8c..148bd6f25 100644
--- a/test/functional/abstraction/PrismMenuGameTest.cpp
+++ b/test/functional/abstraction/PrismMenuGameTest.cpp
@@ -16,7 +16,7 @@
 
 #include "src/utility/solver.h"
 
-TEST(PrismMenuGame, DieAbstractionTest) {
+TEST(PrismMenuGame, DieAbstractionTest_Cudd) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
 
     std::vector<storm::expressions::Expression> initialPredicates;
@@ -33,7 +33,24 @@ TEST(PrismMenuGame, DieAbstractionTest) {
     EXPECT_EQ(0, game.getBottomStates().getNonZeroCount());
 }
 
-TEST(PrismMenuGame, DieAbstractionAndRefinementTest) {
+TEST(PrismMenuGame, DieAbstractionTest_Sylvan) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    
+    std::vector<storm::expressions::Expression> initialPredicates;
+    storm::expressions::ExpressionManager& manager = program.getManager();
+    
+    initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3));
+    
+    storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
+    
+    EXPECT_EQ(10, game.getNumberOfTransitions());
+    EXPECT_EQ(2, game.getNumberOfStates());
+    EXPECT_EQ(0, game.getBottomStates().getNonZeroCount());
+}
+
+TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Cudd) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
     
     std::vector<storm::expressions::Expression> initialPredicates;
@@ -52,7 +69,26 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest) {
     EXPECT_EQ(0, game.getBottomStates().getNonZeroCount());
 }
 
-TEST(PrismMenuGame, DieFullAbstractionTest) {
+TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Sylvan) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    
+    std::vector<storm::expressions::Expression> initialPredicates;
+    storm::expressions::ExpressionManager& manager = program.getManager();
+    
+    initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3));
+    
+    storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("s") == manager.integer(7)}));
+    
+    storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
+    
+    EXPECT_EQ(10, game.getNumberOfTransitions());
+    EXPECT_EQ(3, game.getNumberOfStates());
+    EXPECT_EQ(0, game.getBottomStates().getNonZeroCount());
+}
+
+TEST(PrismMenuGame, DieFullAbstractionTest_Cudd) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
     
     std::vector<storm::expressions::Expression> initialPredicates;
@@ -84,7 +120,39 @@ TEST(PrismMenuGame, DieFullAbstractionTest) {
     EXPECT_EQ(0, game.getBottomStates().getNonZeroCount());
 }
 
-TEST(PrismMenuGame, CrowdsAbstractionTest) {
+TEST(PrismMenuGame, DieFullAbstractionTest_Sylvan) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    
+    std::vector<storm::expressions::Expression> initialPredicates;
+    storm::expressions::ExpressionManager& manager = program.getManager();
+    
+    initialPredicates.push_back(manager.getVariableExpression("s") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("s") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("s") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("s") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("s") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("s") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("s") == manager.integer(6));
+    initialPredicates.push_back(manager.getVariableExpression("s") == manager.integer(7));
+    
+    initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(6));
+    
+    storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
+    
+    EXPECT_EQ(20, game.getNumberOfTransitions());
+    EXPECT_EQ(13, game.getNumberOfStates());
+    EXPECT_EQ(0, game.getBottomStates().getNonZeroCount());
+}
+
+TEST(PrismMenuGame, CrowdsAbstractionTest_Cudd) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
     program = program.substituteConstants();
     
@@ -102,7 +170,25 @@ TEST(PrismMenuGame, CrowdsAbstractionTest) {
     EXPECT_EQ(1, game.getBottomStates().getNonZeroCount());
 }
 
-TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest) {
+TEST(PrismMenuGame, CrowdsAbstractionTest_Sylvan) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    program = program.substituteConstants();
+    
+    std::vector<storm::expressions::Expression> initialPredicates;
+    storm::expressions::ExpressionManager& manager = program.getManager();
+    
+    initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3));
+    
+    storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
+    
+    EXPECT_EQ(11, game.getNumberOfTransitions());
+    EXPECT_EQ(2, game.getNumberOfStates());
+    EXPECT_EQ(1, game.getBottomStates().getNonZeroCount());
+}
+
+TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Cudd) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
     program = program.substituteConstants();
     
@@ -122,7 +208,27 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest) {
     EXPECT_EQ(2, game.getBottomStates().getNonZeroCount());
 }
 
-TEST(PrismMenuGame, CrowdsFullAbstractionTest) {
+TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Sylvan) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    program = program.substituteConstants();
+    
+    std::vector<storm::expressions::Expression> initialPredicates;
+    storm::expressions::ExpressionManager& manager = program.getManager();
+    
+    initialPredicates.push_back(manager.getVariableExpression("phase") < manager.integer(3));
+    
+    storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("observe0") + manager.getVariableExpression("observe1") + manager.getVariableExpression("observe2") + manager.getVariableExpression("observe3") + manager.getVariableExpression("observe4") <= manager.getVariableExpression("runCount")}));
+    
+    storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
+    
+    EXPECT_EQ(28, game.getNumberOfTransitions());
+    EXPECT_EQ(4, game.getNumberOfStates());
+    EXPECT_EQ(2, game.getBottomStates().getNonZeroCount());
+}
+
+TEST(PrismMenuGame, CrowdsFullAbstractionTest_Cudd) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
     program = program.substituteConstants();
     
@@ -194,7 +300,79 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest) {
     EXPECT_EQ(1260, game.getBottomStates().getNonZeroCount());
 }
 
-TEST(PrismMenuGame, TwoDiceAbstractionTest) {
+TEST(PrismMenuGame, CrowdsFullAbstractionTest_Sylvan) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    program = program.substituteConstants();
+    
+    std::vector<storm::expressions::Expression> initialPredicates;
+    storm::expressions::ExpressionManager& manager = program.getManager();
+    
+    initialPredicates.push_back(manager.getVariableExpression("phase") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("phase") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("phase") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("phase") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("phase") == manager.integer(4));
+    
+    initialPredicates.push_back(manager.getVariableExpression("good"));
+    
+    initialPredicates.push_back(manager.getVariableExpression("runCount") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("runCount") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("runCount") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("runCount") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("runCount") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("runCount") == manager.integer(5));
+    
+    initialPredicates.push_back(manager.getVariableExpression("observe0") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("observe0") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("observe0") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("observe0") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("observe0") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("observe0") == manager.integer(5));
+    
+    initialPredicates.push_back(manager.getVariableExpression("observe1") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("observe1") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("observe1") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("observe1") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("observe1") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("observe1") == manager.integer(5));
+    
+    initialPredicates.push_back(manager.getVariableExpression("observe2") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("observe2") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("observe2") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("observe2") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("observe2") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("observe2") == manager.integer(5));
+    
+    initialPredicates.push_back(manager.getVariableExpression("observe3") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("observe3") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("observe3") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("observe3") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("observe3") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("observe3") == manager.integer(5));
+    
+    initialPredicates.push_back(manager.getVariableExpression("observe4") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("observe4") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("observe4") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("observe4") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("observe4") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("observe4") == manager.integer(5));
+    
+    initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(4));
+    
+    storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
+    
+    EXPECT_EQ(15113, game.getNumberOfTransitions());
+    EXPECT_EQ(8607, game.getNumberOfStates());
+    EXPECT_EQ(1260, game.getBottomStates().getNonZeroCount());
+}
+
+TEST(PrismMenuGame, TwoDiceAbstractionTest_Cudd) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
@@ -214,7 +392,27 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest) {
     EXPECT_EQ(0, game.getBottomStates().getNonZeroCount());
 }
 
-TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest) {
+TEST(PrismMenuGame, TwoDiceAbstractionTest_Sylvan) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    program = program.substituteConstants();
+    program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+    
+    std::vector<storm::expressions::Expression> initialPredicates;
+    storm::expressions::ExpressionManager& manager = program.getManager();
+    
+    initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0));
+    
+    storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
+    
+    EXPECT_EQ(34, game.getNumberOfTransitions());
+    EXPECT_EQ(4, game.getNumberOfStates());
+    EXPECT_EQ(0, game.getBottomStates().getNonZeroCount());
+}
+
+TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
@@ -236,7 +434,29 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest) {
     EXPECT_EQ(0, game.getBottomStates().getNonZeroCount());
 }
 
-TEST(PrismMenuGame, TwoDiceFullAbstractionTest) {
+TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    program = program.substituteConstants();
+    program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+    
+    std::vector<storm::expressions::Expression> initialPredicates;
+    storm::expressions::ExpressionManager& manager = program.getManager();
+    
+    initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0));
+    
+    storm::abstraction::prism::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("d1") + manager.getVariableExpression("d2") == manager.integer(7)}));
+    
+    storm::abstraction::MenuGame<storm::dd::DdType::CUDD, double> game = abstractProgram.getAbstractGame();
+    
+    EXPECT_EQ(164, game.getNumberOfTransitions());
+    EXPECT_EQ(8, game.getNumberOfStates());
+    EXPECT_EQ(0, game.getBottomStates().getNonZeroCount());
+}
+
+TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Cudd) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
@@ -287,7 +507,58 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest) {
     EXPECT_EQ(0, game.getBottomStates().getNonZeroCount());
 }
 
-TEST(PrismMenuGame, WlanAbstractionTest) {
+TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Sylvan) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    program = program.substituteConstants();
+    program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+    
+    std::vector<storm::expressions::Expression> initialPredicates;
+    storm::expressions::ExpressionManager& manager = program.getManager();
+    
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(6));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(7));
+    
+    initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(6));
+    
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(6));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(7));
+    
+    initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(6));
+    
+    storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
+    
+    EXPECT_EQ(436, game.getNumberOfTransitions());
+    EXPECT_EQ(169, game.getNumberOfStates());
+    EXPECT_EQ(0, game.getBottomStates().getNonZeroCount());
+}
+
+TEST(PrismMenuGame, WlanAbstractionTest_Cudd) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-4.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
@@ -308,7 +579,28 @@ TEST(PrismMenuGame, WlanAbstractionTest) {
     EXPECT_EQ(4, game.getBottomStates().getNonZeroCount());
 }
 
-TEST(PrismMenuGame, WlanAbstractionAndRefinementTest) {
+TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-4.nm");
+    program = program.substituteConstants();
+    program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+    
+    std::vector<storm::expressions::Expression> initialPredicates;
+    storm::expressions::ExpressionManager& manager = program.getManager();
+    
+    initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("c1") == manager.getVariableExpression("c2"));
+    
+    storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
+    
+    EXPECT_EQ(283, game.getNumberOfTransitions());
+    EXPECT_EQ(4, game.getNumberOfStates());
+    EXPECT_EQ(4, game.getBottomStates().getNonZeroCount());
+}
+
+TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-4.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
@@ -331,7 +623,30 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest) {
     EXPECT_EQ(8, game.getBottomStates().getNonZeroCount());
 }
 
-TEST(PrismMenuGame, WlanFullAbstractionTest) {
+TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-4.nm");
+    program = program.substituteConstants();
+    program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+    
+    std::vector<storm::expressions::Expression> initialPredicates;
+    storm::expressions::ExpressionManager& manager = program.getManager();
+    
+    initialPredicates.push_back(manager.getVariableExpression("s1") < manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("c1") == manager.getVariableExpression("c2"));
+    
+    storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("backoff1") < manager.integer(7)}));
+    
+    storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
+    
+    EXPECT_EQ(568, game.getNumberOfTransitions());
+    EXPECT_EQ(8, game.getNumberOfStates());
+    EXPECT_EQ(8, game.getBottomStates().getNonZeroCount());
+}
+
+TEST(PrismMenuGame, WlanFullAbstractionTest_Cudd) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-4.nm");
     program = program.substituteConstants();
     program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
@@ -450,4 +765,123 @@ TEST(PrismMenuGame, WlanFullAbstractionTest) {
     EXPECT_EQ(0, game.getBottomStates().getNonZeroCount());
 }
 
+TEST(PrismMenuGame, WlanFullAbstractionTest_Sylvan) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-4.nm");
+    program = program.substituteConstants();
+    program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+    
+    std::vector<storm::expressions::Expression> initialPredicates;
+    storm::expressions::ExpressionManager& manager = program.getManager();
+    
+    initialPredicates.push_back(manager.getVariableExpression("col") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("col") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("col") == manager.integer(2));
+    
+    initialPredicates.push_back(manager.getVariableExpression("c1") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("c1") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("c1") == manager.integer(2));
+    
+    initialPredicates.push_back(manager.getVariableExpression("c2") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("c2") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("c2") == manager.integer(2));
+    
+    initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(6));
+    initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(7));
+    
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(6));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(7));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(8));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(9));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(10));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(11));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(12));
+    
+    initialPredicates.push_back(manager.getVariableExpression("slot1") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("slot1") == manager.integer(1));
+    
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(6));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(7));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(8));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(9));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(10));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(11));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(12));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(13));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(14));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(15));
+    
+    initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(1));
+    
+    initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(6));
+    initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(7));
+    
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(6));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(7));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(8));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(9));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(10));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(11));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(12));
+    
+    initialPredicates.push_back(manager.getVariableExpression("slot2") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("slot2") == manager.integer(1));
+    
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(6));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(7));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(8));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(9));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(10));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(11));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(12));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(13));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(14));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(15));
+    
+    initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(1));
+    
+    storm::abstraction::prism::AbstractProgram<storm::dd::DdType::Sylvan, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    storm::abstraction::MenuGame<storm::dd::DdType::Sylvan, double> game = abstractProgram.getAbstractGame();
+    
+    EXPECT_EQ(9503, game.getNumberOfTransitions());
+    EXPECT_EQ(5523, game.getNumberOfStates());
+    EXPECT_EQ(0, game.getBottomStates().getNonZeroCount());
+}
+
 #endif
\ No newline at end of file
diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp
index cfbc9d8df..beea61e70 100644
--- a/test/functional/storage/CuddDdTest.cpp
+++ b/test/functional/storage/CuddDdTest.cpp
@@ -429,7 +429,7 @@ TEST(CuddDd, BddToExpressionTest) {
     indexToExpressionMap[2] = d;
     auto result = bdd.toExpression(*manager, indexToExpressionMap);
     
-    for (auto const& expression : result.first) {
+    for (auto const& expression : result) {
         std::cout << expression << std::endl;
     }
 }
\ No newline at end of file
diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp
index fdb60e5c0..025ce8227 100644
--- a/test/functional/storage/SylvanDdTest.cpp
+++ b/test/functional/storage/SylvanDdTest.cpp
@@ -411,4 +411,27 @@ TEST(SylvanDd, BddOddTest) {
     EXPECT_EQ(9ul, matrix.getRowGroupCount());
     EXPECT_EQ(9ul, matrix.getColumnCount());
     EXPECT_EQ(106ul, matrix.getNonzeroEntryCount());
+}
+
+TEST(SylvanDd, BddToExpressionTest) {
+    std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> ddManager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
+    std::pair<storm::expressions::Variable, storm::expressions::Variable> a = ddManager->addMetaVariable("a");
+    std::pair<storm::expressions::Variable, storm::expressions::Variable> b = ddManager->addMetaVariable("b");
+    
+    storm::dd::Bdd<storm::dd::DdType::Sylvan> bdd = ddManager->getBddOne();
+    bdd &= ddManager->getEncoding(a.first, 1);
+    bdd |= ddManager->getEncoding(b.first, 0);
+    
+    std::shared_ptr<storm::expressions::ExpressionManager> manager = std::make_shared<storm::expressions::ExpressionManager>();
+    storm::expressions::Variable c = manager->declareBooleanVariable("c");
+    storm::expressions::Variable d = manager->declareBooleanVariable("d");
+    
+    std::unordered_map<uint_fast64_t, storm::expressions::Expression> indexToExpressionMap;
+    indexToExpressionMap[0] = c;
+    indexToExpressionMap[2] = d;
+    auto result = bdd.toExpression(*manager, indexToExpressionMap);
+    
+    for (auto const& expression : result) {
+        std::cout << expression << std::endl;
+    }
 }
\ No newline at end of file