diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 665c16847..80f7bd9b7 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -3,4 +3,6 @@ add_subdirectory(storm-pgcl)
 add_subdirectory(storm-pgcl-cli)
 add_subdirectory(storm-gspn)
 add_subdirectory(storm-gspn-cli)
+add_subdirectory(storm-dft)
+add_subdirectory(storm-dft-cli)
 add_subdirectory(test)
diff --git a/src/storm-dft-cli/CMakeLists.txt b/src/storm-dft-cli/CMakeLists.txt
new file mode 100644
index 000000000..f44c57103
--- /dev/null
+++ b/src/storm-dft-cli/CMakeLists.txt
@@ -0,0 +1,4 @@
+# Create storm-dft.
+add_executable(storm-dft-cli ${PROJECT_SOURCE_DIR}/src/storm-dft-cli/storm-dyftee.cpp)
+target_link_libraries(storm-dft-cli storm-dft) # Adding headers for xcode
+set_target_properties(storm-dft-cli PROPERTIES OUTPUT_NAME "storm-dft")
\ No newline at end of file
diff --git a/src/storm/settings/modules/DFTSettings.cpp b/src/storm-dft-cli/settings/modules/DFTSettings.cpp
similarity index 100%
rename from src/storm/settings/modules/DFTSettings.cpp
rename to src/storm-dft-cli/settings/modules/DFTSettings.cpp
diff --git a/src/storm/settings/modules/DFTSettings.h b/src/storm-dft-cli/settings/modules/DFTSettings.h
similarity index 100%
rename from src/storm/settings/modules/DFTSettings.h
rename to src/storm-dft-cli/settings/modules/DFTSettings.h
diff --git a/src/storm/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp
similarity index 98%
rename from src/storm/storm-dyftee.cpp
rename to src/storm-dft-cli/storm-dyftee.cpp
index e7e3002aa..03aa1cab8 100644
--- a/src/storm/storm-dyftee.cpp
+++ b/src/storm-dft-cli/storm-dyftee.cpp
@@ -1,14 +1,14 @@
 #include "storm/logic/Formula.h"
 #include "storm/utility/initialize.h"
 #include "storm/utility/storm.h"
-#include "storm/parser/DFTGalileoParser.h"
-#include "storm/modelchecker/dft/DFTModelChecker.h"
+#include "storm-dft/parser/DFTGalileoParser.h"
+#include "storm-dft/modelchecker/dft/DFTModelChecker.h"
 
-#include "storm/modelchecker/dft/DFTASFChecker.h"
+#include "storm-dft/modelchecker/dft/DFTASFChecker.h"
 #include "storm/cli/cli.h"
 #include "storm/exceptions/BaseException.h"
 #include "storm/utility/macros.h"
-#include "storm/builder/DftSmtBuilder.h"
+#include "storm-dft/builder/DftSmtBuilder.h"
 
 
 #include "storm/settings/modules/GeneralSettings.h"
