diff --git a/src/settings/Argument.h b/src/settings/Argument.h
index a9fe0f268..d0471c01b 100644
--- a/src/settings/Argument.h
+++ b/src/settings/Argument.h
@@ -43,7 +43,7 @@ namespace storm {
              * to this argument.
              * @param isOptional A flag indicating whether the argument is optional.
              */
-			Argument(std::string const& name, std::string const& description, std::vector<userValidationFunction_t> const& validationFunctions): ArgumentBase(name, description), argumentValue(), argumentType(ArgumentTypeInferation::inferToEnumType<T>()), validationFunctions(validationFunctions), isOptional(false), defaultValue(), hasDefaultValue(false) {
+			Argument(std::string const& name, std::string const& description, std::vector<userValidationFunction_t> const& validationFunctions): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType<T>()), validationFunctions(validationFunctions), isOptional(false), defaultValue(), hasDefaultValue(false) {
                 // Intentionally left empty.
 			}
             
@@ -56,9 +56,9 @@ namespace storm {
              * to this argument.
              * @param isOptional A flag indicating whether the argument is optional.
              */
-			Argument(std::string const& name, std::string const& description, std::vector<userValidationFunction_t> const& validationFunctions, bool isOptional, T defaultValue): ArgumentBase(name, description), argumentValue(), argumentType(ArgumentTypeInferation::inferToEnumType<T>()), validationFunctions(validationFunctions), isOptional(isOptional), defaultValue(defaultValue), hasDefaultValue(true) {
-                // Intentionally left empty.
-			}
+			Argument(std::string const& name, std::string const& description, std::vector<userValidationFunction_t> const& validationFunctions, bool isOptional, T defaultValue): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType<T>()), validationFunctions(validationFunctions), isOptional(isOptional), defaultValue(), hasDefaultValue(true) {
+                this->setDefaultValue(defaultValue);
+            }
             
             virtual bool getIsOptional() const override {
                 return this->isOptional;
@@ -106,8 +106,12 @@ namespace storm {
              * @return The value of the argument.
              */
 			T const& getArgumentValue() const {
-                LOG_THROW(this->getHasBeenSet(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve value of argument, because it was not set.");
-				return this->argumentValue;
+                LOG_THROW(this->getHasBeenSet() || this->getHasDefaultValue(), storm::exceptions::IllegalFunctionCallException, "Unable to retrieve value of argument, because it was neither set nor specifies a default value.");
+                if (this->getHasBeenSet()) {
+                    return this->argumentValue;
+                } else {
+                    return this->defaultValue;
+                }
 			}
             
 			virtual bool getHasDefaultValue() const override {
@@ -123,9 +127,9 @@ namespace storm {
 			virtual std::string getValueAsString() const override {
 				switch (this->argumentType) {
 					case ArgumentType::String:
-						return ArgumentTypeInferation::inferToString(ArgumentType::String, this->getArgumentValue());
+						return inferToString(ArgumentType::String, this->getArgumentValue());
 					case ArgumentType::Boolean: {
-						bool iValue = ArgumentTypeInferation::inferToBoolean(ArgumentType::Boolean, this->getArgumentValue());
+						bool iValue = inferToBoolean(ArgumentType::Boolean, this->getArgumentValue());
 						if (iValue) {
 							return "true";
 						} else {
@@ -139,7 +143,7 @@ namespace storm {
 			virtual int_fast64_t getValueAsInteger() const override {
 				switch (this->argumentType) {
 					case ArgumentType::Integer:
-						return ArgumentTypeInferation::inferToInteger(ArgumentType::Integer, this->getArgumentValue());
+						return inferToInteger(ArgumentType::Integer, this->getArgumentValue());
 					default: LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as integer."); break;
                 }
             }
@@ -148,7 +152,7 @@ namespace storm {
             virtual uint_fast64_t getValueAsUnsignedInteger() const override {
                 switch (this->argumentType) {
                     case ArgumentType::UnsignedInteger:
-                        return ArgumentTypeInferation::inferToUnsignedInteger(ArgumentType::UnsignedInteger, this->getArgumentValue());
+                        return inferToUnsignedInteger(ArgumentType::UnsignedInteger, this->getArgumentValue());
                     default: LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as unsigned integer."); break;
                 }
             }
@@ -157,7 +161,7 @@ namespace storm {
             virtual double getValueAsDouble() const override {
                 switch (this->argumentType) {
                     case ArgumentType::Double:
-                        return ArgumentTypeInferation::inferToDouble(ArgumentType::Double, this->getArgumentValue());
+                        return inferToDouble(ArgumentType::Double, this->getArgumentValue());
                     default: LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as double."); break;
                 }
             }
@@ -166,7 +170,7 @@ namespace storm {
             virtual bool getValueAsBoolean() const override {
                 switch (this->argumentType) {
                     case ArgumentType::Boolean:
-                        return ArgumentTypeInferation::inferToBoolean(ArgumentType::Boolean, this->getArgumentValue());
+                        return inferToBoolean(ArgumentType::Boolean, this->getArgumentValue());
                     default: LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as boolean."); break;
                 }
             }
@@ -190,6 +194,11 @@ namespace storm {
             // A flag indicating whether a default value has been provided.
             bool hasDefaultValue;
             
+            /*!
+             * Sets the default value of the argument to the provided value.
+             *
+             * @param newDefault The new default value of the argument.
+             */
             void setDefaultValue(T const& newDefault) {
                 LOG_THROW(this->validate(newDefault), storm::exceptions::IllegalArgumentValueException, "The default value for the argument did not pass all validation functions.");
                 this->defaultValue = newDefault;
diff --git a/src/settings/ArgumentBuilder.h b/src/settings/ArgumentBuilder.h
index 521dfc2c8..712697460 100644
--- a/src/settings/ArgumentBuilder.h
+++ b/src/settings/ArgumentBuilder.h
@@ -12,7 +12,6 @@
 #include <string>
 
 #include "src/settings/ArgumentType.h"
-#include "src/settings/ArgumentTypeInferationHelper.h"
 #include "src/settings/ArgumentBase.h"
 #include "src/settings/Argument.h"
 #include "src/settings/ArgumentValidators.h"
@@ -97,13 +96,14 @@ namespace storm {
              */
 			ArgumentBuilder& setIsOptional(bool isOptional) {
 				this->isOptional = isOptional;
+                LOG_THROW(this->hasDefaultValue, storm::exceptions::IllegalFunctionCallException, "Unable to make argument '" << this->name << "' optional without default value.");
 				return *this;
 			}
             
 #define PPCAT_NX(A, B) A ## B
 #define PPCAT(A, B) PPCAT_NX(A, B)
 #define MACROaddValidationFunction(funcName, funcType) 	ArgumentBuilder& PPCAT(addValidationFunction, funcName) (storm::settings::Argument< funcType >::userValidationFunction_t userValidationFunction) { \
-LOG_THROW(this->type == ArgumentType::funcName, storm::exceptions::IllegalFunctionCallException, "Illegal validation function for argument, because it takes arguments of different type.") \
+LOG_THROW(this->type == ArgumentType::funcName, storm::exceptions::IllegalFunctionCallException, "Illegal validation function for argument, because it takes arguments of different type."); \
 ( PPCAT(this->userValidationFunctions_, funcName) ).push_back(userValidationFunction); \
 return *this; \
 }
@@ -117,12 +117,12 @@ return *this; \
             
             
 #define MACROsetDefaultValue(funcName, funcType) ArgumentBuilder& PPCAT(setDefaultValue, funcName) (funcType const& defaultValue) { \
-LOG_THROW(this->type == ArgumentType::funcName, storm::exceptions::IllegalFunctionCallException, "Illegal default value for argument" << this->name << ", because it is of different type.") \
+LOG_THROW(this->type == ArgumentType::funcName, storm::exceptions::IllegalFunctionCallException, "Illegal default value for argument" << this->name << ", because it is of different type."); \
 PPCAT(this->defaultValue_, funcName) = defaultValue; \
 this->hasDefaultValue = true; \
 return *this; \
 }
-            
+        
             // Add the methods to set a default value.
 			MACROsetDefaultValue(String, std::string)
 			MACROsetDefaultValue(Integer, int_fast64_t)
@@ -141,38 +141,38 @@ return *this; \
 				switch (this->type) {
 					case ArgumentType::String: {
 						if (this->hasDefaultValue) {
-							return std::shared_ptr<ArgumentBase>(new Argument<std::string>(this->name, this->description, userValidationFunctions_String, this->isOptional, this->defaultValue_String));
+							return std::shared_ptr<ArgumentBase>(new Argument<std::string>(this->name, this->description, this->userValidationFunctions_String, this->isOptional, this->defaultValue_String));
 						} else {
-							return std::shared_ptr<ArgumentBase>(new Argument<std::string>(this->name, this->description, userValidationFunctions_String));
+							return std::shared_ptr<ArgumentBase>(new Argument<std::string>(this->name, this->description, this->userValidationFunctions_String));
 						}
 						break;
                     }
 					case ArgumentType::Integer:
 						if (this->hasDefaultValue) {
-							return std::shared_ptr<ArgumentBase>(new Argument<int_fast64_t>(this->name, this->description, userValidationFunctions_Integer, this->isOptional, this->defaultValue_Integer));
+							return std::shared_ptr<ArgumentBase>(new Argument<int_fast64_t>(this->name, this->description, this->userValidationFunctions_Integer, this->isOptional, this->defaultValue_Integer));
 						} else {
-							return std::shared_ptr<ArgumentBase>(new Argument<int_fast64_t>(this->name, this->description, userValidationFunctions_Integer));
+							return std::shared_ptr<ArgumentBase>(new Argument<int_fast64_t>(this->name, this->description, this->userValidationFunctions_Integer));
 						}
 						break;
 					case ArgumentType::UnsignedInteger:
 						if (this->hasDefaultValue) {
-							return std::shared_ptr<ArgumentBase>(new Argument<uint_fast64_t>(this->name, this->description, userValidationFunctions_UnsignedInteger, this->isOptional, this->defaultValue_UnsignedInteger));
+							return std::shared_ptr<ArgumentBase>(new Argument<uint_fast64_t>(this->name, this->description, this->userValidationFunctions_UnsignedInteger, this->isOptional, this->defaultValue_UnsignedInteger));
 						} else {
-							return std::shared_ptr<ArgumentBase>(new Argument<uint_fast64_t>(this->name, this->description, userValidationFunctions_UnsignedInteger));
+							return std::shared_ptr<ArgumentBase>(new Argument<uint_fast64_t>(this->name, this->description, this->userValidationFunctions_UnsignedInteger));
 						}
 						break;
 					case ArgumentType::Double:
 						if (this->hasDefaultValue) {
-							return std::shared_ptr<ArgumentBase>(new Argument<double>(this->name, this->description, userValidationFunctions_Double, this->isOptional, this->defaultValue_Double));
+							return std::shared_ptr<ArgumentBase>(new Argument<double>(this->name, this->description, this->userValidationFunctions_Double, this->isOptional, this->defaultValue_Double));
 						} else {
-							return std::shared_ptr<ArgumentBase>(new Argument<double>(this->name, this->description, userValidationFunctions_Double));
+							return std::shared_ptr<ArgumentBase>(new Argument<double>(this->name, this->description, this->userValidationFunctions_Double));
 						}
 						break;
 					case ArgumentType::Boolean:
 						if (this->hasDefaultValue) {
-							return std::shared_ptr<ArgumentBase>(new Argument<bool>(this->name, this->description, userValidationFunctions_Boolean, this->isOptional, this->defaultValue_Boolean));
+							return std::shared_ptr<ArgumentBase>(new Argument<bool>(this->name, this->description, this->userValidationFunctions_Boolean, this->isOptional, this->defaultValue_Boolean));
 						} else {
-							return std::shared_ptr<ArgumentBase>(new Argument<bool>(this->name, this->description, userValidationFunctions_Boolean));
+							return std::shared_ptr<ArgumentBase>(new Argument<bool>(this->name, this->description, this->userValidationFunctions_Boolean));
 						}
 						break;
 				}
diff --git a/src/settings/ArgumentTypeInferationHelper.cpp b/src/settings/ArgumentTypeInferationHelper.cpp
index 4cf9b1251..5ab1693fd 100644
--- a/src/settings/ArgumentTypeInferationHelper.cpp
+++ b/src/settings/ArgumentTypeInferationHelper.cpp
@@ -2,126 +2,127 @@
 
 namespace storm {
     namespace settings {
+        
         template <typename T>
-        ArgumentType ArgumentTypeInferation::inferToEnumType() {
+        ArgumentType inferToEnumType() {
             LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer type of argument.");
         }
         
         template <>
-        ArgumentType ArgumentTypeInferation::inferToEnumType<std::string>() {
+        ArgumentType inferToEnumType<std::string>() {
             return ArgumentType::String;
         }
         
         template <>
-        ArgumentType ArgumentTypeInferation::inferToEnumType<int_fast64_t>() {
+        ArgumentType inferToEnumType<int_fast64_t>() {
             return ArgumentType::Integer;
         }
         
         template <>
-        ArgumentType ArgumentTypeInferation::inferToEnumType<uint_fast64_t>() {
+        ArgumentType inferToEnumType<uint_fast64_t>() {
             return ArgumentType::UnsignedInteger;
         }
         
         template <>
-        ArgumentType ArgumentTypeInferation::inferToEnumType<double>() {
+        ArgumentType inferToEnumType<double>() {
             return ArgumentType::Double;
         }
         
         template <>
-        ArgumentType ArgumentTypeInferation::inferToEnumType<bool>() {
+        ArgumentType inferToEnumType<bool>() {
             return ArgumentType::Boolean;
         }
         
         template <typename T>
-        std::string const& ArgumentTypeInferation::inferToString(ArgumentType const& argumentType, T const& value) {
+        std::string const& inferToString(ArgumentType const& argumentType, T const& value) {
             LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer string from non-string argument value.");
         }
         
         template <>
-        std::string const& ArgumentTypeInferation::inferToString<std::string>(ArgumentType const& argumentType, std::string const& value) {
+        std::string const& inferToString<std::string>(ArgumentType const& argumentType, std::string const& value) {
             LOG_THROW(argumentType == ArgumentType::String, storm::exceptions::InternalTypeErrorException, "Unable to infer string from non-string argument.");
             return value;
         }
         
         template <typename T>
-        int_fast64_t ArgumentTypeInferation::inferToInteger(ArgumentType const& argumentType, T const& value) {
+        int_fast64_t inferToInteger(ArgumentType const& argumentType, T const& value) {
             LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer integer from non-integer argument value.");
         }
         
         template <>
-        int_fast64_t ArgumentTypeInferation::inferToInteger<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value) {
+        int_fast64_t inferToInteger<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value) {
             LOG_THROW(argumentType == ArgumentType::Integer, storm::exceptions::InternalTypeErrorException, "Unable to infer integer from non-integer argument.");
             return value;
         }
         
         template <typename T>
-        uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger(ArgumentType const& argumentType, T const& value) {
+        uint_fast64_t inferToUnsignedInteger(ArgumentType const& argumentType, T const& value) {
             LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer unsigned integer from non-unsigned argument value.");
         }
         
         template <>
-        uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value) {
+        uint_fast64_t inferToUnsignedInteger<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value) {
             LOG_THROW(argumentType == ArgumentType::UnsignedInteger, storm::exceptions::InternalTypeErrorException, "Unable to infer integer from non-integer argument.");
             return value;
         }
         
         template <typename T>
-        double ArgumentTypeInferation::inferToDouble(ArgumentType const& argumentType, T const& value) {
+        double inferToDouble(ArgumentType const& argumentType, T const& value) {
             LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer double from non-double argument value.");
         }
         
         template <>
-        double ArgumentTypeInferation::inferToDouble<double>(ArgumentType const& argumentType, double const& value) {
-            LOG_THROW(argumentType == ArgumentType::UnsignedInteger, storm::exceptions::InternalTypeErrorException, "Unable to infer double from non-double argument.");
+        double inferToDouble<double>(ArgumentType const& argumentType, double const& value) {
+            LOG_THROW(argumentType == ArgumentType::Double, storm::exceptions::InternalTypeErrorException, "Unable to infer double from non-double argument.");
             return value;
         }
         
         template <typename T>
-        bool ArgumentTypeInferation::inferToBoolean(ArgumentType const& argumentType, T const& value) {
+        bool inferToBoolean(ArgumentType const& argumentType, T const& value) {
             LOG_THROW(false, storm::exceptions::InternalTypeErrorException, "Unable to infer boolean from non-boolean argument value.");
         }
         
         template <>
-        bool ArgumentTypeInferation::inferToBoolean<bool>(ArgumentType const& argumentType, bool const& value) {
+        bool inferToBoolean<bool>(ArgumentType const& argumentType, bool const& value) {
             LOG_THROW(argumentType == ArgumentType::Boolean, storm::exceptions::InternalTypeErrorException, "Unable to infer boolean from non-boolean argument.");
             return value;
         }
         
         // Explicitly instantiate the templates.
-        template ArgumentType ArgumentTypeInferation::inferToEnumType<std::string>();
-        template ArgumentType ArgumentTypeInferation::inferToEnumType<int_fast64_t>();
-        template ArgumentType ArgumentTypeInferation::inferToEnumType<uint_fast64_t>();
-        template ArgumentType ArgumentTypeInferation::inferToEnumType<double>();
-        template ArgumentType ArgumentTypeInferation::inferToEnumType<bool>();
-        
-        template std::string const& ArgumentTypeInferation::inferToString<std::string>(ArgumentType const& argumentType, std::string const& value);
-        template std::string const& ArgumentTypeInferation::inferToString<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
-        template std::string const& ArgumentTypeInferation::inferToString<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
-        template std::string const& ArgumentTypeInferation::inferToString<double>(ArgumentType const& argumentType, double const& value);
-        template std::string const& ArgumentTypeInferation::inferToString<bool>(ArgumentType const& argumentType, bool const& value);
-        
-        template int_fast64_t ArgumentTypeInferation::inferToInteger<std::string>(ArgumentType const& argumentType, std::string const& value);
-        template int_fast64_t ArgumentTypeInferation::inferToInteger<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
-        template int_fast64_t ArgumentTypeInferation::inferToInteger<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
-        template int_fast64_t ArgumentTypeInferation::inferToInteger<double>(ArgumentType const& argumentType, double const& value);
-        template int_fast64_t ArgumentTypeInferation::inferToInteger<bool>(ArgumentType const& argumentType, bool const& value);
-        
-        template uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger<std::string>(ArgumentType const& argumentType, std::string const& value);
-        template uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
-        template uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
-        template uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger<double>(ArgumentType const& argumentType, double const& value);
-        template uint_fast64_t ArgumentTypeInferation::inferToUnsignedInteger<bool>(ArgumentType const& argumentType, bool const& value);
-        
-        template double ArgumentTypeInferation::inferToDouble<std::string>(ArgumentType const& argumentType, std::string const& value);
-        template double ArgumentTypeInferation::inferToDouble<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
-        template double ArgumentTypeInferation::inferToDouble<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
-        template double ArgumentTypeInferation::inferToDouble<double>(ArgumentType const& argumentType, double const& value);
-        template double ArgumentTypeInferation::inferToDouble<bool>(ArgumentType const& argumentType, bool const& value);
-        
-        template bool ArgumentTypeInferation::inferToBoolean<std::string>(ArgumentType const& argumentType, std::string const& value);
-        template bool ArgumentTypeInferation::inferToBoolean<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
-        template bool ArgumentTypeInferation::inferToBoolean<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
-        template bool ArgumentTypeInferation::inferToBoolean<double>(ArgumentType const& argumentType, double const& value);
-        template bool ArgumentTypeInferation::inferToBoolean<bool>(ArgumentType const& argumentType, bool const& value);
+        template ArgumentType inferToEnumType<std::string>();
+        template ArgumentType inferToEnumType<int_fast64_t>();
+        template ArgumentType inferToEnumType<uint_fast64_t>();
+        template ArgumentType inferToEnumType<double>();
+        template ArgumentType inferToEnumType<bool>();
+        
+        template std::string const& inferToString<std::string>(ArgumentType const& argumentType, std::string const& value);
+        template std::string const& inferToString<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
+        template std::string const& inferToString<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
+        template std::string const& inferToString<double>(ArgumentType const& argumentType, double const& value);
+        template std::string const& inferToString<bool>(ArgumentType const& argumentType, bool const& value);
+        
+        template int_fast64_t inferToInteger<std::string>(ArgumentType const& argumentType, std::string const& value);
+        template int_fast64_t inferToInteger<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
+        template int_fast64_t inferToInteger<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
+        template int_fast64_t inferToInteger<double>(ArgumentType const& argumentType, double const& value);
+        template int_fast64_t inferToInteger<bool>(ArgumentType const& argumentType, bool const& value);
+        
+        template uint_fast64_t inferToUnsignedInteger<std::string>(ArgumentType const& argumentType, std::string const& value);
+        template uint_fast64_t inferToUnsignedInteger<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
+        template uint_fast64_t inferToUnsignedInteger<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
+        template uint_fast64_t inferToUnsignedInteger<double>(ArgumentType const& argumentType, double const& value);
+        template uint_fast64_t inferToUnsignedInteger<bool>(ArgumentType const& argumentType, bool const& value);
+        
+        template double inferToDouble<std::string>(ArgumentType const& argumentType, std::string const& value);
+        template double inferToDouble<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
+        template double inferToDouble<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
+        template double inferToDouble<double>(ArgumentType const& argumentType, double const& value);
+        template double inferToDouble<bool>(ArgumentType const& argumentType, bool const& value);
+        
+        template bool inferToBoolean<std::string>(ArgumentType const& argumentType, std::string const& value);
+        template bool inferToBoolean<int_fast64_t>(ArgumentType const& argumentType, int_fast64_t const& value);
+        template bool inferToBoolean<uint_fast64_t>(ArgumentType const& argumentType, uint_fast64_t const& value);
+        template bool inferToBoolean<double>(ArgumentType const& argumentType, double const& value);
+        template bool inferToBoolean<bool>(ArgumentType const& argumentType, bool const& value);
     }
 }
\ No newline at end of file
diff --git a/src/settings/ArgumentTypeInferationHelper.h b/src/settings/ArgumentTypeInferationHelper.h
index 981e09caf..3e3b93122 100644
--- a/src/settings/ArgumentTypeInferationHelper.h
+++ b/src/settings/ArgumentTypeInferationHelper.h
@@ -9,30 +9,47 @@
 #include "src/exceptions/InternalTypeErrorException.h"
 
 namespace storm {
-	namespace settings {
+    namespace settings {
         /*!
-         * This class serves as a helper class to infer the types of arguments.
+         * This function infers the type in our enum of possible types from the template parameter.
+         *
+         * @return The argument type that has been inferred.
          */
-		class ArgumentTypeInferation {
-		public:
-			// Specialized function template that infers the Type of T to our local enum
-            /*!
-             * This function infers the type in our enum of possible types from the template parameter.
-             *
-             * @return The argument type that has been inferred.
-             */
-			template <typename T>
-			static ArgumentType inferToEnumType();
-
-			// Specialized function templates that allow casting the given value to the correct type. If the conversion
-            // fails, an exception is thrown.
-			template <typename T> static std::string const& inferToString(ArgumentType const& argumentType, T const& value);
-			template <typename T> static int_fast64_t inferToInteger(ArgumentType const& argumentType, T const& value);
-			template <typename T> static uint_fast64_t inferToUnsignedInteger(ArgumentType const& argumentType, T const& value);
-			template <typename T> static double inferToDouble(ArgumentType const& argumentType, T const& value);
-			template <typename T> static bool inferToBoolean(ArgumentType const& argumentType, T const& value);
-		};
-	} // namespace settings
+        template <typename T>
+        ArgumentType inferToEnumType();
+        
+        // Specialized function templates that allow casting the given value to the correct type. If the conversion
+        // fails, an exception is thrown.
+        template <typename T>
+        std::string const& inferToString(ArgumentType const& argumentType, T const& value);
+        
+        template <>
+        std::string const& inferToString(ArgumentType const& argumentType, std::string const& value);
+        
+        template <typename T>
+        int_fast64_t inferToInteger(ArgumentType const& argumentType, T const& value);
+        
+        template <>
+        int_fast64_t inferToInteger(ArgumentType const& argumentType, int_fast64_t const& value);
+        
+        template <typename T>
+        uint_fast64_t inferToUnsignedInteger(ArgumentType const& argumentType, T const& value);
+        
+        template <>
+        uint_fast64_t inferToUnsignedInteger(ArgumentType const& argumentType, uint_fast64_t const& value);
+        
+        template <typename T>
+        double inferToDouble(ArgumentType const& argumentType, T const& value);
+        
+        template <>
+        double inferToDouble(ArgumentType const& argumentType, double const& value);
+        
+        template <typename T>
+        bool inferToBoolean(ArgumentType const& argumentType, T const& value);
+        
+        template <>
+        bool inferToBoolean(ArgumentType const& argumentType, bool const& value);
+    } // namespace settings
 } // namespace storm
 
 #endif // STORM_SETTINGS_ARGUMENTTYPEINFERATIONHELPER_H_
\ No newline at end of file
diff --git a/src/settings/ArgumentValidators.h b/src/settings/ArgumentValidators.h
index 619773cf2..aad349a44 100644
--- a/src/settings/ArgumentValidators.h
+++ b/src/settings/ArgumentValidators.h
@@ -115,7 +115,7 @@ namespace storm {
 						}
 					}
 
-                    LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Value " << inputString << " does not match any entry in the list of valid items.");
+                    LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Value '" << inputString << "' does not match any entry in the list of valid items.");
 					return false;
 				};
 			}
diff --git a/src/settings/Option.h b/src/settings/Option.h
index 3345175eb..8f2c2c047 100644
--- a/src/settings/Option.h
+++ b/src/settings/Option.h
@@ -74,7 +74,6 @@ namespace storm {
              * @return True iff the given argument is compatible with the current one.
              */
 			bool isCompatibleWith(Option const& other) {
-                std::cout << "unifying " << *this << " and " << other << std::endl;
                 LOG_THROW(this->getArgumentCount() == other.getArgumentCount(), storm::exceptions::OptionUnificationException, "Unable to unify two options, because their argument count differs.");
 
 				for(size_t i = 0; i != this->arguments.size(); i++) {
diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp
index e36f61d06..db06bf63d 100644
--- a/src/settings/SettingsManager.cpp
+++ b/src/settings/SettingsManager.cpp
@@ -62,9 +62,7 @@ namespace storm {
             std::vector<std::string> argumentCache;
             
             // Walk through all arguments.
-            std::cout << "before... "<< std::endl;
             for (uint_fast64_t i = 0; i < commandLineArguments.size(); ++i) {
-                std::cout << "in ... " << i << std::endl;
                 bool existsNextArgument = i < commandLineArguments.size() - 1;
                 std::string const& currentArgument = commandLineArguments[i];
                 
diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h
index def33aadf..091695323 100644
--- a/src/settings/SettingsManager.h
+++ b/src/settings/SettingsManager.h
@@ -17,7 +17,6 @@
 #include "src/settings/Argument.h"
 #include "src/settings/ArgumentBuilder.h"
 #include "src/settings/ArgumentType.h"
-#include "src/settings/ArgumentTypeInferationHelper.h"
 #include "src/settings/modules/ModuleSettings.h"
 #include "src/settings/modules/GeneralSettings.h"
 #include "src/settings/modules/DebugSettings.h"
diff --git a/src/settings/modules/CounterexampleGeneratorSettings.cpp b/src/settings/modules/CounterexampleGeneratorSettings.cpp
index 3078c6417..cf66717c9 100644
--- a/src/settings/modules/CounterexampleGeneratorSettings.cpp
+++ b/src/settings/modules/CounterexampleGeneratorSettings.cpp
@@ -13,7 +13,7 @@ namespace storm {
             const std::string CounterexampleGeneratorSettings::statisticsOptionName = "stats";
             
             CounterexampleGeneratorSettings::CounterexampleGeneratorSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
-                std::vector<std::string> techniques = {"sat", "milp"};
+                std::vector<std::string> techniques = {"maxsat", "milp"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, minimalCommandSetOptionName, true, "Computes a counterexample for the given model in terms of a minimal command set. Note that this requires the model to be given in a symbolic format.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file containing the properties for which counterexamples are to be generated.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build())
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used to derive the counterexample. Available are {milp, maxsat}").setDefaultValueString("maxsat").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(techniques)).build()).build());
diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp
index 34f6049aa..fa3cea129 100644
--- a/src/settings/modules/GeneralSettings.cpp
+++ b/src/settings/modules/GeneralSettings.cpp
@@ -93,7 +93,8 @@ namespace storm {
             }
             
             double GeneralSettings::getPrecision() const {
-                return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
+                double value = this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
+                return value;
             }
             
             bool GeneralSettings::isExportDotSet() const {
diff --git a/src/settings/modules/GmmxxEquationSolverSettings.cpp b/src/settings/modules/GmmxxEquationSolverSettings.cpp
index fb940ff50..9843461e2 100644
--- a/src/settings/modules/GmmxxEquationSolverSettings.cpp
+++ b/src/settings/modules/GmmxxEquationSolverSettings.cpp
@@ -25,7 +25,7 @@ namespace storm {
                 
                 this->addOption(storm::settings::OptionBuilder(moduleName, restartOptionName, true, "The number of iteration until restarted methods are actually restarted.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of iterations.").setDefaultValueUnsignedInteger(50).build()).build());
                 
-                this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, true, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(10000).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, true, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(20000).build()).build());
                 
                 this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
                 
@@ -47,7 +47,7 @@ namespace storm {
             }
             
             GmmxxEquationSolverSettings::PreconditioningTechnique GmmxxEquationSolverSettings::getPreconditioningTechnique() const {
-                std::string preconditioningTechniqueAsString = this->getOption(techniqueOptionName).getArgumentByName("name").getValueAsString();
+                std::string preconditioningTechniqueAsString = this->getOption(preconditionOptionName).getArgumentByName("name").getValueAsString();
                 if (preconditioningTechniqueAsString == "ilu") {
                     return GmmxxEquationSolverSettings::PreconditioningTechnique::Ilu;
                 } else if (preconditioningTechniqueAsString == "diagonal") {
diff --git a/src/settings/modules/ModuleSettings.cpp b/src/settings/modules/ModuleSettings.cpp
index fbdad7b93..a45c2f6ad 100644
--- a/src/settings/modules/ModuleSettings.cpp
+++ b/src/settings/modules/ModuleSettings.cpp
@@ -49,10 +49,10 @@ namespace storm {
             
             std::unique_ptr<storm::settings::SettingMemento> ModuleSettings::overrideOption(std::string const& name, bool requiredStatus) {
                 bool currentStatus = this->isSet(name);
-                if (currentStatus) {
-                    this->unset(name);
-                } else {
+                if (requiredStatus) {
                     this->set(name);
+                } else {
+                    this->unset(name);
                 }
                 return std::unique_ptr<storm::settings::SettingMemento>(new storm::settings::SettingMemento(*this, name, currentStatus));
             }
diff --git a/src/settings/modules/NativeEquationSolverSettings.cpp b/src/settings/modules/NativeEquationSolverSettings.cpp
index 2749ccbec..a96b424bb 100644
--- a/src/settings/modules/NativeEquationSolverSettings.cpp
+++ b/src/settings/modules/NativeEquationSolverSettings.cpp
@@ -17,7 +17,7 @@ namespace storm {
                 std::vector<std::string> methods = { "jacobi" };
                 this->addOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the native engine. Available are: { jacobi }.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("jacobi").build()).build());
                 
-                this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, true, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(10000).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, true, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(20000).build()).build());
                 
                 this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
                 
diff --git a/src/solver/GmmxxLinearEquationSolver.cpp b/src/solver/GmmxxLinearEquationSolver.cpp
index 6c0802996..4815b5b2b 100644
--- a/src/solver/GmmxxLinearEquationSolver.cpp
+++ b/src/solver/GmmxxLinearEquationSolver.cpp
@@ -24,11 +24,11 @@ namespace storm {
         template<typename ValueType>
         GmmxxLinearEquationSolver<ValueType>::GmmxxLinearEquationSolver() {
             // Get the settings object to customize linear solving.
-            storm::settings::modules::GmmxxEquationSolverSettings const& settings =storm::settings::gmmxxEquationSolverSettings();
+            storm::settings::modules::GmmxxEquationSolverSettings const& settings = storm::settings::gmmxxEquationSolverSettings();
             
             // Get appropriate settings.
             maximalNumberOfIterations = settings.getMaximalIterationCount();
-            precision = settings.getPrecision();;
+            precision = settings.getPrecision();
             relative = settings.getConvergenceCriterion() == storm::settings::modules::GmmxxEquationSolverSettings::ConvergenceCriterion::Relative;
             restart = settings.getRestartIterationCount();
             
@@ -89,7 +89,7 @@ namespace storm {
                     } else if (preconditioner == Preconditioner::None) {
                         gmm::qmr(*gmmA, x, b, gmm::identity_matrix(), iter);
                     }
-                } else if (method == SolutionMethod::Qmr) {
+                } else if (method == SolutionMethod::Gmres) {
                     if (preconditioner == Preconditioner::Ilu) {
                         gmm::gmres(*gmmA, x, b, gmm::ilu_precond<gmm::csr_matrix<ValueType>>(*gmmA), restart, iter);
                     } else if (preconditioner == Preconditioner::Diagonal) {
diff --git a/test/functional/solver/GlpkLpSolverTest.cpp b/test/functional/solver/GlpkLpSolverTest.cpp
index 0db9fdfbd..e72aaff67 100644
--- a/test/functional/solver/GlpkLpSolverTest.cpp
+++ b/test/functional/solver/GlpkLpSolverTest.cpp
@@ -18,7 +18,7 @@ TEST(GlpkLpSolver, LPOptimizeMax) {
     ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleLiteral(0.5) * storm::expressions::Expression::createDoubleVariable("y") + storm::expressions::Expression::createDoubleVariable("z") - storm::expressions::Expression::createDoubleVariable("x") == storm::expressions::Expression::createDoubleLiteral(5)));
     ASSERT_NO_THROW(solver.addConstraint("", storm::expressions::Expression::createDoubleVariable("y") - storm::expressions::Expression::createDoubleVariable("x") <= storm::expressions::Expression::createDoubleLiteral(5.5)));
     ASSERT_NO_THROW(solver.update());
-
+    
     ASSERT_NO_THROW(solver.optimize());
     ASSERT_TRUE(solver.isOptimal());
     ASSERT_FALSE(solver.isUnbounded());
diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
index 80c410e22..8534fc827 100644
--- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
+++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
@@ -1,15 +1,13 @@
 #include "gtest/gtest.h"
 #include "storm-config.h"
 #include "src/settings/SettingsManager.h"
-#include "src/settings/InternalOptionMemento.h"
+#include "src/settings/SettingMemento.h"
 #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
 #include "src/solver/GmmxxLinearEquationSolver.h"
 #include "src/parser/AutoParser.h"
 
 TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
-	storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
-	storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true);
-	ASSERT_TRUE(s->isSet("fixDeadlocks"));
+    std::unique_ptr<storm::settings::SettingMemento> deadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true);
 	std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");
 
 	ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
@@ -19,7 +17,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
 	ASSERT_EQ(2036647ull, dtmc->getNumberOfStates());
 	ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions());
 
-	storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
+    storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
 
 	auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("observe0Greater1");
 	auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
@@ -28,7 +26,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
 	std::vector<double> result = eventuallyFormula->check(mc, false);
     LOG4CPLUS_WARN(logger, "Done.");
 
-	ASSERT_LT(std::abs(result[0] - 0.2296800237), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+    ASSERT_LT(std::abs(result[0] - 0.2296800237), storm::settings::gmmxxEquationSolverSettings().getPrecision());
 
 	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("observeIGreater1");
 	eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
@@ -37,7 +35,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
     result = eventuallyFormula->check(mc, false);
     LOG4CPLUS_WARN(logger, "Done.");
     
-	ASSERT_LT(std::abs(result[0] - 0.05073232193), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+	ASSERT_LT(std::abs(result[0] - 0.05073232193), storm::settings::gmmxxEquationSolverSettings().getPrecision());
 
 	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("observeOnlyTrueSender");
 	eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
@@ -46,14 +44,12 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
     result = eventuallyFormula->check(mc, false);
     LOG4CPLUS_WARN(logger, "Done.");
 
-	ASSERT_LT(std::abs(result[0] - 0.22742171078), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+	ASSERT_LT(std::abs(result[0] - 0.22742171078), storm::settings::gmmxxEquationSolverSettings().getPrecision());
 }
 
 
 TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
-	storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
-	storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true);
-	ASSERT_TRUE(s->isSet("fixDeadlocks"));
+    std::unique_ptr<storm::settings::SettingMemento> deadlockOption = storm::settings::mutableGeneralSettings().overrideFixDeadlocksSet(true);
 	std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew");
 
 	ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
@@ -63,7 +59,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
 	ASSERT_EQ(1312334ull, dtmc->getNumberOfStates());
 	ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions());
 
-	storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
+	storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
 
 	auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
 	auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
@@ -72,7 +68,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
 	std::vector<double> result = eventuallyFormula->check(mc, false);
     LOG4CPLUS_WARN(logger, "Done.");
 
-	ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+	ASSERT_LT(std::abs(result[0] - 1.0), storm::settings::gmmxxEquationSolverSettings().getPrecision());
 
 	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
 	auto boundedUntilFormula = std::make_shared<storm::properties::prctl::BoundedUntil<double>>(std::make_shared<storm::properties::prctl::Ap<double>>("true"), apFormula, 20);
@@ -81,7 +77,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
     result = boundedUntilFormula->check(mc, false);
     LOG4CPLUS_WARN(logger, "Done.");
 
-	ASSERT_LT(std::abs(result[0] - 0.9993949793), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+	ASSERT_LT(std::abs(result[0] - 0.9993949793), storm::settings::gmmxxEquationSolverSettings().getPrecision());
 
 	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
 	auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(apFormula);
@@ -90,5 +86,5 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
 	result = reachabilityRewardFormula->check(mc, false);
     LOG4CPLUS_WARN(logger, "Done.");
 
-	ASSERT_LT(std::abs(result[0] - 1.025106273), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+	ASSERT_LT(std::abs(result[0] - 1.025106273), storm::settings::gmmxxEquationSolverSettings().getPrecision());
 }
diff --git a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
index 242aef71e..a1e5dddf0 100644
--- a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
+++ b/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
@@ -7,7 +7,6 @@
 #include "src/parser/AutoParser.h"
 
 TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
-	storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
 	std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew");
 
 	ASSERT_EQ(abstractModel->getType(), storm::models::MDP);
@@ -24,37 +23,36 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
 
 	std::vector<double> result = mc.checkOptimizingOperator(*eventuallyFormula, true);
 
-	ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+    ASSERT_LT(std::abs(result[0] - 1.0), storm::settings::nativeEquationSolverSettings().getPrecision());
 
 	result = mc.checkOptimizingOperator(*eventuallyFormula, false);
 
-	ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+	ASSERT_LT(std::abs(result[0] - 1.0), storm::settings::nativeEquationSolverSettings().getPrecision());
 
 	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
 	auto boundedEventuallyFormula = std::make_shared<storm::properties::prctl::BoundedEventually<double>>(apFormula, 25);
 
 	result = mc.checkOptimizingOperator(*boundedEventuallyFormula, true);
 
-	ASSERT_LT(std::abs(result[0] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+	ASSERT_LT(std::abs(result[0] - 0.0), storm::settings::nativeEquationSolverSettings().getPrecision());
 
 	result = mc.checkOptimizingOperator(*boundedEventuallyFormula, false);
 
-	ASSERT_LT(std::abs(result[0] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+	ASSERT_LT(std::abs(result[0] - 0.0), storm::settings::nativeEquationSolverSettings().getPrecision());
 
 	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
 	auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(apFormula);
 
 	result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true);
 
-	ASSERT_LT(std::abs(result[0] - 6.172433512), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+	ASSERT_LT(std::abs(result[0] - 6.172433512), storm::settings::nativeEquationSolverSettings().getPrecision());
 
 	result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false);
 
-	ASSERT_LT(std::abs(result[0] - 6.1724344), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+	ASSERT_LT(std::abs(result[0] - 6.1724344), storm::settings::nativeEquationSolverSettings().getPrecision());
 }
 
 TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
-	storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
     // Increase the maximal number of iterations, because the solver does not converge otherwise.
 	// This is done in the main cpp unit
     
@@ -74,7 +72,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
     
 	std::vector<double> result = mc.checkOptimizingOperator(*eventuallyFormula, true);
     
-	ASSERT_LT(std::abs(result[31168] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+	ASSERT_LT(std::abs(result[31168] - 1.0), storm::settings::nativeEquationSolverSettings().getPrecision());
 
     apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("finished");
     auto apFormula2 = std::make_shared<storm::properties::prctl::Ap<double>>("all_coins_equal_0");
@@ -83,7 +81,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
     
 	result = mc.checkOptimizingOperator(*eventuallyFormula, true);
 
-	ASSERT_LT(std::abs(result[31168] - 0.4374282832), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+	ASSERT_LT(std::abs(result[31168] - 0.4374282832), storm::settings::nativeEquationSolverSettings().getPrecision());
     
     apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("finished");
     apFormula2 = std::make_shared<storm::properties::prctl::Ap<double>>("all_coins_equal_1");
@@ -92,7 +90,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
     
 	result = mc.checkOptimizingOperator(*eventuallyFormula, false);
     
-	ASSERT_LT(std::abs(result[31168] - 0.5293286369), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+	ASSERT_LT(std::abs(result[31168] - 0.5293286369), storm::settings::nativeEquationSolverSettings().getPrecision());
 
     apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("finished");
     apFormula2 = std::make_shared<storm::properties::prctl::Ap<double>>("agree");
@@ -102,27 +100,27 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
     
 	result = mc.checkOptimizingOperator(*eventuallyFormula, false);
     
-	ASSERT_LT(std::abs(result[31168] - 0.10414097), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+	ASSERT_LT(std::abs(result[31168] - 0.10414097), storm::settings::nativeEquationSolverSettings().getPrecision());
 
     apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("finished");
 	auto boundedEventuallyFormula = std::make_shared<storm::properties::prctl::BoundedEventually<double>>(apFormula, 50ull);
     
 	result = mc.checkOptimizingOperator(*boundedEventuallyFormula, true);
     
-	ASSERT_LT(std::abs(result[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+	ASSERT_LT(std::abs(result[31168] - 0.0), storm::settings::nativeEquationSolverSettings().getPrecision());
     
 	result = mc.checkOptimizingOperator(*boundedEventuallyFormula, false);
 
-	ASSERT_LT(std::abs(result[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+	ASSERT_LT(std::abs(result[31168] - 0.0), storm::settings::nativeEquationSolverSettings().getPrecision());
 
     apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("finished");
 	auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(apFormula);
     
 	result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true);
     
-	ASSERT_LT(std::abs(result[31168] - 1725.593313), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+	ASSERT_LT(std::abs(result[31168] - 1725.593313), storm::settings::nativeEquationSolverSettings().getPrecision());
 
 	result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false);
 
-	ASSERT_LT(std::abs(result[31168] - 2183.142422), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
+	ASSERT_LT(std::abs(result[31168] - 2183.142422), storm::settings::nativeEquationSolverSettings().getPrecision());
 }
diff --git a/test/performance/storm-performance-tests.cpp b/test/performance/storm-performance-tests.cpp
index c16e2cadd..0c29f19c8 100644
--- a/test/performance/storm-performance-tests.cpp
+++ b/test/performance/storm-performance-tests.cpp
@@ -29,23 +29,8 @@ void setUpLogging() {
 	// logger.addAppender(consoleLogAppender);
 }
 
-/*!
- * Creates an empty settings object as the standard instance of the Settings class.
- */
-void createEmptyOptions() {
-    const char* newArgv[] = {"storm-performance-tests", "--maxiter", "20000"};
-	storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
-	try {
-		storm::settings::SettingsManager::parse(3, newArgv);
-	} catch (storm::exceptions::OptionParserException& e) {
-		std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl;
-		std::cout << std::endl << s->getHelpText();
-	}
-}
-
 int main(int argc, char* argv[]) {
 	setUpLogging();
-	createEmptyOptions();
 	std::cout << "StoRM (Performance) Testing Suite" << std::endl;
 	
 	testing::InitGoogleTest(&argc, argv);