From b7daafc4c1a1ba8fd34bb6d4a03b5391d310657a Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@gmail.com>
Date: Sun, 25 Jul 2021 22:25:12 -0700
Subject: [PATCH] fix in predicate expression simplify pointed out by TQ,
 thanks

---
 src/storm/storage/expressions/PredicateExpression.cpp | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

diff --git a/src/storm/storage/expressions/PredicateExpression.cpp b/src/storm/storage/expressions/PredicateExpression.cpp
index e41d7fe42..8bc829f7d 100644
--- a/src/storm/storage/expressions/PredicateExpression.cpp
+++ b/src/storm/storage/expressions/PredicateExpression.cpp
@@ -64,19 +64,15 @@ namespace storm {
                     simplifiedOperands.push_back(res);
                 }
             }
-            if (trueCount > 1 && (predicate == PredicateType::ExactlyOneOf || predicate == PredicateType::AtMostOneOf)) {
-                return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(this->getManager(),
-                                                                                    false));
-            }
 
             if (simplifiedOperands.size() == 0) {
                 switch(predicate) {
                     case PredicateType::ExactlyOneOf: return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(this->getManager(),
-                                                                                                                          false));
+                                                                                                                          trueCount == 1));
                     case PredicateType::AtLeastOneOf: return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(this->getManager(),
-                                                                                                                          false));
+                                                                                                                          trueCount >= 1));
                     case PredicateType::AtMostOneOf: return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(this->getManager(),
-                                                                                                                          true));
+                                                                                                                         trueCount <= 1));
                 }
             }
             // Return new expression if something changed.