disable tests which depend on mathsat if mathsat is not available, gives a warning in verbose output

src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp

@@ -17,7 +17,11 @@
 
 #include "storm/settings/modules/GeneralSettings.h"
 
+#if defined STORM_HAVE_MSAT
 TEST(GameBasedDtmcModelCheckerTest, Die_Cudd) {
+#else
+TEST(GameBasedDtmcModelCheckerTest, DISABLED_Die_Cudd) {
+#endif
     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);
     
@@ -49,7 +53,11 @@ TEST(GameBasedDtmcModelCheckerTest, Die_Cudd) {
     EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 }
 
+#if defined STORM_HAVE_MSAT
 TEST(GameBasedDtmcModelCheckerTest, Die_Sylvan) {
+#else
+TEST(GameBasedDtmcModelCheckerTest, DISABLED_Die_Sylvan) {
+#endif
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
     
     // A parser that we use for conveniently constructing the formulas.
@@ -82,7 +90,11 @@ TEST(GameBasedDtmcModelCheckerTest, Die_Sylvan) {
     EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 }
 
+#if defined STORM_HAVE_MSAT
 TEST(GameBasedDtmcModelCheckerTest, SynchronousLeader_Cudd) {
+#else
+TEST(GameBasedDtmcModelCheckerTest, DISABLED_SynchronousLeader_Cudd) {
+#endif
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm");
     program = program.substituteConstants();
     
@@ -100,7 +112,11 @@ TEST(GameBasedDtmcModelCheckerTest, SynchronousLeader_Cudd) {
     EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 }
 
+#if defined STORM_HAVE_MSAT
 TEST(GameBasedDtmcModelCheckerTest, SynchronousLeader_Sylvan) {
+#else
+TEST(GameBasedDtmcModelCheckerTest, DISABLED_SynchronousLeader_Sylvan) {
+#endif
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm");
     program = program.substituteConstants();
 

src/test/modelchecker/GameBasedMdpModelCheckerTest.cpp

@@ -16,7 +16,11 @@
 
 #include "storm/utility/storm.h"
 
+#if defined STORM_HAVE_MSAT
 TEST(GameBasedMdpModelCheckerTest, Dice_Cudd) {
+#else
+TEST(GameBasedMdpModelCheckerTest, DISABLED_Dice_Cudd) {
+#endif
     std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm";
 
     storm::prism::Program program = storm::parseProgram(programFile);
@@ -87,7 +91,11 @@ TEST(GameBasedMdpModelCheckerTest, Dice_Cudd) {
     EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 }
 
+#if defined STORM_HAVE_MSAT
 TEST(GameBasedMdpModelCheckerTest, Dice_Sylvan) {
+#else
+TEST(GameBasedMdpModelCheckerTest, DISABLED_Dice_Sylvan) {
+#endif
     std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm";
     
     storm::prism::Program program = storm::parseProgram(programFile);

src/test/permissiveschedulers/SmtPermissiveSchedulerTest.cpp

@@ -11,9 +11,11 @@
 #include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
 
 
-#if defined(STORM_HAVE_MSAT) || defined(STORM_HAVE_Z3)
-
+#if defined STORM_HAVE_MSAT
 TEST(SmtPermissiveSchedulerTest, DieSelection) {
+#else
+TEST(SmtPermissiveSchedulerTest, DISABLED_DieSelection) {
+#endif
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/die_c1.nm");
     storm::parser::FormulaParser formulaParser(program);
     
@@ -57,5 +59,3 @@ TEST(SmtPermissiveSchedulerTest, DieSelection) {
     //
     
 }
-
-#endif // STORM_HAVE_MSAT || STORM_HAVE_Z3