From ed1a5b6cedec2557bb126f95b03d61c3786906bd Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 9 Sep 2020 16:31:22 +0200
Subject: [PATCH] Fixed flagging objectives for reward finiteness check
 incorrectly

---
 .../preprocessing/SparseMultiObjectivePreprocessor.cpp          | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp
index 35d7aeb11..9c54b343f 100644
--- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp
+++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp
@@ -584,7 +584,6 @@ namespace storm {
                     for (uint64_t i = 0; i < formula.getDimension(); ++i) {
                         auto oldTbr = formula.getTimeBoundReference(i);
                         if (oldTbr.isRewardBound()) {
-                            onlyRewardBounds = false;
                             if (oldTbr.hasRewardAccumulation()) {
                                 auto filteredBoundRewards = storm::utility::createFilteredRewardModel(data.model->getRewardModel(oldTbr.getRewardName()), oldTbr.getRewardAccumulation(), data.model->isDiscreteTimeModel());
                                 if (filteredBoundRewards.isDifferentFromUnfilteredModel()) {
@@ -599,6 +598,7 @@ namespace storm {
                                 newTimeBoundReferences.push_back(oldTbr);
                             }
                         } else {
+                            onlyRewardBounds = false;
                             newTimeBoundReferences.push_back(oldTbr);
                         }
                     }