diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
index f2cb7a3d2..5fdc39a05 100644
--- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
+++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
@@ -58,7 +58,7 @@ namespace storm {
                 
                 // Flatten the modules if there is more than one.
                 if (originalProgram.getNumberOfModules() > 1) {
-                    preprocessedModel = originalProgram.flattenModules(this->smtSolverFactory);
+                    preprocessedModel = originalProgram.substituteFormulas().flattenModules(this->smtSolverFactory);
                 } else {
                     preprocessedModel = originalProgram;
                 }
diff --git a/src/test/storm/storage/JaniModelTest.cpp b/src/test/storm/storage/JaniModelTest.cpp
index c7a6b5c11..a18aa279c 100644
--- a/src/test/storm/storage/JaniModelTest.cpp
+++ b/src/test/storm/storage/JaniModelTest.cpp
@@ -14,6 +14,7 @@ TEST(JaniModelTest, FlattenComposition) {
     
     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
     
+    janiModel.substituteFunctions();
     ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
     EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
     EXPECT_EQ(74ull, janiModel.getAutomaton(0).getNumberOfEdges());
@@ -26,6 +27,7 @@ TEST(JaniModelTest, FlattenComposition_Wlan_Mathsat) {
     
     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
     
+    janiModel.substituteFunctions();
     ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
     EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
     EXPECT_EQ(179ull, janiModel.getAutomaton(0).getNumberOfEdges());
@@ -38,6 +40,7 @@ TEST(JaniModelTest, FlattenComposition_Csma_Mathsat) {
     
     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
     
+    janiModel.substituteFunctions();
     ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
     EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
     EXPECT_EQ(70ull, janiModel.getAutomaton(0).getNumberOfEdges());
@@ -50,6 +53,7 @@ TEST(JaniModelTest, FlattenComposition_Firewire_Mathsat) {
     
     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
     
+    janiModel.substituteFunctions();
     ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
     EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
     EXPECT_EQ(5024ull, janiModel.getAutomaton(0).getNumberOfEdges());
@@ -62,6 +66,7 @@ TEST(JaniModelTest, FlattenComposition_Coin_Mathsat) {
     
     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
     
+    janiModel.substituteFunctions();
     ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
     EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
     EXPECT_EQ(13ull, janiModel.getAutomaton(0).getNumberOfEdges());
@@ -74,6 +79,7 @@ TEST(JaniModelTest, FlattenComposition_Dice_Mathsat) {
     
     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
     
+    janiModel.substituteFunctions();
     ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
     EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
     EXPECT_EQ(16ull, janiModel.getAutomaton(0).getNumberOfEdges());
@@ -88,6 +94,7 @@ TEST(JaniModelTest, FlattenComposition_Leader_Z3) {
     
     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
     
+    janiModel.substituteFunctions();
     ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
     EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
     EXPECT_EQ(74ull, janiModel.getAutomaton(0).getNumberOfEdges());
@@ -100,6 +107,7 @@ TEST(JaniModelTest, FlattenComposition_Wlan_Z3) {
     
     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
     
+    janiModel.substituteFunctions();
     ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
     EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
     EXPECT_EQ(179ull, janiModel.getAutomaton(0).getNumberOfEdges());
@@ -112,6 +120,7 @@ TEST(JaniModelTest, FlattenComposition_Csma_Z3) {
 
     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
     
+    janiModel.substituteFunctions();
     ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
     EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
     EXPECT_EQ(70ull, janiModel.getAutomaton(0).getNumberOfEdges());
@@ -124,6 +133,7 @@ TEST(JaniModelTest, FlattenComposition_Firewire_Z3) {
 
     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
     
+    janiModel.substituteFunctions();
     ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
     EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
     EXPECT_EQ(5024ull, janiModel.getAutomaton(0).getNumberOfEdges());
@@ -136,6 +146,7 @@ TEST(JaniModelTest, FlattenComposition_Coin_Z3) {
 
     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
     
+    janiModel.substituteFunctions();
     ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
     EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
     EXPECT_EQ(13ull, janiModel.getAutomaton(0).getNumberOfEdges());
@@ -148,6 +159,7 @@ TEST(JaniModelTest, FlattenComposition_Dice_Z3) {
 
     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
     
+    janiModel.substituteFunctions();
     ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory));
     EXPECT_EQ(1ull, janiModel.getNumberOfAutomata());
     EXPECT_EQ(16ull, janiModel.getAutomaton(0).getNumberOfEdges());
diff --git a/src/test/storm/storage/PrismProgramTest.cpp b/src/test/storm/storage/PrismProgramTest.cpp
index e860fa997..86246f632 100644
--- a/src/test/storm/storage/PrismProgramTest.cpp
+++ b/src/test/storm/storage/PrismProgramTest.cpp
@@ -13,7 +13,7 @@ TEST(PrismProgramTest, FlattenModules) {
 
     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
     
-    ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory));
+    ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory));
     EXPECT_EQ(1ull, program.getNumberOfModules());
     EXPECT_EQ(74ull, program.getModule(0).getNumberOfCommands());
 }
@@ -24,7 +24,7 @@ TEST(PrismProgramTest, FlattenModules_Wlan_Mathsat) {
     
     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
 
-    ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory));
+    ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory));
     EXPECT_EQ(1ull, program.getNumberOfModules());
     EXPECT_EQ(179ull, program.getModule(0).getNumberOfCommands());
 }
@@ -35,7 +35,7 @@ TEST(PrismProgramTest, FlattenModules_Csma_Mathsat) {
     
     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
 
-    ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory));
+    ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory));
     EXPECT_EQ(1ull, program.getNumberOfModules());
     EXPECT_EQ(70ull, program.getModule(0).getNumberOfCommands());
 }
