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(new BinaryBooleanFunctionExpression(first.getBaseExpression().getManager(), first.getType().logicalConnective(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::And))); }