diff --git a/src/storm/storage/expressions/Expression.cpp b/src/storm/storage/expressions/Expression.cpp
index b980cab0a..bb3dca82f 100644
--- a/src/storm/storage/expressions/Expression.cpp
+++ b/src/storm/storage/expressions/Expression.cpp
@@ -246,9 +246,11 @@ namespace storm {
         Expression operator&&(Expression const& first, Expression const& second) {
             assertSameManager(first.getBaseExpression(), second.getBaseExpression());
             if (first.isTrue()) {
+                STORM_LOG_THROW(second.hasBooleanType(), storm::exceptions::InvalidTypeException, "Operator requires boolean operands.");
                 return second;
             }
             if (second.isTrue()) {
+                STORM_LOG_THROW(first.hasBooleanType(), storm::exceptions::InvalidTypeException, "Operator requires boolean operands.");
                 return first;
             }
             return Expression(std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(first.getBaseExpression().getManager(), first.getType().logicalConnective(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::And)));
diff --git a/src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp b/src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp
index aee1eeb24..4cc504f39 100644
--- a/src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp
+++ b/src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp
@@ -19,30 +19,15 @@
 
 TEST(GameBasedDtmcModelCheckerTest, Die_Cudd) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
+	auto checker = std::make_shared<storm::modelchecker::GameBasedMdpModelChecker<storm::dd::DdType::CUDD, storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>>>(program);
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
 
-    // Build the die model with its reward model.
-#ifdef WINDOWS
-    storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
-#else
-    typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
-#endif
-    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program, options);
-    EXPECT_EQ(13ul, model->getNumberOfStates());
-    EXPECT_EQ(20ul, model->getNumberOfTransitions());
-    
-    ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
-    
-    std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>>();
-	auto checker = std::make_shared<storm::modelchecker::GameBasedMdpModelChecker<storm::dd::DdType::CUDD, storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>>>(program);
-    
     std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
 	storm::modelchecker::CheckTask<storm::logic::Formula, double> task(*formula, true);
     
     std::unique_ptr<storm::modelchecker::CheckResult> result = checker->check(task);
-    //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
     
     EXPECT_NEAR(1.0/6.0, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
@@ -51,7 +36,6 @@ TEST(GameBasedDtmcModelCheckerTest, Die_Cudd) {
 	task = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formula, true);
     
     result = checker->check(task);
-    //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
     
     EXPECT_NEAR(1.0/6.0, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
@@ -60,7 +44,6 @@ TEST(GameBasedDtmcModelCheckerTest, Die_Cudd) {
 	task = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formula, true);
     
     result = checker->check(task);
-    //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
     
     EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
@@ -71,27 +54,13 @@ TEST(GameBasedDtmcModelCheckerTest, Die_Sylvan) {
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
-    
-    // Build the die model with its reward model.
-#ifdef WINDOWS
-    storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options;
-#else
-    typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options;
-#endif
-    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program, options);
-    EXPECT_EQ(13ul, model->getNumberOfStates());
-    EXPECT_EQ(20ul, model->getNumberOfTransitions());
-    
-    ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
-    
-    std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>();
+
 	auto checker = std::make_shared<storm::modelchecker::GameBasedMdpModelChecker<storm::dd::DdType::Sylvan, storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>>(program);
     
     std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
 	storm::modelchecker::CheckTask<storm::logic::Formula, double> task(*formula, true);
     
     std::unique_ptr<storm::modelchecker::CheckResult> result = checker->check(task);
-    //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
     
     EXPECT_NEAR(1.0/6.0, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
@@ -100,7 +69,6 @@ TEST(GameBasedDtmcModelCheckerTest, Die_Sylvan) {
 	task = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formula, true);
     
     result = checker->check(task);
-    //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
     
     EXPECT_NEAR(1.0/6.0, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
@@ -109,177 +77,43 @@ TEST(GameBasedDtmcModelCheckerTest, Die_Sylvan) {
 	task = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formula, true);
     
     result = checker->check(task);
-    //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
     
     EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 }
 
-TEST(GameBasedDtmcModelCheckerTest, Crowds_Cudd) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
-    
-    // A parser that we use for conveniently constructing the formulas.
-    storm::parser::FormulaParser formulaParser;
-    
-    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program);
-    EXPECT_EQ(8607ul, model->getNumberOfStates());
-    EXPECT_EQ(15113ul, model->getNumberOfTransitions());
-    
-    ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
-    
-    std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>>();
-	auto checker = std::make_shared<storm::modelchecker::GameBasedMdpModelChecker<storm::dd::DdType::CUDD, storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>>>(program);
-    
-    std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
-	storm::modelchecker::CheckTask<storm::logic::Formula, double> task(*formula, true);
-    
-    std::unique_ptr<storm::modelchecker::CheckResult> result = checker->check(task);
-    //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
-    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
-    
-    EXPECT_NEAR(0.33288236360191303, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-    
-    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]");
-	task = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formula, true);
-    
-    result = checker->check(task);
-    //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
-    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
-    
-    EXPECT_NEAR(0.15222081144084315, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-    
-    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]");
-	task = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formula, true);
-    
-    result = checker->check(task);
-    //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
-    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
-    
-    EXPECT_NEAR(0.3215392962289586, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-}
-
-TEST(GameBasedDtmcModelCheckerTest, Crowds_Sylvan) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
-    
-    // A parser that we use for conveniently constructing the formulas.
-    storm::parser::FormulaParser formulaParser;
-    
-    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program);
-    EXPECT_EQ(8607ul, model->getNumberOfStates());
-    EXPECT_EQ(15113ul, model->getNumberOfTransitions());
-    
-    ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
-    
-    std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>();
-	auto checker = std::make_shared<storm::modelchecker::GameBasedMdpModelChecker<storm::dd::DdType::Sylvan, storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>>(program);
-
-    std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
-	storm::modelchecker::CheckTask<storm::logic::Formula, double> task(*formula, true);
-    
-    std::unique_ptr<storm::modelchecker::CheckResult> result = checker->check(task);
-    //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
-    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
-    
-    // FIXME: precision not optimal.
-    EXPECT_NEAR(0.33288236360191303, quantitativeResult1[0], 10 * storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-    
-    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]");
-	task = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formula, true);
-    
-    result = checker->check(task);
-    //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
-    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
-    
-    // FIXME: precision not optimal.
-    EXPECT_NEAR(0.15222081144084315, quantitativeResult2[0], 10 * storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-    
-    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]");
-	task = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formula, true);
-    
-    result = checker->check(task);
-    //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
-    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
-    
-    // FIXME: precision not optimal.
-    EXPECT_NEAR(0.3215392962289586, quantitativeResult3[0], 10 * storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-}
-
 TEST(GameBasedDtmcModelCheckerTest, SynchronousLeader_Cudd) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm");
