diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h
index 4f026d8db..69af92244 100644
--- a/src/storm-cli-utilities/model-handling.h
+++ b/src/storm-cli-utilities/model-handling.h
@@ -1084,7 +1084,7 @@ namespace storm {
         }
         
         template <storm::dd::DdType DdType, typename BuildValueType, typename VerificationValueType = BuildValueType>
-        std::shared_ptr<storm::models::ModelBase> buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput const& input, ModelProcessingInformation const& mpi) {
+        std::shared_ptr<storm::models::ModelBase> buildPreprocessModelWithValueTypeAndDdlib(SymbolicInput const& input, ModelProcessingInformation const& mpi) {
             auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
             auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
             std::shared_ptr<storm::models::ModelBase> model;
@@ -1104,6 +1104,14 @@ namespace storm {
                     model = preprocessingResult.first;
                     model->printModelInformationToStream(std::cout);
                 }
+            }
+            return model;
+        }
+
+        template <storm::dd::DdType DdType, typename BuildValueType, typename VerificationValueType = BuildValueType>
+        std::shared_ptr<storm::models::ModelBase> buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput const& input, ModelProcessingInformation const& mpi) {
+            auto model = buildPreprocessModelWithValueTypeAndDdlib<DdType, BuildValueType, VerificationValueType>(input, mpi);
+            if (model) {
                 exportModel<DdType, BuildValueType>(model, input);
             }
             return model;
diff --git a/src/storm-conv-cli/storm-conv.cpp b/src/storm-conv-cli/storm-conv.cpp
index bbd700b53..798f23312 100644
--- a/src/storm-conv-cli/storm-conv.cpp
+++ b/src/storm-conv-cli/storm-conv.cpp
@@ -308,6 +308,7 @@ namespace storm {
         
         void processOptions() {
             // Start by setting some urgent options (log levels, etc.)
+            // We cannot use the general variants used for other executables since the "GeneralSettings" module is not available in Storm-conv
             setUrgentOptions();
             
             // Branch on the type of input
diff --git a/src/storm/adapters/MathsatExpressionAdapter.h b/src/storm/adapters/MathsatExpressionAdapter.h
index 88ed84dcd..ca6de5d8c 100644
--- a/src/storm/adapters/MathsatExpressionAdapter.h
+++ b/src/storm/adapters/MathsatExpressionAdapter.h
@@ -106,6 +106,10 @@ namespace storm {
                 STORM_LOG_ASSERT(declarationVariablePair != declarationToVariableMapping.end(), "Unknown variable declaration.");
                 return declarationVariablePair->second;
             }
+            
+            std::unordered_map<storm::expressions::Variable, msat_decl> const& getAllDeclaredVariables() const {
+				return variableToDeclarationMapping;
+			}
 
             virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data) override {
                 msat_term leftResult = boost::any_cast<msat_term>(expression.getFirstOperand()->accept(*this, data));
diff --git a/src/storm/solver/MathsatSmtSolver.cpp b/src/storm/solver/MathsatSmtSolver.cpp
index 219efe530..f8c1d6f86 100644
--- a/src/storm/solver/MathsatSmtSolver.cpp
+++ b/src/storm/solver/MathsatSmtSolver.cpp
@@ -32,6 +32,22 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unable to retrieve double value from model that only contains boolean values.");
         }
         
+        std::string MathsatSmtSolver::MathsatAllsatModelReference::toString() const {
+            std::stringstream str;
+            bool first = true;
+            str << "[";
+            for (auto const& varSlot : variableToSlotMapping) {
+                if (first) {
+                    first = false;
+                } else {
+                    str << ", ";
+                }
+                str << varSlot.first.getName() << "=" << std::boolalpha << getBooleanValue(varSlot.first);
+            }
+            str << "]";
+            return str.str();
+        }
+        
         MathsatSmtSolver::MathsatModelReference::MathsatModelReference(storm::expressions::ExpressionManager const& manager, msat_env const& env, storm::adapters::MathsatExpressionAdapter& expressionAdapter) : ModelReference(manager), env(env), expressionAdapter(expressionAdapter) {
             // Intentionally left empty.
         }
@@ -62,6 +78,25 @@ namespace storm {
             storm::expressions::Expression value = expressionAdapter.translateExpression(msatValue);
             return value.evaluateAsDouble();
         }
+        
+        std::string MathsatSmtSolver::MathsatModelReference::toString() const {
+            std::stringstream str;
+            bool first = true;
+            str << "[";
+            for (auto const& varDecl : expressionAdapter.getAllDeclaredVariables()) {
+                if (first) {
+                    first = false;
+                } else {
+                    str << ", ";
+                }
+                msat_term msatValue = msat_get_model_value(env, expressionAdapter.translateExpression(varDecl.first));
+                STORM_LOG_ASSERT(!MSAT_ERROR_TERM(msatValue), "Unable to retrieve value of variable in model. This could be caused by calls to the solver between checking for satisfiability and model retrieval.");
+                str << varDecl.first.getName() << "=" << expressionAdapter.translateExpression(msatValue);
+            }
+            str << "]";
+            return str.str();
+        }
+        
 #endif
 
 		MathsatSmtSolver::MathsatSmtSolver(storm::expressions::ExpressionManager& manager, Options const& options) : SmtSolver(manager)
diff --git a/src/storm/solver/MathsatSmtSolver.h b/src/storm/solver/MathsatSmtSolver.h
index 0d27c71af..851c00d82 100644
--- a/src/storm/solver/MathsatSmtSolver.h
+++ b/src/storm/solver/MathsatSmtSolver.h
@@ -38,7 +38,8 @@ namespace storm {
                 virtual bool getBooleanValue(storm::expressions::Variable const& variable) const override;
                 virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const override;
                 virtual double getRationalValue(storm::expressions::Variable const& variable) const override;
-                
+                virtual std::string toString() const override;
+
 			private:
 				msat_env const& env;
                 msat_term* model;
@@ -54,7 +55,8 @@ namespace storm {
                 virtual bool getBooleanValue(storm::expressions::Variable const& variable) const override;
                 virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const override;
                 virtual double getRationalValue(storm::expressions::Variable const& variable) const override;
-                
+                virtual std::string toString() const override;
+
 			private:
 				msat_env const& env;
                 storm::adapters::MathsatExpressionAdapter& expressionAdapter;