diff --git a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
index ac2c7dcb7..53e992fd3 100644
--- a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
@@ -12,6 +12,7 @@
 #include "src/builder/DdPrismModelBuilder.h"
 #include "src/models/symbolic/Dtmc.h"
 #include "src/models/symbolic/StandardRewardModel.h"
+#include "src/storage/SymbolicModelDescription.h"
 #include "src/settings/SettingsManager.h"
 #include "src/settings/modules/GeneralSettings.h"
 #include "src/settings/modules/GmmxxEquationSolverSettings.h"
@@ -19,8 +20,9 @@
 #include "src/settings/modules/NativeEquationSolverSettings.h"
 
 TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
-
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
+    
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
     
@@ -80,8 +82,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Cudd) {
 }
 
 TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
-    
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
+
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
     
@@ -141,8 +144,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die_Sylvan) {
 }
 
 TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
-    
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
+
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
     
@@ -185,8 +189,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Cudd) {
 }
 
 TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
-    
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
+
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
     
@@ -229,8 +234,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
 }
 
 TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
-    
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
+
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
     
@@ -281,8 +287,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) {
 }
 
 TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
-    
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
+
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
     
diff --git a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
index 1733fa40f..eb00b67cd 100644
--- a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
@@ -10,6 +10,7 @@
 #include "src/parser/PrismParser.h"
 #include "src/parser/FormulaParser.h"
 #include "src/builder/DdPrismModelBuilder.h"
+#include "src/storage/SymbolicModelDescription.h"
 #include "src/models/symbolic/Dtmc.h"
 #include "src/models/symbolic/Mdp.h"
 #include "src/models/symbolic/StandardRewardModel.h"
@@ -21,8 +22,9 @@
 #include "src/settings/modules/GmmxxEquationSolverSettings.h"
 
 TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
-    
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
+
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
     
@@ -118,8 +120,9 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Cudd) {
 }
 
 TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
-    
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
+
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
     
@@ -215,8 +218,9 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice_Sylvan) {
 }
 
 TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
-    
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
+
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
     
@@ -294,8 +298,9 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
 }
 
 TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
-    
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
+
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
     
diff --git a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
index 5f744cc68..5d8391f5c 100644
--- a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
@@ -6,6 +6,7 @@
 #include "src/logic/Formulas.h"
 #include "src/builder/DdPrismModelBuilder.h"
 #include "src/storage/dd/DdType.h"
+#include "src/storage/SymbolicModelDescription.h"
 
 #include "src/solver/NativeLinearEquationSolver.h"
 #include "src/models/symbolic/StandardRewardModel.h"
@@ -25,7 +26,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Cudd) {
     std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
     
     // Parse the model description.
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
     
@@ -122,7 +124,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster_Sylvan) {
     std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
     
     // Parse the model description.
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
     
@@ -219,7 +222,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Cudd) {
     std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
     
     // Parse the model description.
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
     
@@ -298,7 +302,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded_Sylvan) {
     std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
     
     // Parse the model description.
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
     
@@ -377,7 +382,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Cudd) {
     std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
     
     // Parse the model description.
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
     
@@ -413,7 +419,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling_Sylvan) {
     std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
     
     // Parse the model description.
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
     
@@ -456,7 +463,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Cudd) {
     std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
     
     // Parse the model description.
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
     
@@ -546,7 +554,8 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem_Sylvan) {
     std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
     
     // Parse the model description.
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
     std::shared_ptr<storm::logic::Formula const> formula(nullptr);
     
diff --git a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
index cd6d87afb..ac419c04b 100644
--- a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
@@ -4,6 +4,7 @@
 #include "src/parser/FormulaParser.h"
 #include "src/logic/Formulas.h"
 #include "src/solver/NativeLinearEquationSolver.h"
+#include "src/storage/SymbolicModelDescription.h"
 #include "src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h"
 #include "src/modelchecker/results/HybridQuantitativeCheckResult.h"
 #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
@@ -14,13 +15,12 @@
 #include "src/models/symbolic/Dtmc.h"
 #include "src/settings/SettingsManager.h"
 #include "src/settings/modules/GeneralSettings.h"
-
 #include "src/settings/modules/GmmxxEquationSolverSettings.h"
-
 #include "src/settings/modules/NativeEquationSolverSettings.h"
 
 TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_CUDD) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
@@ -81,7 +81,8 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_CUDD) {
 }
 
 TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
@@ -142,7 +143,8 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die_Sylvan) {
 }
 
 TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_CUDD) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
@@ -186,7 +188,8 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_CUDD) {
 }
 
 TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
@@ -230,7 +233,8 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
 }
 
 TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_CUDD) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
@@ -282,7 +286,8 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_CUDD) {
 }
 
 TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
diff --git a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
index 1762c098f..1fe89c609 100644
--- a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
@@ -7,6 +7,7 @@
 #include "src/modelchecker/results/HybridQuantitativeCheckResult.h"
 #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
 #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
+#include "src/storage/SymbolicModelDescription.h"
 #include "src/parser/FormulaParser.h"
 #include "src/parser/PrismParser.h"
 #include "src/builder/DdPrismModelBuilder.h"
