From 7982d58ef7e43e6a09459310d5a6bb13a7916ddd Mon Sep 17 00:00:00 2001
From: Jan Erik Karuc <jan.karuc@rwth-aachen.de>
Date: Fri, 3 Apr 2020 12:27:13 +0200
Subject: [PATCH] Combine new upper bound geq cases

---
 src/storm/solver/helper/OptimisticValueIterationHelper.h | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/src/storm/solver/helper/OptimisticValueIterationHelper.h b/src/storm/solver/helper/OptimisticValueIterationHelper.h
index 4cfe6c012..c298b0ffe 100644
--- a/src/storm/solver/helper/OptimisticValueIterationHelper.h
+++ b/src/storm/solver/helper/OptimisticValueIterationHelper.h
@@ -175,15 +175,15 @@ namespace storm {
                                     newUpperBoundAlwaysLowerEqual = false;
                                 }
                             }
-                            if (newUpperBoundAlwaysHigherEqual &! newUpperBoundAlwaysLowerEqual) {
-                                // All values moved up or stayed the same (but are not the same)
+                            if (newUpperBoundAlwaysHigherEqual) {
+                                // All values moved up or stayed the same
                                 // That means the guess for an upper bound is actually a lower bound
                                 iterationPrecision = oviinternal::updateIterationPrecision(env, *auxVector, *upperX, relative, relevantValues);
                                 // We assume to have a single fixed point. We can thus safely set the new lower bound, to the wrongly guessed upper bound
                                 // Set lowerX to the upper bound candidate
                                 std::swap(lowerX, upperX);
                                 break;
-                            } else if (newUpperBoundAlwaysLowerEqual &! newUpperBoundAlwaysHigherEqual) {
+                            } else if (newUpperBoundAlwaysLowerEqual) {
                                 // All values moved down or stayed the same and we have a maximum difference of twice the requested precision
                                 // We can safely use twice the requested precision, as we calculate the center of both vectors
                                 bool reachedPrecision;
@@ -199,9 +199,6 @@ namespace storm {
                                     // From now on, we keep updating both bounds
                                     intervalIterationNeeded = true;
                                 }
-                            } else if (newUpperBoundAlwaysHigherEqual && newUpperBoundAlwaysLowerEqual) {
-                                // All values stayed the same. For safety we guess above this value again and check, if all values move down
-                                break;
                             }
                             // At this point, the old upper bounds (auxVector) are not needed anymore.