diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
index b927b6203..80ba611aa 100644
--- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
+++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
@@ -494,7 +494,7 @@ namespace storm {
                             storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(state));
                             
                             for (auto element : transitionMatrix.getRow(nondeterministicChoiceIndices[state])) {
-                                constraint = constraint - storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(element.getColumn()));
+                                constraint = constraint - storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(element.getColumn())) * storm::expressions::Expression::createDoubleLiteral(element.getValue());
                             }
                             
                             constraint = constraint + storm::expressions::Expression::createDoubleLiteral(storm::utility::constantOne<ValueType>() / exitRates[state]) * storm::expressions::Expression::createDoubleVariable("k");
@@ -512,7 +512,7 @@ namespace storm {
                                 storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(state));
 
                                 for (auto element : transitionMatrix.getRow(choice)) {
-                                    constraint = constraint - storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(element.getColumn()));
+                                    constraint = constraint - storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(element.getColumn())) *  storm::expressions::Expression::createDoubleLiteral(element.getValue());
                                 }
                                 
                                 storm::expressions::Expression rightHandSide = storm::expressions::Expression::createDoubleLiteral(storm::utility::constantZero<ValueType>());
diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp
index d8b9284d9..53d31f6f0 100644
--- a/src/settings/SettingsManager.cpp
+++ b/src/settings/SettingsManager.cpp
@@ -110,6 +110,9 @@ namespace storm {
             if (optionActive) {
                 setOptionsArguments(activeOptionName, activeOptionIsShortName ? this->shortNameToOptions : this->longNameToOptions, argumentCache);
             }
+            
+            // Finally check whether all modules are okay with the current settings.
+            this->checkAllModules();
         }
         
         void SettingsManager::setFromConfigurationFile(std::string const& configFilename) {
@@ -325,6 +328,12 @@ namespace storm {
             }
         }
         
+        void SettingsManager::checkAllModules() const {
+            for (auto const& nameModulePair : this->modules) {
+                nameModulePair.second->check();
+            }
+        }
+        
         SettingsManager const& manager() {
             return SettingsManager::manager();
         }
diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h
index 94d309813..1c77e1d56 100644
--- a/src/settings/SettingsManager.h
+++ b/src/settings/SettingsManager.h
@@ -179,6 +179,11 @@ namespace storm {
              */
             static void addOptionToMap(std::string const& name, std::shared_ptr<Option> const& option, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>>& optionMap);
             
+            /*!
+             * Checks all modules for consistency by calling their respective check method.
+             */
+            void checkAllModules() const;
+            
             /*!
              * Retrieves the (print) length of the longest option of all modules.
              *
diff --git a/src/settings/modules/CounterexampleGeneratorSettings.cpp b/src/settings/modules/CounterexampleGeneratorSettings.cpp
index e2e29834d..6191b1643 100644
--- a/src/settings/modules/CounterexampleGeneratorSettings.cpp
+++ b/src/settings/modules/CounterexampleGeneratorSettings.cpp
@@ -1,6 +1,7 @@
 #include "src/settings/modules/CounterexampleGeneratorSettings.h"
 
 #include "src/settings/SettingsManager.h"
+#include "src/exceptions/InvalidSettingsException.h"
 
 namespace storm {
     namespace settings {
@@ -19,7 +20,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, schedulerCutsOptionName, true, "Sets whether to add the scheduler cuts for MILP-based minimal command counterexample generation.").build());
             }
             
-            bool CounterexampleGeneratorSettings::isMinimalCommandGenerationSet() const {
+            bool CounterexampleGeneratorSettings::isMinimalCommandSetGenerationSet() const {
                 return this->getOption(minimalCommandSetOptionName).getHasOptionBeenSet();
             }
             
@@ -40,6 +41,18 @@ namespace storm {
                 return this->getOption(schedulerCutsOptionName).getHasOptionBeenSet();
             }
             
+            bool CounterexampleGeneratorSettings::check() const {
+                // Ensure that the model was given either symbolically or explicitly.
+                STORM_LOG_THROW(!isMinimalCommandSetGenerationSet() || storm::settings::generalSettings().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "For the generation of a minimal command set, the model has to be specified symbolically.");
+                
+                if (isMinimalCommandSetGenerationSet()) {
+                    STORM_LOG_WARN_COND(isUseMaxSatBasedMinimalCommandSetGenerationSet() || !isEncodeReachabilitySet(), "Encoding reachability is only available for the MaxSat-based minimal command set generation, so selecting it has no effect.");
+                    STORM_LOG_WARN_COND(isUseMilpBasedMinimalCommandSetGenerationSet() || !isUseSchedulerCutsSet(), "Using scheduler cuts is only available for the MaxSat-based minimal command set generation, so selecting it has no effect.");
+                }
+                
+                return true;
+            }
+            
         } // namespace modules
     } // namespace settings
 } // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/CounterexampleGeneratorSettings.h b/src/settings/modules/CounterexampleGeneratorSettings.h
index 680224b5a..049747183 100644
--- a/src/settings/modules/CounterexampleGeneratorSettings.h
+++ b/src/settings/modules/CounterexampleGeneratorSettings.h
@@ -24,7 +24,7 @@ namespace storm {
                  *
                  * @return True iff a minimal command set counterexample is to be generated.
                  */
-                bool isMinimalCommandGenerationSet() const;
+                bool isMinimalCommandSetGenerationSet() const;
                 
                 /*!
                  * Retrieves whether the MILP-based technique is to be used to generate a minimal command set
@@ -58,6 +58,8 @@ namespace storm {
                  */
                 bool isUseSchedulerCutsSet() const;
                 
+                bool check() const override;
+                
                 // The name of the module.
                 static const std::string moduleName;
                 
diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp
index 45d3b58a6..585bcfdfb 100644
--- a/src/settings/modules/GeneralSettings.cpp
+++ b/src/settings/modules/GeneralSettings.cpp
@@ -2,6 +2,7 @@
 
 #include "src/settings/SettingsManager.h"
 #include "src/settings/SettingMemento.h"
+#include "src/exceptions/InvalidSettingsException.h"
 
 namespace storm {
     namespace settings {
@@ -266,6 +267,17 @@ namespace storm {
                 return this->getOption(statisticsOptionName).getHasOptionBeenSet();
             }
             
+            bool GeneralSettings::check() const {
+                // Ensure that the model was given either symbolically or explicitly.
+                STORM_LOG_THROW(!isSymbolicSet() || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format, but not both.");
+                
+                // Make sure that one "source" for properties is given.
+                uint_fast64_t propertySources = 0 + (isPctlPropertySet() ? 1 : 0) + (isPctlFileSet() ? 1 : 0) + (isCslPropertySet() ? + 1 : 0) + (isCslFileSet() ? 1 : 0) + (isLtlPropertySet() ? 1 : 0) + (isLtlFileSet() ? 1 : 0);
+                STORM_LOG_THROW(propertySources <= 1, storm::exceptions::InvalidSettingsException, "Please specify exactly one source of properties.");
+                
+                return true;
+            }
+            
         } // namespace modules
     } // namespace settings
 } // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h
index 10e4aa77d..75f48d8f1 100644
--- a/src/settings/modules/GeneralSettings.h
+++ b/src/settings/modules/GeneralSettings.h
@@ -313,6 +313,8 @@ namespace storm {
                  * @return True iff statistics are to be shown for counterexample generation.
                  */
                 bool isShowStatisticsSet() const;
+                
+                bool check() const override;
 
                 // The name of the module.
                 static const std::string moduleName;
diff --git a/src/settings/modules/GlpkSettings.cpp b/src/settings/modules/GlpkSettings.cpp
index c45eb93a5..030a69006 100644
--- a/src/settings/modules/GlpkSettings.cpp
+++ b/src/settings/modules/GlpkSettings.cpp
@@ -19,10 +19,22 @@ namespace storm {
                 return this->getOption(outputOptionName).getHasOptionBeenSet();
             }
             
+            bool GlpkSettings::isIntegerToleranceSet() const {
+                return this->getOption(integerToleranceOption).getHasOptionBeenSet();
+            }
+            
             double GlpkSettings::getIntegerTolerance() const {
                 return this->getOption(integerToleranceOption).getArgumentByName("value").getValueAsDouble();
             }
             
+            bool GlpkSettings::check() const {
+                if (isOutputSet() || isIntegerToleranceSet()) {
+                    STORM_LOG_WARN_COND(storm::settings::generalSettings().getLpSolver() == storm::settings::modules::GeneralSettings::LpSolver::glpk, "glpk is not selected as the used LP solver, so setting options for glpk has no effect.");
+                }
+                
+                return true;
+            }
+            
         } // namespace modules
     } // namespace settings
 } // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/GlpkSettings.h b/src/settings/modules/GlpkSettings.h
