diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h
index 82b809074..034aa9c62 100644
--- a/src/storm-cli-utilities/model-handling.h
+++ b/src/storm-cli-utilities/model-handling.h
@@ -220,7 +220,7 @@ namespace storm {
 
             modelBuildingWatch.stop();
             if (result) {
-                STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl << std::endl);
+                STORM_PRINT("Time for model construction: " << modelBuildingWatch << "." << std::endl << std::endl);
             }
 
             return result;
@@ -332,23 +332,23 @@ namespace storm {
             preprocessingWatch.stop();
 
             if (result.second) {
-                STORM_PRINT_AND_LOG(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl);
+                STORM_PRINT(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl);
             }
             return result;
         }
 
         void printComputingCounterexample(storm::jani::Property const& property) {
-            STORM_PRINT_AND_LOG("Computing counterexample for property " << *property.getRawFormula() << " ..." << std::endl);
+            STORM_PRINT("Computing counterexample for property " << *property.getRawFormula() << " ..." << std::endl);
         }
 
         void printCounterexample(std::shared_ptr<storm::counterexamples::Counterexample> const& counterexample, storm::utility::Stopwatch* watch = nullptr) {
             if (counterexample) {
-                STORM_PRINT_AND_LOG(*counterexample << std::endl);
+                STORM_PRINT(*counterexample << std::endl);
                 if (watch) {
-                    STORM_PRINT_AND_LOG("Time for computation: " << *watch << "." << std::endl);
+                    STORM_PRINT("Time for computation: " << *watch << "." << std::endl);
                 }
             } else {
-                STORM_PRINT_AND_LOG(" failed." << std::endl);
+                STORM_PRINT(" failed." << std::endl);
             }
         }
 
@@ -395,19 +395,19 @@ namespace storm {
             if (result->isQuantitative()) {
                 switch (ft) {
                     case storm::modelchecker::FilterType::VALUES:
-                        STORM_PRINT_AND_LOG(*result);
+                        STORM_PRINT(*result);
                         break;
                     case storm::modelchecker::FilterType::SUM:
-                        STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult<ValueType>().sum());
+                        STORM_PRINT(result->asQuantitativeCheckResult<ValueType>().sum());
                         break;
                     case storm::modelchecker::FilterType::AVG:
-                        STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult<ValueType>().average());
+                        STORM_PRINT(result->asQuantitativeCheckResult<ValueType>().average());
                         break;
                     case storm::modelchecker::FilterType::MIN:
-                        STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult<ValueType>().getMin());
+                        STORM_PRINT(result->asQuantitativeCheckResult<ValueType>().getMin());
                         break;
                     case storm::modelchecker::FilterType::MAX:
-                        STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult<ValueType>().getMax());
+                        STORM_PRINT(result->asQuantitativeCheckResult<ValueType>().getMax());
                         break;
                     case storm::modelchecker::FilterType::ARGMIN:
                     case storm::modelchecker::FilterType::ARGMAX:
@@ -420,16 +420,16 @@ namespace storm {
             } else {
                 switch (ft) {
                     case storm::modelchecker::FilterType::VALUES:
-                        STORM_PRINT_AND_LOG(*result << std::endl);
+                        STORM_PRINT(*result << std::endl);
                         break;
                     case storm::modelchecker::FilterType::EXISTS:
-                        STORM_PRINT_AND_LOG(result->asQualitativeCheckResult().existsTrue());
+                        STORM_PRINT(result->asQualitativeCheckResult().existsTrue());
                         break;
                     case storm::modelchecker::FilterType::FORALL:
-                        STORM_PRINT_AND_LOG(result->asQualitativeCheckResult().forallTrue());
+                        STORM_PRINT(result->asQualitativeCheckResult().forallTrue());
                         break;
                     case storm::modelchecker::FilterType::COUNT:
-                        STORM_PRINT_AND_LOG(result->asQualitativeCheckResult().count());
+                        STORM_PRINT(result->asQualitativeCheckResult().count());
                         break;
                     case storm::modelchecker::FilterType::ARGMIN:
                     case storm::modelchecker::FilterType::ARGMAX:
@@ -441,11 +441,11 @@ namespace storm {
                         STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Filter type only defined for quantitative results.");
                 }
             }
-            STORM_PRINT_AND_LOG(std::endl);
+            STORM_PRINT(std::endl);
         }
 
         void printModelCheckingProperty(storm::jani::Property const& property) {
-            STORM_PRINT_AND_LOG(std::endl << "Model checking property " << *property.getRawFormula() << " ..." << std::endl);
+            STORM_PRINT(std::endl << "Model checking property " << *property.getRawFormula() << " ..." << std::endl);
         }
 
         template<typename ValueType>
@@ -453,13 +453,13 @@ namespace storm {
             if (result) {
                 std::stringstream ss;
                 ss << "'" << *property.getFilter().getStatesFormula() << "'";
-                STORM_PRINT_AND_LOG("Result (for " << (property.getFilter().getStatesFormula()->isInitialFormula() ? "initial" : ss.str()) << " states): ");
+                STORM_PRINT("Result (for " << (property.getFilter().getStatesFormula()->isInitialFormula() ? "initial" : ss.str()) << " states): ");
                 printFilteredResult<ValueType>(result, property.getFilter().getFilterType());
                 if (watch) {
-                    STORM_PRINT_AND_LOG("Time for model checking: " << *watch << "." << std::endl);
+                    STORM_PRINT("Time for model checking: " << *watch << "." << std::endl);
                 }
             } else {
-                STORM_PRINT_AND_LOG(" failed, property is unsupported by selected engine/settings." << std::endl);
+                STORM_PRINT(" failed, property is unsupported by selected engine/settings." << std::endl);
             }
         }
 
diff --git a/src/storm/builder/BuilderOptions.cpp b/src/storm/builder/BuilderOptions.cpp
index b0d2641bd..2ee5bf37c 100644
--- a/src/storm/builder/BuilderOptions.cpp
+++ b/src/storm/builder/BuilderOptions.cpp
@@ -4,6 +4,7 @@
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/IOSettings.h"
+#include "storm/settings/modules/GeneralSettings.h"
 
 #include "storm/utility/macros.h"
 #include "storm/exceptions/InvalidSettingsException.h"
@@ -35,7 +36,7 @@ namespace storm {
             return boost::get<storm::expressions::Expression>(labelOrExpression);
         }
         
-        BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), buildStateValuations(false), buildChoiceOrigins(false), explorationChecks(false), explorationShowProgress(false), explorationShowProgressDelay(0) {
+        BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), buildStateValuations(false), buildChoiceOrigins(false), explorationChecks(false), showProgress(false), showProgressDelay(0) {
             // Intentionally left empty.
         }
         
@@ -54,9 +55,11 @@ namespace storm {
                 }
             }
             
