diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp
index d57dec2e7..f5296a487 100644
--- a/src/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/builder/ExplicitDFTModelBuilder.cpp
@@ -15,7 +15,7 @@ namespace storm {
         }
         
         template <typename ValueType>
-        ExplicitDFTModelBuilder<ValueType>::ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries) : mDft(dft), mStates(((mDft.stateVectorSize() / 64) + 1) * 64, INITIAL_BUCKETSIZE) {
+        ExplicitDFTModelBuilder<ValueType>::ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : mDft(dft), mStates(((mDft.stateVectorSize() / 64) + 1) * 64, INITIAL_BUCKETSIZE), enableDC(enableDC) {
             // stateVectorSize is bound for size of bitvector
 
             mStateGenerationInfo = std::make_shared<storm::storage::DFTStateGenerationInfo>(mDft.buildStateGenerationInfo(symmetries));
@@ -218,7 +218,7 @@ namespace storm {
                         next->checkFailsafe(*newState, queues);
                     }
 
-                    while (!queues.dontCarePropagationDone()) {
+                    while (enableDC && !queues.dontCarePropagationDone()) {
                         DFTElementPointer next = queues.nextDontCarePropagation();
                         next->checkDontCareAnymore(*newState, queues);
                     }
diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h
index 7fc343be2..4f1dff514 100644
--- a/src/builder/ExplicitDFTModelBuilder.h
+++ b/src/builder/ExplicitDFTModelBuilder.h
@@ -55,6 +55,7 @@ namespace storm {
             std::vector<std::pair<uint_fast64_t, storm::storage::BitVector>> mPseudoStatesMapping; // vector of (id to concrete state, bitvector)
             size_t newIndex = 0;
             bool mergeFailedStates = true;
+            bool enableDC = true;
             size_t failedIndex = 0;
             size_t initialStateIndex = 0;
 
@@ -65,7 +66,7 @@ namespace storm {
                 std::set<std::string> beLabels = {};
             };
             
-            ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries);
+            ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC);
 
             std::shared_ptr<storm::models::sparse::Model<ValueType>> buildModel(LabelOptions const& labelOpts);
 
diff --git a/src/modelchecker/DFTAnalyser.h b/src/modelchecker/DFTAnalyser.h
index de128af64..0058f41f0 100644
--- a/src/modelchecker/DFTAnalyser.h
+++ b/src/modelchecker/DFTAnalyser.h
@@ -21,7 +21,7 @@ class DFTAnalyser {
     std::chrono::duration<double> totalTime = std::chrono::duration<double>::zero();
     ValueType checkResult = storm::utility::zero<ValueType>();
 public:
-    void check(storm::storage::DFT<ValueType> dft , std::shared_ptr<const storm::logic::Formula> const& formula, bool symred = true, bool allowModularisation = true) {
+    void check(storm::storage::DFT<ValueType> dft , std::shared_ptr<const storm::logic::Formula> const& formula, bool symred = true, bool allowModularisation = true, bool enableDC = true) {
         
         // Building DFT
         std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
@@ -30,7 +30,7 @@ public:
         // Optimizing DFT
         dft = dft.optimize();
         std::vector<storm::storage::DFT<ValueType>> dfts;
-        checkResult = checkHelper(dft, formula, symred, allowModularisation);
+        checkResult = checkHelper(dft, formula, symred, allowModularisation, enableDC);
         totalTime = std::chrono::high_resolution_clock::now() - totalStart;
             
         
@@ -38,7 +38,7 @@ public:
     }
     
 private:
-    ValueType checkHelper(storm::storage::DFT<ValueType> const& dft , std::shared_ptr<const storm::logic::Formula> const& formula, bool symred = true, bool allowModularisation = true)  {
+    ValueType checkHelper(storm::storage::DFT<ValueType> const& dft , std::shared_ptr<const storm::logic::Formula> const& formula, bool symred = true, bool allowModularisation = true, bool enableDC = true)  {
         std::cout << "check helper called" << std::endl;
         bool invResults = false;
         std::vector<storm::storage::DFT<ValueType>> dfts = {dft};
@@ -82,7 +82,7 @@ private:
         } 
         if(res.empty()) {
             // Model based modularisation.
-            auto const& models = buildMarkovModels(dfts, formula, symred);
+            auto const& models = buildMarkovModels(dfts, formula, symred, enableDC);
 
 
             for (auto const& model : models) {
@@ -132,7 +132,7 @@ private:
     }
     
     
-    std::vector<std::shared_ptr<storm::models::sparse::Model<ValueType>>> buildMarkovModels(std::vector<storm::storage::DFT<ValueType>> const&  dfts,   std::shared_ptr<const storm::logic::Formula> const& formula, bool symred) {
+    std::vector<std::shared_ptr<storm::models::sparse::Model<ValueType>>> buildMarkovModels(std::vector<storm::storage::DFT<ValueType>> const&  dfts,   std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool enableDC) {
         std::vector<std::shared_ptr<storm::models::sparse::Model<ValueType>>> models;
         for(auto& dft : dfts) {
             std::chrono::high_resolution_clock::time_point buildingStart = std::chrono::high_resolution_clock::now();
@@ -150,7 +150,7 @@ private:
             
             // Building Markov Automaton
             std::cout << "Building Model..." << std::endl;
-            storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries);
+            storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
             typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
             std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.buildModel(labeloptions);
             //model->printModelInformationToStream(std::cout);
diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp
index f280bbebf..ea0da3a14 100644
--- a/src/storm-dyftee.cpp
+++ b/src/storm-dyftee.cpp
@@ -11,7 +11,7 @@
  * @param property PCTC formula capturing the property to check.
  */
 template <typename ValueType>
-void analyzeDFT(std::string filename, std::string property, bool symred = false, bool allowModularisation = false) {
+void analyzeDFT(std::string filename, std::string property, bool symred = false, bool allowModularisation = false, bool enableDC = true) {
     storm::settings::SettingsManager& manager = storm::settings::mutableManager();
     manager.setFromString("");
 
@@ -22,7 +22,7 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false,
     assert(formulas.size() == 1);
     
     DFTAnalyser<ValueType> analyser;
-    analyser.check(dft, formulas[0], symred, allowModularisation);
+    analyser.check(dft, formulas[0], symred, allowModularisation, enableDC);
     analyser.printTimings();
     analyser.printResult();
 }
@@ -47,6 +47,7 @@ int main(int argc, char** argv) {
     bool minimal = true;
     bool allowModular = true;
     bool enableModularisation = false;
+    bool disableDC = false;
     std::string filename = argv[1];
     std::string operatorType = "";
     std::string targetFormula = "";
@@ -92,6 +93,8 @@ int main(int argc, char** argv) {
             symred = true;
         } else if (option == "--modularisation") {
             enableModularisation = true;
+        } else if (option == "--disabledc") {
+            disableDC = true;
         } else if (option == "--min") {
             minimal = true;
         } else if (option == "--max") {
@@ -114,8 +117,8 @@ int main(int argc, char** argv) {
     std::cout << "Running " << (parametric ? "parametric " : "") << "DFT analysis on file " << filename << " with property " << pctlFormula << std::endl;
 
     if (parametric) {
-        analyzeDFT<storm::RationalFunction>(filename, pctlFormula, symred, allowModular && enableModularisation );
+        analyzeDFT<storm::RationalFunction>(filename, pctlFormula, symred, allowModular && enableModularisation, !disableDC );
     } else {
-        analyzeDFT<double>(filename, pctlFormula, symred, allowModular && enableModularisation);
+        analyzeDFT<double>(filename, pctlFormula, symred, allowModular && enableModularisation, !disableDC);
     }
 }