+    program = program.substituteConstants();
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
     
-    // Build the die model with its reward model.
-#ifdef WINDOWS
-    storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
-#else
-    typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
-#endif
-    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program, options);
-    EXPECT_EQ(273ul, model->getNumberOfStates());
-    EXPECT_EQ(397ul, model->getNumberOfTransitions());
-    
-    ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
-    
-    std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>>();
 	auto checker = std::make_shared<storm::modelchecker::GameBasedMdpModelChecker<storm::dd::DdType::CUDD, storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>>>(program);
 
     std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
 	storm::modelchecker::CheckTask<storm::logic::Formula, double> task(*formula, true);
     
     std::unique_ptr<storm::modelchecker::CheckResult> result = checker->check(task);
-    //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
     
     EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-    
-    formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]");
-	task = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formula, true);
-    
-    result = checker->check(task);
-    //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
-    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
-    
-    EXPECT_NEAR(0.99999989760000074, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 }
 
 TEST(GameBasedDtmcModelCheckerTest, SynchronousLeader_Sylvan) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm");
-    
+    program = program.substituteConstants();
+
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
     
-    // Build the die model with its reward model.
-#ifdef WINDOWS
-    storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options;
-#else
-    typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options;
-#endif
-    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program, options);
-    EXPECT_EQ(273ul, model->getNumberOfStates());
-    EXPECT_EQ(397ul, model->getNumberOfTransitions());
-    
-    ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
-    
-    std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>();
 	auto checker = std::make_shared<storm::modelchecker::GameBasedMdpModelChecker<storm::dd::DdType::Sylvan, storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>>(program);
 
     std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
 	storm::modelchecker::CheckTask<storm::logic::Formula, double> task(*formula, true);
     
     std::unique_ptr<storm::modelchecker::CheckResult> result = checker->check(task);
