From b82e0608e513831b0f7c5ff345f6fbcd40cc12c2 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 5 May 2017 08:24:31 +0200
Subject: [PATCH] Fix for CheckTask: now properly updating uperator information
 to make nested formulas work again (pointed out by Matt S Bauer)

---
 src/storm/modelchecker/CheckTask.h | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/src/storm/modelchecker/CheckTask.h b/src/storm/modelchecker/CheckTask.h
index 32063b293..4440f1ba3 100644
--- a/src/storm/modelchecker/CheckTask.h
+++ b/src/storm/modelchecker/CheckTask.h
@@ -52,7 +52,6 @@ namespace storm {
             template<typename NewFormulaType>
             CheckTask<NewFormulaType, ValueType> substituteFormula(NewFormulaType const& newFormula) const {
                 CheckTask<NewFormulaType, ValueType> result(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->hint);
-                result.updateOperatorInformation();
                 return result;
             }
             
@@ -68,13 +67,13 @@ namespace storm {
                     }
                     
                     if (operatorFormula.hasBound()) {
-                        if (onlyInitialStatesRelevant) {
-                            this->bound = operatorFormula.getBound();
-                        }
-
-                        if (!optimizationDirection) {
-                            this->optimizationDirection = operatorFormula.getComparisonType() == storm::logic::ComparisonType::Less || operatorFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual ? OptimizationDirection::Maximize : OptimizationDirection::Minimize;
-                        }
+                        this->bound = operatorFormula.getBound();
+                    }
+                    
+                    if (operatorFormula.hasOptimalityType()) {
+                        this->optimizationDirection = operatorFormula.getOptimalityType();
+                    } else if (operatorFormula.hasBound()) {
+                        this->optimizationDirection = operatorFormula.getComparisonType() == storm::logic::ComparisonType::Less || operatorFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual ? OptimizationDirection::Maximize : OptimizationDirection::Minimize;
                     }
                 
                     if (formula.get().isProbabilityOperatorFormula()) {