diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp
index 31a0a8afb..78cbcc042 100644
--- a/src/cli/cli.cpp
+++ b/src/cli/cli.cpp
@@ -219,7 +219,7 @@ namespace storm {
                 
                 // Get the string that assigns values to the unknown currently undefined constants in the model.
                 std::string constantDefinitionString = ioSettings.getConstantDefinitionString();
-                model.preprocess(constantDefinitionString);
+                model = model.preprocess(constantDefinitionString);
 
                 // Then proceed to parsing the properties (if given), since the model we are building may depend on the property.
                 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
diff --git a/src/storage/SymbolicModelDescription.cpp b/src/storage/SymbolicModelDescription.cpp
index adb1e2afc..3bccf3b73 100644
--- a/src/storage/SymbolicModelDescription.cpp
+++ b/src/storage/SymbolicModelDescription.cpp
@@ -17,6 +17,14 @@ namespace storm {
             // Intentionally left empty.
         }
         
+        SymbolicModelDescription& SymbolicModelDescription::operator=(storm::jani::Model const& model) {
+            this->modelDescription = model;
+        }
+        
+        SymbolicModelDescription& SymbolicModelDescription::operator=(storm::prism::Program const& program) {
+            this->modelDescription = program;
+        }
+        
         bool SymbolicModelDescription::hasModel() const {
             return static_cast<bool>(modelDescription);
         }
@@ -47,27 +55,26 @@ namespace storm {
             return boost::get<storm::prism::Program>(modelDescription.get());
         }
         
-        void SymbolicModelDescription::toJani(bool makeVariablesGlobal) {
+        SymbolicModelDescription SymbolicModelDescription::toJani(bool makeVariablesGlobal) const {
             if (this->isJaniModel()) {
-                return;
+                return *this;
             }
             if (this->isPrismProgram()) {
-                modelDescription = this->asPrismProgram().toJani(makeVariablesGlobal);
+                return SymbolicModelDescription(this->asPrismProgram().toJani(makeVariablesGlobal));
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot transform model description to the JANI format.");
             }
         }
         
-        void SymbolicModelDescription::preprocess(std::string const& constantDefinitionString) {
+        SymbolicModelDescription SymbolicModelDescription::preprocess(std::string const& constantDefinitionString) const {
             if (this->isJaniModel()) {
                 std::map<storm::expressions::Variable, storm::expressions::Expression> substitution = storm::utility::jani::parseConstantDefinitionString(this->asJaniModel(), constantDefinitionString);
-                this->modelDescription = this->asJaniModel().defineUndefinedConstants(substitution);
-                this->modelDescription = this->asJaniModel().substituteConstants();
+                return SymbolicModelDescription(this->asJaniModel().defineUndefinedConstants(substitution).substituteConstants());
             } else if (this->isPrismProgram()) {
                 std::map<storm::expressions::Variable, storm::expressions::Expression> substitution = storm::utility::prism::parseConstantDefinitionString(this->asPrismProgram(), constantDefinitionString);
-                this->modelDescription = this->asPrismProgram().defineUndefinedConstants(substitution);
-                this->modelDescription = this->asPrismProgram().substituteConstants();
+                return SymbolicModelDescription(this->asPrismProgram().defineUndefinedConstants(substitution).substituteConstants());
             }
+            return *this;
         }
         
     }
diff --git a/src/storage/SymbolicModelDescription.h b/src/storage/SymbolicModelDescription.h
index cd08f9ba0..8b5b85d88 100644
--- a/src/storage/SymbolicModelDescription.h
+++ b/src/storage/SymbolicModelDescription.h
@@ -14,6 +14,9 @@ namespace storm {
             SymbolicModelDescription(storm::jani::Model const& model);
             SymbolicModelDescription(storm::prism::Program const& program);
 
+            SymbolicModelDescription& operator=(storm::jani::Model const& model);
+            SymbolicModelDescription& operator=(storm::prism::Program const& program);
+            
             bool hasModel() const;
             bool isJaniModel() const;
             bool isPrismProgram() const;
@@ -24,9 +27,9 @@ namespace storm {
             storm::jani::Model const& asJaniModel() const;
             storm::prism::Program const& asPrismProgram() const;
             
-            void toJani(bool makeVariablesGlobal = true);
+            SymbolicModelDescription toJani(bool makeVariablesGlobal = true) const;
             
-            void preprocess(std::string const& constantDefinitionString = "");
+            SymbolicModelDescription preprocess(std::string const& constantDefinitionString = "") const;
             
         private:
             boost::optional<boost::variant<storm::jani::Model, storm::prism::Program>> modelDescription;
diff --git a/src/storage/prism/ToJaniConverter.cpp b/src/storage/prism/ToJaniConverter.cpp
index 7c3d859b2..33ad88fef 100644
--- a/src/storage/prism/ToJaniConverter.cpp
+++ b/src/storage/prism/ToJaniConverter.cpp
@@ -137,11 +137,15 @@ namespace storm {
                 }
                 STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotImplementedException, "Transition reward translation currently not implemented.");
             }
+            STORM_LOG_THROW(transientEdgeAssignments.empty() || transientLocationAssignments.empty() || !program.specifiesSystemComposition(), storm::exceptions::NotImplementedException, "Cannot translate reward models from PRISM to JANI that  specify a custom system composition.");
             
             // Now create the separate JANI automata from the modules of the PRISM program. While doing so, we use the
             // previously built mapping to make variables global that are read by more than one module.
             bool firstModule = true;
             for (auto const& module : program.getModules()) {
+                // Keep track of the action indices contained in this module.
+                std::set<uint_fast64_t> actionIndicesOfModule;
+
                 storm::jani::Automaton automaton(module.getName());
                 for (auto const& variable : module.getIntegerVariables()) {
                     storm::jani::BoundedIntegerVariable newIntegerVariable = *storm::jani::makeBoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression());
@@ -184,6 +188,8 @@ namespace storm {
                 }
                 
                 for (auto const& command : module.getCommands()) {
+                    actionIndicesOfModule.insert(command.getActionIndex());
+                    
                     boost::optional<storm::expressions::Expression> rateExpression;
                     std::vector<storm::jani::EdgeDestination> destinations;
                     if (program.getModelType() == Program::ModelType::CTMC || program.getModelType() == Program::ModelType::CTMDP) {
@@ -224,6 +230,17 @@ namespace storm {
                     automaton.addEdge(newEdge);
                 }
                 
+                // Now remove for all actions of this module the corresponding transient assignments, because we must
+                // not deal out this reward multiple times.
+                // NOTE: This only works for the standard composition and not for any custom compositions. This case
+                // must be checked for earlier.
+                for (auto actionIndex : actionIndicesOfModule) {
+                    auto it = transientEdgeAssignments.find(actionIndex);
+                    if (it != transientEdgeAssignments.end()) {
+                        transientEdgeAssignments.erase(it);
+                    }
+                }
+                
                 janiModel.addAutomaton(automaton);
                 firstModule = false;
             }
diff --git a/test/functional/builder/DdJaniModelBuilderTest.cpp b/test/functional/builder/DdJaniModelBuilderTest.cpp
index 1470e196d..3fc00e217 100644
--- a/test/functional/builder/DdJaniModelBuilderTest.cpp
+++ b/test/functional/builder/DdJaniModelBuilderTest.cpp
@@ -6,6 +6,7 @@
 
 #include "src/storage/dd/Add.h"
 #include "src/storage/dd/Bdd.h"
+#include "src/storage/SymbolicModelDescription.h"
 
 #include "src/models/symbolic/StandardRewardModel.h"
 #include "src/parser/PrismParser.h"
@@ -16,78 +17,70 @@
 #include "src/settings/modules/IOSettings.h"
 
 TEST(DdJaniModelBuilderTest_Sylvan, Dtmc) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
-    storm::jani::Model janiModel = program.toJani(true);
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
     
-    storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder(janiModel);
-    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.build();
+    storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder;
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.build(janiModel);
     EXPECT_EQ(13ul, model->getNumberOfStates());
     EXPECT_EQ(20ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     EXPECT_EQ(677ul, model->getNumberOfStates());
     EXPECT_EQ(867ul, model->getNumberOfTransitions());
         
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     EXPECT_EQ(8607ul, model->getNumberOfStates());
     EXPECT_EQ(15113ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     EXPECT_EQ(273ul, model->getNumberOfStates());
     EXPECT_EQ(397ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
-    janiModel = program.toJani(true);
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
     
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
-    model = builder.build();
+    model = builder.build(janiModel);
     EXPECT_EQ(1728ul, model->getNumberOfStates());
     EXPECT_EQ(2505ul, model->getNumberOfTransitions());
 }
 
 TEST(DdJaniModelBuilderTest_Cudd, Dtmc) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
-    storm::jani::Model janiModel = program.toJani(true);
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
     
-    storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder(janiModel);
-    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.build();
+    storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder;
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.build(janiModel);
     EXPECT_EQ(13ul, model->getNumberOfStates());
     EXPECT_EQ(20ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     EXPECT_EQ(677ul, model->getNumberOfStates());
     EXPECT_EQ(867ul, model->getNumberOfTransitions());
 
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     EXPECT_EQ(8607ul, model->getNumberOfStates());
     EXPECT_EQ(15113ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     EXPECT_EQ(273ul, model->getNumberOfStates());
     EXPECT_EQ(397ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     EXPECT_EQ(1728ul, model->getNumberOfStates());
     EXPECT_EQ(2505ul, model->getNumberOfTransitions());
 }
@@ -96,38 +89,34 @@ TEST(DdJaniModelBuilderTest_Sylvan, Ctmc) {
     // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
     std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
     
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
-    storm::jani::Model janiModel = program.toJani(true);
-    storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder(janiModel);
-    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.build();
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
+    storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder;
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.build(janiModel);
     EXPECT_EQ(276ul, model->getNumberOfStates());
     EXPECT_EQ(1120ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     EXPECT_EQ(3478ul, model->getNumberOfStates());
     EXPECT_EQ(14639ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     EXPECT_EQ(12ul, model->getNumberOfStates());
     EXPECT_EQ(22ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     EXPECT_EQ(810ul, model->getNumberOfStates());
     EXPECT_EQ(3699ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     EXPECT_EQ(66ul, model->getNumberOfStates());
     EXPECT_EQ(189ul, model->getNumberOfTransitions());
 }
@@ -136,47 +125,43 @@ TEST(DdJaniModelBuilderTest_Cudd, Ctmc) {
     // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
     std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
     
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
-    storm::jani::Model janiModel = program.toJani(true);
-    storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder(janiModel);
-    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.build();
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
+    storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder;
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.build(janiModel);
     EXPECT_EQ(276ul, model->getNumberOfStates());
     EXPECT_EQ(1120ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     EXPECT_EQ(3478ul, model->getNumberOfStates());
     EXPECT_EQ(14639ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     EXPECT_EQ(12ul, model->getNumberOfStates());
     EXPECT_EQ(22ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     EXPECT_EQ(810ul, model->getNumberOfStates());
     EXPECT_EQ(3699ul, model->getNumberOfTransitions());
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     EXPECT_EQ(66ul, model->getNumberOfStates());
     EXPECT_EQ(189ul, model->getNumberOfTransitions());
 }
 
 TEST(DdJaniModelBuilderTest_Sylvan, Mdp) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
-    storm::jani::Model janiModel = program.toJani(true);
-    storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder(janiModel);
-    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.build();
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder;
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.build(janiModel);
     
     EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
     std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
@@ -185,10 +170,9 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) {
     EXPECT_EQ(436ul, mdp->getNumberOfTransitions());
     EXPECT_EQ(254ul, mdp->getNumberOfChoices());
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     
     EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
     mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
@@ -197,10 +181,9 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) {
     EXPECT_EQ(654ul, mdp->getNumberOfTransitions());
     EXPECT_EQ(573ul, mdp->getNumberOfChoices());
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     
     EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
     mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
@@ -209,10 +192,9 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) {
     EXPECT_EQ(492ul, mdp->getNumberOfTransitions());
     EXPECT_EQ(400ul, mdp->getNumberOfChoices());
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     
     EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
     mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
@@ -221,10 +203,9 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) {
     EXPECT_EQ(1282ul, mdp->getNumberOfTransitions());
     EXPECT_EQ(1054ul, mdp->getNumberOfChoices());
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     
     EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
     mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
@@ -233,10 +214,9 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) {
     EXPECT_EQ(5585ul, mdp->getNumberOfTransitions());
     EXPECT_EQ(5519ul, mdp->getNumberOfChoices());
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     
     EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
     mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
@@ -247,10 +227,10 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) {
 }
 
 TEST(DdJaniModelBuilderTest_Cudd, Mdp) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
-    storm::jani::Model janiModel = program.toJani(true);
-    storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder(janiModel);
-    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.build();
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder;
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.build(janiModel);
     
     EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
     std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
@@ -259,10 +239,9 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) {
     EXPECT_EQ(436ul, mdp->getNumberOfTransitions());
     EXPECT_EQ(254ul, mdp->getNumberOfChoices());
         
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     
     EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
     mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
@@ -271,10 +250,9 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) {
     EXPECT_EQ(654ul, mdp->getNumberOfTransitions());
     EXPECT_EQ(573ul, mdp->getNumberOfChoices());
         
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     
     EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
     mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
@@ -283,10 +261,9 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) {
     EXPECT_EQ(492ul, mdp->getNumberOfTransitions());
     EXPECT_EQ(400ul, mdp->getNumberOfChoices());
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     
     EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
     mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
@@ -295,10 +272,9 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) {
     EXPECT_EQ(1282ul, mdp->getNumberOfTransitions());
     EXPECT_EQ(1054ul, mdp->getNumberOfChoices());
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     
     EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
     mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
@@ -307,10 +283,9 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) {
     EXPECT_EQ(5585ul, mdp->getNumberOfTransitions());
     EXPECT_EQ(5519ul, mdp->getNumberOfChoices());
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
-    janiModel = program.toJani(true);
-    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
-    model = builder.build();
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
+    janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    model = builder.build(janiModel);
     
     EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
     mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
@@ -321,8 +296,8 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) {
 }
 
 TEST(DdJaniModelBuilderTest_Cudd, IllegalSynchronizingWrites) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2-illegalSynchronizingWrite.nm");
-    storm::jani::Model janiModel = program.toJani(true);
-    storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder(janiModel);
-    EXPECT_THROW(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.build(), storm::exceptions::WrongFormatException);
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2-illegalSynchronizingWrite.nm");
+    storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
+    storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder;
+    EXPECT_THROW(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.build(janiModel), storm::exceptions::WrongFormatException);
 }
\ No newline at end of file
diff --git a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp
index f14808886..aed634c75 100644
--- a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp
+++ b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp
@@ -24,7 +24,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) {
     // Program and formula
     storm::prism::Program program = storm::parseProgram(programFile);
     program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaAsString, program);;
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);;
     std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
     auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
     storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
@@ -95,7 +95,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) {
     
     storm::prism::Program program = storm::parseProgram(programFile);
     program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaAsString, program);;
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);;
     std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
     auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
     storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
@@ -189,7 +189,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_Infty) {
     carl::VariablePool::getInstance().clear();
     storm::prism::Program program = storm::parseProgram(programFile);
     program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaAsString, program);;
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);;
     std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
     auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
     storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
@@ -233,7 +233,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_4Par) {
     carl::VariablePool::getInstance().clear();
     storm::prism::Program program = storm::parseProgram(programFile);
     program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaAsString, program);;
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);;
     std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
     auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
     storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
@@ -297,7 +297,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) {
 
     storm::prism::Program program = storm::parseProgram(programFile);
     program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaAsString, program);;
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);;
     std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
     auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
     storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
@@ -389,7 +389,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_1Par) {
     
     storm::prism::Program program = storm::parseProgram(programFile);
     program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaAsString, program);;
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);;
     std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
     auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
     storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
