From 890dca30cf44c75d7b8f6f33c454d6348778f7af Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 22 May 2020 18:58:06 +0200
Subject: [PATCH] Nativepolytope: When intersecting, check easy cases where one
 of the polytopes are universal first. This also prevents that an internal
 Eigen assertion is raised in cases where an empty and a non-empty matrix are
 concatenated (somehow only relevant for gcc 9.3 in debug mode...).

---
 src/storm/storage/geometry/NativePolytope.cpp | 22 ++++++++++++-------
 1 file changed, 14 insertions(+), 8 deletions(-)

diff --git a/src/storm/storage/geometry/NativePolytope.cpp b/src/storm/storage/geometry/NativePolytope.cpp
index 9f1dc4174..886f01b91 100644
--- a/src/storm/storage/geometry/NativePolytope.cpp
+++ b/src/storm/storage/geometry/NativePolytope.cpp
@@ -190,14 +190,20 @@ namespace storm {
             template <typename ValueType>
             std::shared_ptr<Polytope<ValueType>> NativePolytope<ValueType>::intersection(std::shared_ptr<Polytope<ValueType>> const& rhs) const{
                 STORM_LOG_THROW(rhs->isNativePolytope(), storm::exceptions::InvalidArgumentException, "Invoked operation between a NativePolytope and a different polytope implementation. This is not supported");
-                NativePolytope<ValueType> const& nativeRhs = dynamic_cast<NativePolytope<ValueType> const&>(*rhs);
-                EigenMatrix resultA(A.rows() + nativeRhs.A.rows(), A.cols());
-                resultA << A,
-                           nativeRhs.A;
-                EigenVector resultb(resultA.rows());
-                resultb << b,
-                           nativeRhs.b;
-                return std::make_shared<NativePolytope<ValueType>>(EmptyStatus::Unknown, std::move(resultA), std::move(resultb));
+                if (this->isUniversal()) {
+                    return rhs;
+                } else if (rhs->isUniversal()) {
+                    return std::make_shared<NativePolytope<ValueType>>(*this);
+                } else {
+                    NativePolytope<ValueType> const& nativeRhs = dynamic_cast<NativePolytope<ValueType> const&>(*rhs);
+                    EigenMatrix resultA(A.rows() + nativeRhs.A.rows(), A.cols());
+                    resultA << A,
+                               nativeRhs.A;
+                    EigenVector resultb(resultA.rows());
+                    resultb << b,
+                               nativeRhs.b;
+                    return std::make_shared<NativePolytope<ValueType>>(EmptyStatus::Unknown, std::move(resultA), std::move(resultb));
+                }
             }
             
             template <typename ValueType>