From 20d424e289540a8c7e249a4f42df4bfa4bf95701 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 20 Nov 2020 09:36:59 +0100
Subject: [PATCH] JaniTraverser: Only traverse lower/upper bound expressions of
 BoundedIntegerVariables, if these bounds exists.

---
 src/storm/storage/jani/FunctionEliminator.cpp    |  8 ++++++--
 .../storage/jani/traverser/JaniTraverser.cpp     | 16 ++++++++++++----
 2 files changed, 18 insertions(+), 6 deletions(-)

diff --git a/src/storm/storage/jani/FunctionEliminator.cpp b/src/storm/storage/jani/FunctionEliminator.cpp
index c81ffbeae..21906c8cf 100644
--- a/src/storm/storage/jani/FunctionEliminator.cpp
+++ b/src/storm/storage/jani/FunctionEliminator.cpp
@@ -334,8 +334,12 @@ namespace storm {
                     if (variable.hasInitExpression()) {
                         variable.setInitExpression(functionEliminationVisitor->eliminate(variable.getInitExpression()));
                     }
-                    variable.setLowerBound(functionEliminationVisitor->eliminate(variable.getLowerBound()));
-                    variable.setUpperBound(functionEliminationVisitor->eliminate(variable.getUpperBound()));
+                    if (variable.hasLowerBound()) {
+                        variable.setLowerBound(functionEliminationVisitor->eliminate(variable.getLowerBound()));
+                    }
+                    if (variable.hasUpperBound()) {
+                        variable.setUpperBound(functionEliminationVisitor->eliminate(variable.getUpperBound()));
+                    }
                 }
                 
                 void traverse(UnboundedIntegerVariable& variable, boost::any const& data) override {
diff --git a/src/storm/storage/jani/traverser/JaniTraverser.cpp b/src/storm/storage/jani/traverser/JaniTraverser.cpp
index 8800f7e56..0518544c8 100644
--- a/src/storm/storage/jani/traverser/JaniTraverser.cpp
+++ b/src/storm/storage/jani/traverser/JaniTraverser.cpp
@@ -95,8 +95,12 @@ namespace storm {
             if (variable.hasInitExpression()) {
                 traverse(variable.getInitExpression(), data);
             }
-            traverse(variable.getLowerBound(), data);
-            traverse(variable.getUpperBound(), data);
+            if (variable.hasLowerBound()) {
+                traverse(variable.getLowerBound(), data);
+            }
+            if (variable.hasUpperBound()) {
+                traverse(variable.getUpperBound(), data);
+            }
         }
         
         void JaniTraverser::traverse(UnboundedIntegerVariable& variable, boost::any const& data) {
@@ -276,8 +280,12 @@ namespace storm {
             if (variable.hasInitExpression()) {
                 traverse(variable.getInitExpression(), data);
             }
-            traverse(variable.getLowerBound(), data);
-            traverse(variable.getUpperBound(), data);
+            if (variable.hasLowerBound()) {
+                traverse(variable.getLowerBound(), data);
+            }
+            if (variable.hasUpperBound()) {
+                traverse(variable.getUpperBound(), data);
+            }
         }
         
         void ConstJaniTraverser::traverse(UnboundedIntegerVariable const& variable, boost::any const& data) {