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.