From 38795a67b4fbb1a16d8289efa437156ef25267ef Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 26 Jul 2019 08:34:16 +0200
Subject: [PATCH] PolytopeTree: Better union of childs

---
 src/storm/storage/geometry/PolytopeTree.h | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/src/storm/storage/geometry/PolytopeTree.h b/src/storm/storage/geometry/PolytopeTree.h
index 016c8cbcc..e09710eeb 100644
--- a/src/storm/storage/geometry/PolytopeTree.h
+++ b/src/storm/storage/geometry/PolytopeTree.h
@@ -49,19 +49,20 @@ namespace storm {
                         } else {
                             // This is an inner node. Traverse the children and set this to the convex union of its children.
                             std::vector<PolytopeTree<ValueType>> newChildren;
-                            std::shared_ptr<Polytope<ValueType>> newPolytope = nullptr;
+                            std::vector<std::vector<ValueType>> newPolytopeVertices;
                             for (auto& c : children) {
                                 c.setMinus(rhs);
                                 if (c.polytope != nullptr) {
                                     newChildren.push_back(c);
-                                    if (newPolytope) {
-                                        newPolytope = newPolytope->convexUnion(c.polytope);
-                                    } else {
-                                        newPolytope = c.polytope;
-                                    }
+                                    auto cVertices = c.polytope->getVertices();
+                                    newPolytopeVertices.insert(newPolytopeVertices.end(), cVertices.begin(), cVertices.end());
                                 }
                             }
-                            polytope = newPolytope; // nullptr, if no children left
+                            if (newPolytopeVertices.empty()) {
+                                polytope = nullptr;
+                            } else {
+                                polytope = storm::storage::geometry::Polytope<ValueType>::create(newPolytopeVertices);
+                            }
                             children = std::move(newChildren);
                         }
                     }