-            explorationChecks = storm::settings::getModule<storm::settings::modules::IOSettings>().isExplorationChecksSet();
-            explorationShowProgress = storm::settings::getModule<storm::settings::modules::IOSettings>().isExplorationShowProgressSet();
-            explorationShowProgressDelay = storm::settings::getModule<storm::settings::modules::IOSettings>().getExplorationShowProgressDelay();
+            auto const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
+            auto const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
+            explorationChecks = ioSettings.isExplorationChecksSet();
+            showProgress = generalSettings.isVerboseSet();
+            showProgressDelay = generalSettings.getShowProgressDelay();
         }
         
         void BuilderOptions::preserveFormula(storm::logic::Formula const& formula) {
@@ -166,12 +169,12 @@ namespace storm {
             return explorationChecks;
         }
         
-        bool BuilderOptions::isExplorationShowProgressSet() const {
-            return explorationShowProgress;
+        bool BuilderOptions::isShowProgressSet() const {
+            return showProgress;
         }
 
-        uint64_t BuilderOptions::getExplorationShowProgressDelay() const {
-            return explorationShowProgressDelay;
+        uint64_t BuilderOptions::getShowProgressDelay() const {
+            return showProgressDelay;
         }
 
         BuilderOptions& BuilderOptions::setExplorationChecks(bool newValue) {
diff --git a/src/storm/builder/BuilderOptions.h b/src/storm/builder/BuilderOptions.h
index f3a6edfbf..fe56994c7 100644
--- a/src/storm/builder/BuilderOptions.h
+++ b/src/storm/builder/BuilderOptions.h
@@ -106,8 +106,8 @@ namespace storm {
             bool isBuildAllRewardModelsSet() const;
             bool isBuildAllLabelsSet() const;
             bool isExplorationChecksSet() const;
-            bool isExplorationShowProgressSet() const;
-            uint64_t getExplorationShowProgressDelay() const;
+            bool isShowProgressSet() const;
+            uint64_t getShowProgressDelay() const;
 
             /**
              * Should all reward models be built? If not set, only required reward models are build.
@@ -190,10 +190,10 @@ namespace storm {
             bool explorationChecks;
             
             /// A flag that stores whether the progress of exploration is to be printed.
-            bool explorationShowProgress;
+            bool showProgress;
             
             /// The delay for printing progress information.
-            uint64_t explorationShowProgressDelay;
+            uint64_t showProgressDelay;
         };
         
     }
diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp
index 665190e6c..7a552e9bd 100644
--- a/src/storm/builder/ExplicitModelBuilder.cpp
+++ b/src/storm/builder/ExplicitModelBuilder.cpp
@@ -240,13 +240,13 @@ namespace storm {
                     ++currentRowGroup;
                 }
                 
-                if (generator->getOptions().isExplorationShowProgressSet()) {
+                if (generator->getOptions().isShowProgressSet()) {
                     ++numberOfExploredStatesSinceLastMessage;
                     ++numberOfExploredStates;
                     
                     auto now = std::chrono::high_resolution_clock::now();
                     auto durationSinceLastMessage = std::chrono::duration_cast<std::chrono::seconds>(now - timeOfLastMessage).count();
-                    if (static_cast<uint64_t>(durationSinceLastMessage) >= generator->getOptions().getExplorationShowProgressDelay()) {
+                    if (static_cast<uint64_t>(durationSinceLastMessage) >= generator->getOptions().getShowProgressDelay()) {
                         auto statesPerSecond = numberOfExploredStatesSinceLastMessage / durationSinceLastMessage;
                         auto durationSinceStart = std::chrono::duration_cast<std::chrono::seconds>(now - timeOfStart).count();
                         std::cout << "Explored " << numberOfExploredStates << " states in " << durationSinceStart << " seconds (currently " << statesPerSecond << " states per second)." << std::endl;
diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
index a550ee130..54779b96a 100644
--- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
+++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
@@ -528,13 +528,13 @@ namespace storm {
                 }
                 modelData["exploration_checks"] = cpptempl::make_data(list);
                 list = cpptempl::data_list();
-                if (options.isExplorationShowProgressSet()) {
+                if (options.isShowProgressSet()) {
                     list.push_back(cpptempl::data_map());
                 }
                 modelData["expl_progress"] = cpptempl::make_data(list);
                 
                 std::stringstream progressDelayStream;
-                progressDelayStream << options.getExplorationShowProgressDelay();
+                progressDelayStream << options.getShowProgressDelay();
                 modelData["expl_progress_interval"] = cpptempl::make_data(progressDelayStream.str());
                 list = cpptempl::data_list();
                 if (std::is_same<storm::RationalNumber, ValueType>::value) {
diff --git a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
index f4cca554f..d7986e56d 100644
--- a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
@@ -31,10 +31,7 @@ namespace storm {
                 std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> statesWithProbability01 = storm::utility::graph::performProb01(model, transitionMatrix, phiStates, psiStates);
                 storm::dd::Bdd<DdType> maybeStates = !statesWithProbability01.first && !statesWithProbability01.second && model.getReachableStates();
                 
-                // Perform some logging.
-                STORM_LOG_INFO("Found " << statesWithProbability01.first.getNonZeroCount() << " 'no' states.");
-                STORM_LOG_INFO("Found " << statesWithProbability01.second.getNonZeroCount() << " 'yes' states.");
-                STORM_LOG_INFO("Found " << maybeStates.getNonZeroCount() << " 'maybe' states.");
+                STORM_LOG_INFO("Preprocessing: " << statesWithProbability01.first.getNonZeroCount() << " states with probability 1, " << statesWithProbability01.second.getNonZeroCount() << " with probability 0 (" << maybeStates.getNonZeroCount() << " states remaining).");
                 
                 // Check whether we need to compute exact probabilities for some states.
                 if (qualitative) {
@@ -109,6 +106,8 @@ namespace storm {
                 storm::dd::Bdd<DdType> statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(model, transitionMatrix.notZero(), phiStates, psiStates, stepBound);
                 storm::dd::Bdd<DdType> maybeStates = statesWithProbabilityGreater0 && !psiStates && model.getReachableStates();
                 
+                STORM_LOG_INFO("Preprocessing: " << statesWithProbabilityGreater0.getNonZeroCount() << " states with probability greater 0.");
+
                 // If there are maybe states, we need to perform matrix-vector multiplications.
                 if (!maybeStates.isZero()) {
                     // Create the ODD for the translation between symbolic and explicit storage.
@@ -204,9 +203,8 @@ namespace storm {
                 storm::dd::Bdd<DdType> infinityStates = storm::utility::graph::performProb1(model, transitionMatrix.notZero(), model.getReachableStates(), targetStates);
                 infinityStates = !infinityStates && model.getReachableStates();
                 storm::dd::Bdd<DdType> maybeStates = (!targetStates && !infinityStates) && model.getReachableStates();
-                STORM_LOG_INFO("Found " << infinityStates.getNonZeroCount() << " 'infinity' states.");
-                STORM_LOG_INFO("Found " << targetStates.getNonZeroCount() << " 'target' states.");
-                STORM_LOG_INFO("Found " << maybeStates.getNonZeroCount() << " 'maybe' states.");
+
+                STORM_LOG_INFO("Preprocessing: " << infinityStates.getNonZeroCount() << " states with reward infinity, " << targetStates.getNonZeroCount() << " target states (" << maybeStates.getNonZeroCount() << " states remaining).");
                 
                 // Check whether we need to compute exact rewards for some states.
                 if (qualitative) {
diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
index fd808cdae..d6b41030a 100644
--- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
@@ -68,11 +68,8 @@ namespace storm {
                 }
                 storm::dd::Bdd<DdType> maybeStates = !statesWithProbability01.first && !statesWithProbability01.second && model.getReachableStates();
                 
-                // Perform some logging.
-                STORM_LOG_INFO("Found " << statesWithProbability01.first.getNonZeroCount() << " 'no' states.");
-                STORM_LOG_INFO("Found " << statesWithProbability01.second.getNonZeroCount() << " 'yes' states.");
-                STORM_LOG_INFO("Found " << maybeStates.getNonZeroCount() << " 'maybe' states.");
-                
+                STORM_LOG_INFO("Preprocessing: " << statesWithProbability01.first.getNonZeroCount() << " states with probability 1, " << statesWithProbability01.second.getNonZeroCount() << " with probability 0 (" << maybeStates.getNonZeroCount() << " states remaining).");
+
                 // Check whether we need to compute exact probabilities for some states.
                 if (qualitative) {
                     // Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1.
@@ -162,6 +159,8 @@ namespace storm {
                 }
                 storm::dd::Bdd<DdType> maybeStates = statesWithProbabilityGreater0 && !psiStates && model.getReachableStates();
                 
+                STORM_LOG_INFO("Preprocessing: " << statesWithProbabilityGreater0.getNonZeroCount() << " states with probability greater 0.");
+
                 // If there are maybe states, we need to perform matrix-vector multiplications.
                 if (!maybeStates.isZero()) {
                     // Create the ODD for the translation between symbolic and explicit storage.
@@ -339,10 +338,9 @@ namespace storm {
                 infinityStates = !infinityStates && model.getReachableStates();
                 storm::dd::Bdd<DdType> maybeStatesWithTargetStates = !infinityStates && model.getReachableStates();
                 storm::dd::Bdd<DdType> maybeStates = !targetStates && maybeStatesWithTargetStates;
-                STORM_LOG_INFO("Found " << infinityStates.getNonZeroCount() << " 'infinity' states.");
-                STORM_LOG_INFO("Found " << targetStates.getNonZeroCount() << " 'target' states.");
-                STORM_LOG_INFO("Found " << maybeStates.getNonZeroCount() << " 'maybe' states.");
-                
+
+                STORM_LOG_INFO("Preprocessing: " << infinityStates.getNonZeroCount() << " states with reward infinity, " << targetStates.getNonZeroCount() << " target states (" << maybeStates.getNonZeroCount() << " states remaining).");
+
                 // Check whether we need to compute exact rewards for some states.
                 if (qualitative) {
                     // Set the values for all maybe-states to 1 to indicate that their reward values
diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
index 6107e3acb..67db97164 100644
--- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
@@ -40,9 +40,10 @@ namespace storm {
                 } else {
                     maybeStates = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates, true, stepBound);
                     maybeStates &= ~psiStates;
-                    STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
                 }
                 
+                STORM_LOG_INFO("Preprocessing: " << maybeStates.getNumberOfSetBits() << " non-target states with probability greater 0.");
+                
                 storm::utility::vector::setVectorValues<ValueType>(result, psiStates, storm::utility::one<ValueType>());
                 
                 if (!maybeStates.empty()) {
@@ -92,17 +93,17 @@ namespace storm {
                             STORM_LOG_THROW(storm::utility::isZero(resultsForNonMaybeStates[state]), storm::exceptions::IllegalArgumentException, "Expected that the result hint specifies probabilities in {0,1} for non-maybe states");
                         }
                     }
+
+                    STORM_LOG_INFO("Preprocessing: " << statesWithProbability1.getNumberOfSetBits() << " states with probability 1 (" << maybeStates.getNumberOfSetBits() << " states remaining).");
                 } else {
                     // Get all states that have probability 0 and 1 of satisfying the until-formula.
                     std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates);
                     storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first);
                     statesWithProbability1 = std::move(statesWithProbability01.second);
                     maybeStates = ~(statesWithProbability0 | statesWithProbability1);
-                                    
-                    STORM_LOG_INFO("Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states.");
-                    STORM_LOG_INFO("Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states.");
-                    STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
-                    
+
+                    STORM_LOG_INFO("Preprocessing: " << statesWithProbability1.getNumberOfSetBits() << " states with probability 1, " << statesWithProbability0.getNumberOfSetBits() << " with probability 0 (" << maybeStates.getNumberOfSetBits() << " states remaining).");
+
                     // Set values of resulting vector that are known exactly.
                     storm::utility::vector::setVectorValues<ValueType>(result, statesWithProbability0, storm::utility::zero<ValueType>());
                     storm::utility::vector::setVectorValues<ValueType>(result, statesWithProbability1, storm::utility::one<ValueType>());
@@ -246,15 +247,15 @@ namespace storm {
                 if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().getComputeOnlyMaybeStates()) {
                     maybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getMaybeStates();
                     storm::utility::vector::setVectorValues(result, ~(maybeStates | targetStates), storm::utility::infinity<ValueType>());
+
+                    STORM_LOG_INFO("Preprocessing: " << targetStates.getNumberOfSetBits() << " target states (" << maybeStates.getNumberOfSetBits() << " states remaining).");
                 } else {
                     storm::storage::BitVector trueStates(transitionMatrix.getRowCount(), true);
                     storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(backwardTransitions, trueStates, targetStates);
                     infinityStates.complement();
                     maybeStates = ~(targetStates | infinityStates);
                     
-                    STORM_LOG_INFO("Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states.");
-                    STORM_LOG_INFO("Found " << targetStates.getNumberOfSetBits() << " 'target' states.");
-                    STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
+                    STORM_LOG_INFO("Preprocessing: " << infinityStates.getNumberOfSetBits() << " states with reward infinity, " << targetStates.getNumberOfSetBits() << " target states (" << maybeStates.getNumberOfSetBits() << " states remaining).");
                     
                     storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity<ValueType>());
                 }
diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
index 85713333a..3d135248e 100644
--- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
@@ -52,9 +52,10 @@ namespace storm {
                         maybeStates = storm::utility::graph::performProbGreater0E(backwardTransitions, phiStates, psiStates, true, stepBound);
                     }
                     maybeStates &= ~psiStates;
-                    STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
                 }
                 
+                STORM_LOG_INFO("Preprocessing: " << maybeStates.getNumberOfSetBits() << " non-target states with probability greater 0.");
+                
                 if (!maybeStates.empty()) {
                     // We can eliminate the rows and columns from the original transition probability matrix that have probability 0.
                     storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false);
@@ -404,9 +405,6 @@ namespace storm {
                 result.statesWithProbability0 = std::move(statesWithProbability01.first);
                 result.statesWithProbability1 = std::move(statesWithProbability01.second);
                 result.maybeStates = ~(result.statesWithProbability0 | result.statesWithProbability1);
-                STORM_LOG_INFO("Found " << result.statesWithProbability0.getNumberOfSetBits() << " 'no' states.");
-                STORM_LOG_INFO("Found " << result.statesWithProbability1.getNumberOfSetBits() << " 'yes' states.");
-                STORM_LOG_INFO("Found " << result.maybeStates.getNumberOfSetBits() << " 'maybe' states.");
                 
                 return result;
             }
@@ -687,6 +685,8 @@ namespace storm {
                 // that is strictly between 0 and 1) and the states that satisfy the formula with probablity 1 and 0, respectively.
                 QualitativeStateSetsUntilProbabilities qualitativeStateSets = getQualitativeStateSetsUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, hint);
                 
+                STORM_LOG_INFO("Preprocessing: " << qualitativeStateSets.statesWithProbability1.getNumberOfSetBits() << " states with probability 1, " << qualitativeStateSets.statesWithProbability0.getNumberOfSetBits() << " with probability 0 (" << qualitativeStateSets.maybeStates.getNumberOfSetBits() << " states remaining).");
+                
                 // Set values of resulting vector that are known exactly.
                 storm::utility::vector::setVectorValues<ValueType>(result, qualitativeStateSets.statesWithProbability1, storm::utility::one<ValueType>());
                 
@@ -870,9 +870,6 @@ namespace storm {
                 }
                 result.infinityStates.complement();
                 result.maybeStates = ~(targetStates | result.infinityStates);
-                STORM_LOG_INFO("Found " << result.infinityStates.getNumberOfSetBits() << " 'infinity' states.");
-                STORM_LOG_INFO("Found " << targetStates.getNumberOfSetBits() << " 'target' states.");
-                STORM_LOG_INFO("Found " << result.maybeStates.getNumberOfSetBits() << " 'maybe' states.");
                 return result;
             }
             
@@ -1019,6 +1016,9 @@ namespace storm {
                 
                 // Determine which states have a reward that is infinity or less than infinity.
                 QualitativeStateSetsReachabilityRewards qualitativeStateSets = getQualitativeStateSetsReachabilityRewards(goal, transitionMatrix, backwardTransitions, targetStates, hint);
+                
+                STORM_LOG_INFO("Preprocessing: " << qualitativeStateSets.infinityStates.getNumberOfSetBits() << " states with reward infinity, " << targetStates.getNumberOfSetBits() << " target states (" << qualitativeStateSets.maybeStates.getNumberOfSetBits() << " states remaining).");
+
                 storm::utility::vector::setVectorValues(result, qualitativeStateSets.infinityStates, storm::utility::infinity<ValueType>());
                 
                 // If requested, we will produce a scheduler.
diff --git a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp
index c54d15b92..cf8019aea 100644
--- a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp
@@ -25,10 +25,7 @@ namespace storm {
                 std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> statesWithProbability01 = storm::utility::graph::performProb01(model, transitionMatrix, phiStates, psiStates);
                 storm::dd::Bdd<DdType> maybeStates = !statesWithProbability01.first && !statesWithProbability01.second && model.getReachableStates();
                 
-                // Perform some logging.
-                STORM_LOG_INFO("Found " << statesWithProbability01.first.getNonZeroCount() << " 'no' states.");
-                STORM_LOG_INFO("Found " << statesWithProbability01.second.getNonZeroCount() << " 'yes' states.");
-                STORM_LOG_INFO("Found " << maybeStates.getNonZeroCount() << " 'maybe' states.");
+                STORM_LOG_INFO("Preprocessing: " << statesWithProbability01.first.getNonZeroCount() << " states with probability 1, " << statesWithProbability01.second.getNonZeroCount() << " with probability 0 (" << maybeStates.getNonZeroCount() << " states remaining).");
                 
                 // Check whether we need to compute exact probabilities for some states.
                 if (qualitative) {
@@ -146,9 +143,8 @@ namespace storm {
                 storm::dd::Bdd<DdType> infinityStates = storm::utility::graph::performProb1(model, transitionMatrix.notZero(), model.getReachableStates(), targetStates);
                 infinityStates = !infinityStates && model.getReachableStates();
                 storm::dd::Bdd<DdType> maybeStates = (!targetStates && !infinityStates) && model.getReachableStates();
-                STORM_LOG_INFO("Found " << infinityStates.getNonZeroCount() << " 'infinity' states.");
-                STORM_LOG_INFO("Found " << targetStates.getNonZeroCount() << " 'target' states.");
-                STORM_LOG_INFO("Found " << maybeStates.getNonZeroCount() << " 'maybe' states.");
+
+                STORM_LOG_INFO("Preprocessing: " << infinityStates.getNonZeroCount() << " states with reward infinity, " << targetStates.getNonZeroCount() << " target states (" << maybeStates.getNonZeroCount() << " states remaining).");
                 
                 // Check whether we need to compute exact rewards for some states.
                 if (qualitative) {
diff --git a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
index c6231a5eb..bca6bec0f 100644
--- a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
@@ -49,10 +49,7 @@ namespace storm {
                 
                 storm::dd::Bdd<DdType> maybeStates = !statesWithProbability01.first && !statesWithProbability01.second && model.getReachableStates();
                 
-                // Perform some logging.
-                STORM_LOG_INFO("Found " << statesWithProbability01.first.getNonZeroCount() << " 'no' states.");
-                STORM_LOG_INFO("Found " << statesWithProbability01.second.getNonZeroCount() << " 'yes' states.");
-                STORM_LOG_INFO("Found " << maybeStates.getNonZeroCount() << " 'maybe' states.");
+                STORM_LOG_INFO("Preprocessing: " << statesWithProbability01.first.getNonZeroCount() << " states with probability 1, " << statesWithProbability01.second.getNonZeroCount() << " with probability 0 (" << maybeStates.getNonZeroCount() << " states remaining).");
                 
                 // Check whether we need to compute exact probabilities for some states.
                 if (qualitative) {
@@ -199,7 +196,6 @@ namespace storm {
                 storm::dd::Bdd<DdType> infinityStates;
                 storm::dd::Bdd<DdType> transitionMatrixBdd = transitionMatrix.notZero();
                 if (dir == OptimizationDirection::Minimize) {
-                    STORM_LOG_WARN("Results of reward computation may be too low, because of zero-reward loops.");
                     infinityStates = storm::utility::graph::performProb1E(model, transitionMatrixBdd, model.getReachableStates(), targetStates, storm::utility::graph::performProbGreater0E(model, transitionMatrixBdd, model.getReachableStates(), targetStates));
                 } else {
                     infinityStates = storm::utility::graph::performProb1A(model, transitionMatrixBdd, targetStates, storm::utility::graph::performProbGreater0A(model, transitionMatrixBdd, model.getReachableStates(), targetStates));
@@ -207,10 +203,9 @@ namespace storm {
                 infinityStates = !infinityStates && model.getReachableStates();
                 
                 storm::dd::Bdd<DdType> maybeStates = (!targetStates && !infinityStates) && model.getReachableStates();
-                STORM_LOG_INFO("Found " << infinityStates.getNonZeroCount() << " 'infinity' states.");
-                STORM_LOG_INFO("Found " << targetStates.getNonZeroCount() << " 'target' states.");
-                STORM_LOG_INFO("Found " << maybeStates.getNonZeroCount() << " 'maybe' states.");
                 
+                STORM_LOG_INFO("Preprocessing: " << infinityStates.getNonZeroCount() << " states with reward infinity, " << targetStates.getNonZeroCount() << " target states (" << maybeStates.getNonZeroCount() << " states remaining).");
+
                 // Check whether we need to compute exact rewards for some states.
                 if (qualitative) {
                     // Set the values for all maybe-states to 1 to indicate that their reward values
diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp
index e38c5daf2..b271ca581 100644
--- a/src/storm/settings/SettingsManager.cpp
+++ b/src/storm/settings/SettingsManager.cpp
@@ -61,7 +61,6 @@ namespace storm {
             this->executableName = executableName;
         }
 
-
         void SettingsManager::setFromCommandLine(int const argc, char const * const argv[]) {
             // We convert the arguments to a vector of strings and strip off the first element since it refers to the
             // name of the program.
@@ -289,7 +288,6 @@ namespace storm {
                     this->addOption(option);
                 }
             }
-
         }
         
         void SettingsManager::addOption(std::shared_ptr<Option> const& option) {
@@ -390,7 +388,6 @@ namespace storm {
             for (auto const& nameModulePair : this->modules) {
                 nameModulePair.second->finalize();
                 nameModulePair.second->check();
-
             }
         }
         
diff --git a/src/storm/settings/modules/GeneralSettings.cpp b/src/storm/settings/modules/GeneralSettings.cpp
index 7edb76e7b..63c5e21bf 100644
--- a/src/storm/settings/modules/GeneralSettings.cpp
+++ b/src/storm/settings/modules/GeneralSettings.cpp
@@ -22,6 +22,7 @@ namespace storm {
             const std::string GeneralSettings::versionOptionName = "version";
             const std::string GeneralSettings::verboseOptionName = "verbose";
             const std::string GeneralSettings::verboseOptionShortName = "v";
+            const std::string GeneralSettings::showProgressOptionName = "progress";
             const std::string GeneralSettings::precisionOptionName = "precision";
             const std::string GeneralSettings::precisionOptionShortName = "eps";
             const std::string GeneralSettings::configOptionName = "config";
@@ -37,6 +38,7 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("hint", "A regular expression to show help for all matching entities or 'all' for the complete help.").setDefaultValueString("all").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, versionOptionName, false, "Prints the version information.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, verboseOptionName, false, "Enables more verbose output.").setShortName(verboseOptionShortName).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, showProgressOptionName, false, "Sets when additional information (if available) about the progress is printed.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("delay", "The delay to wait (in seconds) between emitting information (0 means never print progress).").setDefaultValueUnsignedInteger(5).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The internally used precision.").setShortName(precisionOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to use.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, configOptionName, false, "If given, this file will be read and parsed for additional configuration settings.").setShortName(configOptionShortName)
@@ -63,6 +65,10 @@ namespace storm {
                 return this->getOption(verboseOptionName).getHasOptionBeenSet();
             }
             
+            uint64_t GeneralSettings::getShowProgressDelay() const {
+                return this->getOption(showProgressOptionName).getArgumentByName("delay").getValueAsUnsignedInteger();
+            }
+            
             double GeneralSettings::getPrecision() const {
                 return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
             }
diff --git a/src/storm/settings/modules/GeneralSettings.h b/src/storm/settings/modules/GeneralSettings.h
index 42f22fb3b..00553ef27 100644
--- a/src/storm/settings/modules/GeneralSettings.h
+++ b/src/storm/settings/modules/GeneralSettings.h
@@ -50,6 +50,13 @@ namespace storm {
                  */
                 bool isVerboseSet() const;
 
+                /*!
+                 * Retrieves the delay for printing information about the exploration progress.
+                 *
+                 * @return The desired delay in seconds. If 0, no information about the progress shall be printed.
+                 */
+                uint64_t getShowProgressDelay() const;
+                
                 /*!
                  * Retrieves the precision to use for numerical operations.
                  *
@@ -114,6 +121,8 @@ namespace storm {
                 static const std::string versionOptionName;
                 static const std::string verboseOptionName;
                 static const std::string verboseOptionShortName;
+                static const std::string showProgressOptionName;
+                static const std::string showProgressOptionShortName;
                 static const std::string precisionOptionName;
                 static const std::string precisionOptionShortName;
                 static const std::string configOptionName;
diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp
index 7d26b54ac..012f94b04 100644
--- a/src/storm/settings/modules/IOSettings.cpp
+++ b/src/storm/settings/modules/IOSettings.cpp
@@ -34,8 +34,6 @@ namespace storm {
             const std::string IOSettings::explorationOrderOptionShortName = "eo";
             const std::string IOSettings::explorationChecksOptionName = "explchecks";
             const std::string IOSettings::explorationChecksOptionShortName = "ec";
-            const std::string IOSettings::explorationShowProgressOptionName = "explprog";
-            const std::string IOSettings::explorationShowProgressOptionShortName = "ep";
             const std::string IOSettings::transitionRewardsOptionName = "transrew";
             const std::string IOSettings::stateRewardsOptionName = "staterew";
             const std::string IOSettings::choiceLabelingOptionName = "choicelab";
@@ -86,7 +84,6 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(explorationOrders)).setDefaultValueString("bfs").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, explorationChecksOptionName, false, "If set, additional checks (if available) are performed during model exploration to debug the model.").setShortName(explorationChecksOptionShortName).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, explorationShowProgressOptionName, false, "Sets when additional information (if available) about the exploration progress is printed.").setShortName(explorationShowProgressOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("delay", "The delay to wait between emitting information.").setDefaultValueUnsignedInteger(0).build()).build());
 
                 this->addOption(storm::settings::OptionBuilder(moduleName, transitionRewardsOptionName, false, "If given, the transition rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
@@ -197,15 +194,7 @@ namespace storm {
             bool IOSettings::isExplorationChecksSet() const {
                 return this->getOption(explorationChecksOptionName).getHasOptionBeenSet();
             }
-            
-            bool IOSettings::isExplorationShowProgressSet() const {
-                return this->getOption(explorationShowProgressOptionName).getArgumentByName("delay").getValueAsUnsignedInteger() > 0;
-            }
-
-            uint64_t IOSettings::getExplorationShowProgressDelay() const {
-                return this->getOption(explorationShowProgressOptionName).getArgumentByName("delay").getValueAsUnsignedInteger();
-            }
-            
+                        
             bool IOSettings::isTransitionRewardsSet() const {
                 return this->getOption(transitionRewardsOptionName).getHasOptionBeenSet();
             }
diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h
index e68c6b515..392af6d6d 100644
--- a/src/storm/settings/modules/IOSettings.h
+++ b/src/storm/settings/modules/IOSettings.h
@@ -178,21 +178,7 @@ namespace storm {
                  * @return True if additional checks are to be performed.
                  */
                 bool isExplorationChecksSet() const;
-                
-                /*!
-                 * Retrieves whether to show information about exploration progress.
-                 *
-                 * @return True if information is to be shown.
-                 */
-                bool isExplorationShowProgressSet() const;
-                
-                /*!
-                 * Retrieves the delay for printing information about the exploration progress.
-                 *
-                 * @return The desired delay in seconds. If 0, no information about the progress shall be printed.
-                 */
-                uint64_t getExplorationShowProgressDelay() const;
-                
+                                                
                 /*!
                  * Retrieves the exploration order if it was set.
                  *
@@ -348,8 +334,6 @@ namespace storm {
                 static const std::string jitOptionName;
                 static const std::string explorationChecksOptionName;
                 static const std::string explorationChecksOptionShortName;
-                static const std::string explorationShowProgressOptionName;
-                static const std::string explorationShowProgressOptionShortName;
                 static const std::string explorationOrderOptionName;
                 static const std::string explorationOrderOptionShortName;
                 static const std::string transitionRewardsOptionName;
diff --git a/src/storm/solver/AbstractEquationSolver.cpp b/src/storm/solver/AbstractEquationSolver.cpp
index 788a8d789..18a82f498 100644
--- a/src/storm/solver/AbstractEquationSolver.cpp
+++ b/src/storm/solver/AbstractEquationSolver.cpp
@@ -3,12 +3,23 @@
 #include "storm/adapters/RationalNumberAdapter.h"
 #include "storm/adapters/RationalFunctionAdapter.h"
 
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/IOSettings.h"
+#include "storm/settings/modules/GeneralSettings.h"
+
 #include "storm/utility/macros.h"
 #include "storm/exceptions/UnmetRequirementException.h"
 
 namespace storm {
     namespace solver {
         
+        template<typename ValueType>
+        AbstractEquationSolver<ValueType>::AbstractEquationSolver() {
+            auto const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
+            showProgressFlag = generalSettings.isVerboseSet();
+            showProgressDelay = generalSettings.getShowProgressDelay();
+        }
+        
         template<typename ValueType>
         void AbstractEquationSolver<ValueType>::setTerminationCondition(std::unique_ptr<TerminationCondition<ValueType>> terminationCondition) {
             this->terminationCondition = std::move(terminationCondition);
@@ -176,8 +187,43 @@ namespace storm {
             }
         }
         
-        template class AbstractEquationSolver<double>;
+        template<typename ValueType>
+        bool AbstractEquationSolver<ValueType>::isShowProgressSet() const {
+            return showProgressFlag;
+        }
+        
+        template<typename ValueType>
+        uint64_t AbstractEquationSolver<ValueType>::getShowProgressDelay() const {
+            return showProgressDelay;
+        }
         
+        template<typename ValueType>
+        void AbstractEquationSolver<ValueType>::startMeasureProgress() const {
+            timeOfStart = std::chrono::high_resolution_clock::now();
+            timeOfLastMessage = timeOfStart;
+            iterationOfLastMessage = 0;
+        }
+        
+        template<typename ValueType>
+        void AbstractEquationSolver<ValueType>::showProgressIterative(uint64_t iteration, boost::optional<uint64_t> const& bound) const {
+            if (this->isShowProgressSet()) {
+                auto now = std::chrono::high_resolution_clock::now();
+                auto durationSinceLastMessage = static_cast<uint64_t>(std::chrono::duration_cast<std::chrono::seconds>(now - timeOfLastMessage).count());
+                if (durationSinceLastMessage >= this->getShowProgressDelay()) {
+                    uint64_t numberOfIterationsSinceLastMessage = iteration - iterationOfLastMessage;
+                    STORM_LOG_INFO("Completed " << iteration << " iterations "
+                                   << (bound ? "(out of " + std::to_string(bound.get()) + ") " : "")
+                                   << "in " << std::chrono::duration_cast<std::chrono::seconds>(now - timeOfStart).count() << "s (currently " << (static_cast<double>(numberOfIterationsSinceLastMessage) / durationSinceLastMessage) << " per second)."
+                                   );
+                    timeOfLastMessage = std::chrono::high_resolution_clock::now();
+                    iterationOfLastMessage = iteration;
+                }
+            }
+        }
+        
+        template class AbstractEquationSolver<double>;
+        template class AbstractEquationSolver<float>;
+
 #ifdef STORM_HAVE_CARL
         template class AbstractEquationSolver<storm::RationalNumber>;
         template class AbstractEquationSolver<storm::RationalFunction>;
diff --git a/src/storm/solver/AbstractEquationSolver.h b/src/storm/solver/AbstractEquationSolver.h
index 72776d522..362239360 100644
--- a/src/storm/solver/AbstractEquationSolver.h
+++ b/src/storm/solver/AbstractEquationSolver.h
@@ -13,6 +13,8 @@ namespace storm {
         template<typename ValueType>
         class AbstractEquationSolver {
         public:
+            AbstractEquationSolver();
+            
             /*!
              * Sets a custom termination condition that is used together with the regular termination condition of the
              * solver.
@@ -128,6 +130,26 @@ namespace storm {
              */
             void setBounds(std::vector<ValueType> const& lower, std::vector<ValueType> const& upper);
             
+            /*!
+             * Retrieves whether progress is to be shown.
+             */
+            bool isShowProgressSet() const;
+            
+            /*!
+             * Retrieves the delay between progress emissions.
+             */
+            uint64_t getShowProgressDelay() const;
+            
+            /*!
+             * Starts to measure progress.
+             */
+            void startMeasureProgress() const;
+            
+            /*!
+             * Shows progress if this solver is asked to do so.
+             */
+            void showProgressIterative(uint64_t iterations, boost::optional<uint64_t> const& bound = boost::none) const;
+
         protected:
             /*!
              * Retrieves the custom termination condition (if any was set).
@@ -156,6 +178,18 @@ namespace storm {
             
             // Lower bounds if they were set.
             boost::optional<std::vector<ValueType>> upperBounds;
+
+        private:
+            // A flag that indicates whether progress is to be shown.
+            bool showProgressFlag;
+            
+            // The delay between progress emission.
+            uint64_t showProgressDelay;
+            
+            // Time points that are used when showing progress.
+            mutable uint64_t iterationOfLastMessage;
+            mutable std::chrono::high_resolution_clock::time_point timeOfStart;
+            mutable std::chrono::high_resolution_clock::time_point timeOfLastMessage;
         };
         
     }
diff --git a/src/storm/solver/EigenLinearEquationSolver.cpp b/src/storm/solver/EigenLinearEquationSolver.cpp
index f2df524b3..e8ddb13d5 100644
--- a/src/storm/solver/EigenLinearEquationSolver.cpp
+++ b/src/storm/solver/EigenLinearEquationSolver.cpp
@@ -174,7 +174,7 @@ namespace storm {
                 typename EigenLinearEquationSolverSettings<ValueType>::Preconditioner preconditioner = this->getSettings().getPreconditioner();
                 if (solutionMethod == EigenLinearEquationSolverSettings<ValueType>::SolutionMethod::BiCGSTAB) {
                     if (preconditioner == EigenLinearEquationSolverSettings<ValueType>::Preconditioner::Ilu) {
-                        STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with BicGSTAB with Ilu preconditioner (Eigen library).");
+                        STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with BiCGSTAB with Ilu preconditioner (Eigen library).");
 
                         StormEigen::BiCGSTAB<StormEigen::SparseMatrix<ValueType>, StormEigen::IncompleteLUT<ValueType>> solver;
                         solver.compute(*this->eigenA);
@@ -184,7 +184,7 @@ namespace storm {
                         converged = solver.info() == StormEigen::ComputationInfo::Success;
                         numberOfIterations = solver.iterations();
                     } else if (preconditioner == EigenLinearEquationSolverSettings<ValueType>::Preconditioner::Diagonal) {
-                        STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with BicGSTAB with Diagonal preconditioner (Eigen library).");
+                        STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with BiCGSTAB with Diagonal preconditioner (Eigen library).");
 
                         StormEigen::BiCGSTAB<StormEigen::SparseMatrix<ValueType>, StormEigen::DiagonalPreconditioner<ValueType>> solver;
                         solver.setTolerance(this->getSettings().getPrecision());
@@ -194,7 +194,7 @@ namespace storm {
                         converged = solver.info() == StormEigen::ComputationInfo::Success;
                         numberOfIterations = solver.iterations();
                     } else {
-                        STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with BicGSTAB with identity preconditioner (Eigen library).");
+                        STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with BiCGSTAB with identity preconditioner (Eigen library).");
 
                         StormEigen::BiCGSTAB<StormEigen::SparseMatrix<ValueType>, StormEigen::IdentityPreconditioner> solver;
                         solver.setTolerance(this->getSettings().getPrecision());
diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
index fba6865ee..0ddd5b5fe 100644
--- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
@@ -165,6 +165,7 @@ namespace storm {
             
             Status status = Status::InProgress;
             uint64_t iterations = 0;
+            this->startMeasureProgress();
             do {
                 // Solve the equation system for the 'DTMC'.
                 solver->solveEquations(x, subB);
@@ -208,6 +209,9 @@ namespace storm {
                     solver->setMatrix(std::move(submatrix));
                 }
                 
+                // Potentially show progress.
+                this->showProgressIterative(iterations);
+                
                 // Update environment variables.
                 ++iterations;
                 status = updateStatusIfNotConverged(status, x, iterations, dir == storm::OptimizationDirection::Minimize ? SolverGuarantee::GreaterOrEqual : SolverGuarantee::LessOrEqual);
@@ -334,6 +338,7 @@ namespace storm {
             // Proceed with the iterations as long as the method did not converge or reach the maximum number of iterations.
             uint64_t iterations = 0;
 
+            this->startMeasureProgress();
             Status status = Status::InProgress;
             while (status == Status::InProgress) {
                 // Compute x' = min/max(A*x + b).
@@ -350,6 +355,9 @@ namespace storm {
                     status = Status::Converged;
                 }
                 
+                // Potentially show progress.
+                this->showProgressIterative(iterations);
+                
                 // Update environment variables.
                 std::swap(currentX, newX);
                 ++iterations;
@@ -377,6 +385,30 @@ namespace storm {
             return status == Status::Converged || status == Status::TerminatedEarly;
         }
         
+        template<typename ValueType>
+        void preserveOldRelevantValues(std::vector<ValueType> const& allValues, storm::storage::BitVector const& relevantValues, std::vector<ValueType>& oldValues) {
+            storm::utility::vector::selectVectorValues(oldValues, relevantValues, allValues);
+        }
+        
+        template<typename ValueType>
+        ValueType computeMaxAbsDiff(std::vector<ValueType> const& allValues, storm::storage::BitVector const& relevantValues, std::vector<ValueType> const& oldValues) {
+            ValueType result = storm::utility::zero<ValueType>();
+            auto oldValueIt = oldValues.begin();
+            for (auto value : relevantValues) {
+                result = storm::utility::max<ValueType>(result, storm::utility::abs<ValueType>(allValues[value] - *oldValueIt));
+            }
+            return result;
+        }
+        
+        template<typename ValueType>
+        ValueType computeMaxAbsDiff(std::vector<ValueType> const& allOldValues, std::vector<ValueType> const& allNewValues, storm::storage::BitVector const& relevantValues) {
+            ValueType result = storm::utility::zero<ValueType>();
+            for (auto value : relevantValues) {
+                result = storm::utility::max<ValueType>(result, storm::utility::abs<ValueType>(allNewValues[value] - allOldValues[value]));
+            }
+            return result;
+        }
+        
         template<typename ValueType>
         bool IterativeMinMaxLinearEquationSolver<ValueType>::solveEquationsSoundValueIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
             STORM_LOG_THROW(this->hasUpperBound(), storm::exceptions::UnmetRequirementException, "Solver requires upper bound, but none was given.");
@@ -407,79 +439,114 @@ namespace storm {
             uint64_t iterations = 0;
             
             Status status = Status::InProgress;
-            ValueType upperDiff;
-            ValueType lowerDiff;
+            bool doConvergenceCheck = true;
+            bool useDiffs = this->hasRelevantValues();
+            std::vector<ValueType> oldValues;
+            if (useGaussSeidelMultiplication && useDiffs) {
+                oldValues.resize(this->getRelevantValues().getNumberOfSetBits());
+            }
+            ValueType maxLowerDiff = storm::utility::zero<ValueType>();
+            ValueType maxUpperDiff = storm::utility::zero<ValueType>();
             ValueType precision = static_cast<ValueType>(this->getSettings().getPrecision());
             if (!this->getSettings().getRelativeTerminationCriterion()) {
                 precision *= storm::utility::convertNumber<ValueType>(2.0);
             }
+            this->startMeasureProgress();
             while (status == Status::InProgress && iterations < this->getSettings().getMaximalNumberOfIterations()) {
                 // Remember in which directions we took steps in this iteration.
                 bool lowerStep = false;
                 bool upperStep = false;
 
                 // In every thousandth iteration, we improve both bounds.
-                if (iterations % 1000 == 0 || lowerDiff == upperDiff) {
+                if (iterations % 1000 == 0 || maxLowerDiff == maxUpperDiff) {
                     lowerStep = true;
                     upperStep = true;
                     if (useGaussSeidelMultiplication) {
-                        lowerDiff = (*lowerX)[0];
+                        if (useDiffs) {
+                            preserveOldRelevantValues(*lowerX, this->getRelevantValues(), oldValues);
+                        }
                         this->linEqSolverA->multiplyAndReduceGaussSeidel(dir, this->A->getRowGroupIndices(), *lowerX, &b);
-                        lowerDiff = (*lowerX)[0] - lowerDiff;
-                        upperDiff = (*upperX)[0];
+                        if (useDiffs) {
+                            maxLowerDiff = computeMaxAbsDiff(*lowerX, this->getRelevantValues(), oldValues);
+                            preserveOldRelevantValues(*upperX, this->getRelevantValues(), oldValues);
+                        }
                         this->linEqSolverA->multiplyAndReduceGaussSeidel(dir, this->A->getRowGroupIndices(), *upperX, &b);
-                        upperDiff = upperDiff - (*upperX)[0];
+                        if (useDiffs) {
+                            maxUpperDiff = computeMaxAbsDiff(*upperX, this->getRelevantValues(), oldValues);
+                        }
                     } else {
                         this->linEqSolverA->multiplyAndReduce(dir, this->A->getRowGroupIndices(), *lowerX, &b, *tmp);
-                        lowerDiff = (*tmp)[0] - (*lowerX)[0];
+                        if (useDiffs) {
+                            maxLowerDiff = computeMaxAbsDiff(*lowerX, *tmp, this->getRelevantValues());
+                        }
                         std::swap(lowerX, tmp);
                         this->linEqSolverA->multiplyAndReduce(dir, this->A->getRowGroupIndices(), *upperX, &b, *tmp);
-                        upperDiff = (*upperX)[0] - (*tmp)[0];
+                        if (useDiffs) {
+                            maxUpperDiff = computeMaxAbsDiff(*upperX, *tmp, this->getRelevantValues());
+                        }
                         std::swap(upperX, tmp);
                     }
                 } else {
                     // In the following iterations, we improve the bound with the greatest difference.
                     if (useGaussSeidelMultiplication) {
-                        if (lowerDiff >= upperDiff) {
-                            lowerDiff = (*lowerX)[0];
+                        if (maxLowerDiff >= maxUpperDiff) {
+                            if (useDiffs) {
+                                preserveOldRelevantValues(*lowerX, this->getRelevantValues(), oldValues);
+                            }
                             this->linEqSolverA->multiplyAndReduceGaussSeidel(dir, this->A->getRowGroupIndices(), *lowerX, &b);
-                            lowerDiff = (*lowerX)[0] - lowerDiff;
+                            if (useDiffs) {
+                                maxLowerDiff = computeMaxAbsDiff(*lowerX, this->getRelevantValues(), oldValues);
+                            }
                             lowerStep = true;
                         } else {
-                            upperDiff = (*upperX)[0];
+                            if (useDiffs) {
+                                preserveOldRelevantValues(*upperX, this->getRelevantValues(), oldValues);
+                            }
                             this->linEqSolverA->multiplyAndReduceGaussSeidel(dir, this->A->getRowGroupIndices(), *upperX, &b);
-                            upperDiff = upperDiff - (*upperX)[0];
+                            if (useDiffs) {
+                                maxUpperDiff = computeMaxAbsDiff(*upperX, this->getRelevantValues(), oldValues);
+                            }
                             upperStep = true;
                         }
                     } else {
-                        if (lowerDiff >= upperDiff) {
+                        if (maxLowerDiff >= maxUpperDiff) {
                             this->linEqSolverA->multiplyAndReduce(dir, this->A->getRowGroupIndices(), *lowerX, &b, *tmp);
-                            lowerDiff = (*tmp)[0] - (*lowerX)[0];
+                            if (useDiffs) {
+                                maxLowerDiff = computeMaxAbsDiff(*lowerX, *tmp, this->getRelevantValues());
+                            }
                             std::swap(tmp, lowerX);
                             lowerStep = true;
                         } else {
                             this->linEqSolverA->multiplyAndReduce(dir, this->A->getRowGroupIndices(), *upperX, &b, *tmp);
-                            upperDiff = (*upperX)[0] - (*tmp)[0];
+                            if (useDiffs) {
+                                maxUpperDiff = computeMaxAbsDiff(*upperX, *tmp, this->getRelevantValues());
+                            }
                             std::swap(tmp, upperX);
                             upperStep = true;
                         }
                     }
                 }
-                STORM_LOG_ASSERT(lowerDiff >= storm::utility::zero<ValueType>(), "Expected non-negative lower diff.");
-                STORM_LOG_ASSERT(upperDiff >= storm::utility::zero<ValueType>(), "Expected non-negative upper diff.");
+                STORM_LOG_ASSERT(maxLowerDiff >= storm::utility::zero<ValueType>(), "Expected non-negative lower diff.");
+                STORM_LOG_ASSERT(maxUpperDiff >= storm::utility::zero<ValueType>(), "Expected non-negative upper diff.");
                 if (iterations % 1000 == 0) {
-                    STORM_LOG_TRACE("Iteration " << iterations << ": lower difference: " << lowerDiff << ", upper difference: " << upperDiff << ".");
+                    STORM_LOG_TRACE("Iteration " << iterations << ": lower difference: " << maxLowerDiff << ", upper difference: " << maxUpperDiff << ".");
                 }
 
-                // Determine whether the method converged.
-                if (this->hasRelevantValues()) {
-                    status = storm::utility::vector::equalModuloPrecision<ValueType>(*lowerX, *upperX, this->getRelevantValues(), precision, this->getSettings().getRelativeTerminationCriterion()) ? Status::Converged : status;
-                } else {
-                    status = storm::utility::vector::equalModuloPrecision<ValueType>(*lowerX, *upperX, precision, this->getSettings().getRelativeTerminationCriterion()) ? Status::Converged : status;
+                if (doConvergenceCheck) {
+                    // Determine whether the method converged.
+                    if (this->hasRelevantValues()) {
+                        status = storm::utility::vector::equalModuloPrecision<ValueType>(*lowerX, *upperX, this->getRelevantValues(), precision, this->getSettings().getRelativeTerminationCriterion()) ? Status::Converged : status;
+                    } else {
+                        status = storm::utility::vector::equalModuloPrecision<ValueType>(*lowerX, *upperX, precision, this->getSettings().getRelativeTerminationCriterion()) ? Status::Converged : status;
+                    }
                 }
                 
+                // Potentially show progress.
+                this->showProgressIterative(iterations);
+                
                 // Update environment variables.
                 ++iterations;
+                doConvergenceCheck = !doConvergenceCheck;
                 if (lowerStep) {
                     status = updateStatusIfNotConverged(status, *lowerX, iterations, SolverGuarantee::LessOrEqual);
                 }
diff --git a/src/storm/solver/LinearEquationSolver.cpp b/src/storm/solver/LinearEquationSolver.cpp
index 8d00d0178..87b4bc45c 100644
--- a/src/storm/solver/LinearEquationSolver.cpp
+++ b/src/storm/solver/LinearEquationSolver.cpp
@@ -46,9 +46,13 @@ namespace storm {
             std::vector<ValueType>* nextX = cachedRowVector.get();
             
             // Now perform matrix-vector multiplication as long as we meet the bound.
+            this->startMeasureProgress();
             for (uint_fast64_t i = 0; i < n; ++i) {
                 this->multiply(*currentX, b, *nextX);
                 std::swap(nextX, currentX);
+
+                // Potentially show progress.
+                this->showProgressIterative(i, n);
             }
             
             // If we performed an odd number of repetitions, we need to swap the contents of currentVector and x,
@@ -164,9 +168,9 @@ namespace storm {
             EquationSolverType actualEquationSolver = coreSettings.getEquationSolver();
             if (generalSettings.isSoundSet()) {
                 if (coreSettings.isEquationSolverSetFromDefaultValue()) {
-                    STORM_LOG_WARN_COND(actualEquationSolver == EquationSolverType::Native, "Switching to native equation solver to guarantee soundness. To select other solvers, please explicitly specify a solver.");
+                    STORM_LOG_INFO_COND(actualEquationSolver == EquationSolverType::Native, "Switching to native equation solver to guarantee soundness. To select other solvers, please explicitly specify a solver.");
                 } else {
-                    STORM_LOG_WARN_COND(actualEquationSolver == EquationSolverType::Native, "Switching to native equation solver from explicitly selected solver '" << storm::solver::toString(actualEquationSolver) << "' to guarantee soundness.");
+                    STORM_LOG_INFO_COND(actualEquationSolver == EquationSolverType::Native, "Switching to native equation solver from explicitly selected solver '" << storm::solver::toString(actualEquationSolver) << "' to guarantee soundness.");
                 }
                 actualEquationSolver = EquationSolverType::Native;
             }
diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp
index 06e690d0d..ca6366869 100644
--- a/src/storm/solver/MinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp
@@ -173,7 +173,7 @@ namespace storm {
                 auto const& minMaxSettings = storm::settings::getModule<storm::settings::modules::MinMaxEquationSolverSettings>();
                 if (std::is_same<ValueType, storm::RationalNumber>::value) {
                     if (minMaxSettings.isMinMaxEquationSolvingMethodSetFromDefaultValue() && minMaxSettings.getMinMaxEquationSolvingMethod() != MinMaxMethod::PolicyIteration) {
-                        STORM_LOG_WARN("Selecting policy iteration as the solution method to guarantee exact results. If you want to override this, please explicitly specify a different method.");
+                        STORM_LOG_INFO("Selecting policy iteration as the solution method to guarantee exact results. If you want to override this, please explicitly specify a different method.");
                         this->setMinMaxMethod(MinMaxMethod::PolicyIteration);
                         wasSet = true;
                     }
diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp
index 5b4a2172d..eb4a0e3c0 100644
--- a/src/storm/solver/NativeLinearEquationSolver.cpp
+++ b/src/storm/solver/NativeLinearEquationSolver.cpp
@@ -163,6 +163,7 @@ namespace storm {
             bool converged = false;
             bool terminate = false;
             
+            this->startMeasureProgress();
             while (!converged && !terminate && iterations < this->getSettings().getMaximalNumberOfIterations()) {
                 A->performSuccessiveOverRelaxationStep(omega, x, b);
                 
@@ -175,6 +176,9 @@ namespace storm {
                     *this->cachedRowVector = x;
                 }
                 
+                // Potentially show progress.
+                this->showProgressIterative(iterations);
+
                 // Increase iteration count so we can abort if convergence is too slow.
                 ++iterations;
             }
@@ -211,6 +215,7 @@ namespace storm {
             bool converged = false;
             bool terminate = false;
 
+            this->startMeasureProgress();
             while (!converged && !terminate && iterations < this->getSettings().getMaximalNumberOfIterations()) {
                 // Compute D^-1 * (b - LU * x) and store result in nextX.
                 multiplier.multAdd(jacobiLU, *currentX, nullptr, *nextX);
@@ -225,6 +230,9 @@ namespace storm {
                 // Swap the two pointers as a preparation for the next iteration.
                 std::swap(nextX, currentX);
                 
+                // Potentially show progress.
+                this->showProgressIterative(iterations);
+                
                 // Increase iteration count so we can abort if convergence is too slow.
                 ++iterations;
             }
@@ -334,6 +342,7 @@ namespace storm {
             // (3) Perform iterations until convergence.
             bool converged = false;
             uint64_t iterations = 0;
+            this->startMeasureProgress();
             while (!converged && iterations < this->getSettings().getMaximalNumberOfIterations()) {
                 // Perform one Walker-Chae step.
                 walkerChaeData->matrix.performWalkerChaeStep(*currentX, walkerChaeData->columnSums, walkerChaeData->b, currentAx, *nextX);
@@ -347,6 +356,9 @@ namespace storm {
                 // Swap the x vectors for the next iteration.
                 std::swap(currentX, nextX);
                 
+                // Potentially show progress.
+                this->showProgressIterative(iterations);
+
                 // Increase iteration count so we can abort if convergence is too slow.
                 ++iterations;
             }
@@ -394,6 +406,7 @@ namespace storm {
             bool converged = false;
             bool terminate = this->terminateNow(*currentX, SolverGuarantee::LessOrEqual);
             uint64_t iterations = 0;
+            this->startMeasureProgress();
             while (!converged && !terminate && iterations < this->getSettings().getMaximalNumberOfIterations()) {
                 if (useGaussSeidelMultiplication) {
                     *nextX = *currentX;
@@ -406,6 +419,9 @@ namespace storm {
                 converged = storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *nextX, static_cast<ValueType>(this->getSettings().getPrecision()), this->getSettings().getRelativeTerminationCriterion());
                 terminate = this->terminateNow(*currentX, SolverGuarantee::LessOrEqual);
                 
+                // Potentially show progress.
+                this->showProgressIterative(iterations);
+
                 // Set up next iteration.
                 std::swap(currentX, nextX);
                 ++iterations;
@@ -424,6 +440,30 @@ namespace storm {
             return converged;
         }
         
+        template<typename ValueType>
+        void preserveOldRelevantValues(std::vector<ValueType> const& allValues, storm::storage::BitVector const& relevantValues, std::vector<ValueType>& oldValues) {
+            storm::utility::vector::selectVectorValues(oldValues, relevantValues, allValues);
+        }
+        
+        template<typename ValueType>
+        ValueType computeMaxAbsDiff(std::vector<ValueType> const& allValues, storm::storage::BitVector const& relevantValues, std::vector<ValueType> const& oldValues) {
+            ValueType result = storm::utility::zero<ValueType>();
+            auto oldValueIt = oldValues.begin();
+            for (auto value : relevantValues) {
+                result = storm::utility::max<ValueType>(result, storm::utility::abs<ValueType>(allValues[value] - *oldValueIt));
+            }
+            return result;
+        }
+        
+        template<typename ValueType>
+        ValueType computeMaxAbsDiff(std::vector<ValueType> const& allOldValues, std::vector<ValueType> const& allNewValues, storm::storage::BitVector const& relevantValues) {
+            ValueType result = storm::utility::zero<ValueType>();
+            for (auto value : relevantValues) {
+                result = storm::utility::max<ValueType>(result, storm::utility::abs<ValueType>(allNewValues[value] - allOldValues[value]));
+            }
+            return result;
+        }
+        
         template<typename ValueType>
         bool NativeLinearEquationSolver<ValueType>::solveEquationsSoundPower(std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
             STORM_LOG_THROW(this->hasLowerBound(), storm::exceptions::UnmetRequirementException, "Solver requires upper bound, but none was given.");
@@ -446,68 +486,96 @@ namespace storm {
             bool terminate = false;
             uint64_t iterations = 0;
             bool doConvergenceCheck = true;
-            ValueType upperDiff;
-            ValueType lowerDiff;
+            bool useDiffs = this->hasRelevantValues();
+            std::vector<ValueType> oldValues;
+            if (useGaussSeidelMultiplication && useDiffs) {
+                oldValues.resize(this->getRelevantValues().getNumberOfSetBits());
+            }
+            ValueType maxLowerDiff = storm::utility::zero<ValueType>();
+            ValueType maxUpperDiff = storm::utility::zero<ValueType>();
             ValueType precision = static_cast<ValueType>(this->getSettings().getPrecision());
             if (!this->getSettings().getRelativeTerminationCriterion()) {
                 precision *= storm::utility::convertNumber<ValueType>(2.0);
             }
+            this->startMeasureProgress();
             while (!converged && !terminate && iterations < this->getSettings().getMaximalNumberOfIterations()) {
                 // Remember in which directions we took steps in this iteration.
                 bool lowerStep = false;
                 bool upperStep = false;
                 
-                // In every thousandth iteration, we improve both bounds.
-                if (iterations % 1000 == 0 || lowerDiff == upperDiff) {
+                // In every thousandth iteration or if the differences are the same, we improve both bounds.
+                if (iterations % 1000 == 0 || maxLowerDiff == maxUpperDiff) {
                     lowerStep = true;
                     upperStep = true;
                     if (useGaussSeidelMultiplication) {
-                        lowerDiff = (*lowerX)[0];
+                        if (useDiffs) {
+                            preserveOldRelevantValues(*lowerX, this->getRelevantValues(), oldValues);
+                        }
                         this->multiplier.multAddGaussSeidelBackward(*this->A, *lowerX, &b);
-                        lowerDiff = (*lowerX)[0] - lowerDiff;
-                        upperDiff = (*upperX)[0];
+                        if (useDiffs) {
+                            maxLowerDiff = computeMaxAbsDiff(*lowerX, this->getRelevantValues(), oldValues);
+                            preserveOldRelevantValues(*upperX, this->getRelevantValues(), oldValues);
+                        }
                         this->multiplier.multAddGaussSeidelBackward(*this->A, *upperX, &b);
-                        upperDiff = upperDiff - (*upperX)[0];
+                        if (useDiffs) {
+                            maxUpperDiff = computeMaxAbsDiff(*upperX, this->getRelevantValues(), oldValues);
+                        }
                     } else {
                         this->multiplier.multAdd(*this->A, *lowerX, &b, *tmp);
-                        lowerDiff = (*tmp)[0] - (*lowerX)[0];
+                        if (useDiffs) {
+                            maxLowerDiff = computeMaxAbsDiff(*lowerX, *tmp, this->getRelevantValues());
+                        }
                         std::swap(tmp, lowerX);
                         this->multiplier.multAdd(*this->A, *upperX, &b, *tmp);
-                        upperDiff = (*upperX)[0] - (*tmp)[0];
+                        if (useDiffs) {
+                            maxUpperDiff = computeMaxAbsDiff(*upperX, *tmp, this->getRelevantValues());
+                        }
                         std::swap(tmp, upperX);
                     }
                 } else {
                     // In the following iterations, we improve the bound with the greatest difference.
                     if (useGaussSeidelMultiplication) {
-                        if (lowerDiff >= upperDiff) {
-                            lowerDiff = (*lowerX)[0];
+                        if (maxLowerDiff >= maxUpperDiff) {
+                            if (useDiffs) {
+                                preserveOldRelevantValues(*lowerX, this->getRelevantValues(), oldValues);
+                            }
                             this->multiplier.multAddGaussSeidelBackward(*this->A, *lowerX, &b);
-                            lowerDiff = (*lowerX)[0] - lowerDiff;
+                            if (useDiffs) {
+                                maxLowerDiff = computeMaxAbsDiff(*lowerX, this->getRelevantValues(), oldValues);
+                            }
                             lowerStep = true;
                         } else {
-                            upperDiff = (*upperX)[0];
+                            if (useDiffs) {
+                                preserveOldRelevantValues(*upperX, this->getRelevantValues(), oldValues);
+                            }
                             this->multiplier.multAddGaussSeidelBackward(*this->A, *upperX, &b);
-                            upperDiff = upperDiff - (*upperX)[0];
+                            if (useDiffs) {
+                                maxUpperDiff = computeMaxAbsDiff(*upperX, this->getRelevantValues(), oldValues);
+                            }
                             upperStep = true;
                         }
                     } else {
-                        if (lowerDiff >= upperDiff) {
+                        if (maxLowerDiff >= maxUpperDiff) {
                             this->multiplier.multAdd(*this->A, *lowerX, &b, *tmp);
-                            lowerDiff = (*tmp)[0] - (*lowerX)[0];
+                            if (useDiffs) {
+                                maxLowerDiff = computeMaxAbsDiff(*lowerX, *tmp, this->getRelevantValues());
+                            }
                             std::swap(tmp, lowerX);
                             lowerStep = true;
                         } else {
                             this->multiplier.multAdd(*this->A, *upperX, &b, *tmp);
-                            upperDiff = (*upperX)[0] - (*tmp)[0];
+                            if (useDiffs) {
+                                maxUpperDiff = computeMaxAbsDiff(*upperX, *tmp, this->getRelevantValues());
+                            }
                             std::swap(tmp, upperX);
                             upperStep = true;
                         }
                     }
                 }
-                STORM_LOG_ASSERT(lowerDiff >= storm::utility::zero<ValueType>(), "Expected non-negative lower diff.");
-                STORM_LOG_ASSERT(upperDiff >= storm::utility::zero<ValueType>(), "Expected non-negative upper diff.");
+                STORM_LOG_ASSERT(maxLowerDiff >= storm::utility::zero<ValueType>(), "Expected non-negative lower diff.");
+                STORM_LOG_ASSERT(maxUpperDiff >= storm::utility::zero<ValueType>(), "Expected non-negative upper diff.");
                 if (iterations % 1000 == 0) {
-                    STORM_LOG_TRACE("Iteration " << iterations << ": lower difference: " << lowerDiff << ", upper difference: " << upperDiff << ".");
+                    STORM_LOG_TRACE("Iteration " << iterations << ": lower difference: " << maxLowerDiff << ", upper difference: " << maxUpperDiff << ".");
                 }
                 
                 if (doConvergenceCheck) {
@@ -527,6 +595,9 @@ namespace storm {
                     }
                 }
                 
+                // Potentially show progress.
+                this->showProgressIterative(iterations);
+                
                 // Set up next iteration.
                 ++iterations;
                 doConvergenceCheck = !doConvergenceCheck;
diff --git a/src/storm/solver/SolveGoal.h b/src/storm/solver/SolveGoal.h
index cd058b656..3d0cab095 100644
--- a/src/storm/solver/SolveGoal.h
+++ b/src/storm/solver/SolveGoal.h
@@ -101,7 +101,8 @@ namespace storm {
                 } else {
                     solver->setTerminationCondition(std::make_unique<TerminateIfFilteredExtremumBelowThreshold<ValueType>>(goal.relevantValues(), goal.boundIsStrict(), goal.thresholdValue(), false));
                 }
-            } else if (goal.hasRelevantValues()) {
+            }
+            if (goal.hasRelevantValues()) {
                 solver->setRelevantValues(std::move(goal.relevantValues()));
             }
             return solver;
diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp
index 03ba63cd9..696fc77f1 100644
--- a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp
@@ -52,9 +52,13 @@ namespace storm {
                 auxiliaryRowGroupVector = std::make_unique<std::vector<ValueType>>(this->A->getRowGroupCount());
             }
             
+            this->startMeasureProgress();
             for (uint64_t i = 0; i < n; ++i) {
                 linEqSolverA->multiplyAndReduce(dir, this->A->getRowGroupIndices(), x, b, *auxiliaryRowGroupVector);
                 std::swap(x, *auxiliaryRowGroupVector);
+
+                // Potentially show progress.
+                this->showProgressIterative(i, n);
             }
             
             if (!this->isCachingEnabled()) {
diff --git a/src/storm/storage/dd/BisimulationDecomposition.cpp b/src/storm/storage/dd/BisimulationDecomposition.cpp
index 6efbd7f5a..c025fb5d3 100644
--- a/src/storm/storage/dd/BisimulationDecomposition.cpp
+++ b/src/storm/storage/dd/BisimulationDecomposition.cpp
@@ -10,7 +10,7 @@
 #include "storm/models/symbolic/StandardRewardModel.h"
 
 #include "storm/settings/SettingsManager.h"
-#include "storm/settings/modules/IOSettings.h"
+#include "storm/settings/modules/GeneralSettings.h"
 
 #include "storm/utility/macros.h"
 #include "storm/exceptions/InvalidOperationException.h"
@@ -32,25 +32,25 @@ namespace storm {
         
         template <storm::dd::DdType DdType, typename ValueType>
         BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, bisimulationType), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, preservationInformation))) {
-            auto const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
-            showProgress = ioSettings.isExplorationShowProgressSet();
-            showProgressDelay = ioSettings.getExplorationShowProgressDelay();
+            auto const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
+            showProgress = generalSettings.isVerboseSet();
+            showProgressDelay = generalSettings.getShowProgressDelay();
             this->refineWrtRewardModels();
         }
         
         template <storm::dd::DdType DdType, typename ValueType>
         BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, formulas, bisimulationType), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, preservationInformation))) {
-            auto const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
-            showProgress = ioSettings.isExplorationShowProgressSet();
-            showProgressDelay = ioSettings.getExplorationShowProgressDelay();
+            auto const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
+            showProgress = generalSettings.isVerboseSet();
+            showProgressDelay = generalSettings.getShowProgressDelay();
             this->refineWrtRewardModels();
         }
         
         template <storm::dd::DdType DdType, typename ValueType>
         BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& initialPartition, bisimulation::PreservationInformation<DdType, ValueType> const& preservationInformation) : model(model), preservationInformation(preservationInformation), refiner(createRefiner(model, initialPartition)) {
-            auto const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
-            showProgress = ioSettings.isExplorationShowProgressSet();
-            showProgressDelay = ioSettings.getExplorationShowProgressDelay();
+            auto const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
+            showProgress = generalSettings.isVerboseSet();
+            showProgressDelay = generalSettings.getShowProgressDelay();
             this->refineWrtRewardModels();
         }
         
diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp
index c423df21f..58771a38d 100644
--- a/src/storm/utility/constants.cpp
+++ b/src/storm/utility/constants.cpp
@@ -189,6 +189,16 @@ namespace storm {
             return std::pow(value, exponent);
         }
 
+        template<typename ValueType>
+        ValueType max(ValueType const& first, ValueType const& second) {
+            return std::max(first, second);
+        }
+        
+        template<typename ValueType>
+        ValueType min(ValueType const& first, ValueType const& second) {
+            return std::min(first, second);
+        }
+        
         template<typename ValueType>
         ValueType sqrt(ValueType const& number) {
             return std::sqrt(number);
@@ -299,7 +309,7 @@ namespace storm {
         ClnRationalNumber convertNumber(std::string const& number) {
             return carl::parse<ClnRationalNumber>(number);
         }
-
+        
         template<>
         ClnRationalNumber sqrt(ClnRationalNumber const& number) {
             return carl::sqrt(number);
@@ -673,6 +683,8 @@ namespace storm {
         template double minimum(std::map<uint64_t, double> const&);
         template double maximum(std::map<uint64_t, double> const&);
         template double pow(double const& value, uint_fast64_t exponent);
+        template double max(double const& first, double const& second);
+        template double min(double const& first, double const& second);
         template double sqrt(double const& number);
         template double abs(double const& number);
         template double floor(double const& number);
@@ -699,6 +711,8 @@ namespace storm {
         template float minimum(std::map<uint64_t, float> const&);
         template float maximum(std::map<uint64_t, float> const&);
         template float pow(float const& value, uint_fast64_t exponent);
+        template float max(float const& first, float const& second);
+        template float min(float const& first, float const& second);
         template float sqrt(float const& number);
         template float abs(float const& number);
         template float floor(float const& number);
@@ -766,6 +780,8 @@ namespace storm {
         template std::pair<storm::ClnRationalNumber, storm::ClnRationalNumber> minmax(std::vector<storm::ClnRationalNumber> const&);
         template storm::ClnRationalNumber minimum(std::vector<storm::ClnRationalNumber> const&);
         template storm::ClnRationalNumber maximum(std::vector<storm::ClnRationalNumber> const&);
+        template storm::ClnRationalNumber max(storm::ClnRationalNumber const& first, storm::ClnRationalNumber const& second);
+        template storm::ClnRationalNumber min(storm::ClnRationalNumber const& first, storm::ClnRationalNumber const& second);
         template storm::ClnRationalNumber pow(storm::ClnRationalNumber const& value, uint_fast64_t exponent);
         template storm::ClnRationalNumber sqrt(storm::ClnRationalNumber const& number);
         template storm::ClnRationalNumber abs(storm::ClnRationalNumber const& number);
@@ -799,6 +815,8 @@ namespace storm {
         template std::pair<storm::GmpRationalNumber, storm::GmpRationalNumber> minmax(std::vector<storm::GmpRationalNumber> const&);
         template storm::GmpRationalNumber minimum(std::vector<storm::GmpRationalNumber> const&);
         template storm::GmpRationalNumber maximum(std::vector<storm::GmpRationalNumber> const&);
+        template storm::GmpRationalNumber max(storm::GmpRationalNumber const& first, storm::GmpRationalNumber const& second);
+        template storm::GmpRationalNumber min(storm::GmpRationalNumber const& first, storm::GmpRationalNumber const& second);
         template storm::GmpRationalNumber pow(storm::GmpRationalNumber const& value, uint_fast64_t exponent);
         template storm::GmpRationalNumber sqrt(storm::GmpRationalNumber const& number);
         template storm::GmpRationalNumber abs(storm::GmpRationalNumber const& number);
diff --git a/src/storm/utility/constants.h b/src/storm/utility/constants.h
index 7669524ba..5c0db58bc 100644
--- a/src/storm/utility/constants.h
+++ b/src/storm/utility/constants.h
@@ -84,6 +84,12 @@ namespace storm {
         template<typename ValueType>
         ValueType pow(ValueType const& value, uint_fast64_t exponent);
 
+        template<typename ValueType>
+        ValueType max(ValueType const& first, ValueType const& second);
+
+        template<typename ValueType>
+        ValueType min(ValueType const& first, ValueType const& second);
+
         template<typename ValueType>
         ValueType sqrt(ValueType const& number);
         
diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h
index ff60d5946..0bb468043 100644
--- a/src/storm/utility/vector.h
+++ b/src/storm/utility/vector.h
@@ -151,9 +151,10 @@ namespace storm {
              */
             template<class T>
             void selectVectorValues(std::vector<T>& vector, storm::storage::BitVector const& positions, std::vector<T> const& values) {
-                uint_fast64_t oldPosition = 0;
+                auto targetIt = vector.begin();
                 for (auto position : positions) {
-                    vector[oldPosition++] = values[position];
+                    *targetIt = values[position];
+                    ++targetIt;
                 }
             }
 
@@ -167,10 +168,10 @@ namespace storm {
              */
             template<class T>
             void selectVectorValues(std::vector<T>& vector, storm::storage::BitVector const& positions, std::vector<uint_fast64_t> const& rowGrouping, std::vector<T> const& values) {
-                uint_fast64_t oldPosition = 0;
+                auto targetIt = vector.begin();
                 for (auto position : positions) {
-                    for (uint_fast64_t i = rowGrouping[position]; i < rowGrouping[position + 1]; ++i) {
-                        vector[oldPosition++] = values[i];
+                    for (uint_fast64_t i = rowGrouping[position]; i < rowGrouping[position + 1]; ++i, ++targetIt) {
+                        *targetIt = values[i];
                     }
                 }
             }
@@ -186,8 +187,9 @@ namespace storm {
              */
             template<class T>
             void selectVectorValues(std::vector<T>& vector, std::vector<uint_fast64_t> const& rowGroupToRowIndexMapping, std::vector<uint_fast64_t> const& rowGrouping, std::vector<T> const& values) {
-                for (uint_fast64_t i = 0; i < vector.size(); ++i) {
-                    vector[i] = values[rowGrouping[i] + rowGroupToRowIndexMapping[i]];
+                auto targetIt = vector.begin();
+                for (uint_fast64_t i = 0; i < vector.size(); ++i, ++targetIt) {
+                    *targetIt = values[rowGrouping[i] + rowGroupToRowIndexMapping[i]];
                 }
             }
             
@@ -216,10 +218,10 @@ namespace storm {
              */
             template<class T>
             void selectVectorValuesRepeatedly(std::vector<T>& vector, storm::storage::BitVector const& positions, std::vector<uint_fast64_t> const& rowGrouping, std::vector<T> const& values) {
-                uint_fast64_t oldPosition = 0;
+                auto targetIt = vector.begin();
                 for (auto position : positions) {
-                    for (uint_fast64_t i = rowGrouping[position]; i < rowGrouping[position + 1]; ++i) {
-                        vector[oldPosition++] = values[position];
+                    for (uint_fast64_t i = rowGrouping[position]; i < rowGrouping[position + 1]; ++i, ++targetIt) {
+                        *targetIt = values[position];
                     }
                 }
             }
@@ -238,14 +240,12 @@ namespace storm {
             
             template<class T>
             void addFilteredVectorGroupsToGroupedVector(std::vector<T>& target, std::vector<T> const& source, storm::storage::BitVector const& filter, std::vector<uint_fast64_t> const& rowGroupIndices) {
-                uint_fast64_t currentPosition = 0;
+                auto targetIt = target.begin();
                 for (auto group : filter) {
                     auto it = source.cbegin() + rowGroupIndices[group];
                     auto ite = source.cbegin() + rowGroupIndices[group + 1];
-                    while (it != ite) {
-                        target[currentPosition] += *it;
-                        ++currentPosition;
-                        ++it;
+                    for (; it != ite; ++targetIt, ++it) {
+                        *targetIt += *it;
                     }
                 }
             }
@@ -269,10 +269,8 @@ namespace storm {
                     uint_fast64_t current = *rowGroupIt;
                     ++rowGroupIt;
                     uint_fast64_t next = *rowGroupIt;
-                    while (current < next) {
+                    for (; current < next; ++targetIt, ++current) {
                         *targetIt += *sourceIt;
-                        ++targetIt;
-                        ++current;
                     }
                 }
             }
@@ -287,14 +285,12 @@ namespace storm {
              */
             template<class T>
             void addFilteredVectorToGroupedVector(std::vector<T>& target, std::vector<T> const& source, storm::storage::BitVector const& filter, std::vector<uint_fast64_t> const& rowGroupIndices) {
-                uint_fast64_t currentPosition = 0;
+                auto targetIt = target.begin();
                 for (auto group : filter) {
                     uint_fast64_t current = rowGroupIndices[group];
                     uint_fast64_t next = rowGroupIndices[group + 1];
-                    while (current < next) {
-                        target[currentPosition] += source[group];
-                        ++currentPosition;
-                        ++current;
+                    for (; current < next; ++current, ++targetIt) {
+                        *targetIt += source[group];
                     }
                 }
             }