@@ -46,7 +46,7 @@ TEST(PrismProgramTest, FlattenModules_Firewire_Mathsat) {
     
     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
 
-    ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory));
+    ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory));
     EXPECT_EQ(1ull, program.getNumberOfModules());
     EXPECT_EQ(5024ull, program.getModule(0).getNumberOfCommands());
 }
@@ -57,7 +57,7 @@ TEST(PrismProgramTest, FlattenModules_Coin_Mathsat) {
     
     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
 
-    ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory));
+    ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory));
     EXPECT_EQ(1ull, program.getNumberOfModules());
     EXPECT_EQ(13ull, program.getModule(0).getNumberOfCommands());
 }
@@ -68,7 +68,7 @@ TEST(PrismProgramTest, FlattenModules_Dice_Mathsat) {
 
     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>();
 
-    ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory));
+    ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory));
     EXPECT_EQ(1ull, program.getNumberOfModules());
     EXPECT_EQ(16ull, program.getModule(0).getNumberOfCommands());
 }
@@ -81,7 +81,7 @@ TEST(PrismProgramTest, FlattenModules_Leader_Z3) {
     
     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
     
-    ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory));
+    ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory));
     EXPECT_EQ(1ull, program.getNumberOfModules());
     EXPECT_EQ(74ull, program.getModule(0).getNumberOfCommands());
 }
@@ -92,7 +92,7 @@ TEST(PrismProgramTest, FlattenModules_Wlan_Z3) {
     
     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
     
-    ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory));
+    ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory));
     EXPECT_EQ(1ull, program.getNumberOfModules());
     EXPECT_EQ(179ull, program.getModule(0).getNumberOfCommands());
 }
@@ -103,7 +103,7 @@ TEST(PrismProgramTest, FlattenModules_Csma_Z3) {
     
     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
     
-    ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory));
+    ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory));
     EXPECT_EQ(1ull, program.getNumberOfModules());
     EXPECT_EQ(70ull, program.getModule(0).getNumberOfCommands());
 }
@@ -114,7 +114,7 @@ TEST(PrismProgramTest, FlattenModules_Firewire_Z3) {
     
     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
     
-    ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory));
+    ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory));
     EXPECT_EQ(1ull, program.getNumberOfModules());
     EXPECT_EQ(5024ull, program.getModule(0).getNumberOfCommands());
 }
@@ -125,7 +125,7 @@ TEST(PrismProgramTest, FlattenModules_Coin_Z3) {
     
     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
     
-    ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory));
+    ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory));
     EXPECT_EQ(1ull, program.getNumberOfModules());
     EXPECT_EQ(13ull, program.getModule(0).getNumberOfCommands());
 }
@@ -136,7 +136,7 @@ TEST(PrismProgramTest, FlattenModules_Dice_Z3) {
     
     std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
     
-    ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory));
+    ASSERT_NO_THROW(program = program.substituteFormulas().flattenModules(smtSolverFactory));
     EXPECT_EQ(1ull, program.getNumberOfModules());
     EXPECT_EQ(16ull, program.getModule(0).getNumberOfCommands());
 }