@@ -455,7 +455,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_Const) {
     
     storm::prism::Program program = storm::parseProgram(programFile);
     program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaAsString, program);;
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);;
     std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
     auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
     storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
diff --git a/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp
index 1ceb6c4e6..2b2aa9d2c 100644
--- a/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp
+++ b/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp
@@ -23,7 +23,7 @@ TEST(SparseMdpRegionModelCheckerTest, two_dice_Prob) {
     carl::VariablePool::getInstance().clear();
 
     storm::prism::Program program = storm::parseProgram(programFile);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaFile, program);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaFile, program);
     std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
     auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
     storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
@@ -91,7 +91,7 @@ TEST(SparseMdpRegionModelCheckerTest, coin_Prob) {
     carl::VariablePool::getInstance().clear();
 
     storm::prism::Program program = storm::parseProgram(programFile);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaAsString, program);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);
     std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
     auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
     storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
diff --git a/test/functional/utility/ModelInstantiatorTest.cpp b/test/functional/utility/ModelInstantiatorTest.cpp
index 2dd74c66a..d1319613c 100644
--- a/test/functional/utility/ModelInstantiatorTest.cpp
+++ b/test/functional/utility/ModelInstantiatorTest.cpp
@@ -26,7 +26,7 @@ TEST(ModelInstantiatorTest, BrpProb) {
     // Program and formula
     storm::prism::Program program = storm::parseProgram(programFile);
     program.checkValidity();
-    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulaAsString, program);
+    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);
     ASSERT_TRUE(formulas.size()==1);
     // Parametric model
     storm::generator::NextStateGeneratorOptions options(*formulas.front());
@@ -144,7 +144,7 @@ TEST(ModelInstantiatorTest, Brp_Rew) {
     // Program and formula
     storm::prism::Program program = storm::parseProgram(programFile);
     program.checkValidity();
-    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulaAsString, program);
+    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);
     ASSERT_TRUE(formulas.size()==1);
     // Parametric model
     storm::generator::NextStateGeneratorOptions options(*formulas.front());
@@ -214,7 +214,7 @@ TEST(ModelInstantiatorTest, Consensus) {
     // Program and formula
     storm::prism::Program program = storm::parseProgram(programFile);
     program.checkValidity();
-    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulaAsString, program);
+    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);
     ASSERT_TRUE(formulas.size()==1);
     // Parametric model
     storm::generator::NextStateGeneratorOptions options(*formulas.front());