diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c
index 742dcffa9..0c6da75c9 100644
--- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c
+++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c
@@ -90,7 +90,7 @@ VOID_TASK_IMPL_1(mtbdd_gc_mark_rec, MDD, mtbdd)
     if (mtbdd == mtbdd_true) return;
     if (mtbdd == mtbdd_false) return;
 
-    if (llmsset_mark(nodes, mtbdd)) {
+    if (llmsset_mark(nodes, mtbdd&0x000000ffffffffff)) {
         mtbddnode_t n = GETNODE(mtbdd);
         if (!mtbddnode_isleaf(n)) {
             SPAWN(mtbdd_gc_mark_rec, mtbddnode_getlow(n));
diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index 0f636adfb..79616701c 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -347,7 +347,6 @@ namespace storm {
             std::set<storm::expressions::Variable> assignedGlobalVariables;
             std::set_intersection(assignedVariables.begin(), assignedVariables.end(), generationInfo.allGlobalVariables.begin(), generationInfo.allGlobalVariables.end(), std::inserter(assignedGlobalVariables, assignedGlobalVariables.begin()));
             
-            int index = 0;
             // All unassigned boolean variables need to keep their value.
             for (storm::prism::BooleanVariable const& booleanVariable : module.getBooleanVariables()) {
                 if (assignedVariables.find(booleanVariable.getExpressionVariable()) == assignedVariables.end()) {
diff --git a/src/models/symbolic/Model.h b/src/models/symbolic/Model.h
index 9115f3a25..3b8804ebe 100644
--- a/src/models/symbolic/Model.h
+++ b/src/models/symbolic/Model.h
@@ -49,12 +49,12 @@ namespace storm {
                 static const storm::dd::DdType DdType = Type;
                 typedef StandardRewardModel<Type, ValueType> RewardModelType;
                 
-                Model(Model<Type> const& other) = default;
-                Model& operator=(Model<Type> const& other) = default;
+                Model(Model<Type, ValueType> const& other) = default;
+                Model& operator=(Model<Type, ValueType> const& other) = default;
                 
 #ifndef WINDOWS
-                Model(Model<Type>&& other) = default;
-                Model& operator=(Model<Type>&& other) = default;
+                Model(Model<Type, ValueType>&& other) = default;
+                Model& operator=(Model<Type, ValueType>&& other) = default;
 #endif
                 
                 /*!
diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp
index 1c3495335..eba059635 100644
--- a/src/solver/Z3SmtSolver.cpp
+++ b/src/solver/Z3SmtSolver.cpp
@@ -323,7 +323,7 @@ namespace storm {
 
 		std::vector<storm::expressions::Expression> Z3SmtSolver::getUnsatAssumptions() {
 #ifdef STORM_HAVE_Z3
-            STORM_LOG_THROW(lastResult == SmtSolver::CheckResult::Unsat, storm::exceptions::InvalidStateException, "Unable to generate unsatisfiable core of assumptions, because the last check did not determine the formulas to be unsatisfiable.")
+            STORM_LOG_THROW(lastResult == SmtSolver::CheckResult::Unsat, storm::exceptions::InvalidStateException, "Unable to generate unsatisfiable core of assumptions, because the last check did not determine the formulas to be unsatisfiable.");
             STORM_LOG_THROW(lastCheckAssumptions, storm::exceptions::InvalidStateException, "Unable to generate unsatisfiable core of assumptions, because the last check did not involve assumptions.");
 
 			z3::expr_vector z3UnsatAssumptions = this->solver->unsat_core();
diff --git a/src/storage/dd/Add.h b/src/storage/dd/Add.h
index 5134044ec..b90f4f1b0 100644
--- a/src/storage/dd/Add.h
+++ b/src/storage/dd/Add.h
@@ -2,6 +2,7 @@
 #define STORM_STORAGE_DD_ADD_H_
 
 #include <map>
+#include <functional>
 
 #include "src/storage/dd/Dd.h"
 #include "src/storage/dd/DdType.h"
@@ -584,7 +585,8 @@ namespace storm {
              */
             AddIterator<LibraryType, ValueType> end(bool enumerateDontCareMetaVariables = true) const;
             
-            friend std::ostream & operator<<(std::ostream& out, const Add<LibraryType, ValueType>& add);
+            template<DdType LibraryTypePrime, typename ValueTypePrime>
+            friend std::ostream & operator<<(std::ostream& out, Add<LibraryTypePrime, ValueTypePrime> const& add);
             
             /*!
              * Converts the ADD to a BDD by mapping all values unequal to zero to 1. This effectively does the same as
diff --git a/src/storage/dd/Bdd.h b/src/storage/dd/Bdd.h
index a64cebf28..a9c9c906a 100644
--- a/src/storage/dd/Bdd.h
+++ b/src/storage/dd/Bdd.h
@@ -1,6 +1,8 @@
 #ifndef STORM_STORAGE_DD_BDD_H_
 #define STORM_STORAGE_DD_BDD_H_
 
+#include <functional>
+
 #include "src/storage/dd/Dd.h"
 #include "src/storage/dd/DdType.h"
 
diff --git a/src/storage/dd/Odd.h b/src/storage/dd/Odd.h
index 131785adf..a62fd5d74 100644
--- a/src/storage/dd/Odd.h
+++ b/src/storage/dd/Odd.h
@@ -3,6 +3,7 @@
 
 #include <vector>
 #include <map>
+#include <memory>
 
 namespace storm {
     namespace dd {
diff --git a/src/storage/dd/cudd/InternalCuddAdd.h b/src/storage/dd/cudd/InternalCuddAdd.h
index 63b176a0f..ddd153215 100644
--- a/src/storage/dd/cudd/InternalCuddAdd.h
+++ b/src/storage/dd/cudd/InternalCuddAdd.h
@@ -3,6 +3,8 @@
 
 #include <set>
 #include <unordered_map>
+#include <functional>
+#include <memory>
 
 #include "src/storage/dd/DdType.h"
 #include "src/storage/dd/InternalAdd.h"
diff --git a/src/storage/dd/cudd/InternalCuddBdd.h b/src/storage/dd/cudd/InternalCuddBdd.h
index b8c02da06..2855d71c1 100644
--- a/src/storage/dd/cudd/InternalCuddBdd.h
+++ b/src/storage/dd/cudd/InternalCuddBdd.h
@@ -3,6 +3,8 @@
 
 #include <set>
 #include <unordered_map>
+#include <functional>
+#include <memory>
 
 #include "src/storage/dd/DdType.h"
 #include "src/storage/dd/InternalBdd.h"
diff --git a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp
index c754887bb..77ed14982 100644
--- a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp
+++ b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp
@@ -19,7 +19,7 @@ namespace storm {
                 lace_init(0, 1000000);
                 lace_startup(0, 0, 0);
                 
-                sylvan::Sylvan::initPackage(1ull << 16, 1ull << 32, 1ull << 16, 1ull << 32);
+                sylvan::Sylvan::initPackage(1ull << 16, 1ull << 28, 1ul << 16, 1ull << 25);
                 sylvan::Sylvan::initBdd(1);
                 sylvan::Sylvan::initMtbdd();
             }