index c23b2add0..b58e91746 100644
--- a/src/settings/modules/GlpkSettings.h
+++ b/src/settings/modules/GlpkSettings.h
@@ -26,6 +26,13 @@ namespace storm {
                  */
                 bool isOutputSet() const;
                 
+                /*!
+                 * Retrieves whether the integer tolerance has been set.
+                 *
+                 * @return True iff the integer tolerance has been set.
+                 */
+                bool isIntegerToleranceSet() const;
+                
                 /*!
                  * Retrieves the integer tolerance to be used.
                  *
@@ -33,6 +40,8 @@ namespace storm {
                  */
                 double getIntegerTolerance() const;
                 
+                bool check() const override;
+                
                 // The name of the module.
                 static const std::string moduleName;
                 
diff --git a/src/settings/modules/GmmxxEquationSolverSettings.cpp b/src/settings/modules/GmmxxEquationSolverSettings.cpp
index c9c8b1840..4b9f27f9e 100644
--- a/src/settings/modules/GmmxxEquationSolverSettings.cpp
+++ b/src/settings/modules/GmmxxEquationSolverSettings.cpp
@@ -32,6 +32,10 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
             }
             
+            bool GmmxxEquationSolverSettings::isLinearEquationSystemTechniqueSet() const {
+                return this->getOption(techniqueOptionName).getHasOptionBeenSet();
+            }
+            
             GmmxxEquationSolverSettings::LinearEquationTechnique GmmxxEquationSolverSettings::getLinearEquationSystemTechnique() const {
                 std::string linearEquationSystemTechniqueAsString = this->getOption(techniqueOptionName).getArgumentByName("name").getValueAsString();
                 if (linearEquationSystemTechniqueAsString == "bicgstab") {
@@ -46,6 +50,10 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown solution technique '" << linearEquationSystemTechniqueAsString << "' selected.");
             }
             
+            bool GmmxxEquationSolverSettings::isPreconditioningTechniqueSet() const {
+                return this->getOption(preconditionOptionName).getHasOptionBeenSet();
+            }
+            
             GmmxxEquationSolverSettings::PreconditioningTechnique GmmxxEquationSolverSettings::getPreconditioningTechnique() const {
                 std::string preconditioningTechniqueAsString = this->getOption(preconditionOptionName).getArgumentByName("name").getValueAsString();
                 if (preconditioningTechniqueAsString == "ilu") {
@@ -58,22 +66,46 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown preconditioning technique '" << preconditioningTechniqueAsString << "' selected.");
             }
             
+            bool GmmxxEquationSolverSettings::isRestartIterationCountSet() const {
+                return this->getOption(restartOptionName).getHasOptionBeenSet();
+            }
+            
             uint_fast64_t GmmxxEquationSolverSettings::getRestartIterationCount() const {
                 return this->getOption(restartOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
             }
             
+            bool GmmxxEquationSolverSettings::isMaximalIterationCountSet() const {
+                return this->getOption(maximalIterationsOptionName).getHasOptionBeenSet();
+            }
+            
             uint_fast64_t GmmxxEquationSolverSettings::getMaximalIterationCount() const {
                 return this->getOption(maximalIterationsOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
             }
             
+            bool GmmxxEquationSolverSettings::isPrecisionSet() const {
+                return this->getOption(precisionOptionName).getHasOptionBeenSet();
+            }
+            
             double GmmxxEquationSolverSettings::getPrecision() const {
                 return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
             }
             
+            bool GmmxxEquationSolverSettings::isConvergenceCriterionSet() const {
+                return this->getOption(absoluteOptionName).getHasOptionBeenSet();
+            }
+            
             GmmxxEquationSolverSettings::ConvergenceCriterion GmmxxEquationSolverSettings::getConvergenceCriterion() const {
                 return this->getOption(absoluteOptionName).getHasOptionBeenSet() ? GmmxxEquationSolverSettings::ConvergenceCriterion::Absolute : GmmxxEquationSolverSettings::ConvergenceCriterion::Relative;
             }
             
+            bool GmmxxEquationSolverSettings::check() const {
+                bool optionsSet = isLinearEquationSystemTechniqueSet() || isPreconditioningTechniqueSet() || isRestartIterationCountSet() | isMaximalIterationCountSet() || isPrecisionSet() || isConvergenceCriterionSet();
+                
+                STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver() == storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx || !optionsSet, "gmm++ is not selected as the equation solver, so setting options for gmm++ has no effect.");
+                
+                return true;
+            }
+            
         } // namespace modules
     } // namespace settings
 } // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/GmmxxEquationSolverSettings.h b/src/settings/modules/GmmxxEquationSolverSettings.h
