From c7d7be8b83f7083aa2c4d07b50e9059b275d9587 Mon Sep 17 00:00:00 2001
From: Stefan Pranger <stefan.pranger@student.tugraz.at>
Date: Tue, 22 Dec 2020 17:02:21 +0100
Subject: [PATCH] nondetTs may also be gameNondetTs in LraViHelper

---
 .../helper/infinitehorizon/internal/LraViHelper.cpp             | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp
index 101d21543..583468754 100644
--- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp
+++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp
@@ -485,7 +485,7 @@ namespace storm {
                 
                 template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
                 bool LraViHelper<ValueType, ComponentType, TransitionsType>::nondetTs() const {
-                    return TransitionsType == LraViTransitionsType::NondetTsNoIs;
+                    return TransitionsType == LraViTransitionsType::NondetTsNoIs || gameNondetTs();
                 }
                 
                 template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>