diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt
index d6dbe8207..d870d2b21 100644
--- a/src/test/CMakeLists.txt
+++ b/src/test/CMakeLists.txt
@@ -1,23 +1,2 @@
-# Base path for test files
-set(STORM_TESTS_BASE_PATH "${PROJECT_SOURCE_DIR}/src/test")
-
-# Test Sources
-file(GLOB_RECURSE ALL_FILES ${STORM_TESTS_BASE_PATH}/*.h ${STORM_TESTS_BASE_PATH}/*.cpp)
-
-register_source_groups_from_filestructure("${ALL_FILES}" test)
-
-# Note that the tests also need the source files, except for the main file
-include_directories(${GTEST_INCLUDE_DIR})
-
-foreach (testsuite abstraction adapter builder logic modelchecker parser permissiveschedulers solver storage transformer utility)
-
-	  file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp)
-      add_executable (test-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp)
-	  target_link_libraries(test-${testsuite} storm)
-	  target_link_libraries(test-${testsuite} ${STORM_TEST_LINK_LIBRARIES})
-
-	  add_dependencies(test-${testsuite} test-resources)
-	  add_test(NAME run-test-${testsuite} COMMAND $<TARGET_FILE:test-${testsuite}>)
-      add_dependencies(tests test-${testsuite})
-	
-endforeach ()
+add_subdirectory(storm)
+add_subdirectory(storm-pars)
\ No newline at end of file
diff --git a/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp b/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp
deleted file mode 100644
index e4fa1d161..000000000
--- a/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp
+++ /dev/null
@@ -1,385 +0,0 @@
-#include "gtest/gtest.h"
-#include "storm-config.h"
-
-#ifdef STORM_HAVE_CARL
-
-#include "storm/adapters/RationalFunctionAdapter.h"
-
-#include "storm/modelchecker/parametric/SparseDtmcRegionChecker.h"
-#include "storm/storage/ParameterRegion.h"
-
-#include "storm/api/storm.h"
-
-TEST(SparseDtmcParameterLiftingTest, Brp_Prob) {
-    
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
-    std::string formulaAsString = "P<=0.84 [F s=5 ]";
-    std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
-
-    // Program and formula
-    storm::prism::Program program = storm::api::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
-    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
-    
-    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
-    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
-    modelParameters.insert(rewParameters.begin(), rewParameters.end());
-    
-    storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
-    regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
-
-    //start testing
-    auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
-    auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
-    auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
-
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-
-    carl::VariablePool::getInstance().clear();
-}
-
-TEST(SparseDtmcParameterLiftingTest, Brp_Rew) {
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
-    std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
-    std::string constantsAsString = "pL=0.9,TOAck=0.5";
-    carl::VariablePool::getInstance().clear();
-    
-    storm::prism::Program program = storm::api::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
-    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
-    
-    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
-    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
-    modelParameters.insert(rewParameters.begin(), rewParameters.end());
-    
-    storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
-    regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
-    
-    //start testing
-    auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
-    auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
-    auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
-
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    
-    carl::VariablePool::getInstance().clear();
-}
-
-TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded) {
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
-    std::string formulaAsString = "R>2.5 [ C<=300]";
-    std::string constantsAsString = "pL=0.9,TOAck=0.5";
-    carl::VariablePool::getInstance().clear();
-    
-    storm::prism::Program program = storm::api::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
-    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
-    
-    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
-    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
-    modelParameters.insert(rewParameters.begin(), rewParameters.end());
-    
-    storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
-    regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
-    
-    //start testing
-    auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
-    auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
-    auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
-
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    
-    carl::VariablePool::getInstance().clear();
-}
-
-TEST(SparseDtmcParameterLiftingTest, Brp_Prob_exactValidation) {
-    
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
-    std::string formulaAsString = "P<=0.84 [F s=5 ]";
-    std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
-
-    // Program and formula
-    storm::prism::Program program = storm::api::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
-    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
-    
-    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
-    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
-    modelParameters.insert(rewParameters.begin(), rewParameters.end());
-    
-    storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
-    auto settings = regionChecker.getSettings();
-    settings.applyExactValidation = true;
-    regionChecker.setSettings(settings);
-    regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
-
-    //start testing
-    auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
-    auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
-    auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
-
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-
-    carl::VariablePool::getInstance().clear();
-}
-
-TEST(SparseDtmcParameterLiftingTest, Brp_Rew_exactValidation) {
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
-    std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
-    std::string constantsAsString = "pL=0.9,TOAck=0.5";
-    carl::VariablePool::getInstance().clear();
-    
-    storm::prism::Program program = storm::api::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
-    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
-    
-    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
-    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
-    modelParameters.insert(rewParameters.begin(), rewParameters.end());
-    
-    storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
-    auto settings = regionChecker.getSettings();
-    settings.applyExactValidation = true;
-    regionChecker.setSettings(settings);
-    regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
-    
-    //start testing
-    auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
-    auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
-    auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
-
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    
-    carl::VariablePool::getInstance().clear();
-}
-
-TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded_exactValidation) {
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
-    std::string formulaAsString = "R>2.5 [ C<=300]";
-    std::string constantsAsString = "pL=0.9,TOAck=0.5";
-    carl::VariablePool::getInstance().clear();
-    
-    storm::prism::Program program = storm::api::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
-    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
-    
-    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
-    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
-    modelParameters.insert(rewParameters.begin(), rewParameters.end());
-    
-    storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
-    auto settings = regionChecker.getSettings();
-    settings.applyExactValidation = true;
-    regionChecker.setSettings(settings);
-    regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
-    
-    //start testing
-    auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
-    auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
-    auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
-
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    
-    carl::VariablePool::getInstance().clear();
-}
-
-TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Infty) {
-    
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
-    std::string formulaAsString = "R>2.5 [F (s=0&srep=3) ]";
-    std::string constantsAsString = "";
-    carl::VariablePool::getInstance().clear();
-    storm::prism::Program program = storm::api::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
-    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
-    
-    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
-    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
-    modelParameters.insert(rewParameters.begin(), rewParameters.end());
-    
-    storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
-    regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
-
-    //start testing
-    auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters);
-    
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-
-    carl::VariablePool::getInstance().clear();
-}
-
-TEST(SparseDtmcParameterLiftingTest, Brp_Rew_4Par) {
-    
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
-    std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
-    std::string constantsAsString = ""; //!! this model will have 4 parameters
-    carl::VariablePool::getInstance().clear();
-    storm::prism::Program program = storm::api::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
-    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
-    
-    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
-    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
-    modelParameters.insert(rewParameters.begin(), rewParameters.end());
-    
-    storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
-    regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
-    
-    //start testing
-    auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters);
-    auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9", modelParameters);
-    auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2", modelParameters);
-
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    
-    carl::VariablePool::getInstance().clear();
-}
-
-TEST(SparseDtmcParameterLiftingTest, Crowds_Prob) {
-    
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
-    std::string formulaAsString = "P<0.5 [F \"observe0Greater1\" ]";
-    std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
-    carl::VariablePool::getInstance().clear();
-
-    storm::prism::Program program = storm::api::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
-    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
-    
-    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
-    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
-    modelParameters.insert(rewParameters.begin(), rewParameters.end());
-   
-    storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
-    regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
-
-    //start testing
-    auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2", modelParameters);
-    auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3", modelParameters);
-    auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters);
-    auto allVioHardRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9", modelParameters);
-
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::CenterViolated, regionChecker.analyzeRegion(allVioHardRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-
-    carl::VariablePool::getInstance().clear();
-}
-
-TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_stepBounded) {
-    
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
-    std::string formulaAsString = "P<0.5 [F<=300 \"observe0Greater1\" ]";
-    std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
-    carl::VariablePool::getInstance().clear();
-
-    storm::prism::Program program = storm::api::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
-    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
-    
-    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
-    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
-    modelParameters.insert(rewParameters.begin(), rewParameters.end());
-   
-    storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
-    regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
-
-    //start testing
-    auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2", modelParameters);
-    auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3", modelParameters);
-    auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters);
-    auto allVioHardRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9", modelParameters);
-
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::CenterViolated, regionChecker.analyzeRegion(allVioHardRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-
-    carl::VariablePool::getInstance().clear();
-}
-
-TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_1Par) {
-    
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
-    std::string formulaAsString = "P>0.75 [F \"observe0Greater1\" ]";
-    std::string constantsAsString = "badC=0.3"; //e.g. pL=0.9,TOACK=0.5
-    carl::VariablePool::getInstance().clear();
-
-    
-    storm::prism::Program program = storm::api::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
-    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
-    
-    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
-    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
-    modelParameters.insert(rewParameters.begin(), rewParameters.end());
-    
-    storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
-    regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
-    
-    //start testing
-    auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.9<=PF<=0.99", modelParameters);
-    auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.9", modelParameters);
-    auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.01<=PF<=0.8", modelParameters);
-
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    
-    carl::VariablePool::getInstance().clear();
-}
-
-TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_Const) {
-    
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
-    std::string formulaAsString = "P>0.6 [F \"observe0Greater1\" ]";
-    std::string constantsAsString = "PF=0.9,badC=0.2";
-    carl::VariablePool::getInstance().clear();
-    
-    storm::prism::Program program = storm::api::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
-    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
-    
-    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
-    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
-    modelParameters.insert(rewParameters.begin(), rewParameters.end());
-    
-    storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
-    regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
-
-    //start testing
-    auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("", modelParameters);
-    
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-
-    carl::VariablePool::getInstance().clear();
-}
-
-#endif
diff --git a/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp b/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp
deleted file mode 100644
index b51b33df0..000000000
--- a/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp
+++ /dev/null
@@ -1,313 +0,0 @@
-#include "gtest/gtest.h"
-#include "storm-config.h"
-
-#ifdef STORM_HAVE_CARL
-
-#include "storm/adapters/RationalFunctionAdapter.h"
-
-#include "storm/modelchecker/parametric/SparseMdpRegionChecker.h"
-#include "storm/storage/ParameterRegion.h"
-
-#include "storm/api/storm.h"
-
-TEST(SparseMdpParameterLiftingTest, two_dice_Prob) {
-    
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm";
-    std::string formulaFile = "P<=0.17 [ F \"doubles\" ]";
-    
-    carl::VariablePool::getInstance().clear();
-
-    storm::prism::Program program = storm::api::parseProgram(programFile);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program));
-    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
-    
-    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
-    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
-    modelParameters.insert(rewParameters.begin(), rewParameters.end());
-    
-    storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
-    regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
-    
-    auto allSatRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
-    auto exBothRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters);
-    auto allVioRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
-
-    
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    
-    carl::VariablePool::getInstance().clear();
-}
-
-TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded) {
-    
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm";
-    std::string formulaFile = "P<=0.17 [ F<100 \"doubles\" ]";
-    
-    carl::VariablePool::getInstance().clear();
-
-    storm::prism::Program program = storm::api::parseProgram(programFile);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program));
-    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
-    
-    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
-    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
-    modelParameters.insert(rewParameters.begin(), rewParameters.end());
-    
-    storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
-    regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
-    
-    auto allSatRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
-    auto exBothRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters);
-    auto allVioRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
-
-    
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    
-    carl::VariablePool::getInstance().clear();
-}
-
-TEST(SparseMdpParameterLiftingTest, two_dice_Prob_exactValidation) {
-    
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm";
-    std::string formulaFile = "P<=0.17 [ F \"doubles\" ]";
-    
-    carl::VariablePool::getInstance().clear();
-
-    storm::prism::Program program = storm::api::parseProgram(programFile);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program));
-    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
-    
-    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
-    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
-    modelParameters.insert(rewParameters.begin(), rewParameters.end());
-    
-    storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
-    regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
-    
-    auto allSatRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
-    auto exBothRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters);
-    auto allVioRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
-
-    
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    
-    carl::VariablePool::getInstance().clear();
-}
-
-TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded_exactValidation) {
-    
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm";
-    std::string formulaFile = "P<=0.17 [ F<100 \"doubles\" ]";
-    
-    carl::VariablePool::getInstance().clear();
-
-    storm::prism::Program program = storm::api::parseProgram(programFile);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program));
-    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
-    
-    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
-    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
-    modelParameters.insert(rewParameters.begin(), rewParameters.end());
-    
-    storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
-    regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
-    
-    auto allSatRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
-    auto exBothRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters);
-    auto allVioRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
-
-    
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    
-    carl::VariablePool::getInstance().clear();
-}
-
-TEST(SparseMdpParameterLiftingTest, coin_Prob) {
-    
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/coin2_2.nm";
-    std::string formulaAsString = "P>0.25 [F \"finished\"&\"all_coins_equal_1\" ]";
-    
-    storm::prism::Program program = storm::api::parseProgram(programFile);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
-    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
-    
-    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
-    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
-    modelParameters.insert(rewParameters.begin(), rewParameters.end());
-    
-    storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
-    regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
-    
-    //start testing
-    auto allSatRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.3<=p1<=0.45,0.2<=p2<=0.54", modelParameters);
-    auto exBothRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=p1<=0.65,0.5<=p2<=0.7", modelParameters);
-    auto allVioRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=p1<=0.7,0.55<=p2<=0.6", modelParameters);
-        
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-
-    carl::VariablePool::getInstance().clear();
-}
-
-TEST(SparseMdpParameterLiftingTest, brp_Prop) {
-    
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
-    std::string formulaAsString = "P<=0.84 [ F (s=5 & T) ]";
-    std::string constantsAsString = "TOMsg=0.0,TOAck=0.0";
-
-    storm::prism::Program program = storm::api::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
-    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
-    
-    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
-    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
-    modelParameters.insert(rewParameters.begin(), rewParameters.end());
-    
-    storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
-    regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
-    
-    //start testing
-    auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
-    auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
-    auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
-        
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-
-    carl::VariablePool::getInstance().clear();
-}
-
-TEST(SparseMdpParameterLiftingTest, brp_Rew) {
-    
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
-    std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
-    std::string constantsAsString = "pL=0.9,TOAck=0.5";
-
-
-    storm::prism::Program program = storm::api::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
-    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
-    
-    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
-    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
-    modelParameters.insert(rewParameters.begin(), rewParameters.end());
-    
-    storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
-    regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
-    
-   //start testing
-    auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
-    auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
-    auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
-
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-
-    carl::VariablePool::getInstance().clear();
-}
-
-TEST(SparseMdpParameterLiftingTest, brp_Rew_bounded) {
-    
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
-    std::string formulaAsString = "R>2.5 [ C<=300 ]";
-    std::string constantsAsString = "pL=0.9,TOAck=0.5";
-
-    storm::prism::Program program = storm::api::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
-    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
-    
-    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
-    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
-    modelParameters.insert(rewParameters.begin(), rewParameters.end());
-    
-    storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
-    regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
-    
-   //start testing
-    auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
-    auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
-    auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
-
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-
-    carl::VariablePool::getInstance().clear();
-}
-
-
-TEST(SparseMdpParameterLiftingTest, Brp_Rew_Infty) {
-    
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
-    std::string formulaAsString = "R>2.5 [F (s=0&srep=3) ]";
-    std::string constantsAsString = "";
-    carl::VariablePool::getInstance().clear();
-    storm::prism::Program program = storm::api::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
-    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
-    
-    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
-    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
-    modelParameters.insert(rewParameters.begin(), rewParameters.end());
-    
-    storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
-    regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
-
-    //start testing
-    auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters);
-    
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-
-    carl::VariablePool::getInstance().clear();
-}
-
-TEST(SparseMdpParameterLiftingTest, Brp_Rew_4Par) {
-    
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
-    std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
-    std::string constantsAsString = ""; //!! this model will have 4 parameters
-    carl::VariablePool::getInstance().clear();
-    storm::prism::Program program = storm::api::parseProgram(programFile);
-    program = storm::utility::prism::preprocess(program, constantsAsString);
-    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
-    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
-    
-    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
-    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
-    modelParameters.insert(rewParameters.begin(), rewParameters.end());
-    
-    storm::modelchecker::parametric::SparseMdpRegionChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double, storm::RationalNumber> regionChecker(*model);
-    regionChecker.specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formulas[0], true));
-    
-    //start testing
-    auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters);
-    auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9", modelParameters);
-    auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2", modelParameters);
-
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, regionChecker.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, regionChecker.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, regionChecker.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
-    
-    carl::VariablePool::getInstance().clear();
-}
-
-
-
-
-
-#endif
diff --git a/src/test/storm-pars/CMakeLists.txt b/src/test/storm-pars/CMakeLists.txt
new file mode 100644
index 000000000..2c2345121
--- /dev/null
+++ b/src/test/storm-pars/CMakeLists.txt
@@ -0,0 +1,23 @@
+# Base path for test files
+set(STORM_TESTS_BASE_PATH "${PROJECT_SOURCE_DIR}/src/test/storm-pars")
+
+# Test Sources
+file(GLOB_RECURSE ALL_FILES ${STORM_TESTS_BASE_PATH}/*.h ${STORM_TESTS_BASE_PATH}/*.cpp)
+
+register_source_groups_from_filestructure("${ALL_FILES}" test)
+
+# Note that the tests also need the source files, except for the main file
+include_directories(${GTEST_INCLUDE_DIR})
+
+foreach (testsuite modelchecker)
+
+	  file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp)
+      add_executable (test-pars-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp)
+	  target_link_libraries(test-pars-${testsuite} storm-pars)
+	  target_link_libraries(test-pars-${testsuite} ${STORM_TEST_LINK_LIBRARIES})
+
+	  add_dependencies(test-pars-${testsuite} test-resources)
+	  add_test(NAME run-test-pars-${testsuite} COMMAND $<TARGET_FILE:test-pars-${testsuite}>)
+      add_dependencies(tests test-pars-${testsuite})
+	
+endforeach ()
diff --git a/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp b/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp
new file mode 100644
index 000000000..31def397a
--- /dev/null
+++ b/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp
@@ -0,0 +1,362 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#ifdef STORM_HAVE_CARL
+
+#include "storm/adapters/RationalFunctionAdapter.h"
+
+#include "storm-pars/api/storm-pars.h"
+#include "storm/api/storm.h"
+
+TEST(SparseDtmcParameterLiftingTest, Brp_Prob) {
+    
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
+    std::string formulaAsString = "P<=0.84 [F s=5 ]";
+    std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
+
+    // Program and formula
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, constantsAsString);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
+    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+    
+    auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
+    
+    //start testing
+    auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
+    auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
+    auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
+
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+
+    carl::VariablePool::getInstance().clear();
+}
+
+TEST(SparseDtmcParameterLiftingTest, Brp_Rew) {
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
+    std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
+    std::string constantsAsString = "pL=0.9,TOAck=0.5";
+    carl::VariablePool::getInstance().clear();
+    
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, constantsAsString);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
+    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+    
+    auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
+    
+    //start testing
+    auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
+    auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
+    auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
+
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    
+    carl::VariablePool::getInstance().clear();
+}
+
+TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded) {
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
+    std::string formulaAsString = "R>2.5 [ C<=300]";
+    std::string constantsAsString = "pL=0.9,TOAck=0.5";
+    carl::VariablePool::getInstance().clear();
+    
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, constantsAsString);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
+    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+    
+    auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
+    
+    //start testing
+    auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
+    auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
+    auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
+
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    
+    carl::VariablePool::getInstance().clear();
+}
+
+TEST(SparseDtmcParameterLiftingTest, Brp_Prob_exactValidation) {
+    
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm";
+    std::string formulaAsString = "P<=0.84 [F s=5 ]";
+    std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
+
+    // Program and formula
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, constantsAsString);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
+    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+    
+    auto regionChecker = storm::api::initializeValidatingRegionModelChecker<storm::RationalFunction, double, storm::RationalNumber>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
+
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+    
+    //start testing
+    auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
+    auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
+    auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
+
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+
+    carl::VariablePool::getInstance().clear();
+}
+
+TEST(SparseDtmcParameterLiftingTest, Brp_Rew_exactValidation) {
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
+    std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
+    std::string constantsAsString = "pL=0.9,TOAck=0.5";
+    carl::VariablePool::getInstance().clear();
+    
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, constantsAsString);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
+    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+    
+    auto regionChecker = storm::api::initializeValidatingRegionModelChecker<storm::RationalFunction, double, storm::RationalNumber>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
+
+    //start testing
+    auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
+    auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
+    auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
+
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    
+    carl::VariablePool::getInstance().clear();
+}
+
+TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded_exactValidation) {
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
+    std::string formulaAsString = "R>2.5 [ C<=300]";
+    std::string constantsAsString = "pL=0.9,TOAck=0.5";
+    carl::VariablePool::getInstance().clear();
+    
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, constantsAsString);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
+    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+    
+    auto regionChecker = storm::api::initializeValidatingRegionModelChecker<storm::RationalFunction, double, storm::RationalNumber>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
+    
+    //start testing
+    auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
+    auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
+    auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
+
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    
+    carl::VariablePool::getInstance().clear();
+}
+
+TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Infty) {
+    
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
+    std::string formulaAsString = "R>2.5 [F (s=0&srep=3) ]";
+    std::string constantsAsString = "";
+    carl::VariablePool::getInstance().clear();
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, constantsAsString);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
+    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+    
+    auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
+
+    //start testing
+    auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters);
+    
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+
+    carl::VariablePool::getInstance().clear();
+}
+
+TEST(SparseDtmcParameterLiftingTest, Brp_Rew_4Par) {
+    
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
+    std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
+    std::string constantsAsString = ""; //!! this model will have 4 parameters
+    carl::VariablePool::getInstance().clear();
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, constantsAsString);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
+    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+    
+    auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
+    
+    //start testing
+    auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters);
+    auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9", modelParameters);
+    auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2", modelParameters);
+
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    
+    carl::VariablePool::getInstance().clear();
+}
+
+TEST(SparseDtmcParameterLiftingTest, Crowds_Prob) {
+    
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
+    std::string formulaAsString = "P<0.5 [F \"observe0Greater1\" ]";
+    std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
+    carl::VariablePool::getInstance().clear();
+
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, constantsAsString);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
+    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+   
+    auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
+
+    //start testing
+    auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=PF<=0.75,0.15<=badC<=0.2", modelParameters);
+    auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.75<=PF<=0.8,0.2<=badC<=0.3", modelParameters);
+    auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters);
+    auto allVioHardRegion=storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.95,0.2<=badC<=0.9", modelParameters);
+
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::CenterViolated, regionChecker->analyzeRegion(allVioHardRegion, storm::modelchecker::RegionResult::Unknown, true));
+
+    carl::VariablePool::getInstance().clear();
+}
+
+TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_stepBounded) {
+    
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
+    std::string formulaAsString = "P<0.5 [F<=300 \"observe0Greater1\" ]";
+    std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
+    carl::VariablePool::getInstance().clear();
+
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, constantsAsString);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
+    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+   
+    auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
+
+    //start testing
+    auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=PF<=0.75,0.15<=badC<=0.2", modelParameters);
+    auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.75<=PF<=0.8,0.2<=badC<=0.3", modelParameters);
+    auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.95,0.2<=badC<=0.2", modelParameters);
+    auto allVioHardRegion=storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.95,0.2<=badC<=0.9", modelParameters);
+
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::CenterViolated, regionChecker->analyzeRegion(allVioHardRegion, storm::modelchecker::RegionResult::Unknown, true));
+
+    carl::VariablePool::getInstance().clear();
+}
+
+TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_1Par) {
+    
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
+    std::string formulaAsString = "P>0.75 [F \"observe0Greater1\" ]";
+    std::string constantsAsString = "badC=0.3"; //e.g. pL=0.9,TOACK=0.5
+    carl::VariablePool::getInstance().clear();
+
+    
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, constantsAsString);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
+    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+    
+    auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
+    
+    //start testing
+    auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.9<=PF<=0.99", modelParameters);
+    auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.8<=PF<=0.9", modelParameters);
+    auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.01<=PF<=0.8", modelParameters);
+
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    
+    carl::VariablePool::getInstance().clear();
+}
+
+TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_Const) {
+    
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/crowds3_5.pm";
+    std::string formulaAsString = "P>0.6 [F \"observe0Greater1\" ]";
+    std::string constantsAsString = "PF=0.9,badC=0.2";
+    carl::VariablePool::getInstance().clear();
+    
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, constantsAsString);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
+    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+    
+    auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
+
+    //start testing
+    auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("", modelParameters);
+    
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+
+    carl::VariablePool::getInstance().clear();
+}
+
+#endif
diff --git a/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp b/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp
new file mode 100644
index 000000000..fd690b876
--- /dev/null
+++ b/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp
@@ -0,0 +1,301 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#ifdef STORM_HAVE_CARL
+
+#include "storm/adapters/RationalFunctionAdapter.h"
+
+#include "storm-pars/api/storm-pars.h"
+#include "storm/api/storm.h"
+
+TEST(SparseMdpParameterLiftingTest, two_dice_Prob) {
+    
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm";
+    std::string formulaFile = "P<=0.17 [ F \"doubles\" ]";
+    
+    carl::VariablePool::getInstance().clear();
+
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program));
+    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+    
+    auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
+    
+    auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
+    auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters);
+    auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
+
+    
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    
+    carl::VariablePool::getInstance().clear();
+}
+
+TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded) {
+    
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm";
+    std::string formulaFile = "P<=0.17 [ F<100 \"doubles\" ]";
+    
+    carl::VariablePool::getInstance().clear();
+
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program));
+    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+    
+    auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
+    
+    auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
+    auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters);
+    auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
+
+    
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    
+    carl::VariablePool::getInstance().clear();
+}
+
+TEST(SparseMdpParameterLiftingTest, two_dice_Prob_exactValidation) {
+    
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm";
+    std::string formulaFile = "P<=0.17 [ F \"doubles\" ]";
+    
+    carl::VariablePool::getInstance().clear();
+
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program));
+    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+    
+    auto regionChecker = storm::api::initializeValidatingRegionModelChecker<storm::RationalFunction, double, storm::RationalNumber>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
+    
+    auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
+    auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters);
+    auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
+
+    
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    
+    carl::VariablePool::getInstance().clear();
+}
+
+TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded_exactValidation) {
+    
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm";
+    std::string formulaFile = "P<=0.17 [ F<100 \"doubles\" ]";
+    
+    carl::VariablePool::getInstance().clear();
+
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaFile, program));
+    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+    
+    auto regionChecker = storm::api::initializeValidatingRegionModelChecker<storm::RationalFunction, double, storm::RationalNumber>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
+    
+    auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.495<=p1<=0.5,0.5<=p2<=0.505", modelParameters);
+    auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.45<=p1<=0.55,0.45<=p2<=0.55", modelParameters);
+    auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.6<=p1<=0.7,0.6<=p2<=0.6", modelParameters);
+
+    
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    
+    carl::VariablePool::getInstance().clear();
+}
+
+TEST(SparseMdpParameterLiftingTest, coin_Prob) {
+    
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/coin2_2.nm";
+    std::string formulaAsString = "P>0.25 [F \"finished\"&\"all_coins_equal_1\" ]";
+    
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
+    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+    
+    auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
+    
+    //start testing
+    auto allSatRegion = storm::api::parseRegion<storm::RationalFunction>("0.3<=p1<=0.45,0.2<=p2<=0.54", modelParameters);
+    auto exBothRegion = storm::api::parseRegion<storm::RationalFunction>("0.4<=p1<=0.65,0.5<=p2<=0.7", modelParameters);
+    auto allVioRegion = storm::api::parseRegion<storm::RationalFunction>("0.4<=p1<=0.7,0.55<=p2<=0.6", modelParameters);
+        
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+
+    carl::VariablePool::getInstance().clear();
+}
+
+TEST(SparseMdpParameterLiftingTest, brp_Prop) {
+    
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
+    std::string formulaAsString = "P<=0.84 [ F (s=5 & T) ]";
+    std::string constantsAsString = "TOMsg=0.0,TOAck=0.0";
+
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, constantsAsString);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
+    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+    
+    auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
+    
+    //start testing
+    auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pL<=0.9,0.75<=pK<=0.95", modelParameters);
+    auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.4<=pL<=0.65,0.75<=pK<=0.95", modelParameters);
+    auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pL<=0.73,0.2<=pK<=0.715", modelParameters);
+        
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+
+    carl::VariablePool::getInstance().clear();
+}
+
+TEST(SparseMdpParameterLiftingTest, brp_Rew) {
+    
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
+    std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
+    std::string constantsAsString = "pL=0.9,TOAck=0.5";
+
+
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, constantsAsString);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
+    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+    
+    auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
+    
+   //start testing
+    auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
+    auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
+    auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
+
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+
+    carl::VariablePool::getInstance().clear();
+}
+
+TEST(SparseMdpParameterLiftingTest, brp_Rew_bounded) {
+    
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
+    std::string formulaAsString = "R>2.5 [ C<=300 ]";
+    std::string constantsAsString = "pL=0.9,TOAck=0.5";
+
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, constantsAsString);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
+    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+    
+    auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
+    
+   //start testing
+    auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.875,0.75<=TOMsg<=0.95", modelParameters);
+    auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.6<=pK<=0.9,0.5<=TOMsg<=0.95", modelParameters);
+    auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.3,0.2<=TOMsg<=0.3", modelParameters);
+
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+
+    carl::VariablePool::getInstance().clear();
+}
+
+
+TEST(SparseMdpParameterLiftingTest, Brp_Rew_Infty) {
+    
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
+    std::string formulaAsString = "R>2.5 [F (s=0&srep=3) ]";
+    std::string constantsAsString = "";
+    carl::VariablePool::getInstance().clear();
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, constantsAsString);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
+    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+    
+    auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
+
+    //start testing
+    auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters);
+    
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+
+    carl::VariablePool::getInstance().clear();
+}
+
+TEST(SparseMdpParameterLiftingTest, Brp_Rew_4Par) {
+    
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/brp16_2.nm";
+    std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
+    std::string constantsAsString = ""; //!! this model will have 4 parameters
+    carl::VariablePool::getInstance().clear();
+    storm::prism::Program program = storm::api::parseProgram(programFile);
+    program = storm::utility::prism::preprocess(program, constantsAsString);
+    std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program));
+    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::api::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
+    
+    auto modelParameters = storm::models::sparse::getProbabilityParameters(*model);
+    auto rewParameters = storm::models::sparse::getRewardParameters(*model);
+    modelParameters.insert(rewParameters.begin(), rewParameters.end());
+    
+    auto regionChecker = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formulas[0], true));
+    
+    //start testing
+    auto allSatRegion=storm::api::parseRegion<storm::RationalFunction>("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9", modelParameters);
+    auto exBothRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9", modelParameters);
+    auto allVioRegion=storm::api::parseRegion<storm::RationalFunction>("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2", modelParameters);
+
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllSat, regionChecker->analyzeRegion(allSatRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::ExistsBoth, regionChecker->analyzeRegion(exBothRegion, storm::modelchecker::RegionResult::Unknown, true));
+    EXPECT_EQ(storm::modelchecker::RegionResult::AllViolated, regionChecker->analyzeRegion(allVioRegion, storm::modelchecker::RegionResult::Unknown, true));
+    
+    carl::VariablePool::getInstance().clear();
+}
+
+
+
+
+
+#endif
diff --git a/src/test/storm-pars/storm-test.cpp b/src/test/storm-pars/storm-test.cpp
new file mode 100644
index 000000000..203c56b40
--- /dev/null
+++ b/src/test/storm-pars/storm-test.cpp
@@ -0,0 +1,8 @@
+#include "gtest/gtest.h"
+#include "storm/settings/SettingsManager.h"
+
+int main(int argc, char **argv) {
+  storm::settings::initializeAll("Storm-pars (Functional) Testing Suite", "test-pars");
+  ::testing::InitGoogleTest(&argc, argv);
+  return RUN_ALL_TESTS();
+}
diff --git a/src/test/storm/CMakeLists.txt b/src/test/storm/CMakeLists.txt
new file mode 100644
index 000000000..0ae2fc509
--- /dev/null
+++ b/src/test/storm/CMakeLists.txt
@@ -0,0 +1,23 @@
+# Base path for test files
+set(STORM_TESTS_BASE_PATH "${PROJECT_SOURCE_DIR}/src/test/storm")
+
+# Test Sources
+file(GLOB_RECURSE ALL_FILES ${STORM_TESTS_BASE_PATH}/*.h ${STORM_TESTS_BASE_PATH}/*.cpp)
+
+register_source_groups_from_filestructure("${ALL_FILES}" test)
+
+# Note that the tests also need the source files, except for the main file
+include_directories(${GTEST_INCLUDE_DIR})
+
+foreach (testsuite abstraction adapter builder logic modelchecker parser permissiveschedulers solver storage transformer utility)
+
+	  file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp)
+      add_executable (test-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp)
+	  target_link_libraries(test-${testsuite} storm)
+	  target_link_libraries(test-${testsuite} ${STORM_TEST_LINK_LIBRARIES})
+
+	  add_dependencies(test-${testsuite} test-resources)
+	  add_test(NAME run-test-${testsuite} COMMAND $<TARGET_FILE:test-${testsuite}>)
+      add_dependencies(tests test-${testsuite})
+	
+endforeach ()
diff --git a/src/test/abstraction/PrismMenuGameTest.cpp b/src/test/storm/abstraction/PrismMenuGameTest.cpp
similarity index 100%
rename from src/test/abstraction/PrismMenuGameTest.cpp
rename to src/test/storm/abstraction/PrismMenuGameTest.cpp
diff --git a/src/test/adapter/MathsatExpressionAdapterTest.cpp b/src/test/storm/adapter/MathsatExpressionAdapterTest.cpp
similarity index 100%
rename from src/test/adapter/MathsatExpressionAdapterTest.cpp
rename to src/test/storm/adapter/MathsatExpressionAdapterTest.cpp
diff --git a/src/test/adapter/Z3ExpressionAdapterTest.cpp b/src/test/storm/adapter/Z3ExpressionAdapterTest.cpp
similarity index 100%
rename from src/test/adapter/Z3ExpressionAdapterTest.cpp
rename to src/test/storm/adapter/Z3ExpressionAdapterTest.cpp
diff --git a/src/test/builder/DdJaniModelBuilderTest.cpp b/src/test/storm/builder/DdJaniModelBuilderTest.cpp
similarity index 100%
rename from src/test/builder/DdJaniModelBuilderTest.cpp
rename to src/test/storm/builder/DdJaniModelBuilderTest.cpp
diff --git a/src/test/builder/DdPrismModelBuilderTest.cpp b/src/test/storm/builder/DdPrismModelBuilderTest.cpp
similarity index 100%
rename from src/test/builder/DdPrismModelBuilderTest.cpp
rename to src/test/storm/builder/DdPrismModelBuilderTest.cpp
diff --git a/src/test/builder/ExplicitJaniModelBuilderTest.cpp b/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp
similarity index 100%
rename from src/test/builder/ExplicitJaniModelBuilderTest.cpp
rename to src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp
diff --git a/src/test/builder/ExplicitJitJaniModelBuilderTest.cpp b/src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp
similarity index 100%
rename from src/test/builder/ExplicitJitJaniModelBuilderTest.cpp
rename to src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp
diff --git a/src/test/builder/ExplicitPrismModelBuilderTest.cpp b/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp
similarity index 100%
rename from src/test/builder/ExplicitPrismModelBuilderTest.cpp
rename to src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp
diff --git a/src/test/logic/FragmentCheckerTest.cpp b/src/test/storm/logic/FragmentCheckerTest.cpp
similarity index 100%
rename from src/test/logic/FragmentCheckerTest.cpp
rename to src/test/storm/logic/FragmentCheckerTest.cpp
diff --git a/src/test/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
similarity index 100%
rename from src/test/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
rename to src/test/storm/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
diff --git a/src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp b/src/test/storm/modelchecker/GameBasedDtmcModelCheckerTest.cpp
similarity index 100%
rename from src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp
rename to src/test/storm/modelchecker/GameBasedDtmcModelCheckerTest.cpp
diff --git a/src/test/modelchecker/GameBasedMdpModelCheckerTest.cpp b/src/test/storm/modelchecker/GameBasedMdpModelCheckerTest.cpp
similarity index 100%
rename from src/test/modelchecker/GameBasedMdpModelCheckerTest.cpp
rename to src/test/storm/modelchecker/GameBasedMdpModelCheckerTest.cpp
diff --git a/src/test/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
similarity index 100%
rename from src/test/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
rename to src/test/storm/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
diff --git a/src/test/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
similarity index 100%
rename from src/test/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
rename to src/test/storm/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
diff --git a/src/test/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
similarity index 100%
rename from src/test/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
rename to src/test/storm/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
diff --git a/src/test/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
similarity index 100%
rename from src/test/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
rename to src/test/storm/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
diff --git a/src/test/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
similarity index 100%
rename from src/test/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
rename to src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
diff --git a/src/test/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
similarity index 100%
rename from src/test/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
rename to src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
diff --git a/src/test/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/NativeCtmcCslModelCheckerTest.cpp
similarity index 100%
rename from src/test/modelchecker/NativeCtmcCslModelCheckerTest.cpp
rename to src/test/storm/modelchecker/NativeCtmcCslModelCheckerTest.cpp
diff --git a/src/test/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
similarity index 100%
rename from src/test/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
rename to src/test/storm/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
diff --git a/src/test/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
similarity index 100%
rename from src/test/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
rename to src/test/storm/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
diff --git a/src/test/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
similarity index 100%
rename from src/test/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
rename to src/test/storm/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
diff --git a/src/test/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
similarity index 100%
rename from src/test/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
rename to src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
diff --git a/src/test/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
similarity index 100%
rename from src/test/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
rename to src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
diff --git a/src/test/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp
similarity index 100%
rename from src/test/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp
rename to src/test/storm/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp
diff --git a/src/test/modelchecker/SparseExplorationModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseExplorationModelCheckerTest.cpp
similarity index 100%
rename from src/test/modelchecker/SparseExplorationModelCheckerTest.cpp
rename to src/test/storm/modelchecker/SparseExplorationModelCheckerTest.cpp
diff --git a/src/test/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp
similarity index 100%
rename from src/test/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp
rename to src/test/storm/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp
diff --git a/src/test/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp
similarity index 100%
rename from src/test/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp
rename to src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp
diff --git a/src/test/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp
similarity index 100%
rename from src/test/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp
rename to src/test/storm/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp
diff --git a/src/test/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp
similarity index 100%
rename from src/test/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp
rename to src/test/storm/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp
diff --git a/src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
similarity index 100%
rename from src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
rename to src/test/storm/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
diff --git a/src/test/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
similarity index 100%
rename from src/test/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
rename to src/test/storm/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
diff --git a/src/test/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
similarity index 100%
rename from src/test/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
rename to src/test/storm/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
diff --git a/src/test/parser/.gitignore b/src/test/storm/parser/.gitignore
similarity index 100%
rename from src/test/parser/.gitignore
rename to src/test/storm/parser/.gitignore
diff --git a/src/test/parser/AutoParserTest.cpp b/src/test/storm/parser/AutoParserTest.cpp
similarity index 100%
rename from src/test/parser/AutoParserTest.cpp
rename to src/test/storm/parser/AutoParserTest.cpp
diff --git a/src/test/parser/DeterministicModelParserTest.cpp b/src/test/storm/parser/DeterministicModelParserTest.cpp
similarity index 100%
rename from src/test/parser/DeterministicModelParserTest.cpp
rename to src/test/storm/parser/DeterministicModelParserTest.cpp
diff --git a/src/test/parser/DeterministicSparseTransitionParserTest.cpp b/src/test/storm/parser/DeterministicSparseTransitionParserTest.cpp
similarity index 100%
rename from src/test/parser/DeterministicSparseTransitionParserTest.cpp
rename to src/test/storm/parser/DeterministicSparseTransitionParserTest.cpp
diff --git a/src/test/parser/DirectEncodingParserTest.cpp b/src/test/storm/parser/DirectEncodingParserTest.cpp
similarity index 100%
rename from src/test/parser/DirectEncodingParserTest.cpp
rename to src/test/storm/parser/DirectEncodingParserTest.cpp
diff --git a/src/test/parser/FormulaParserTest.cpp b/src/test/storm/parser/FormulaParserTest.cpp
similarity index 100%
rename from src/test/parser/FormulaParserTest.cpp
rename to src/test/storm/parser/FormulaParserTest.cpp
diff --git a/src/test/parser/MappedFileTest.cpp b/src/test/storm/parser/MappedFileTest.cpp
similarity index 100%
rename from src/test/parser/MappedFileTest.cpp
rename to src/test/storm/parser/MappedFileTest.cpp
diff --git a/src/test/parser/MarkovAutomatonParserTest.cpp b/src/test/storm/parser/MarkovAutomatonParserTest.cpp
similarity index 100%
rename from src/test/parser/MarkovAutomatonParserTest.cpp
rename to src/test/storm/parser/MarkovAutomatonParserTest.cpp
diff --git a/src/test/parser/MarkovAutomatonSparseTransitionParserTest.cpp b/src/test/storm/parser/MarkovAutomatonSparseTransitionParserTest.cpp
similarity index 100%
rename from src/test/parser/MarkovAutomatonSparseTransitionParserTest.cpp
rename to src/test/storm/parser/MarkovAutomatonSparseTransitionParserTest.cpp
diff --git a/src/test/parser/NondeterministicModelParserTest.cpp b/src/test/storm/parser/NondeterministicModelParserTest.cpp
similarity index 100%
rename from src/test/parser/NondeterministicModelParserTest.cpp
rename to src/test/storm/parser/NondeterministicModelParserTest.cpp
diff --git a/src/test/parser/NondeterministicSparseTransitionParserTest.cpp b/src/test/storm/parser/NondeterministicSparseTransitionParserTest.cpp
similarity index 100%
rename from src/test/parser/NondeterministicSparseTransitionParserTest.cpp
rename to src/test/storm/parser/NondeterministicSparseTransitionParserTest.cpp
diff --git a/src/test/parser/PrismParserTest.cpp b/src/test/storm/parser/PrismParserTest.cpp
similarity index 100%
rename from src/test/parser/PrismParserTest.cpp
rename to src/test/storm/parser/PrismParserTest.cpp
diff --git a/src/test/parser/SparseItemLabelingParserTest.cpp b/src/test/storm/parser/SparseItemLabelingParserTest.cpp
similarity index 100%
rename from src/test/parser/SparseItemLabelingParserTest.cpp
rename to src/test/storm/parser/SparseItemLabelingParserTest.cpp
diff --git a/src/test/parser/SparseStateRewardParserTest.cpp b/src/test/storm/parser/SparseStateRewardParserTest.cpp
similarity index 100%
rename from src/test/parser/SparseStateRewardParserTest.cpp
rename to src/test/storm/parser/SparseStateRewardParserTest.cpp
diff --git a/src/test/permissiveschedulers/MilpPermissiveSchedulerTest.cpp b/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
similarity index 100%
rename from src/test/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
rename to src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
diff --git a/src/test/permissiveschedulers/SmtPermissiveSchedulerTest.cpp b/src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
similarity index 100%
rename from src/test/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
rename to src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
diff --git a/src/test/solver/CudaPluginTest.cpp b/src/test/storm/solver/CudaPluginTest.cpp
similarity index 100%
rename from src/test/solver/CudaPluginTest.cpp
rename to src/test/storm/solver/CudaPluginTest.cpp
diff --git a/src/test/solver/EigenLinearEquationSolverTest.cpp b/src/test/storm/solver/EigenLinearEquationSolverTest.cpp
similarity index 100%
rename from src/test/solver/EigenLinearEquationSolverTest.cpp
rename to src/test/storm/solver/EigenLinearEquationSolverTest.cpp
diff --git a/src/test/solver/EliminationLinearEquationSolverTest.cpp b/src/test/storm/solver/EliminationLinearEquationSolverTest.cpp
similarity index 100%
rename from src/test/solver/EliminationLinearEquationSolverTest.cpp
rename to src/test/storm/solver/EliminationLinearEquationSolverTest.cpp
diff --git a/src/test/solver/FullySymbolicGameSolverTest.cpp b/src/test/storm/solver/FullySymbolicGameSolverTest.cpp
similarity index 100%
rename from src/test/solver/FullySymbolicGameSolverTest.cpp
rename to src/test/storm/solver/FullySymbolicGameSolverTest.cpp
diff --git a/src/test/solver/GameSolverTest.cpp b/src/test/storm/solver/GameSolverTest.cpp
similarity index 100%
rename from src/test/solver/GameSolverTest.cpp
rename to src/test/storm/solver/GameSolverTest.cpp
diff --git a/src/test/solver/GlpkLpSolverTest.cpp b/src/test/storm/solver/GlpkLpSolverTest.cpp
similarity index 100%
rename from src/test/solver/GlpkLpSolverTest.cpp
rename to src/test/storm/solver/GlpkLpSolverTest.cpp
diff --git a/src/test/solver/GmmxxLinearEquationSolverTest.cpp b/src/test/storm/solver/GmmxxLinearEquationSolverTest.cpp
similarity index 100%
rename from src/test/solver/GmmxxLinearEquationSolverTest.cpp
rename to src/test/storm/solver/GmmxxLinearEquationSolverTest.cpp
diff --git a/src/test/solver/GmmxxMinMaxLinearEquationSolverTest.cpp b/src/test/storm/solver/GmmxxMinMaxLinearEquationSolverTest.cpp
similarity index 100%
rename from src/test/solver/GmmxxMinMaxLinearEquationSolverTest.cpp
rename to src/test/storm/solver/GmmxxMinMaxLinearEquationSolverTest.cpp
diff --git a/src/test/solver/GurobiLpSolverTest.cpp b/src/test/storm/solver/GurobiLpSolverTest.cpp
similarity index 100%
rename from src/test/solver/GurobiLpSolverTest.cpp
rename to src/test/storm/solver/GurobiLpSolverTest.cpp
diff --git a/src/test/solver/MathsatSmtSolverTest.cpp b/src/test/storm/solver/MathsatSmtSolverTest.cpp
similarity index 100%
rename from src/test/solver/MathsatSmtSolverTest.cpp
rename to src/test/storm/solver/MathsatSmtSolverTest.cpp
diff --git a/src/test/solver/MinMaxTechniqueSelectionTest.cpp b/src/test/storm/solver/MinMaxTechniqueSelectionTest.cpp
similarity index 100%
rename from src/test/solver/MinMaxTechniqueSelectionTest.cpp
rename to src/test/storm/solver/MinMaxTechniqueSelectionTest.cpp
diff --git a/src/test/solver/NativeLinearEquationSolverTest.cpp b/src/test/storm/solver/NativeLinearEquationSolverTest.cpp
similarity index 100%
rename from src/test/solver/NativeLinearEquationSolverTest.cpp
rename to src/test/storm/solver/NativeLinearEquationSolverTest.cpp
diff --git a/src/test/solver/NativeMinMaxLinearEquationSolverTest.cpp b/src/test/storm/solver/NativeMinMaxLinearEquationSolverTest.cpp
similarity index 100%
rename from src/test/solver/NativeMinMaxLinearEquationSolverTest.cpp
rename to src/test/storm/solver/NativeMinMaxLinearEquationSolverTest.cpp
diff --git a/src/test/solver/Z3LpSolverTest.cpp b/src/test/storm/solver/Z3LpSolverTest.cpp
similarity index 100%
rename from src/test/solver/Z3LpSolverTest.cpp
rename to src/test/storm/solver/Z3LpSolverTest.cpp
diff --git a/src/test/solver/Z3SmtSolverTest.cpp b/src/test/storm/solver/Z3SmtSolverTest.cpp
similarity index 100%
rename from src/test/solver/Z3SmtSolverTest.cpp
rename to src/test/storm/solver/Z3SmtSolverTest.cpp
diff --git a/src/test/storage/BitVectorHashMapTest.cpp b/src/test/storm/storage/BitVectorHashMapTest.cpp
similarity index 100%
rename from src/test/storage/BitVectorHashMapTest.cpp
rename to src/test/storm/storage/BitVectorHashMapTest.cpp
diff --git a/src/test/storage/BitVectorTest.cpp b/src/test/storm/storage/BitVectorTest.cpp
similarity index 100%
rename from src/test/storage/BitVectorTest.cpp
rename to src/test/storm/storage/BitVectorTest.cpp
diff --git a/src/test/storage/CuddDdTest.cpp b/src/test/storm/storage/CuddDdTest.cpp
similarity index 100%
rename from src/test/storage/CuddDdTest.cpp
rename to src/test/storm/storage/CuddDdTest.cpp
diff --git a/src/test/storage/DeterministicModelBisimulationDecompositionTest.cpp b/src/test/storm/storage/DeterministicModelBisimulationDecompositionTest.cpp
similarity index 100%
rename from src/test/storage/DeterministicModelBisimulationDecompositionTest.cpp
rename to src/test/storm/storage/DeterministicModelBisimulationDecompositionTest.cpp
diff --git a/src/test/storage/ExpressionEvalutionTest.cpp b/src/test/storm/storage/ExpressionEvalutionTest.cpp
similarity index 100%
rename from src/test/storage/ExpressionEvalutionTest.cpp
rename to src/test/storm/storage/ExpressionEvalutionTest.cpp
diff --git a/src/test/storage/ExpressionTest.cpp b/src/test/storm/storage/ExpressionTest.cpp
similarity index 100%
rename from src/test/storage/ExpressionTest.cpp
rename to src/test/storm/storage/ExpressionTest.cpp
diff --git a/src/test/storage/JaniModelTest.cpp b/src/test/storm/storage/JaniModelTest.cpp
similarity index 100%
rename from src/test/storage/JaniModelTest.cpp
rename to src/test/storm/storage/JaniModelTest.cpp
diff --git a/src/test/storage/MaximalEndComponentDecompositionTest.cpp b/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp
similarity index 100%
rename from src/test/storage/MaximalEndComponentDecompositionTest.cpp
rename to src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp
diff --git a/src/test/storage/NondeterministicModelBisimulationDecompositionTest.cpp b/src/test/storm/storage/NondeterministicModelBisimulationDecompositionTest.cpp
similarity index 100%
rename from src/test/storage/NondeterministicModelBisimulationDecompositionTest.cpp
rename to src/test/storm/storage/NondeterministicModelBisimulationDecompositionTest.cpp
diff --git a/src/test/storage/PrismProgramTest.cpp b/src/test/storm/storage/PrismProgramTest.cpp
similarity index 100%
rename from src/test/storage/PrismProgramTest.cpp
rename to src/test/storm/storage/PrismProgramTest.cpp
diff --git a/src/test/storage/SchedulerTest.cpp b/src/test/storm/storage/SchedulerTest.cpp
similarity index 100%
rename from src/test/storage/SchedulerTest.cpp
rename to src/test/storm/storage/SchedulerTest.cpp
diff --git a/src/test/storage/SparseMatrixTest.cpp b/src/test/storm/storage/SparseMatrixTest.cpp
similarity index 100%
rename from src/test/storage/SparseMatrixTest.cpp
rename to src/test/storm/storage/SparseMatrixTest.cpp
diff --git a/src/test/storage/StronglyConnectedComponentDecompositionTest.cpp b/src/test/storm/storage/StronglyConnectedComponentDecompositionTest.cpp
similarity index 100%
rename from src/test/storage/StronglyConnectedComponentDecompositionTest.cpp
rename to src/test/storm/storage/StronglyConnectedComponentDecompositionTest.cpp
diff --git a/src/test/storage/SylvanDdTest.cpp b/src/test/storm/storage/SylvanDdTest.cpp
similarity index 100%
rename from src/test/storage/SylvanDdTest.cpp
rename to src/test/storm/storage/SylvanDdTest.cpp
diff --git a/src/test/storm-test.cpp b/src/test/storm/storm-test.cpp
similarity index 100%
rename from src/test/storm-test.cpp
rename to src/test/storm/storm-test.cpp
diff --git a/src/test/transformer/EndComponentEliminatorTest.cpp b/src/test/storm/transformer/EndComponentEliminatorTest.cpp
similarity index 100%
rename from src/test/transformer/EndComponentEliminatorTest.cpp
rename to src/test/storm/transformer/EndComponentEliminatorTest.cpp
diff --git a/src/test/utility/GraphTest.cpp b/src/test/storm/utility/GraphTest.cpp
similarity index 100%
rename from src/test/utility/GraphTest.cpp
rename to src/test/storm/utility/GraphTest.cpp
diff --git a/src/test/utility/KSPTest.cpp b/src/test/storm/utility/KSPTest.cpp
similarity index 100%
rename from src/test/utility/KSPTest.cpp
rename to src/test/storm/utility/KSPTest.cpp
diff --git a/src/test/utility/ModelInstantiatorTest.cpp b/src/test/storm/utility/ModelInstantiatorTest.cpp
similarity index 100%
rename from src/test/utility/ModelInstantiatorTest.cpp
rename to src/test/storm/utility/ModelInstantiatorTest.cpp
diff --git a/src/test/utility/VectorTest.cpp b/src/test/storm/utility/VectorTest.cpp
similarity index 100%
rename from src/test/utility/VectorTest.cpp
rename to src/test/storm/utility/VectorTest.cpp