From d7aa7cc7c8754a6a4ee89df9703e055c2051cb71 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Wed, 14 Dec 2016 16:51:28 +0100
Subject: [PATCH] expression AND with true is immediately simplified

---
 src/storm/storage/expressions/Expression.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/storm/storage/expressions/Expression.cpp b/src/storm/storage/expressions/Expression.cpp
index 9dbd46986..c9ca8a320 100644
--- a/src/storm/storage/expressions/Expression.cpp
+++ b/src/storm/storage/expressions/Expression.cpp
@@ -235,6 +235,12 @@ namespace storm {
         
         Expression operator&&(Expression const& first, Expression const& second) {
             assertSameManager(first.getBaseExpression(), second.getBaseExpression());
+            if (first.isTrue()) {
+                return second;
+            }
+            if (second.isTrue()) {
+                return first;
+            }
             return Expression(std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(first.getBaseExpression().getManager(), first.getType().logicalConnective(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::And)));
         }