diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h
index 0b1268913..b63b7adad 100644
--- a/src/cli/entrypoints.h
+++ b/src/cli/entrypoints.h
@@ -131,47 +131,32 @@ namespace storm {
     
         template<typename ValueType, storm::dd::DdType LibraryType>
         void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
-            storm::storage::ModelProgramPair modelProgramPair = buildSymbolicModel<ValueType, LibraryType>(program, formulas);
-            STORM_LOG_THROW(modelProgramPair.model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason.");
+            storm::storage::ModelFormulasPair modelFormulasPair = buildSymbolicModel<ValueType, LibraryType>(program, formulas);
+            STORM_LOG_THROW(modelFormulasPair.model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason.");
             
             // Preprocess the model if needed.
-            BRANCH_ON_MODELTYPE(modelProgramPair.model, modelProgramPair.model, ValueType, LibraryType, preprocessModel, formulas);
+            BRANCH_ON_MODELTYPE(modelFormulasPair.model, modelFormulasPair.model, ValueType, LibraryType, preprocessModel, formulas);
             
             // Print some information about the model.
-            modelProgramPair.model->printModelInformationToStream(std::cout);
+            modelFormulasPair.model->printModelInformationToStream(std::cout);
             
             // Verify the model, if a formula was given.
             if (!formulas.empty()) {
-                // There may be constants of the model appearing in the formulas, so we replace all their occurrences
-                // by their definitions in the translated program.
-                
-                // Start by building a mapping from constants of the (translated) model to their defining expressions.
-                std::map<storm::expressions::Variable, storm::expressions::Expression> constantSubstitution;
-                for (auto const& constant : modelProgramPair.program.getConstants()) {
-                    if (constant.isDefined()) {
-                        constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression());
-                    }
-                }
-                
-                std::vector<std::shared_ptr<storm::logic::Formula>> preparedFormulas;
-                for (auto const& formula : formulas) {
-                    preparedFormulas.emplace_back(formula->substitute(constantSubstitution));
-                }
-                
-                if (modelProgramPair.model->isSparseModel()) {
+
+                if (modelFormulasPair.model->isSparseModel()) {
                     if(storm::settings::generalSettings().isCounterexampleSet()) {
                         // If we were requested to generate a counterexample, we now do so for each formula.
-                        for(auto const& formula : preparedFormulas) {
-                            generateCounterexample<ValueType>(program, modelProgramPair.model->as<storm::models::sparse::Model<ValueType>>(), formula);
+                        for(auto const& formula : modelFormulasPair.formulas) {
+                            generateCounterexample<ValueType>(program, modelFormulasPair.model->as<storm::models::sparse::Model<ValueType>>(), formula);
                         }
                     } else {
-                        verifySparseModel<ValueType>(modelProgramPair.model->as<storm::models::sparse::Model<ValueType>>(), preparedFormulas);
+                        verifySparseModel<ValueType>(modelFormulasPair.model->as<storm::models::sparse::Model<ValueType>>(), modelFormulasPair.formulas);
                     }
-                } else if (modelProgramPair.model->isSymbolicModel()) {
+                } else if (modelFormulasPair.model->isSymbolicModel()) {
                     if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
-                        verifySymbolicModelWithHybridEngine(modelProgramPair.model->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
+                        verifySymbolicModelWithHybridEngine(modelFormulasPair.model->as<storm::models::symbolic::Model<LibraryType>>(), modelFormulasPair.formulas);
                     } else {
-                        verifySymbolicModelWithSymbolicEngine(modelProgramPair.model->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
+                        verifySymbolicModelWithSymbolicEngine(modelFormulasPair.model->as<storm::models::symbolic::Model<LibraryType>>(), modelFormulasPair.formulas);
                     }
                 } else {
                     STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type.");
diff --git a/src/storage/ModelFormulasPair.h b/src/storage/ModelFormulasPair.h
new file mode 100644
index 000000000..57181a566
--- /dev/null
+++ b/src/storage/ModelFormulasPair.h
@@ -0,0 +1,16 @@
+#pragma once
+#include "../models/ModelBase.h"
+
+
+namespace storm {
+    namespace logic {
+        class Formula;
+    }
+
+    namespace storage {
+        struct ModelFormulasPair {
+            std::shared_ptr<storm::models::ModelBase> model;
+            std::vector<std::shared_ptr<storm::logic::Formula>> formulas;
+        };
+    }
+}
\ No newline at end of file
diff --git a/src/storage/ModelProgramPair.h b/src/storage/ModelProgramPair.h
deleted file mode 100644
index c50b6d306..000000000
--- a/src/storage/ModelProgramPair.h
+++ /dev/null
@@ -1,12 +0,0 @@
-#include "../models/ModelBase.h"
-#include "prism/Program.h"
-
-
-namespace storm {
-    namespace storage {
-        struct ModelProgramPair {
-            std::shared_ptr<storm::models::ModelBase> model;
-            storm::prism::Program program;
-        };
-    }
-}
\ No newline at end of file
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index fee721878..7947b4c78 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -171,6 +171,21 @@ namespace storm {
             }
             return result;
         }
+
+        std::string Program::getUndefinedConstantsAsString() const {
+            std::stringstream stream;
+            bool printComma = false;
+            for (auto const& constant : getUndefinedConstants()) {
+                if (printComma) {
+                    stream << ", ";
+                } else {
+                    printComma = true;
+                }
+                stream << constant.get().getName() << " (" << constant.get().getType() << ")";
+            }
+            stream << ".";
+            return stream.str();
+        }
         
         bool Program::hasConstant(std::string const& constantName) const {
             return this->constantToIndexMap.find(constantName) != this->constantToIndexMap.end();
diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h
index b4e6d45b5..45ac16b62 100644
--- a/src/storage/prism/Program.h
+++ b/src/storage/prism/Program.h
@@ -89,7 +89,14 @@ namespace storm {
              * @return The undefined constants in the program.
              */
             std::vector<std::reference_wrapper<storm::prism::Constant const>> getUndefinedConstants() const;
-            
+
+            /*!
+             * Retrieves the undefined constants in the program as a comma-separated string.
+             *
+             * @return A string with the undefined constants in the program, separated by a comma
+             */
+            std::string getUndefinedConstantsAsString() const;
+
             /*!
              * Retrieves whether the given constant exists in the program.
              *
diff --git a/src/utility/storm.h b/src/utility/storm.h
index 0b58a3d02..c45560338 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -8,6 +8,7 @@
 #include <cstdio>
 #include <sstream>
 #include <memory>
+#include <src/storage/ModelFormulasPair.h>
 
 #include "initialize.h"
 
@@ -46,7 +47,7 @@
 // Headers for model processing.
 #include "src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h"
 #include "src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h"
-#include "src/storage/ModelProgramPair.h"
+#include "src/storage/ModelFormulasPair.h"
 
 // Headers for model checking.
 #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
@@ -85,10 +86,13 @@ namespace storm {
     storm::prism::Program parseProgram(std::string const& path);
     std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForExplicit(std::string const& inputString);
     std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program);
+
+
             
     template<typename ValueType, storm::dd::DdType LibraryType = storm::dd::DdType::CUDD>
-    storm::storage::ModelProgramPair buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
-        storm::storage::ModelProgramPair result;
+    storm::storage::ModelFormulasPair buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
+        storm::storage::ModelFormulasPair result;
+        storm::prism::Program translatedProgram;
 
         storm::settings::modules::GeneralSettings settings = storm::settings::generalSettings();
 
@@ -108,7 +112,7 @@ namespace storm {
 
             storm::builder::ExplicitPrismModelBuilder<ValueType> builder;
             result.model = builder.translateProgram(program, options);
-            result.program = builder.getTranslatedProgram();
+            translatedProgram = builder.getTranslatedProgram();
         } else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd || settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
             typename storm::builder::DdPrismModelBuilder<LibraryType>::Options options;
             options = typename storm::builder::DdPrismModelBuilder<LibraryType>::Options(formulas);
@@ -116,9 +120,22 @@ namespace storm {
 
             storm::builder::DdPrismModelBuilder<LibraryType> builder;
             result.model = builder.translateProgram(program, options);
-            result.program = builder.getTranslatedProgram();
+            translatedProgram = builder.getTranslatedProgram();
+        }
+        // There may be constants of the model appearing in the formulas, so we replace all their occurrences
+        // by their definitions in the translated program.
+
+        // Start by building a mapping from constants of the (translated) model to their defining expressions.
+        std::map<storm::expressions::Variable, storm::expressions::Expression> constantSubstitution;
+        for (auto const& constant : translatedProgram.getConstants()) {
+            if (constant.isDefined()) {
+                constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression());
+            }
         }
 
+        for (auto const& formula : formulas) {
+            result.formulas.emplace_back(formula->substitute(constantSubstitution));
+        }
         return result;
     }