index 7504f7456..07bc90174 100644
--- a/src/settings/modules/GmmxxEquationSolverSettings.h
+++ b/src/settings/modules/GmmxxEquationSolverSettings.h
@@ -28,6 +28,13 @@ namespace storm {
                  */
                 GmmxxEquationSolverSettings(storm::settings::SettingsManager& settingsManager);
                 
+                /*!
+                 * Retrieves whether the linear equation system technique has been set.
+                 *
+                 * @return True iff the linear equation system technique has been set.
+                 */
+                bool isLinearEquationSystemTechniqueSet() const;
+                
                 /*!
                  * Retrieves the technique that is to be used for solving systems of linear equations.
                  *
@@ -35,6 +42,13 @@ namespace storm {
                  */
                 LinearEquationTechnique getLinearEquationSystemTechnique() const;
                 
+                /*!
+                 * Retrieves whether the preconditioning technique has been set.
+                 *
+                 * @return True iff the preconditioning technique has been set.
+                 */
+                bool isPreconditioningTechniqueSet() const;
+                
                 /*!
                  * Retrieves the technique that is to be used for preconditioning solving systems of linear equations.
                  *
@@ -42,6 +56,13 @@ namespace storm {
                  */
                 PreconditioningTechnique getPreconditioningTechnique() const;
                 
+                /*!
+                 * Retrieves whether the restart iteration count has been set.
+                 *
+                 * @return True iff the restart iteration count has been set.
+                 */
+                bool isRestartIterationCountSet() const;
+                
                 /*!
                  * Retrieves the number of iterations after which restarted techniques are to be restarted.
                  *
@@ -49,6 +70,13 @@ namespace storm {
                  */
                 uint_fast64_t getRestartIterationCount() const;
                 
+                /*!
+                 * Retrieves whether the maximal iteration count has been set.
+                 *
+                 * @return True iff the maximal iteration count has been set.
+                 */
+                bool isMaximalIterationCountSet() const;
+                
                 /*!
                  * Retrieves the maximal number of iterations to perform until giving up on converging.
                  *
@@ -56,6 +84,13 @@ namespace storm {
                  */
                 uint_fast64_t getMaximalIterationCount() const;
                 
+                /*!
+                 * Retrieves whether the precision has been set.
+                 *
+                 * @return True iff the precision has been set.
+                 */
+                bool isPrecisionSet() const;
+                
                 /*!
                  * Retrieves the precision that is used for detecting convergence.
                  *
@@ -63,6 +98,13 @@ namespace storm {
                  */
                 double getPrecision() const;
                 
+                /*!
+                 * Retrieves whether the convergence criterion has been set.
+                 *
+                 * @return True iff the convergence criterion has been set.
+                 */
+                bool isConvergenceCriterionSet() const;
+                
                 /*!
                  * Retrieves the selected convergence criterion.
                  *
@@ -70,6 +112,8 @@ namespace storm {
                  */
                 ConvergenceCriterion getConvergenceCriterion() const;
                 
+                bool check() const override;
+                
                 // The name of the module.
                 static const std::string moduleName;
                 
diff --git a/src/settings/modules/GurobiSettings.cpp b/src/settings/modules/GurobiSettings.cpp
index 1038fce26..86751cc1d 100644
--- a/src/settings/modules/GurobiSettings.cpp
+++ b/src/settings/modules/GurobiSettings.cpp
@@ -19,10 +19,18 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, integerToleranceOption, true, "Sets Gurobi's precision for integer variables.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
             }
             
+            bool GurobiSettings::isIntegerToleranceSet() const {
+                return this->getOption(integerToleranceOption).getHasOptionBeenSet();
+            }
+            
             double GurobiSettings::getIntegerTolerance() const {
                 return this->getOption(integerToleranceOption).getArgumentByName("value").getValueAsDouble();
             }
             
+            bool GurobiSettings::isNumberOfThreadsSet() const {
+                return this->getOption(threadsOption).getHasOptionBeenSet();
+            }
+            
             uint_fast64_t GurobiSettings::getNumberOfThreads() const {
                 return this->getOption(threadsOption).getArgumentByName("count").getValueAsUnsignedInteger();
             }
@@ -31,6 +39,14 @@ namespace storm {
                 return this->getOption(outputOption).getHasOptionBeenSet();
             }
             
