From 9fbb58788418c095fa0d6c1c006234286a48d28d Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 5 Aug 2020 11:46:19 +0200
Subject: [PATCH] LraViHelper: Fix for NondetTsNoIs

---
 .../helper/infinitehorizon/internal/LraViHelper.cpp           | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp
index d4c3ba856..af4ab9dfd 100644
--- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp
+++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp
@@ -96,7 +96,9 @@ namespace storm {
                             // The currently processed state is timed.
                             if (nondetTs()) {
                                 tsTransitionsBuilder.newRowGroup(currTsRow);
-                                tsToIsTransitionsBuilder.newRowGroup(currTsRow);
+                                if (_hasInstantStates) {
+                                    tsToIsTransitionsBuilder.newRowGroup(currTsRow);
+                                }
                             }
                             // We need to uniformize which means that a diagonal entry for the selfloop will be inserted.
                             // If there are exit rates, the uniformization factor needs to be updated.