From 70e2263783d9beaaef55785473fe09612d7fc533 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 11 Mar 2020 11:56:59 +0100 Subject: [PATCH] MarkovAutomatonCslModelCheckerTest: Prevent this test from failing in cases where z3 is installed without optimization support. --- .../MarkovAutomatonCslModelCheckerTest.cpp | 26 ++++++++++++------- 1 file changed, 16 insertions(+), 10 deletions(-) diff --git a/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp b/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp index 31c0ca29c..03c54a27a 100755 --- a/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp @@ -332,15 +332,21 @@ namespace { result = checker->check(this->env(), tasks[6]); EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result))); } - - result = checker->check(this->env(), tasks[7]); - EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[8]); - EXPECT_NEAR(this->parseNumber("407"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[9]); - EXPECT_NEAR(this->parseNumber("27"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - + +#ifndef STORM_HAVE_Z3_OPTIMIZE + if (!storm::utility::isZero(this->precision())) { +#endif + // Checking LRA properties exactly requires an exact LP solver. + result = checker->check(this->env(), tasks[7]); + EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[8]); + EXPECT_NEAR(this->parseNumber("407"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[9]); + EXPECT_NEAR(this->parseNumber("27"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); +#ifndef STORM_HAVE_Z3_OPTIMIZE + } +#endif } }