+            bool GurobiSettings::check() const {
+                if (isOutputSet() || isIntegerToleranceSet() || isNumberOfThreadsSet()) {
+                    STORM_LOG_WARN_COND(storm::settings::generalSettings().getLpSolver() == storm::settings::modules::GeneralSettings::LpSolver::Gurobi, "Gurobi is not selected as the used LP solver, so setting options for Gurobi has no effect.");
+                }
+                
+                return true;
+            }
+            
         } // namespace modules
     } // namespace settings
 } // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/GurobiSettings.h b/src/settings/modules/GurobiSettings.h
index d0e92127b..ce7fcd78f 100644
--- a/src/settings/modules/GurobiSettings.h
+++ b/src/settings/modules/GurobiSettings.h
@@ -19,6 +19,13 @@ namespace storm {
                  */
                 GurobiSettings(storm::settings::SettingsManager& settingsManager);
                 
+                /*!
+                 * Retrieves whether the integer tolerance has been set.
+                 *
+                 * @return True iff the integer tolerance has been set.
+                 */
+                bool isIntegerToleranceSet() const;
+                
                 /*!
                  * Retrieves the integer tolerance to be used.
                  *
@@ -26,6 +33,13 @@ namespace storm {
                  */
                 double getIntegerTolerance() const;
                 
+                /*!
+                 * Retrieves whether the number of threads has been set.
+                 *
+                 * @return True iff the number of threads has been set.
+                 */
+                bool isNumberOfThreadsSet() const;
+                
                 /*!
                  * Retrieves the maximal number of threads Gurobi is allowed to use.
                  *
@@ -40,6 +54,8 @@ namespace storm {
                  */
                 bool isOutputSet() const;
                 
+                bool check() const override;
+                
                 // The name of the module.
                 static const std::string moduleName;
                 
diff --git a/src/settings/modules/NativeEquationSolverSettings.cpp b/src/settings/modules/NativeEquationSolverSettings.cpp
index b03feece6..76af99b3e 100644
--- a/src/settings/modules/NativeEquationSolverSettings.cpp
+++ b/src/settings/modules/NativeEquationSolverSettings.cpp
@@ -24,6 +24,10 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
             }
             
+            bool NativeEquationSolverSettings::isLinearEquationSystemTechniqueSet() const {
+                return this->getOption(techniqueOptionName).getHasOptionBeenSet();
+            }
+            
             NativeEquationSolverSettings::LinearEquationTechnique NativeEquationSolverSettings::getLinearEquationSystemTechnique() const {
                 std::string linearEquationSystemTechniqueAsString = this->getOption(techniqueOptionName).getArgumentByName("name").getValueAsString();
                 if (linearEquationSystemTechniqueAsString == "jacobi") {
@@ -32,18 +36,38 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown solution technique '" << linearEquationSystemTechniqueAsString << "' selected.");
             }
             
+            bool NativeEquationSolverSettings::isMaximalIterationCountSet() const {
+                return this->getOption(maximalIterationsOptionName).getHasOptionBeenSet();
+            }
+            
             uint_fast64_t NativeEquationSolverSettings::getMaximalIterationCount() const {
                 return this->getOption(maximalIterationsOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
             }
             
+            bool NativeEquationSolverSettings::isPrecisionSet() const {
+                return this->getOption(precisionOptionName).getHasOptionBeenSet();
+            }
+            
             double NativeEquationSolverSettings::getPrecision() const {
                 return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
             }
             
+            bool NativeEquationSolverSettings::isConvergenceCriterionSet() const {
+                return this->getOption(absoluteOptionName).getHasOptionBeenSet();
+            }
+            
             NativeEquationSolverSettings::ConvergenceCriterion NativeEquationSolverSettings::getConvergenceCriterion() const {
                 return this->getOption(absoluteOptionName).getHasOptionBeenSet() ? NativeEquationSolverSettings::ConvergenceCriterion::Absolute : NativeEquationSolverSettings::ConvergenceCriterion::Relative;
             }
             
+            bool NativeEquationSolverSettings::check() const {
+                bool optionSet = isLinearEquationSystemTechniqueSet() || isMaximalIterationCountSet() || isPrecisionSet() || isConvergenceCriterionSet();
+                
+                STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver() == storm::settings::modules::GeneralSettings::EquationSolver::Native || !optionSet, "Native is not selected as the equation solver, so setting options for native has no effect.");
+                
+                return true;
+            }
+            
         } // namespace modules
     } // namespace settings
 } // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/NativeEquationSolverSettings.h b/src/settings/modules/NativeEquationSolverSettings.h