diff --git a/src/storm-dft/CMakeLists.txt b/src/storm-dft/CMakeLists.txt
new file mode 100644
index 000000000..df0c067e0
--- /dev/null
+++ b/src/storm-dft/CMakeLists.txt
@@ -0,0 +1,13 @@
+file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-dft/*.h ${PROJECT_SOURCE_DIR}/src/storm-dft/*.cpp)
+
+register_source_groups_from_filestructure("${ALL_FILES}" storm-dft)
+
+
+
+file(GLOB_RECURSE STORM_DFT_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-dft/*/*.cpp)
+file(GLOB_RECURSE STORM_DFT_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-dft/*/*.h)
+
+
+# Create storm-pgcl.
+add_library(storm-dft SHARED ${STORM_DFT_SOURCES} ${STORM_DFT_HEADERS})
+target_link_libraries(storm-dft storm ${STORM_DFT_LINK_LIBRARIES})
diff --git a/src/storm/builder/DftExplorationHeuristic.cpp b/src/storm-dft/builder/DftExplorationHeuristic.cpp
similarity index 98%
rename from src/storm/builder/DftExplorationHeuristic.cpp
rename to src/storm-dft/builder/DftExplorationHeuristic.cpp
index 9662c48ba..0bcbd98ae 100644
--- a/src/storm/builder/DftExplorationHeuristic.cpp
+++ b/src/storm-dft/builder/DftExplorationHeuristic.cpp
@@ -1,4 +1,5 @@
-#include "storm/builder/DftExplorationHeuristic.h"
+#include "DftExplorationHeuristic.h"
+
 #include "storm/adapters/CarlAdapter.h"
 #include "storm/utility/macros.h"
 #include "storm/utility/constants.h"
diff --git a/src/storm/builder/DftExplorationHeuristic.h b/src/storm-dft/builder/DftExplorationHeuristic.h
similarity index 97%
rename from src/storm/builder/DftExplorationHeuristic.h
rename to src/storm-dft/builder/DftExplorationHeuristic.h
index af8aef4a1..874cfb586 100644
--- a/src/storm/builder/DftExplorationHeuristic.h
+++ b/src/storm-dft/builder/DftExplorationHeuristic.h
@@ -1,6 +1,4 @@
-#ifndef STORM_BUILDER_DFTEXPLORATIONHEURISTIC_H_
-#define STORM_BUILDER_DFTEXPLORATIONHEURISTIC_H_
-
+#pragma once
 #include <memory>
 
 namespace storm {
@@ -186,5 +184,3 @@ namespace storm {
 
     }
 }
-
-#endif /* STORM_BUILDER_DFTEXPLORATIONHEURISTIC_H_ */
diff --git a/src/storm/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
similarity index 99%
rename from src/storm/builder/ExplicitDFTModelBuilder.cpp
rename to src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
index de261ce2a..bdee4eedc 100644
--- a/src/storm/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
@@ -1,12 +1,16 @@
-#include "storm/builder/ExplicitDFTModelBuilder.h"
+#include "ExplicitDFTModelBuilder.h"
+
+#include <map>
+
 #include "storm/models/sparse/MarkovAutomaton.h"
 #include "storm/models/sparse/Ctmc.h"
 #include "storm/utility/constants.h"
 #include "storm/utility/vector.h"
 #include "storm/exceptions/UnexpectedException.h"
-#include "storm/settings/modules/DFTSettings.h"
 #include "storm/settings/SettingsManager.h"
-#include <map>
+
+#include "storm-dft/settings/modules/DFTSettings.h"
+
 
 namespace storm {
     namespace builder {
diff --git a/src/storm/builder/ExplicitDFTModelBuilder.h b/src/storm-dft/builder/ExplicitDFTModelBuilder.h
similarity index 95%
rename from src/storm/builder/ExplicitDFTModelBuilder.h
rename to src/storm-dft/builder/ExplicitDFTModelBuilder.h
index f79ee5b2f..d3d191a8a 100644
--- a/src/storm/builder/ExplicitDFTModelBuilder.h
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.h
@@ -1,17 +1,23 @@
-#ifndef EXPLICITDFTMODELBUILDER_H
-#define	EXPLICITDFTMODELBUILDER_H
+#pragma  once
+
+#include <boost/container/flat_set.hpp>
+#include <boost/optional/optional.hpp>
+#include <stack>
+#include <unordered_set>
+
 
 #include "storm/models/sparse/StateLabeling.h"
 #include "storm/models/sparse/StandardRewardModel.h"
 #include "storm/models/sparse/Model.h"
 #include "storm/storage/SparseMatrix.h"
 #include "storm/storage/BitVectorHashMap.h"
-#include "storm/storage/dft/DFT.h"
-#include "storm/storage/dft/SymmetricUnits.h"
-#include <boost/container/flat_set.hpp>
-#include <boost/optional/optional.hpp>
-#include <stack>
-#include <unordered_set>
+
+#include "storm-dft/storage/dft/DFT.h"
+#include "storm-dft/storage/dft/SymmetricUnits.h"
+
+
+
+
 
 namespace storm {
     namespace builder {
@@ -93,5 +99,3 @@ namespace storm {
         };
     }
 }
-
-#endif	/* EXPLICITDFTMODELBUILDER_H */
diff --git a/src/storm/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
similarity index 99%
rename from src/storm/builder/ExplicitDFTModelBuilderApprox.cpp
rename to src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
index 0581ecc12..194372a30 100644
--- a/src/storm/builder/ExplicitDFTModelBuilderApprox.cpp
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
@@ -1,13 +1,17 @@
-#include "storm/builder/ExplicitDFTModelBuilderApprox.h"
+#include "ExplicitDFTModelBuilderApprox.h"
+
+#include <map>
+
 #include "storm/models/sparse/MarkovAutomaton.h"
 #include "storm/models/sparse/Ctmc.h"
 #include "storm/utility/constants.h"
 #include "storm/utility/vector.h"
 #include "storm/utility/bitoperations.h"
 #include "storm/exceptions/UnexpectedException.h"
-#include "storm/settings/modules/DFTSettings.h"
 #include "storm/settings/SettingsManager.h"
-#include <map>
+
+#include "storm-dft/settings/modules/DFTSettings.h"
+
 
 namespace storm {
     namespace builder {
diff --git a/src/storm/builder/ExplicitDFTModelBuilderApprox.h b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h
similarity index 97%
rename from src/storm/builder/ExplicitDFTModelBuilderApprox.h
rename to src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h
index 3533d077f..52bcbf2c9 100644
--- a/src/storm/builder/ExplicitDFTModelBuilderApprox.h
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h
@@ -1,22 +1,23 @@
-#ifndef EXPLICITDFTMODELBUILDERAPPROX_H
-#define	EXPLICITDFTMODELBUILDERAPPROX_H
+#pragma once
 
-#include "storm/builder/DftExplorationHeuristic.h"
-#include "storm/models/sparse/StateLabeling.h"
-#include "storm/models/sparse/StandardRewardModel.h"
-#include "storm/models/sparse/Model.h"
-#include "storm/generator/DftNextStateGenerator.h"
-#include "storm/storage/SparseMatrix.h"
-#include "storm/storage/sparse/StateStorage.h"
-#include "storm/storage/dft/DFT.h"
-#include "storm/storage/dft/SymmetricUnits.h"
-#include "storm/storage/BucketPriorityQueue.h"
 #include <boost/container/flat_set.hpp>
 #include <boost/optional/optional.hpp>
 #include <stack>
 #include <unordered_set>
 #include <limits>
 
+#include "storm/models/sparse/StateLabeling.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/models/sparse/Model.h"
+#include "storm/storage/SparseMatrix.h"
+#include "storm/storage/sparse/StateStorage.h"
+
+#include "storm-dft/builder/DftExplorationHeuristic.h"
+#include "storm-dft/generator/DftNextStateGenerator.h"
+#include "storm-dft/storage/dft/DFT.h"
+#include "storm-dft/storage/dft/SymmetricUnits.h"
+#include "storm-dft/storage/BucketPriorityQueue.h"
+
 namespace storm {
     namespace builder {
 
@@ -331,5 +332,3 @@ namespace storm {
 
     }
 }
-
-#endif	/* EXPLICITDFTMODELBUILDERAPPROX_H */
diff --git a/src/storm/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp
similarity index 99%
rename from src/storm/generator/DftNextStateGenerator.cpp
rename to src/storm-dft/generator/DftNextStateGenerator.cpp
index 023bcd85a..3f1361f93 100644
--- a/src/storm/generator/DftNextStateGenerator.cpp
+++ b/src/storm-dft/generator/DftNextStateGenerator.cpp
@@ -1,4 +1,4 @@
-#include "storm/generator/DftNextStateGenerator.h"
+#include "DftNextStateGenerator.h"
 
 #include "storm/utility/constants.h"
 #include "storm/utility/macros.h"
diff --git a/src/storm/generator/DftNextStateGenerator.h b/src/storm-dft/generator/DftNextStateGenerator.h
similarity index 93%
rename from src/storm/generator/DftNextStateGenerator.h
rename to src/storm-dft/generator/DftNextStateGenerator.h
index fa8295a4f..2f614afe6 100644
--- a/src/storm/generator/DftNextStateGenerator.h
+++ b/src/storm-dft/generator/DftNextStateGenerator.h
@@ -1,11 +1,11 @@
-#ifndef STORM_GENERATOR_DFTNEXTSTATEGENERATOR_H_
-#define STORM_GENERATOR_DFTNEXTSTATEGENERATOR_H_
+#pragma once
 
 #include "storm/generator/NextStateGenerator.h"
-#include "storm/storage/dft/DFT.h"
-
 #include "storm/utility/ConstantsComparator.h"
 
+#include "storm-dft/storage/dft/DFT.h"
+
+
 namespace storm {
     namespace generator {
         
@@ -69,5 +69,3 @@ namespace storm {
         
     }
 }
-
-#endif /* STORM_GENERATOR_DFTNEXTSTATEGENERATOR_H_ */
diff --git a/src/storm/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
similarity index 100%
rename from src/storm/modelchecker/dft/DFTASFChecker.cpp
rename to src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
diff --git a/src/storm/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h
similarity index 97%
rename from src/storm/modelchecker/dft/DFTASFChecker.h
rename to src/storm-dft/modelchecker/dft/DFTASFChecker.h
index 6e7d31e79..c4a47116d 100644
--- a/src/storm/modelchecker/dft/DFTASFChecker.h
+++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h
@@ -3,7 +3,8 @@
 #include <string>
 #include <vector>
 #include <unordered_map>
-#include "storm/storage/dft/DFT.h"
+
+#include "storm-dft/storage/dft/DFT.h"
 
 
 namespace storm {
diff --git a/src/storm/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
similarity index 99%
rename from src/storm/modelchecker/dft/DFTModelChecker.cpp
rename to src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index 39a3966c8..584d1edca 100644
--- a/src/storm/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
@@ -1,12 +1,13 @@
-#include "storm/modelchecker/dft/DFTModelChecker.h"
+#include "DFTModelChecker.h"
 
-#include "storm/builder/ExplicitDFTModelBuilder.h"
-#include "storm/builder/ExplicitDFTModelBuilderApprox.h"
 #include "storm/builder/ParallelCompositionBuilder.h"
-#include "storm/storage/dft/DFTIsomorphism.h"
 #include "storm/settings/modules/DFTSettings.h"
 #include "storm/utility/bitoperations.h"
 
+#include "storm-dft/builder/ExplicitDFTModelBuilder.h"
+#include "storm-dft/builder/ExplicitDFTModelBuilderApprox.h"
+#include "storm-dft/storage/dft/DFTIsomorphism.h"
+
 namespace storm {
     namespace modelchecker {
 
diff --git a/src/storm/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h
similarity index 97%
rename from src/storm/modelchecker/dft/DFTModelChecker.h
rename to src/storm-dft/modelchecker/dft/DFTModelChecker.h
index 1637c50ac..7cee7b0e4 100644
--- a/src/storm/modelchecker/dft/DFTModelChecker.h
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h
@@ -1,9 +1,10 @@
-#ifndef STORM_MODELCHECKER_DFT_DFTMODELCHECKER_H_
+#pragma  once
 
 #include "storm/logic/Formula.h"
 #include "storm/modelchecker/results/CheckResult.h"
-#include "storm/storage/dft/DFT.h"
-#include "storm/utility/storm.h"
+#include "storm/utility/storm.h" // TODO this should not be included here.
+
+#include "storm-dft/storage/dft/DFT.h"
 
 #include <chrono>
 
@@ -136,5 +137,4 @@ namespace storm {
 
         };
     }
-}
-#endif /* STORM_MODELCHECKER_DFT_DFTMODELCHECKER_H_ */
+}
\ No newline at end of file
diff --git a/src/storm/parser/DFTGalileoParser.cpp b/src/storm-dft/parser/DFTGalileoParser.cpp
similarity index 100%
rename from src/storm/parser/DFTGalileoParser.cpp
rename to src/storm-dft/parser/DFTGalileoParser.cpp
diff --git a/src/storm/parser/DFTGalileoParser.h b/src/storm-dft/parser/DFTGalileoParser.h
similarity index 87%
rename from src/storm/parser/DFTGalileoParser.h
rename to src/storm-dft/parser/DFTGalileoParser.h
index 51cb54c0a..3f19683ff 100644
--- a/src/storm/parser/DFTGalileoParser.h
+++ b/src/storm-dft/parser/DFTGalileoParser.h
@@ -1,13 +1,14 @@
-#ifndef DFTGALILEOPARSER_H
-#define	DFTGALILEOPARSER_H
+#pragma  once
+
+#include <map>
 
-#include "storm/storage/dft/DFT.h"
-#include "storm/storage/dft/DFTBuilder.h"
 #include "storm/storage/expressions/ExpressionManager.h"
 #include "storm/parser/ExpressionParser.h"
 #include "storm/storage/expressions/ExpressionEvaluator.h"
 
-#include <map>
+#include "storm-dft/storage/dft/DFT.h"
+#include "storm-dft/storage/dft/DFTBuilder.h"
+
 
 namespace storm {
     namespace parser {
@@ -39,6 +40,3 @@ namespace storm {
         };
     }
 }
-
-#endif	/* DFTGALILEOPARSER_H */
-
diff --git a/src/storm/storage/BucketPriorityQueue.cpp b/src/storm-dft/storage/BucketPriorityQueue.cpp
similarity index 99%
rename from src/storm/storage/BucketPriorityQueue.cpp
rename to src/storm-dft/storage/BucketPriorityQueue.cpp
index 96a06e74a..89d7c7cce 100644
--- a/src/storm/storage/BucketPriorityQueue.cpp
+++ b/src/storm-dft/storage/BucketPriorityQueue.cpp
@@ -1,4 +1,4 @@
-#include "storm/storage/BucketPriorityQueue.h"
+#include "BucketPriorityQueue.h"
 #include "storm/utility/macros.h"
 #include "storm/adapters/CarlAdapter.h"
 
diff --git a/src/storm/storage/BucketPriorityQueue.h b/src/storm-dft/storage/BucketPriorityQueue.h
similarity index 89%
rename from src/storm/storage/BucketPriorityQueue.h
rename to src/storm-dft/storage/BucketPriorityQueue.h
index d11ba150d..a332311a7 100644
--- a/src/storm/storage/BucketPriorityQueue.h
+++ b/src/storm-dft/storage/BucketPriorityQueue.h
@@ -1,12 +1,12 @@
-#ifndef STORM_STORAGE_BUCKETPRIORITYQUEUE_H_
-#define STORM_STORAGE_BUCKETPRIORITYQUEUE_H_
+#pragma once
 
-#include "storm/builder/DftExplorationHeuristic.h"
 #include <algorithm>
 #include <functional>
 #include <unordered_map>
 #include <vector>
 
+#include "storm-dft/builder/DftExplorationHeuristic.h"
+
 namespace storm {
     namespace storage {
 
@@ -69,5 +69,3 @@ namespace storm {
 
     }
 }
-
-#endif // STORM_STORAGE_BUCKETPRIORITYQUEUE_H_
diff --git a/src/storm/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp
similarity index 99%
rename from src/storm/storage/dft/DFT.cpp
rename to src/storm-dft/storage/dft/DFT.cpp
index d118ba75e..8f19119a2 100644
--- a/src/storm/storage/dft/DFT.cpp
+++ b/src/storm-dft/storage/dft/DFT.cpp
@@ -1,13 +1,15 @@
-#include <boost/container/flat_set.hpp>
+#include "DFT.h"
 
+#include <boost/container/flat_set.hpp>
 #include <map>
-#include "DFT.h"
-#include "DFTBuilder.h"
+
 #include "storm/exceptions/NotSupportedException.h"
+#include "storm/utility/iota_n.h"
+#include "storm/utility/vector.h"
+
+#include "storm-dft/storage/dft/DFTBuilder.h"
+#include "storm-dft/storage/dft/DFTIsomorphism.h"
 
-#include "DFTIsomorphism.h"
-#include "utility/iota_n.h"
-#include "utility/vector.h"
 
 namespace storm {
     namespace storage {
diff --git a/src/storm/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h
similarity index 97%
rename from src/storm/storage/dft/DFT.h
rename to src/storm-dft/storage/dft/DFT.h
index 4b54391f2..9ef232a65 100644
--- a/src/storm/storage/dft/DFT.h
+++ b/src/storm-dft/storage/dft/DFT.h
@@ -1,6 +1,4 @@
-
-#ifndef DFT_H
-#define	DFT_H
+#pragma  once
 
 #include <memory>
 #include <unordered_map>
@@ -10,13 +8,14 @@
 
 #include <boost/iterator/counting_iterator.hpp>
 
-#include "DFTElements.h"
-#include "elements/DFTRestriction.h"
-#include "../BitVector.h"
-#include "SymmetricUnits.h"
-#include "../../utility/math.h"
+#include "storm/storage/BitVector.h"
+#include "storm/utility/math.h"
 #include "storm/utility/macros.h"
-#include "DFTStateGenerationInfo.h"
+
+#include "storm-dft/storage/dft/DFTElements.h"
+#include "storm-dft/storage/dft/SymmetricUnits.h"
+#include "storm-dft/storage/dft/DFTStateGenerationInfo.h"
+
 
 namespace storm {
     namespace storage {
@@ -38,8 +37,6 @@ namespace storm {
         
         template<typename T> class DFTBuilder;
 
-        
-        
 
         /**
          * Represents a Dynamic Fault Tree
@@ -281,5 +278,3 @@ namespace storm {
        
     }
 }
-#endif	/* DFT_H */
-
diff --git a/src/storm/storage/dft/DFTBuilder.cpp b/src/storm-dft/storage/dft/DFTBuilder.cpp
similarity index 98%
rename from src/storm/storage/dft/DFTBuilder.cpp
rename to src/storm-dft/storage/dft/DFTBuilder.cpp
index 4e6e53944..612008226 100644
--- a/src/storm/storage/dft/DFTBuilder.cpp
+++ b/src/storm-dft/storage/dft/DFTBuilder.cpp
@@ -1,14 +1,13 @@
-
-
 #include "DFTBuilder.h"
 
 #include <algorithm>
 
-#include "DFT.h"
-#include "OrderDFTElementsById.h"
 #include "storm/utility/macros.h"
 #include "storm/exceptions/NotSupportedException.h"
-#include "../../exceptions/WrongFormatException.h"
+#include "storm/exceptions/WrongFormatException.h"
+
+#include "storm-dft/storage/dft/DFT.h"
+#include "storm-dft/storage/dft/OrderDFTElementsById.h"
 
 
 namespace storm {
diff --git a/src/storm/storage/dft/DFTBuilder.h b/src/storm-dft/storage/dft/DFTBuilder.h
similarity index 98%
rename from src/storm/storage/dft/DFTBuilder.h
rename to src/storm-dft/storage/dft/DFTBuilder.h
index 3964079ff..f9a11d52b 100644
--- a/src/storm/storage/dft/DFTBuilder.h
+++ b/src/storm-dft/storage/dft/DFTBuilder.h
@@ -1,14 +1,14 @@
-
-#ifndef DFTBUILDER_H
-#define	DFTBUILDER_H
-
-#include "DFTElements.h"
-#include "elements/DFTRestriction.h"
+#pragma  once
 #include <iostream>
 #include <unordered_map>
 #include <map>
+
 #include "storm/utility/macros.h"
 
+#include "storm-dft/storage/dft/DFTElements.h"
+#include "storm-dft/storage/dft/elements/DFTRestriction.h"
+
+
 namespace storm {
     namespace storage {
         template<typename ValueType>
@@ -190,8 +190,3 @@ namespace storm {
         };
     }
 }
-
-
-
-#endif	/* DFTBUILDER_H */
-
diff --git a/src/storm/storage/dft/DFTElementState.h b/src/storm-dft/storage/dft/DFTElementState.h
similarity index 96%
rename from src/storm/storage/dft/DFTElementState.h
rename to src/storm-dft/storage/dft/DFTElementState.h
index 8fc30e32b..4eab014f7 100644
--- a/src/storm/storage/dft/DFTElementState.h
+++ b/src/storm-dft/storage/dft/DFTElementState.h
@@ -1,6 +1,4 @@
-
-#ifndef DFTELEMENTSTATE_H
-#define	DFTELEMENTSTATE_H
+#pragma once
 
 #include "storm/utility/macros.h"
 
@@ -77,6 +75,3 @@ namespace storm {
     }
 }
 
-
-#endif	/* DFTELEMENTSTATE_H */
-
diff --git a/src/storm/storage/dft/DFTElementType.h b/src/storm-dft/storage/dft/DFTElementType.h
similarity index 97%
rename from src/storm/storage/dft/DFTElementType.h
rename to src/storm-dft/storage/dft/DFTElementType.h
index ddd339c0a..800da161f 100644
--- a/src/storm/storage/dft/DFTElementType.h
+++ b/src/storm-dft/storage/dft/DFTElementType.h
@@ -1,5 +1,4 @@
-#ifndef DFTELEMENTTYPE_H
-#define DFTELEMENTTYPE_H
+#pragma  once
 
 #include "storm/utility/macros.h"
 
@@ -83,5 +82,3 @@ namespace storm {
         
     }
 }
-
-#endif	/* DFTELEMENTTYPE_H */
diff --git a/src/storm-dft/storage/dft/DFTElements.h b/src/storm-dft/storage/dft/DFTElements.h
new file mode 100644
index 000000000..8cbfec680
--- /dev/null
+++ b/src/storm-dft/storage/dft/DFTElements.h
@@ -0,0 +1,12 @@
+#pragma once
+
+#include "storm-dft/storage/dft/elements/DFTAnd.h"
+#include "storm-dft/storage/dft/elements/DFTBE.h"
+#include "storm-dft/storage/dft/elements/DFTConst.h"
+#include "storm-dft/storage/dft/elements/DFTDependency.h"
+#include "storm-dft/storage/dft/elements/DFTOr.h"
+#include "storm-dft/storage/dft/elements/DFTPand.h"
+#include "storm-dft/storage/dft/elements/DFTPor.h"
+#include "storm-dft/storage/dft/elements/DFTRestriction.h"
+#include "storm-dft/storage/dft/elements/DFTSpare.h"
+#include "storm-dft/storage/dft/elements/DFTVot.h"
diff --git a/src/storm/storage/dft/DFTIsomorphism.h b/src/storm-dft/storage/dft/DFTIsomorphism.h
similarity index 99%
rename from src/storm/storage/dft/DFTIsomorphism.h
rename to src/storm-dft/storage/dft/DFTIsomorphism.h
index 1f66e5449..86625c975 100644
--- a/src/storm/storage/dft/DFTIsomorphism.h
+++ b/src/storm-dft/storage/dft/DFTIsomorphism.h
@@ -3,9 +3,10 @@
 #include <vector>
 #include <unordered_map>
 #include <utility>
-#include "DFTElementType.h"
-#include "DFTElements.h"
-#include "DFT.h"
+
+#include "storm-dft/storage/dft/DFTElementType.h"
+#include "storm-dft/storage/dft/DFTElements.h"
+#include "storm-dft/storage/dft/DFT.h"
 
 namespace storm {
 namespace storage {
diff --git a/src/storm/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp
similarity index 99%
rename from src/storm/storage/dft/DFTState.cpp
rename to src/storm-dft/storage/dft/DFTState.cpp
index cc0eaabec..78c0937d8 100644
--- a/src/storm/storage/dft/DFTState.cpp
+++ b/src/storm-dft/storage/dft/DFTState.cpp
@@ -1,6 +1,6 @@
 #include "DFTState.h"
-#include "DFTElements.h"
-#include "DFT.h"
+#include "storm-dft/storage/dft/DFTElements.h"
+#include "storm-dft/storage/dft/DFT.h"
 
 namespace storm {
     namespace storage {
diff --git a/src/storm/storage/dft/DFTState.h b/src/storm-dft/storage/dft/DFTState.h
similarity index 98%
rename from src/storm/storage/dft/DFTState.h
rename to src/storm-dft/storage/dft/DFTState.h
index 7b73d2ce7..4dfcf3a13 100644
--- a/src/storm/storage/dft/DFTState.h
+++ b/src/storm-dft/storage/dft/DFTState.h
@@ -1,13 +1,13 @@
-#ifndef DFTSTATE_H
-#define	DFTSTATE_H
-
-#include "storm/storage/dft/DFTElementState.h"
-#include "storm/storage/BitVector.h"
-#include "storm/builder/DftExplorationHeuristic.h"
+#pragma once
 
 #include <sstream>
 #include <memory>
 
+#include "storm/storage/BitVector.h"
+
+#include "storm-dft/storage/dft/DFTElementState.h"
+#include "storm-dft/builder/DftExplorationHeuristic.h"
+
 namespace storm {
     namespace storage {
 
@@ -306,5 +306,3 @@ namespace std {
     };
 }
 
-#endif	/* DFTSTATE_H */
-
diff --git a/src/storm/storage/dft/DFTStateGenerationInfo.h b/src/storm-dft/storage/dft/DFTStateGenerationInfo.h
similarity index 100%
rename from src/storm/storage/dft/DFTStateGenerationInfo.h
rename to src/storm-dft/storage/dft/DFTStateGenerationInfo.h
diff --git a/src/storm/storage/dft/DFTStateSpaceGenerationQueues.h b/src/storm-dft/storage/dft/DFTStateSpaceGenerationQueues.h
similarity index 95%
rename from src/storm/storage/dft/DFTStateSpaceGenerationQueues.h
rename to src/storm-dft/storage/dft/DFTStateSpaceGenerationQueues.h
index bd71b5fbf..a969cc83b 100644
--- a/src/storm/storage/dft/DFTStateSpaceGenerationQueues.h
+++ b/src/storm-dft/storage/dft/DFTStateSpaceGenerationQueues.h
@@ -1,12 +1,11 @@
-#ifndef DFTSTATESPACEGENERATIONQUEUES_H
-#define	DFTSTATESPACEGENERATIONQUEUES_H
+#pragma once
 
 #include <list>
 #include <queue>
 #include <vector>
 #include <deque>
 
-#include "OrderDFTElementsById.h"
+#include "storm-dft/storage/dft/OrderDFTElementsById.h"
 
 namespace storm {
     namespace storage {
@@ -99,7 +98,4 @@ namespace storm {
         };
 
     }
-}
-
-#endif	/* DFTSTATESPACEGENERATIONQUEUES_H */
-
+}
\ No newline at end of file
diff --git a/src/storm/storage/dft/DFTUnit.h b/src/storm-dft/storage/dft/DFTUnit.h
similarity index 83%
rename from src/storm/storage/dft/DFTUnit.h
rename to src/storm-dft/storage/dft/DFTUnit.h
index 5e179f091..6af505770 100644
--- a/src/storm/storage/dft/DFTUnit.h
+++ b/src/storm-dft/storage/dft/DFTUnit.h
@@ -1,7 +1,6 @@
-#ifndef DFTUNIT_H
-#define	DFTUNIT_H
+#pragma once
 
-#include "../BitVector.h"
+#include "storm/storage/BitVector.h"
 
 namespace storm {
     namespace storage {
diff --git a/src/storm/storage/dft/OrderDFTElementsById.cpp b/src/storm-dft/storage/dft/OrderDFTElementsById.cpp
similarity index 95%
rename from src/storm/storage/dft/OrderDFTElementsById.cpp
rename to src/storm-dft/storage/dft/OrderDFTElementsById.cpp
index 6c9493bee..8812eb763 100644
--- a/src/storm/storage/dft/OrderDFTElementsById.cpp
+++ b/src/storm-dft/storage/dft/OrderDFTElementsById.cpp
@@ -1,5 +1,5 @@
 #include "OrderDFTElementsById.h"
-#include "DFTElements.h"
+#include "storm-dft/storage/dft/DFTElements.h"
 
 namespace storm {
     namespace storage {
diff --git a/src/storm/storage/dft/OrderDFTElementsById.h b/src/storm-dft/storage/dft/OrderDFTElementsById.h
similarity index 89%
rename from src/storm/storage/dft/OrderDFTElementsById.h
rename to src/storm-dft/storage/dft/OrderDFTElementsById.h
index 821a2de45..d73a1ae2e 100644
--- a/src/storm/storage/dft/OrderDFTElementsById.h
+++ b/src/storm-dft/storage/dft/OrderDFTElementsById.h
@@ -1,6 +1,4 @@
-#ifndef ORDERDFTELEMENTS_H
-#define	ORDERDFTELEMENTS_H
-
+#pragma  once
 #include <memory>
 
 namespace storm {
@@ -25,6 +23,3 @@ namespace storm {
 
     }
 }
-
-#endif	/* ORDERDFTELEMENTSBYID_H */
-
diff --git a/src/storm/storage/dft/SymmetricUnits.h b/src/storm-dft/storage/dft/SymmetricUnits.h
similarity index 100%
rename from src/storm/storage/dft/SymmetricUnits.h
rename to src/storm-dft/storage/dft/SymmetricUnits.h
diff --git a/src/storm/storage/dft/elements/DFTAnd.h b/src/storm-dft/storage/dft/elements/DFTAnd.h
similarity index 100%
rename from src/storm/storage/dft/elements/DFTAnd.h
rename to src/storm-dft/storage/dft/elements/DFTAnd.h
diff --git a/src/storm/storage/dft/elements/DFTBE.h b/src/storm-dft/storage/dft/elements/DFTBE.h
similarity index 100%
rename from src/storm/storage/dft/elements/DFTBE.h
rename to src/storm-dft/storage/dft/elements/DFTBE.h
diff --git a/src/storm/storage/dft/elements/DFTConst.h b/src/storm-dft/storage/dft/elements/DFTConst.h
similarity index 100%
rename from src/storm/storage/dft/elements/DFTConst.h
rename to src/storm-dft/storage/dft/elements/DFTConst.h
diff --git a/src/storm/storage/dft/elements/DFTDependency.h b/src/storm-dft/storage/dft/elements/DFTDependency.h
similarity index 100%
rename from src/storm/storage/dft/elements/DFTDependency.h
rename to src/storm-dft/storage/dft/elements/DFTDependency.h
diff --git a/src/storm/storage/dft/elements/DFTElement.cpp b/src/storm-dft/storage/dft/elements/DFTElement.cpp
similarity index 100%
rename from src/storm/storage/dft/elements/DFTElement.cpp
rename to src/storm-dft/storage/dft/elements/DFTElement.cpp
diff --git a/src/storm/storage/dft/elements/DFTElement.h b/src/storm-dft/storage/dft/elements/DFTElement.h
similarity index 100%
rename from src/storm/storage/dft/elements/DFTElement.h
rename to src/storm-dft/storage/dft/elements/DFTElement.h
diff --git a/src/storm/storage/dft/elements/DFTGate.h b/src/storm-dft/storage/dft/elements/DFTGate.h
similarity index 100%
rename from src/storm/storage/dft/elements/DFTGate.h
rename to src/storm-dft/storage/dft/elements/DFTGate.h
diff --git a/src/storm/storage/dft/elements/DFTOr.h b/src/storm-dft/storage/dft/elements/DFTOr.h
similarity index 100%
rename from src/storm/storage/dft/elements/DFTOr.h
rename to src/storm-dft/storage/dft/elements/DFTOr.h
diff --git a/src/storm/storage/dft/elements/DFTPand.h b/src/storm-dft/storage/dft/elements/DFTPand.h
similarity index 100%
rename from src/storm/storage/dft/elements/DFTPand.h
rename to src/storm-dft/storage/dft/elements/DFTPand.h
diff --git a/src/storm/storage/dft/elements/DFTPor.h b/src/storm-dft/storage/dft/elements/DFTPor.h
similarity index 100%
rename from src/storm/storage/dft/elements/DFTPor.h
rename to src/storm-dft/storage/dft/elements/DFTPor.h
diff --git a/src/storm/storage/dft/elements/DFTRestriction.h b/src/storm-dft/storage/dft/elements/DFTRestriction.h
similarity index 100%
rename from src/storm/storage/dft/elements/DFTRestriction.h
rename to src/storm-dft/storage/dft/elements/DFTRestriction.h
diff --git a/src/storm/storage/dft/elements/DFTSpare.h b/src/storm-dft/storage/dft/elements/DFTSpare.h
similarity index 100%
rename from src/storm/storage/dft/elements/DFTSpare.h
rename to src/storm-dft/storage/dft/elements/DFTSpare.h
diff --git a/src/storm/storage/dft/elements/DFTVot.h b/src/storm-dft/storage/dft/elements/DFTVot.h
similarity index 100%
rename from src/storm/storage/dft/elements/DFTVot.h
rename to src/storm-dft/storage/dft/elements/DFTVot.h
diff --git a/src/storm/CMakeLists.txt b/src/storm/CMakeLists.txt
index 91b2abd53..f0d64ab0c 100644
--- a/src/storm/CMakeLists.txt
+++ b/src/storm/CMakeLists.txt
@@ -10,7 +10,6 @@ register_source_groups_from_filestructure("${ALL_FILES}" storm)
 file(GLOB_RECURSE STORM_HEADERS ${PROJECT_SOURCE_DIR}/src/storm/*.h)
 file(GLOB_RECURSE STORM_SOURCES_WITHOUT_MAIN ${PROJECT_SOURCE_DIR}/src/storm/*/*.cpp)
 file(GLOB_RECURSE STORM_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm/storm.cpp)
-file(GLOB_RECURSE STORM_DFT_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm/storm-dyftee.cpp)
 
 # Additional include files like the storm-config.h
 file(GLOB_RECURSE STORM_BUILD_HEADERS ${PROJECT_BINARY_DIR}/include/*.h)
@@ -18,7 +17,6 @@ file(GLOB_RECURSE STORM_BUILD_HEADERS ${PROJECT_BINARY_DIR}/include/*.h)
 set(STORM_LIB_SOURCES ${STORM_SOURCES_WITHOUT_MAIN})
 set(STORM_LIB_HEADERS ${STORM_HEADERS})
 set(STORM_MAIN_SOURCES  ${STORM_MAIN_FILE})
-set(STORM_DFT_MAIN_SOURCES ${STORM_DFT_MAIN_FILE})
 
 # Add custom additional include or link directories
 if (ADDITIONAL_INCLUDE_DIRS)
@@ -48,10 +46,6 @@ add_executable(storm-main ${STORM_MAIN_SOURCES} ${STORM_MAIN_HEADERS})
 target_link_libraries(storm-main storm)
 set_target_properties(storm-main PROPERTIES OUTPUT_NAME "storm")
 
-# Create storm-dft.
-add_executable(storm-dft-main ${STORM_DFT_MAIN_SOURCES} ${STORM_MAIN_HEADERS})
-target_link_libraries(storm-dft-main storm) # Adding headers for xcode
-set_target_properties(storm-dft-main PROPERTIES OUTPUT_NAME "storm-dft")
 
 # Install storm headers to include directory.
 foreach(HEADER ${STORM_LIB_HEADERS})
diff --git a/src/storm/builder/DftSmtBuilder.cpp b/src/storm/builder/DftSmtBuilder.cpp
deleted file mode 100644
index 198f71ebf..000000000
--- a/src/storm/builder/DftSmtBuilder.cpp
+++ /dev/null
@@ -1,120 +0,0 @@
-#include "storm/builder/DftSmtBuilder.h"
-#include "storm/exceptions/NotImplementedException.h"
-
-namespace storm {
-    namespace builder {
-
-        template <typename ValueType>
-        DFTSMTBuilder<ValueType>::DFTSMTBuilder() : manager(std::make_shared<storm::expressions::ExpressionManager>()) {
-            solver = storm::utility::solver::SmtSolverFactory().create(*manager);
-        }
-
-        template <typename ValueType>
-        void DFTSMTBuilder<ValueType>::convertToSMT(storm::storage::DFT<ValueType> const& dft) {
-            std::cout << "Convert DFT to SMT" << std::endl;
-            timeMax = manager->integer(dft.nrBasicElements());
-            timeFailSafe = manager->integer(dft.nrBasicElements() + 1);
-            timeZero = manager->integer(0);
-            
-            // Convert all elements
-            for (size_t i = 0; i < dft.nrElements(); ++i) {
-                std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = dft.getElement(i);
-                std::cout << "Consider " << element->toString() << std::endl;
-                if (element->isBasicElement()) {
-                    storm::expressions::Variable varBE = convert(std::static_pointer_cast<storm::storage::DFTBE<ValueType> const>(element));
-                    varsBE.push_back(varBE);
-                } else if (element->isGate()) {
-                    storm::expressions::Variable varGate = convert(std::static_pointer_cast<storm::storage::DFTGate<ValueType> const>(element));
-                    if (dft.getTopLevelIndex() == i) {
-                        topLevel = varGate;
-                    }
-                } else if (element->isDependency()) {
-                    convert(std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(element));
-                } else if (element->isRestriction()) {
-                    convert(std::static_pointer_cast<storm::storage::DFTRestriction<ValueType> const>(element));
-                }
-            }
-            
-            // No simultaneous fails can occur
-            for (size_t i = 0; i < varsBE.size() - 1; ++i) {
-                storm::expressions::Expression be = varsBE[i];
-                for (size_t j = i + 1; j < varsBE.size(); ++j) {
-                    storm::expressions::Expression assertion = be != varsBE[j];
-                    solver->add(assertion);
-                }
-            }
-            
-            // For every time-point one BE must fail
-            for (size_t time = 1; time <= dft.nrBasicElements(); ++time) {
-                storm::expressions::Expression exprTime = manager->integer(time);
-                storm::expressions::Expression assertion = varsBE[0] == exprTime;
-                for (size_t i = 1; i < varsBE.size(); ++i) {
-                    assertion = assertion || varsBE[i] == exprTime;
-                }
-                assertion = assertion || topLevel <= exprTime;
-                solver->add(assertion);
-            }
-            
-        }
-        
-        template <typename ValueType>
-        storm::expressions::Variable DFTSMTBuilder<ValueType>::convert(std::shared_ptr<storm::storage::DFTBE<ValueType> const> const& be) {
-            storm::expressions::Variable var = manager->declareIntegerVariable(be->name());
-            storm::expressions::Expression assertion = timeZero < var && var < timeFailSafe;
-            solver->add(assertion);
-            return var;
-        }
-        
-        template <typename ValueType>
-        storm::expressions::Variable DFTSMTBuilder<ValueType>::convert(std::shared_ptr<storm::storage::DFTGate<ValueType> const> const& gate) {
-            storm::expressions::Variable var = manager->declareIntegerVariable(gate->name());
-            storm::expressions::Expression assertion = timeZero < var && var <= timeFailSafe;
-            solver->add(assertion);
-            return var;
-        }
-        
-        template <typename ValueType>
-        storm::expressions::Variable DFTSMTBuilder<ValueType>::convert(std::shared_ptr<storm::storage::DFTDependency<ValueType> const> const& dependency) {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The dependency cannot be converted into SMT.");
-        }
-        
-        template <typename ValueType>
-        storm::expressions::Variable DFTSMTBuilder<ValueType>::convert(std::shared_ptr<storm::storage::DFTRestriction<ValueType> const> const& restriction) {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The restriction cannot be converted into SMT.");
-        }
-
-        template <typename ValueType>
-        bool DFTSMTBuilder<ValueType>::check() const {
-            std::cout << "Check" << std::endl;
-            storm::solver::SmtSolver::CheckResult result = solver->check();
-            switch (result) {
-                case solver::SmtSolver::CheckResult::Sat:
-                {
-                    std::cout << "SAT with model:" << std::endl;
-                    std::shared_ptr<storm::solver::SmtSolver::ModelReference> model = solver->getModel();
-                    for (auto const& pair : *manager) {
-                        std::cout << pair.first.getName() << "->" << model->getIntegerValue(pair.first) << std::endl;
-                    }
-                    return true;
-                }
-                case solver::SmtSolver::CheckResult::Unsat:
-                    return false;
-                case solver::SmtSolver::CheckResult::Unknown:
-                default:
-                    STORM_LOG_ASSERT(false, "Result is unknown.");
-                    return false;
-            }
-        }
-        
-
-        // Explicitly instantiate the class.
-        template class DFTSMTBuilder<double>;
-
-#ifdef STORM_HAVE_CARL
-        template class DFTSMTBuilder<storm::RationalFunction>;
-#endif
-
-    } // namespace builder
-} // namespace storm
-
-
diff --git a/src/storm/builder/DftSmtBuilder.h b/src/storm/builder/DftSmtBuilder.h
deleted file mode 100644
index 158a62f33..000000000
--- a/src/storm/builder/DftSmtBuilder.h
+++ /dev/null
@@ -1,49 +0,0 @@
-#ifndef DFTSMTBUILDER_H
-#define	DFTSMTBUILDER_H
-
-#include "storm/solver/SmtSolver.h"
-#include "storm/utility/solver.h"
-#include "storm/storage/dft/DFT.h"
-
-namespace storm {
-    namespace builder {
-
-        template<typename ValueType>
-        class DFTSMTBuilder {
-
-        public:
-            DFTSMTBuilder();
-            
-            void convertToSMT(storm::storage::DFT<ValueType> const& dft);
-            
-            bool check() const;
-
-        private:
-            
-            std::shared_ptr<storm::solver::SmtSolver> solver;
-            
-            std::shared_ptr<storm::expressions::ExpressionManager> manager;
-            
-            storm::expressions::Expression timeMax;
-            
-            storm::expressions::Expression timeFailSafe;
-            
-            storm::expressions::Expression timeZero;
-            
-            storm::expressions::Expression topLevel;
-            
-            std::vector<storm::expressions::Variable> varsBE;
-
-            storm::expressions::Variable convert(std::shared_ptr<storm::storage::DFTBE<ValueType> const> const& be);
-
-            storm::expressions::Variable convert(std::shared_ptr<storm::storage::DFTGate<ValueType> const> const& gate);
-            
-            storm::expressions::Variable convert(std::shared_ptr<storm::storage::DFTDependency<ValueType> const> const& dependency);
-            
-            storm::expressions::Variable convert(std::shared_ptr<storm::storage::DFTRestriction<ValueType> const> const& restriction);
-
-        };
-    }
-}
-
-#endif	/* DFTSMTBUILDER_H */
diff --git a/src/storm/storage/dft/DFTElements.h b/src/storm/storage/dft/DFTElements.h
deleted file mode 100644
index d65403403..000000000
--- a/src/storm/storage/dft/DFTElements.h
+++ /dev/null
@@ -1,12 +0,0 @@
-#pragma once
-
-#include "elements/DFTAnd.h"
-#include "elements/DFTBE.h"
-#include "elements/DFTConst.h"
-#include "elements/DFTDependency.h"
-#include "elements/DFTOr.h"
-#include "elements/DFTPand.h"
-#include "elements/DFTPor.h"
-#include "elements/DFTRestriction.h"
-#include "elements/DFTSpare.h"
-#include "elements/DFTVot.h"
diff --git a/src/storm/utility/math.h b/src/storm/utility/math.h
index 850c137a9..499cb2ac8 100644
--- a/src/storm/utility/math.h
+++ b/src/storm/utility/math.h
@@ -3,6 +3,7 @@
 
 #include <cmath>
 
+#include "storm/utility/macros.h"
 #include "storm/utility/OsDetection.h"
 
 namespace storm {