@@ -19,7 +20,8 @@
 #include "src/settings/modules/NativeEquationSolverSettings.h"
 
 TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
@@ -115,7 +117,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) {
 }
 
 TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
@@ -211,7 +214,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) {
 }
 
 TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
@@ -290,7 +294,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
 }
 
 TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
diff --git a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
index 3d1f3621f..c5ff7e1d1 100644
--- a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
@@ -4,6 +4,7 @@
 #include "src/parser/FormulaParser.h"
 #include "src/logic/Formulas.h"
 #include "src/utility/solver.h"
+#include "src/storage/SymbolicModelDescription.h"
 #include "src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
 #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
 #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
@@ -18,7 +19,8 @@
 #include "src/settings/modules/GeneralSettings.h"
 
 TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
@@ -79,7 +81,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Cudd) {
 }
 
 TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
@@ -141,7 +144,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) {
 }
 
 TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
@@ -185,7 +189,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) {
 }
 
 TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
@@ -232,7 +237,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
 }
 
 TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
@@ -284,7 +290,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) {
 }
 
 TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
diff --git a/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
index efe1b3283..ea024ccb7 100644
--- a/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
@@ -3,6 +3,7 @@
 
 #include "src/logic/Formulas.h"
 #include "src/utility/solver.h"
+#include "src/storage/SymbolicModelDescription.h"
 #include "src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
 #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
 #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
@@ -18,7 +19,8 @@
 #include "src/settings/modules/GeneralSettings.h"
 
 TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
@@ -115,7 +117,8 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Cudd) {
 }
 
 TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
@@ -212,7 +215,8 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Sylvan) {
 }
 
 TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
@@ -291,7 +295,8 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
 }
 
 TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp
index 2813e1a9b..e8c2e26fc 100644
--- a/test/functional/utility/GraphTest.cpp
+++ b/test/functional/utility/GraphTest.cpp
@@ -1,6 +1,7 @@
 #include "gtest/gtest.h"
 #include "storm-config.h"
 
+#include "src/storage/SymbolicModelDescription.h"
 #include "src/parser/PrismParser.h"
 #include "src/models/symbolic/Dtmc.h"
 #include "src/models/symbolic/Mdp.h"
@@ -16,7 +17,8 @@
 #include "src/storage/dd/DdManager.h"
 
 TEST(GraphTest, SymbolicProb01_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
     
     ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
@@ -37,7 +39,8 @@ TEST(GraphTest, SymbolicProb01_Cudd) {
 }
 
 TEST(GraphTest, SymbolicProb01_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
     
     ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
@@ -58,7 +61,8 @@ TEST(GraphTest, SymbolicProb01_Sylvan) {
 }
 
 TEST(GraphTest, SymbolicProb01MinMax_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
     
     ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@@ -75,7 +79,8 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) {
         EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount());
     }
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
+    program = modelDescription.preprocess().asPrismProgram();
     model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
     
     ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@@ -100,7 +105,8 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) {
         EXPECT_EQ(35ul, statesWithProbability01.second.getNonZeroCount());
     }
         
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
+    program = modelDescription.preprocess().asPrismProgram();
     model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
     
     ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@@ -119,7 +125,8 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) {
 }
 
 TEST(GraphTest, SymbolicProb01MinMax_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
     
     ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@@ -136,7 +143,8 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) {
         EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount());
     }
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
+    program = modelDescription.preprocess().asPrismProgram();
     model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
     
     ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@@ -161,7 +169,8 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) {
         EXPECT_EQ(35ul, statesWithProbability01.second.getNonZeroCount());
     }
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
+    program = modelDescription.preprocess().asPrismProgram();
     model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
     
     ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@@ -180,7 +189,8 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) {
 }
 
 TEST(GraphTest, ExplicitProb01) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
     
     ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
@@ -201,7 +211,8 @@ TEST(GraphTest, ExplicitProb01) {
 }
 
 TEST(GraphTest, ExplicitProb01MinMax) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
     std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
     
     ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@@ -216,7 +227,8 @@ TEST(GraphTest, ExplicitProb01MinMax) {
     EXPECT_EQ(0ul, statesWithProbability01.first.getNumberOfSetBits());
     EXPECT_EQ(364ul, statesWithProbability01.second.getNumberOfSetBits());
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
+    program = modelDescription.preprocess().asPrismProgram();
     model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
     
     ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@@ -237,7 +249,8 @@ TEST(GraphTest, ExplicitProb01MinMax) {
     EXPECT_EQ(83ul, statesWithProbability01.first.getNumberOfSetBits());
     EXPECT_EQ(35ul, statesWithProbability01.second.getNumberOfSetBits());
     
-    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
+    modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
+    program = modelDescription.preprocess().asPrismProgram();
     model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
     
     ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
@@ -249,4 +262,4 @@ TEST(GraphTest, ExplicitProb01MinMax) {
     ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::sparse::Mdp<double>>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("collision_max_backoff")));
     EXPECT_EQ(993ul, statesWithProbability01.first.getNumberOfSetBits());
     EXPECT_EQ(16ul, statesWithProbability01.second.getNumberOfSetBits());
-}
\ No newline at end of file
+}