diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp
index f62afa00f..a2b837080 100644
--- a/src/builder/DdJaniModelBuilder.cpp
+++ b/src/builder/DdJaniModelBuilder.cpp
@@ -102,22 +102,6 @@ namespace storm {
             }
         }
         
-        template <storm::dd::DdType Type, typename ValueType>
-        DdJaniModelBuilder<Type, ValueType>::DdJaniModelBuilder(storm::jani::Model const& model, Options const& options) : model(model), options(options) {
-            if (this->model->hasUndefinedConstants()) {
-                std::vector<std::reference_wrapper<storm::jani::Constant const>> undefinedConstants = this->model->getUndefinedConstants();
-                std::vector<std::string> strings;
-                for (auto const& constant : undefinedConstants) {
-                    std::stringstream stream;
-                    stream << constant.get().getName() << " (" << constant.get().getType() << ")";
-                    strings.push_back(stream.str());
-                }
-                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " << boost::join(strings, ", ") << ".");
-            }
-            
-            this->model = this->model->substituteConstants();
-        }
-        
         template <storm::dd::DdType Type, typename ValueType>
         struct CompositionVariables {
             CompositionVariables() : manager(std::make_shared<storm::dd::DdManager<Type>>()),
@@ -1732,31 +1716,42 @@ namespace storm {
         }
         
         template <storm::dd::DdType Type, typename ValueType>
-        std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> DdJaniModelBuilder<Type, ValueType>::build() {
+        std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> DdJaniModelBuilder<Type, ValueType>::build(storm::jani::Model const& model, Options const& options) {
+            if (model.hasUndefinedConstants()) {
+                std::vector<std::reference_wrapper<storm::jani::Constant const>> undefinedConstants = model.getUndefinedConstants();
+                std::vector<std::string> strings;
+                for (auto const& constant : undefinedConstants) {
+                    std::stringstream stream;
+                    stream << constant.get().getName() << " (" << constant.get().getType() << ")";
+                    strings.push_back(stream.str());
+                }
+                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Model still contains these undefined constants: " << boost::join(strings, ", ") << ".");
+            }
+            
             // Create all necessary variables.
-            CompositionVariableCreator<Type, ValueType> variableCreator(*this->model);
+            CompositionVariableCreator<Type, ValueType> variableCreator(model);
             CompositionVariables<Type, ValueType> variables = variableCreator.create();
             
             // Create a builder to compose and build the model.
-//            SeparateEdgesSystemComposer<Type, ValueType> composer(*this->model, variables);
-            CombinedEdgesSystemComposer<Type, ValueType> composer(*this->model, variables);
+//            SeparateEdgesSystemComposer<Type, ValueType> composer(model, variables);
+            CombinedEdgesSystemComposer<Type, ValueType> composer(model, variables);
             ComposerResult<Type, ValueType> system = composer.compose();
             
             // Postprocess the variables in place.
-            postprocessVariables(this->model->getModelType(), system, variables);
+            postprocessVariables(model.getModelType(), system, variables);
             
             // Postprocess the system in place and get the states that were terminal (i.e. whose transitions were cut off).
-            storm::dd::Bdd<Type> terminalStates = postprocessSystem(*this->model, system, variables, options);
+            storm::dd::Bdd<Type> terminalStates = postprocessSystem(model, system, variables, options);
             
             // Start creating the model components.
             ModelComponents<Type, ValueType> modelComponents;
             
             // Build initial states.
-            modelComponents.initialStates = computeInitialStates(*this->model, variables);
+            modelComponents.initialStates = computeInitialStates(model, variables);
             
             // Perform reachability analysis to obtain reachable states.
             storm::dd::Bdd<Type> transitionMatrixBdd = system.transitions.notZero();
-            if (this->model->getModelType() == storm::jani::ModelType::MDP) {
+            if (model.getModelType() == storm::jani::ModelType::MDP) {
                 transitionMatrixBdd = transitionMatrixBdd.existsAbstract(variables.allNondeterminismVariables);
             }
             modelComponents.reachableStates = storm::utility::dd::computeReachableStates(modelComponents.initialStates, transitionMatrixBdd, variables.rowMetaVariables, variables.columnMetaVariables);
@@ -1770,13 +1765,13 @@ namespace storm {
             modelComponents.transitionMatrix = system.transitions * reachableStatesAdd;
             
             // Fix deadlocks if existing.
-            modelComponents.deadlockStates = fixDeadlocks(this->model->getModelType(), modelComponents.transitionMatrix, transitionMatrixBdd, modelComponents.reachableStates, variables);
+            modelComponents.deadlockStates = fixDeadlocks(model.getModelType(), modelComponents.transitionMatrix, transitionMatrixBdd, modelComponents.reachableStates, variables);
             
             // Cut the deadlock states by removing all states that we 'converted' to deadlock states by making them terminal.
             modelComponents.deadlockStates = modelComponents.deadlockStates && !terminalStates;
             
             // Finally, create the model.
-            return createModel(this->model->getModelType(), variables, modelComponents);
+            return createModel(model.getModelType(), variables, modelComponents);
         }
         
         template class DdJaniModelBuilder<storm::dd::DdType::CUDD, double>;
diff --git a/src/builder/DdJaniModelBuilder.h b/src/builder/DdJaniModelBuilder.h
index 348d017ad..f1b16af1a 100644
--- a/src/builder/DdJaniModelBuilder.h
+++ b/src/builder/DdJaniModelBuilder.h
@@ -77,11 +77,6 @@ namespace storm {
                 boost::optional<storm::expressions::Expression> negatedTerminalStates;
             };
             
-            /*!
-             * Creates a builder for the given model that uses the given options.
-             */
-            DdJaniModelBuilder(storm::jani::Model const& model, Options const& options = Options());
-            
             /*!
              * Translates the given program into a symbolic model (i.e. one that stores the transition relation as a
              * decision diagram).
@@ -89,22 +84,7 @@ namespace storm {
              * @param model The model to translate.
              * @return A pointer to the resulting model.
              */
-            std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> build();
-            
-            /*!
-             * Retrieves the model that was actually translated (i.e. including constant substitutions etc.). Note
-             * that this function may only be called after a succesful translation.
-             *
-             * @return The translated model.
-             */
-            storm::jani::Model const& getTranslatedModel() const;
-                        
-        private:
-            /// The model to translate.
-            boost::optional<storm::jani::Model> model;
-            
-            /// The options to use for building the model.
-            Options options;
+            std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> build(storm::jani::Model const& model, Options const& options = Options());
         };
         
     }
diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index 6c495e15c..859a2424e 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -1222,17 +1222,10 @@ namespace storm {
             return storm::models::symbolic::StandardRewardModel<Type, ValueType>(stateRewards, stateActionRewards, transitionRewards);
         }
         
-        template <storm::dd::DdType Type, typename ValueType>
-        storm::prism::Program const& DdPrismModelBuilder<Type, ValueType>::getTranslatedProgram() const {
-            return preparedProgram.get();
-        }
-        
         template <storm::dd::DdType Type, typename ValueType>
         std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> DdPrismModelBuilder<Type, ValueType>::build(storm::prism::Program const& program, Options const& options) {
-            preparedProgram = program;
-            
-            if (preparedProgram->hasUndefinedConstants()) {
-                std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = preparedProgram->getUndefinedConstants();
+            if (program.hasUndefinedConstants()) {
+                std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = program.getUndefinedConstants();
                 std::stringstream stream;
                 bool printComma = false;
                 for (auto const& constant : undefinedConstants) {
@@ -1247,13 +1240,11 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str());
             }
             
-            preparedProgram = preparedProgram->substituteConstants();
-            
-            STORM_LOG_DEBUG("Building representation of program:" << std::endl << *preparedProgram << std::endl);
+            STORM_LOG_DEBUG("Building representation of program:" << std::endl << program << std::endl);
             
             // Start by initializing the structure used for storing all information needed during the model generation.
             // In particular, this creates the meta variables used to encode the model.
-            GenerationInformation generationInfo(*preparedProgram);
+            GenerationInformation generationInfo(program);
             
             SystemResult system = createSystemDecisionDiagram(generationInfo);
             storm::dd::Add<Type, ValueType> transitionMatrix = system.allTransitionsDd;
@@ -1264,7 +1255,7 @@ namespace storm {
             // If we were asked to treat some states as terminal states, we cut away their transitions now.
             storm::dd::Bdd<Type> terminalStatesBdd = generationInfo.manager->getBddZero();
             if (options.terminalStates || options.negatedTerminalStates) {
-                std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = preparedProgram->getConstantsSubstitution();
+                std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = program.getConstantsSubstitution();
                 
                 if (options.terminalStates) {
                     storm::expressions::Expression terminalExpression;
@@ -1273,7 +1264,7 @@ namespace storm {
                     } else {
                         std::string const& labelName = boost::get<std::string>(options.terminalStates.get());
                         if (program.hasLabel(labelName)) {
-                            terminalExpression = preparedProgram->getLabelExpression(labelName);
+                            terminalExpression = program.getLabelExpression(labelName);
                         } else {
                             STORM_LOG_THROW(labelName == "init" || labelName == "deadlock", storm::exceptions::InvalidArgumentException, "Terminal states refer to illegal label '" << labelName << "'.");
                         }
@@ -1294,7 +1285,7 @@ namespace storm {
                     } else {
                         std::string const& labelName = boost::get<std::string>(options.negatedTerminalStates.get());
                         if (program.hasLabel(labelName)) {
-                            negatedTerminalExpression = preparedProgram->getLabelExpression(labelName);
+                            negatedTerminalExpression = program.getLabelExpression(labelName);
                         } else {
                             STORM_LOG_THROW(labelName == "init" || labelName == "deadlock", storm::exceptions::InvalidArgumentException, "Terminal states refer to illegal label '" << labelName << "'.");
                         }
@@ -1377,18 +1368,18 @@ namespace storm {
             
             // First, we make sure that all selected reward models actually exist.
             for (auto const& rewardModelName : options.rewardModelsToBuild) {
-                STORM_LOG_THROW(rewardModelName.empty() || preparedProgram->hasRewardModel(rewardModelName), storm::exceptions::InvalidArgumentException, "Model does not possess a reward model with the name '" << rewardModelName << "'.");
+                STORM_LOG_THROW(rewardModelName.empty() || program.hasRewardModel(rewardModelName), storm::exceptions::InvalidArgumentException, "Model does not possess a reward model with the name '" << rewardModelName << "'.");
             }
             
-            for (auto const& rewardModel : preparedProgram->getRewardModels()) {
+            for (auto const& rewardModel : program.getRewardModels()) {
                 if (options.buildAllRewardModels || options.rewardModelsToBuild.find(rewardModel.getName()) != options.rewardModelsToBuild.end()) {
                     selectedRewardModels.push_back(rewardModel);
                 }
             }
             // If no reward model was selected until now and a referenced reward model appears to be unique, we build
             // the only existing reward model (given that no explicit name was given for the referenced reward model).
-            if (selectedRewardModels.empty() && preparedProgram->getNumberOfRewardModels() == 1 && options.rewardModelsToBuild.size() == 1 && *options.rewardModelsToBuild.begin() == "") {
-                selectedRewardModels.push_back(preparedProgram->getRewardModel(0));
+            if (selectedRewardModels.empty() && program.getNumberOfRewardModels() == 1 && options.rewardModelsToBuild.size() == 1 && *options.rewardModelsToBuild.begin() == "") {
+                selectedRewardModels.push_back(program.getRewardModel(0));
             }
             
             std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<Type, ValueType>> rewardModels;
@@ -1398,7 +1389,7 @@ namespace storm {
             
             // Build the labels that can be accessed as a shortcut.
             std::map<std::string, storm::expressions::Expression> labelToExpressionMapping;
-            for (auto const& label : preparedProgram->getLabels()) {
+            for (auto const& label : program.getLabels()) {
                 labelToExpressionMapping.emplace(label.getName(), label.getStatePredicateExpression());
             }
             
diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h
index 6db0c4639..464a0a071 100644
--- a/src/builder/DdPrismModelBuilder.h
+++ b/src/builder/DdPrismModelBuilder.h
@@ -98,14 +98,6 @@ namespace storm {
              */
             std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> build(storm::prism::Program const& program, Options const& options = Options());
             
-            /*!
-             * Retrieves the program that was actually translated (i.e. including constant substitutions etc.). Note
-             * that this function may only be called after a succesful translation.
-             *
-             * @return The translated program.
-             */
-            storm::prism::Program const& getTranslatedProgram() const;
-            
         private:
             // This structure can store the decision diagrams representing a particular action.
             struct UpdateDecisionDiagram {
@@ -243,9 +235,6 @@ namespace storm {
             static SystemResult createSystemDecisionDiagram(GenerationInformation& generationInfo);
             
             static storm::dd::Bdd<Type> createInitialStatesDecisionDiagram(GenerationInformation& generationInfo);
-            
-            // This member holds the program that was most recently translated (if any).
-            boost::optional<storm::prism::Program> preparedProgram;
         };
         
     } // namespace adapters
diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp
index 0629e0707..31a0a8afb 100644
--- a/src/cli/cli.cpp
+++ b/src/cli/cli.cpp
@@ -231,27 +231,20 @@ namespace storm {
                     }
                 }
 
-                // There may be constants of the model appearing in the formulas, so we replace all their occurrences
-                // by their definitions in the translated program.
-                std::vector<std::shared_ptr<storm::logic::Formula const>> preprocessedFormulas;
-                for (auto const& formula : formulas) {
-                    preprocessedFormulas.emplace_back(formula->substitute(constantsSubstitution));
-                }
-
                 if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isParametricSet()) {
 #ifdef STORM_HAVE_CARL
-                    buildAndCheckSymbolicModel<storm::RationalFunction>(preprocessedProgram, preprocessedFormulas, true);
+                    buildAndCheckSymbolicModel<storm::RationalFunction>(model, formulas, true);
 #else
                     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build.");
 #endif
                 } else if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isExactSet()) {
 #ifdef STORM_HAVE_CARL
-                    buildAndCheckSymbolicModel<storm::RationalNumber>(preprocessedProgram, preprocessedFormulas, true);
+                    buildAndCheckSymbolicModel<storm::RationalNumber>(model, formulas, true);
 #else
                     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No exact numbers are supported in this build.");
 #endif
                 } else {
-                    buildAndCheckSymbolicModel<double>(preprocessedProgram, preprocessedFormulas, true);
+                    buildAndCheckSymbolicModel<double>(model, formulas, true);
                 }
             } else if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExplicitSet()) {
                 STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Only the sparse engine supports explicit model input.");
diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h
index b41a0f07f..f4b009b7e 100644
--- a/src/cli/entrypoints.h
+++ b/src/cli/entrypoints.h
@@ -3,7 +3,10 @@
 
 #include "src/utility/storm.h"
 
+#include "src/storage/SymbolicModelDescription.h"
+
 #include "src/exceptions/NotImplementedException.h"
+#include "src/exceptions/InvalidSettingsException.h"
 
 namespace storm {
     namespace cli {
@@ -49,12 +52,14 @@ namespace storm {
 #endif
 
         template<storm::dd::DdType DdType>
-        void verifySymbolicModelWithAbstractionRefinementEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
+        void verifySymbolicModelWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Abstraction Refinement is not yet implemented.");
         }
         
         template<typename ValueType>
-        void verifySymbolicModelWithExplorationEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
+        void verifySymbolicModelWithExplorationEngine(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
+            STORM_LOG_THROW(model.isPrismProgram(), storm::exceptions::InvalidSettingsException, "Exploration engine is currently only applicable to PRISM models.");
+            storm::prism::Program const& program = model.asPrismProgram();
             STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Currently exploration-based verification is only available for DTMCs and MDPs.");
 
             for (auto const& formula : formulas) {
@@ -98,7 +103,7 @@ namespace storm {
         
 #ifdef STORM_HAVE_CARL
         template<>
-        void verifySymbolicModelWithExplorationEngine<storm::RationalFunction>(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) {
+        void verifySymbolicModelWithExplorationEngine<storm::RationalFunction>(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) {
             STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Exploration-based verification does currently not support parametric models.");
         }
 #endif
@@ -177,81 +182,80 @@ namespace storm {
     }
         
         template<storm::dd::DdType LibraryType>
-        void buildAndCheckSymbolicModelWithSymbolicEngine(bool hybrid, storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
+        void buildAndCheckSymbolicModelWithSymbolicEngine(bool hybrid, storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
             // Start by building the model.
-            auto model = buildSymbolicModel<double, LibraryType>(program, formulas);
+            auto markovModel = buildSymbolicModel<double, LibraryType>(model, formulas);
             
             // Print some information about the model.
-            model->printModelInformationToStream(std::cout);
+            markovModel->printModelInformationToStream(std::cout);
             
             // Then select the correct engine.
             if (hybrid) {
-                verifySymbolicModelWithHybridEngine(model, formulas, onlyInitialStatesRelevant);
+                verifySymbolicModelWithHybridEngine(markovModel, formulas, onlyInitialStatesRelevant);
             } else {
-                verifySymbolicModelWithDdEngine(model, formulas, onlyInitialStatesRelevant);
+                verifySymbolicModelWithDdEngine(markovModel, formulas, onlyInitialStatesRelevant);
             }
         }
         
         template<typename ValueType>
-        void buildAndCheckSymbolicModelWithSparseEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
+        void buildAndCheckSymbolicModelWithSparseEngine(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
             // Start by building the model.
-            std::shared_ptr<storm::models::ModelBase> model = buildSparseModel<ValueType>(program, formulas);
+            std::shared_ptr<storm::models::ModelBase> markovModel = buildSparseModel<ValueType>(model, formulas);
             
             // Print some information about the model.
-            model->printModelInformationToStream(std::cout);
+            markovModel->printModelInformationToStream(std::cout);
             
             // Preprocess the model.
-            BRANCH_ON_SPARSE_MODELTYPE(model, model, ValueType, preprocessModel, formulas);
+            BRANCH_ON_SPARSE_MODELTYPE(markovModel, markovModel, ValueType, preprocessModel, formulas);
             
-            std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->template as<storm::models::sparse::Model<ValueType>>();
+            std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = markovModel->template as<storm::models::sparse::Model<ValueType>>();
             
             // Finally, treat the formulas.
             if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isCounterexampleSet()) {
-                generateCounterexamples<ValueType>(program, sparseModel, formulas);
+                generateCounterexamples<ValueType>(model, sparseModel, formulas);
             } else {
                 verifySparseModel<ValueType>(sparseModel, formulas, onlyInitialStatesRelevant);
             }
         }
         
         template<typename ValueType>
-        void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
+        void buildAndCheckSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
             if (storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) {
                 auto ddlib = storm::settings::getModule<storm::settings::modules::CoreSettings>().getDdLibraryType();
                 if (ddlib == storm::dd::DdType::CUDD) {
-                    verifySymbolicModelWithAbstractionRefinementEngine<storm::dd::DdType::CUDD>(program, formulas, onlyInitialStatesRelevant);
+                    verifySymbolicModelWithAbstractionRefinementEngine<storm::dd::DdType::CUDD>(model, formulas, onlyInitialStatesRelevant);
                 } else {
-                    verifySymbolicModelWithAbstractionRefinementEngine<storm::dd::DdType::Sylvan>(program, formulas, onlyInitialStatesRelevant);
+                    verifySymbolicModelWithAbstractionRefinementEngine<storm::dd::DdType::Sylvan>(model, formulas, onlyInitialStatesRelevant);
                 }
             } else if (storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Exploration) {
-                verifySymbolicModelWithExplorationEngine<ValueType>(program, formulas, onlyInitialStatesRelevant);
+                verifySymbolicModelWithExplorationEngine<ValueType>(model, formulas, onlyInitialStatesRelevant);
             } else {
                 auto engine = storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine();
                 if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid) {
                     auto ddlib = storm::settings::getModule<storm::settings::modules::CoreSettings>().getDdLibraryType();
                     if (ddlib == storm::dd::DdType::CUDD) {
-                        buildAndCheckSymbolicModelWithSymbolicEngine<storm::dd::DdType::CUDD>(engine == storm::settings::modules::CoreSettings::Engine::Hybrid, program, formulas, onlyInitialStatesRelevant);
+                        buildAndCheckSymbolicModelWithSymbolicEngine<storm::dd::DdType::CUDD>(engine == storm::settings::modules::CoreSettings::Engine::Hybrid, model, formulas, onlyInitialStatesRelevant);
                     } else {
-                        buildAndCheckSymbolicModelWithSymbolicEngine<storm::dd::DdType::Sylvan>(engine == storm::settings::modules::CoreSettings::Engine::Hybrid, program, formulas, onlyInitialStatesRelevant);
+                        buildAndCheckSymbolicModelWithSymbolicEngine<storm::dd::DdType::Sylvan>(engine == storm::settings::modules::CoreSettings::Engine::Hybrid, model, formulas, onlyInitialStatesRelevant);
                     }
                 } else {
                     STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Illegal engine.");
-                    
-                    buildAndCheckSymbolicModelWithSparseEngine<ValueType>(program, formulas, onlyInitialStatesRelevant);
+                    buildAndCheckSymbolicModelWithSparseEngine<ValueType>(model, formulas, onlyInitialStatesRelevant);
                 }
             }
         }
         
 #ifdef STORM_HAVE_CARL
         template<>
-        void buildAndCheckSymbolicModel<storm::RationalNumber>(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) {
+        void buildAndCheckSymbolicModel<storm::RationalNumber>(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) {
             STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one.");
-            buildAndCheckSymbolicModelWithSparseEngine<storm::RationalNumber>(program, formulas, onlyInitialStatesRelevant);
+            buildAndCheckSymbolicModelWithSparseEngine<storm::RationalNumber>(model, formulas, onlyInitialStatesRelevant);
         }
         
         template<>
-        void buildAndCheckSymbolicModel<storm::RationalFunction>(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) {
+        void buildAndCheckSymbolicModel<storm::RationalFunction>(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) {
             STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one.");
-            buildAndCheckSymbolicModelWithSparseEngine<storm::RationalFunction>(program, formulas, onlyInitialStatesRelevant);
+            buildAndCheckSymbolicModelWithSparseEngine<storm::RationalFunction>(model, formulas, onlyInitialStatesRelevant);
         }
 #endif
         
diff --git a/src/storage/SymbolicModelDescription.h b/src/storage/SymbolicModelDescription.h
index ec9acf91f..77da92d82 100644
--- a/src/storage/SymbolicModelDescription.h
+++ b/src/storage/SymbolicModelDescription.h
@@ -10,7 +10,7 @@ namespace storm {
         
         class SymbolicModelDescription {
         public:
-            SymbolicModelDescription();
+            SymbolicModelDescription() = default;
             SymbolicModelDescription(storm::jani::Model const& model);
             SymbolicModelDescription(storm::prism::Program const& program);
 
diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp
index 0bec35317..9a9a95d8f 100644
--- a/src/storage/jani/Model.cpp
+++ b/src/storage/jani/Model.cpp
@@ -34,6 +34,10 @@ namespace storm {
             silentActionIndex = addAction(storm::jani::Action(SILENT_ACTION_NAME));
         }
         
+        storm::expressions::ExpressionManager& Model::getManager() const {
+            return *expressionManager;
+        }
+        
         uint64_t Model::getJaniVersion() const {
             return version;
         }
@@ -104,7 +108,7 @@ namespace storm {
         std::vector<Constant>& Model::getConstants() {
             return constants;
         }
-
+        
         Variable const& Model::addVariable(Variable const& variable) {
             if (variable.isBooleanVariable()) {
                 return addVariable(variable.asBooleanVariable());
diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h
index 946871cc5..375c4d792 100644
--- a/src/storage/jani/Model.h
+++ b/src/storage/jani/Model.h
@@ -30,6 +30,11 @@ namespace storm {
              * Creates an empty model with the given type.
              */
             Model(std::string const& name, ModelType const& modelType, uint64_t version = 1, boost::optional<std::shared_ptr<storm::expressions::ExpressionManager>> const& expressionManager = boost::none);
+
+            /*!
+             * Retrieves the expression manager responsible for the expressions in the model.
+             */
+            storm::expressions::ExpressionManager& getManager() const;
             
             /*!
              * Retrieves the JANI-version of the model.
@@ -106,7 +111,7 @@ namespace storm {
              * Retrieves the constant with the given name (if any).
              */
             Constant const& getConstant(std::string const& name) const;
-
+            
             /*!
              * Adds the given variable to this model.
              */
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index 99f4d3e4f..126f53c4e 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -332,7 +332,6 @@ namespace storm {
             return constantsSubstitution;
         }
         
-        
         std::size_t Program::getNumberOfConstants() const {
             return this->getConstants().size();
         }
diff --git a/src/utility/storm.cpp b/src/utility/storm.cpp
index 6ce361d5c..c567c05cb 100644
--- a/src/utility/storm.cpp
+++ b/src/utility/storm.cpp
@@ -43,12 +43,23 @@ namespace storm {
         return parseFormulas(formulaParser, inputString);
     }
 
+    std::vector<std::shared_ptr<storm::logic::Formula const>> substituteConstantsInFormulas(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
+        std::vector<std::shared_ptr<storm::logic::Formula const>> preprocessedFormulas;
+        for (auto const& formula : formulas) {
+            preprocessedFormulas.emplace_back(formula->substitute(substitution));
+        }
+        return preprocessedFormulas;
+    }
+    
     std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForJaniModel(std::string const& inputString, storm::jani::Model const& model) {
         storm::parser::FormulaParser formulaParser(model.getManager().getSharedPointer());
-        return parseFormulas(formulaParser, inputString);
+        auto formulas = parseFormulas(formulaParser, inputString);
+        return substituteConstantsInFormulas(formulas, model.getConstantsSubstitution());
     }
+    
     std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForPrismProgram(std::string const& inputString, storm::prism::Program const& program) {
         storm::parser::FormulaParser formulaParser(program);
-        return parseFormulas(formulaParser, inputString);
+        auto formulas = parseFormulas(formulaParser, inputString);
+        return substituteConstantsInFormulas(formulas, program.getConstantsSubstitution());
     } 
 }
diff --git a/src/utility/storm.h b/src/utility/storm.h
index d1c767615..c5df89d64 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -48,11 +48,13 @@
 // Headers of builders.
 #include "src/builder/ExplicitModelBuilder.h"
 #include "src/builder/DdPrismModelBuilder.h"
+#include "src/builder/DdJaniModelBuilder.h"
 
 // Headers for model processing.
 #include "src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h"
 #include "src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h"
 #include "src/storage/ModelFormulasPair.h"
+#include "src/storage/SymbolicModelDescription.h"
 
 // Headers for model checking.
 #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
@@ -79,9 +81,9 @@
 #include "src/counterexamples/MILPMinimalLabelSetGenerator.h"
 #include "src/counterexamples/SMTMinimalCommandSetGenerator.h"
 
-// Headers related to PRISM model building.
+// Headers related to model building.
 #include "src/generator/PrismNextStateGenerator.h"
-#include "src/utility/prism.h"
+#include "src/generator/JaniNextStateGenerator.h"
 
 // Headers related to exception handling.
 #include "src/exceptions/InvalidStateException.h"
@@ -101,10 +103,11 @@ namespace storm {
     std::pair<storm::jani::Model, std::vector<storm::jani::Property>> parseJaniModel(std::string const& path);
     storm::prism::Program parseProgram(std::string const& path);
     std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForExplicit(std::string const& inputString);
-    std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program);
+    std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForPrismProgram(std::string const& inputString, storm::prism::Program const& program);
+    std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForJaniModel(std::string const& inputString, storm::jani::Model const& model);
 
     template<typename ValueType>
-    std::shared_ptr<storm::models::sparse::Model<ValueType>> buildSparseModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
+    std::shared_ptr<storm::models::sparse::Model<ValueType>> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
         storm::generator::NextStateGeneratorOptions options(formulas);
 
         // Generate command labels if we are going to build a counterexample later.
@@ -112,18 +115,34 @@ namespace storm {
             options.setBuildChoiceLabels(true);
         }
 
-        std::shared_ptr<storm::generator::NextStateGenerator<ValueType, uint32_t>> generator = std::make_shared<storm::generator::PrismNextStateGenerator<ValueType, uint32_t>>(program, options);
+        std::shared_ptr<storm::generator::NextStateGenerator<ValueType, uint32_t>> generator;
+        if (model.isPrismProgram()) {
+            generator = std::make_shared<storm::generator::PrismNextStateGenerator<ValueType, uint32_t>>(model.asPrismProgram(), options);
+        } else if (model.isJaniModel()) {
+            generator = std::make_shared<storm::generator::JaniNextStateGenerator<ValueType, uint32_t>>(model.asJaniModel(), options);
+        } else {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot build sparse model from this symbolic model description.");
+        }
         storm::builder::ExplicitModelBuilder<ValueType> builder(generator);
         return builder.build();
     }
 
     template<typename ValueType, storm::dd::DdType LibraryType = storm::dd::DdType::CUDD>
-    std::shared_ptr<storm::models::symbolic::Model<LibraryType, ValueType>> buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
-        typename storm::builder::DdPrismModelBuilder<LibraryType, ValueType>::Options options;
-        options = typename storm::builder::DdPrismModelBuilder<LibraryType, ValueType>::Options(formulas);
-
-        storm::builder::DdPrismModelBuilder<LibraryType, ValueType> builder;
-        return builder.build(program, options);
+    std::shared_ptr<storm::models::symbolic::Model<LibraryType, ValueType>> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
+        if (model.isPrismProgram()) {
+            typename storm::builder::DdPrismModelBuilder<LibraryType, ValueType>::Options options;
+            options = typename storm::builder::DdPrismModelBuilder<LibraryType, ValueType>::Options(formulas);
+            
+            storm::builder::DdPrismModelBuilder<LibraryType, ValueType> builder;
+            return builder.build(model.asPrismProgram(), options);
+        } else {
+            STORM_LOG_THROW(model.isJaniModel(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model for the given symbolic model description.");
+            typename storm::builder::DdJaniModelBuilder<LibraryType, ValueType>::Options options;
+            options = typename storm::builder::DdJaniModelBuilder<LibraryType, ValueType>::Options(formulas);
+            
+            storm::builder::DdJaniModelBuilder<LibraryType, ValueType> builder;
+            return builder.build(model.asJaniModel(), options);
+        }
     }
     
     template<typename ModelType>
@@ -205,11 +224,13 @@ namespace storm {
     }
 
     template<typename ValueType>
-    void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<storm::logic::Formula const> const& formula) {
+    void generateCounterexample(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::models::sparse::Model<ValueType>> markovModel, std::shared_ptr<storm::logic::Formula const> const& formula) {
         if (storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>().isMinimalCommandSetGenerationSet()) {
-            STORM_LOG_THROW(model->getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for MDPs.");
-
-            std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
+            STORM_LOG_THROW(model.isPrismProgram(), storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for PRISM models.");
+            STORM_LOG_THROW(markovModel->getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for MDPs.");
+            storm::prism::Program const& program = model.asPrismProgram();
+            
+            std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = markovModel->template as<storm::models::sparse::Mdp<ValueType>>();
 
             // Determine whether we are required to use the MILP-version or the SAT-version.
             bool useMILP = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>().isUseMilpBasedMinimalCommandSetGenerationSet();
@@ -227,20 +248,20 @@ namespace storm {
 
 #ifdef STORM_HAVE_CARL
     template<>
-    inline void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> model, std::shared_ptr<storm::logic::Formula const> const& formula) {
-        STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model.");
+    inline void generateCounterexample(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> markovModel, std::shared_ptr<storm::logic::Formula const> const& formula) {
+        STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for exact arithmetic model.");
     }
 
     template<>
-    inline void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula const> const& formula) {
+    inline void generateCounterexample(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> markovModel, std::shared_ptr<storm::logic::Formula const> const& formula) {
         STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model.");
     }
 #endif
 
     template<typename ValueType>
-    void generateCounterexamples(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
+    void generateCounterexamples(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::models::sparse::Model<ValueType>> markovModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
         for (auto const& formula : formulas) {
-            generateCounterexample(program, model, formula);
+            generateCounterexample(model, markovModel, formula);
         }
     }
 
@@ -408,7 +429,7 @@ namespace storm {
         // Program and formula
         storm::prism::Program program = parseProgram(programFilePath);
         program.checkValidity();
-        std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = parseFormulasForProgram(formulaString, program);;
+        std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = parseFormulasForPrismProgram(formulaString, program);
         if(formulas.size()!=1) {
             STORM_LOG_ERROR("The given formulaString does not specify exactly one formula");
             return false;