From 5bcdb5f95aaf441f1f8e4cf2b05ff011662bf487 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 27 Aug 2020 17:33:22 +0200
Subject: [PATCH] Fixed --sound switch for LRA properties on deterministic
 models.

---
 .../SparseDeterministicInfiniteHorizonHelper.cpp                | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp
index 511a67787..23ceaf9cb 100644
--- a/src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp
+++ b/src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp
@@ -405,6 +405,8 @@ namespace storm {
                     solver->setBounds(*lowerUpperBounds.first, *lowerUpperBounds.second);
                     // Check solver requirements
                     auto requirements = solver->getRequirements(env);
+                    requirements.clearUpperBounds();
+                    requirements.clearLowerBounds();
                     STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UnmetRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
                     sspValues.assign(sspMatrixVector.first.getRowCount(), (*lowerUpperBounds.first + *lowerUpperBounds.second) / storm::utility::convertNumber<ValueType,uint64_t>(2));
                     solver->solveEquations(env, sspValues, sspMatrixVector.second);