From ba0d81ca52172d4bd68fbf10c7a60a3714dc29d2 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 12 Oct 2016 21:13:09 +0200
Subject: [PATCH] bugfix for PRISM program: only check initial values of
 variables if they have one

Former-commit-id: c5c548bd62f28b1d2cdc70bb75f7c84d12233c62 [formerly c27c72bd59e9f07a05cb8e9c5f56b65906ff7a2f]
Former-commit-id: 97acb66693b15d0464a7dbc15c70a13c73f60f10
---
 src/storage/prism/Module.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp
index 095ac3e11..0a4347396 100644
--- a/src/storage/prism/Module.cpp
+++ b/src/storage/prism/Module.cpp
@@ -196,12 +196,12 @@ namespace storm {
         
         bool Module::containsVariablesOnlyInUpdateProbabilities(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const {
             for (auto const& booleanVariable : this->getBooleanVariables()) {
-                if (booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
+                if (booleanVariable.hasInitialValue() && booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
                     return false;
                 }
             }
             for (auto const& integerVariable : this->getIntegerVariables()) {
-                if (integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
+                if (integerVariable.hasInitialValue() && integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
                     return false;
                 }
                 if (integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) {