index 826d40941..9d6e43ecd 100644
--- a/src/settings/modules/NativeEquationSolverSettings.h
+++ b/src/settings/modules/NativeEquationSolverSettings.h
@@ -25,6 +25,13 @@ namespace storm {
                  */
                 NativeEquationSolverSettings(storm::settings::SettingsManager& settingsManager);
                 
+                /*!
+                 * Retrieves whether the linear equation system technique has been set.
+                 *
+                 * @return True iff the linear equation system technique has been set.
+                 */
+                bool isLinearEquationSystemTechniqueSet() const;
+                
                 /*!
                  * Retrieves the technique that is to be used for solving systems of linear equations.
                  *
@@ -32,6 +39,13 @@ namespace storm {
                  */
                 LinearEquationTechnique getLinearEquationSystemTechnique() const;
                 
+                /*!
+                 * Retrieves whether the maximal iteration count has been set.
+                 *
+                 * @return True iff the maximal iteration count has been set.
+                 */
+                bool isMaximalIterationCountSet() const;
+                
                 /*!
                  * Retrieves the maximal number of iterations to perform until giving up on converging.
                  *
@@ -39,6 +53,13 @@ namespace storm {
                  */
                 uint_fast64_t getMaximalIterationCount() const;
                 
+                /*!
+                 * Retrieves whether the precision has been set.
+                 *
+                 * @return True iff the precision has been set.
+                 */
+                bool isPrecisionSet() const;
+                
                 /*!
                  * Retrieves the precision that is used for detecting convergence.
                  *
@@ -46,6 +67,13 @@ namespace storm {
                  */
                 double getPrecision() const;
                 
+                /*!
+                 * Retrieves whether the convergence criterion has been set.
+                 *
+                 * @return True iff the convergence criterion has been set.
+                 */
+                bool isConvergenceCriterionSet() const;
+                
                 /*!
                  * Retrieves the selected convergence criterion.
                  *
@@ -53,6 +81,8 @@ namespace storm {
                  */
                 ConvergenceCriterion getConvergenceCriterion() const;
                 
+                bool check() const override;
+                
                 // The name of the module.
                 static const std::string moduleName;
                 
diff --git a/src/utility/cli.h b/src/utility/cli.h
index b428ef4aa..d0110e67f 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -259,7 +259,7 @@ namespace storm {
             }
             
             void generateCounterexample(std::shared_ptr<storm::models::AbstractModel<double>> model, std::shared_ptr<storm::properties::prctl::AbstractPrctlFormula<double>> const& formula) {
-                if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandGenerationSet()) {
+                if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) {
                     STORM_LOG_THROW(model->getType() == storm::models::MDP, storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for MDPs.");
                     STORM_LOG_THROW(storm::settings::generalSettings().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "Minimal command set generation is only available for symbolic models.");
                     
diff --git a/src/utility/macros.h b/src/utility/macros.h
index 511fdcc12..795f16e96 100644
--- a/src/utility/macros.h
+++ b/src/utility/macros.h
@@ -44,14 +44,48 @@ extern log4cplus::Logger logger;
     LOG4CPLUS_WARN(logger, message);            \
 } while (false)
 
+#define STORM_LOG_WARN_COND(cond, message)      \
+{                                               \
+    if (!(cond)) {                              \
+        LOG4CPLUS_WARN(logger, message);        \
+    }                                           \
+} while (false)
+
 #define STORM_LOG_INFO(message)                 \
 {                                               \
     LOG4CPLUS_INFO(logger, message);            \
 } while (false)
 
+#define STORM_LOG_INFO_COND(cond, message)      \
+{                                               \
+    if (!(cond)) {                              \
+        LOG4CPLUS_INFO(logger, message);        \
+    }                                           \
+} while (false)
+
 #define STORM_LOG_ERROR(message)                \
 {                                               \
     LOG4CPLUS_ERROR(logger, message);           \
 } while (false)
 
+#define STORM_LOG_ERROR_COND(cond, message)     \
+{                                               \
+    if (!(cond)) {                              \
+        LOG4CPLUS_ERROR(logger, message);       \
+    }                                           \
+} while (false)
+
+/*!
+ * Define the macros that print information and optionally also log it.
+ */
+#define STORM_PRINT(message)                    \
+{                                               \
+    STORM_LOG_INFO(message);                    \
+}
+
+#define STORM_PRINT_AND_LOG(message)            \
+{                                               \
+    STORM_PRINT(message);                       \
+}
+
 #endif /* STORM_UTILITY_MACROS_H_ */
\ No newline at end of file