From 628331fda3ae2ca30ae6413b51c83e4d61abbbca Mon Sep 17 00:00:00 2001
From: Alexander Bork <alexander.bork@rwth-aachen.de>
Date: Wed, 7 Aug 2019 16:30:21 +0200
Subject: [PATCH] Fixed error that SMT solver was always used in the FDEP
 conflict search

---
 src/storm-dft-cli/storm-dft.cpp | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp
index 1cc9a02e2..34bd53b69 100644
--- a/src/storm-dft-cli/storm-dft.cpp
+++ b/src/storm-dft-cli/storm-dft.cpp
@@ -117,13 +117,17 @@ void processOptions() {
                                         "Lower bound: " << std::to_string(preResults.lowerBEBound) << std::endl <<
                                         "Upper bound: " << std::to_string(preResults.upperBEBound) << std::endl);
 
-    preResults.fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true,
+    preResults.fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, useSMT,
                                                                                                solverTimeout);
 
-    STORM_LOG_DEBUG("========================================" << std::endl <<
-                                                               "FDEP CONFLICTS" << std::endl <<
-                                                               "========================================"
-                                                               << std::endl);
+    if (preResults.fdepConflicts.empty()) {
+        STORM_LOG_DEBUG("No FDEP conflicts found" << std::endl);
+    } else {
+        STORM_LOG_DEBUG("========================================" << std::endl <<
+                                                                   "FDEP CONFLICTS" << std::endl <<
+                                                                   "========================================"
+                                                                   << std::endl);
+    }
     for (auto pair: preResults.fdepConflicts) {
         STORM_LOG_DEBUG("Conflict between " << dft->getElement(pair.first)->name() << " and "
                                             << dft->getElement(pair.second)->name() << std::endl);