-    //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
     
     EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-    
-    formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]");
-	task = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formula, true);
-    
-    result = checker->check(task);
-    //result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
-    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
-    
-    EXPECT_NEAR(0.99999989760000074, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 }
diff --git a/src/test/modelchecker/GameBasedMdpModelCheckerTest.cpp b/src/test/modelchecker/GameBasedMdpModelCheckerTest.cpp
index 71f86a62f..441b03b37 100644
--- a/src/test/modelchecker/GameBasedMdpModelCheckerTest.cpp
+++ b/src/test/modelchecker/GameBasedMdpModelCheckerTest.cpp
@@ -87,55 +87,73 @@ TEST(GameBasedMdpModelCheckerTest, Dice_Cudd) {
     EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 }
 
-TEST(GameBasedMdpModelCheckerTest, AsynchronousLeader_Cudd) {
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm";
-
+TEST(GameBasedMdpModelCheckerTest, Dice_Sylvan) {
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm";
+    
     storm::prism::Program program = storm::parseProgram(programFile);
-	// Build the die model
+    
+    // Build the die model
 #ifdef WINDOWS
-    storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
+    storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options;
 #else
-    typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
+    typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options;
 #endif
-    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().build(program, options);
-
-    ASSERT_EQ(3172ull, model->getNumberOfStates());
-    ASSERT_EQ(7144ull, model->getNumberOfTransitions());
-
-	std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
-	auto mdpModelchecker = std::make_shared<storm::modelchecker::GameBasedMdpModelChecker<storm::dd::DdType::CUDD, storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>>(program);
-
-	// A parser that we use for conveniently constructing the formulas.
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>().build(program, options);
+    
+    ASSERT_EQ(model->getNumberOfStates(), 169ull);
+    ASSERT_EQ(model->getNumberOfTransitions(), 436ull);
+    
+    std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
+    auto mdpModelchecker = std::make_shared<storm::modelchecker::GameBasedMdpModelChecker<storm::dd::DdType::Sylvan, storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>>(program);
+    
+    // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
-    std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
-	storm::modelchecker::CheckTask<storm::logic::Formula, double> task(*formula, true);
-
+    
+    std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
+    storm::modelchecker::CheckTask<storm::logic::Formula, double> task(*formula, true);
+    
     std::unique_ptr<storm::modelchecker::CheckResult> result = mdpModelchecker->check(task);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
-
-    EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-
-    formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]");
-	task = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formula, true);
-
+    
+    EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    
+    formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]");
+    task = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formula, true);
+    
     result = mdpModelchecker->check(task);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
-
-    EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-
-    formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]");
-	task = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formula, true);
-
+    
+    EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    
+    formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]");
+    task = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formula, true);
+    
     result = mdpModelchecker->check(task);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
-
-    EXPECT_NEAR(0.0625, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-
-    formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]");
-	task = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formula, true);
-
+    
+    EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    
+    formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]");
+    task = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formula, true);
+    
     result = mdpModelchecker->check(task);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
-
-    EXPECT_NEAR(0.0625, quantitativeResult4[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    
+    EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    
+    formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]");
+    task = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formula, true);
+    
+    result = mdpModelchecker->check(task);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
+    
+    EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    
+    formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]");
+    task = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formula, true);
+    
+    result = mdpModelchecker->check(task);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
+    
+    EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 }