diff --git a/src/storm-dft/modelchecker/DFTModelChecker.cpp b/src/storm-dft/modelchecker/DFTModelChecker.cpp
index e1aeb628d..67025a472 100644
--- a/src/storm-dft/modelchecker/DFTModelChecker.cpp
+++ b/src/storm-dft/modelchecker/DFTModelChecker.cpp
@@ -3,12 +3,10 @@
 #include "storm-dft/api/storm-dft.h"
 #include "storm-dft/builder/ExplicitDFTModelBuilder.h"
 #include "storm-dft/settings/modules/DftIOSettings.h"
-#include "storm-dft/settings/modules/FaultTreeSettings.h"
 #include "storm-dft/utility/SymmetryFinder.h"
 #include "storm/adapters/RationalFunctionAdapter.h"
 #include "storm/builder/ParallelCompositionBuilder.h"
 #include "storm/exceptions/InvalidModelException.h"
-#include "storm/io/DirectEncodingExporter.h"
 #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 #include "storm/models/ModelType.h"
@@ -299,14 +297,7 @@ typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::che
         STORM_LOG_TRACE("Symmetries: \n" << symmetries);
     }
 
-    auto const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
-    ValueType const precision = std::is_same<ValueType, storm::RationalFunction>::value
-                                    ? storm::utility::zero<ValueType>()
-                                    : storm::utility::convertNumber<ValueType>(generalSettings.getPrecision());
     if (approximationError > 0.0) {
-        // Comparator for checking the error of the approximation
-        storm::utility::ConstantsComparator<ValueType> comparator(precision);
-
         // Build approximate Markov Automata for lower and upper bound
         approximation_result approxResult = std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
         std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
@@ -356,7 +347,7 @@ typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::che
             // Check lower bounds
             newResult = checkModel(model, {property});
             STORM_LOG_ASSERT(newResult.size() == 1, "Wrong size for result vector.");
-            STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(newResult[0], approxResult.first),
+            STORM_LOG_ASSERT(iteration == 0 || storm::utility::isNonNegative(newResult[0] - approxResult.first),
                              "New under-approximation " << newResult[0] << " is smaller than old result " << approxResult.first);
             approxResult.first = newResult[0];
 
@@ -368,11 +359,11 @@ typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::che
             // Check upper bound
             newResult = checkModel(model, {property});
             STORM_LOG_ASSERT(newResult.size() == 1, "Wrong size for result vector.");
-            STORM_LOG_ASSERT(iteration == 0 || !comparator.isLess(approxResult.second, newResult[0]),
+            STORM_LOG_ASSERT(iteration == 0 || storm::utility::isNonNegative(approxResult.second - newResult[0]),
                              "New over-approximation " << newResult[0] << " is greater than old result " << approxResult.second);
             approxResult.second = newResult[0];
 
-            STORM_LOG_ASSERT(comparator.isLess(approxResult.first, approxResult.second) || comparator.isEqual(approxResult.first, approxResult.second),
+            STORM_LOG_ASSERT(storm::utility::isNonNegative(approxResult.second - approxResult.first),
                              "Under-approximation " << approxResult.first << " is greater than over-approximation " << approxResult.second);
             totalTimer.stop();
             if (printInfo && dftIOSettings.isShowDftStatisticsSet()) {
@@ -398,7 +389,6 @@ typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::che
         return results;
     } else {
         // Build a single Markov Automaton
-        auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
         STORM_LOG_DEBUG("Building Model...");
         storm::dft::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries);
         builder.buildModel(0, 0.0);
diff --git a/src/storm-dft/modelchecker/DFTModelChecker.h b/src/storm-dft/modelchecker/DFTModelChecker.h
index a78318ca6..4bb6e2ce5 100644
--- a/src/storm-dft/modelchecker/DFTModelChecker.h
+++ b/src/storm-dft/modelchecker/DFTModelChecker.h
@@ -1,13 +1,11 @@
 #pragma once
 
+#include "storm-dft/storage/DFT.h"
+#include "storm-dft/utility/RelevantEvents.h"
 #include "storm/api/storm.h"
 #include "storm/logic/Formula.h"
-#include "storm/modelchecker/results/CheckResult.h"
 #include "storm/utility/Stopwatch.h"
 
-#include "storm-dft/storage/DFT.h"
-#include "storm-dft/utility/RelevantEvents.h"
-
 namespace storm::dft {
 namespace modelchecker {
 
@@ -48,9 +46,9 @@ class DFTModelChecker {
      * @param allowDCForRelevant Whether to allow Don't Care propagation for relevant events
      * @param approximationError Error allowed for approximation. Value 0 indicates no approximation.
      * @param approximationHeuristic Heuristic used for state space exploration.
-     * @param eliminateChains If true, chains of non-Markovian states are elimianted from the resulting MA
+     * @param eliminateChains If true, chains of non-Markovian states are eliminated from the resulting MA
      * @param labelBehavior Behavior of labels of eliminated states
-     * @return Model checking results for the given properties..
+     * @return Model checking results for the given properties.
      */
     dft_results check(storm::dft::storage::DFT<ValueType> const& origDft, property_vector const& properties, bool symred = true,
                       bool allowModularisation = true, storm::dft::utility::RelevantEvents const& relevantEvents = {}, bool allowDCForRelevant = false,
@@ -95,7 +93,7 @@ class DFTModelChecker {
      * @param allowDCForRelevant Whether to allow Don't Care propagation for relevant events
      * @param approximationError Error allowed for approximation. Value 0 indicates no approximation.
      * @param approximationHeuristic Heuristic used for approximation.
-     * @param eliminateChains If true, chains of non-Markovian states are elimianted from the resulting MA
+     * @param eliminateChains If true, chains of non-Markovian states are eliminated from the resulting MA
      * @param labelBehavior Behavior of labels of eliminated states
      * @return Model checking results (or in case of approximation two results for lower and upper bound)
      */
@@ -131,7 +129,7 @@ class DFTModelChecker {
      * @param allowDCForRelevant Whether to allow Don't Care propagation for relevant events
      * @param approximationError Error allowed for approximation. Value 0 indicates no approximation.
      * @param approximationHeuristic Heuristic used for approximation.
-     * @param eliminateChains If true, chains of non-Markovian states are elimianted from the resulting MA
+     * @param eliminateChains If true, chains of non-Markovian states are eliminated from the resulting MA
      * @param labelBehavior Behavior of labels of eliminated states
      *
      * @return Model checking result