diff --git a/src/builder/DftSmtBuilder.cpp b/src/builder/DftSmtBuilder.cpp
index 1d60b2c74..c1226531c 100644
--- a/src/builder/DftSmtBuilder.cpp
+++ b/src/builder/DftSmtBuilder.cpp
@@ -1,4 +1,4 @@
-#include "src/builder/DFTSMTBuilder.h"
+#include "src/builder/DftSmtBuilder.h"
 #include "src/exceptions/NotImplementedException.h"
 
 namespace storm {
diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp
index 51061050e..fb0c0b1e6 100644
--- a/src/storm-dyftee.cpp
+++ b/src/storm-dyftee.cpp
@@ -117,6 +117,7 @@ int main(const int argc, const char** argv) {
         parametric = generalSettings.isParametricSet();
 #endif
         
+#ifdef STORM_HAVE_Z3
         if (dftSettings.solveWithSMT()) {
             // Solve with SMT
             if (parametric) {
@@ -127,6 +128,7 @@ int main(const int argc, const char** argv) {
             storm::utility::cleanUp();
             return 0;
         }
+#endif
         
         // Set min or max
         bool minimal = true;