From ccb5a89de356152e187992a592b77f8d373cb18d Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 20 Sep 2018 09:55:56 +0200
Subject: [PATCH] Formula substitutions need to be performed before constant
 substitutions because otherwise, constants appearing in formula expressions
 can not be handled properly

---
 src/storm/storage/prism/Program.cpp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp
index 6b0c4b876..3c6936d52 100644
--- a/src/storm/storage/prism/Program.cpp
+++ b/src/storm/storage/prism/Program.cpp
@@ -857,6 +857,10 @@ namespace storm {
         }
         
         Program Program::substituteConstantsFormulas(bool substituteConstants, bool substituteFormulas) const {
+            // Formulas need to be substituted first. otherwise, constants appearing in formula expressions can not be handled properly
+            if (substituteConstants && substituteFormulas) {
+                return this->substituteFormulas().substituteConstants();
+            }
             
             // We start by creating the appropriate substitution.
             std::map<storm::expressions::Variable, storm::expressions::Expression> substitution = getConstantsFormulasSubstitution(substituteConstants, substituteFormulas);
@@ -1316,7 +1320,7 @@ namespace storm {
         
         Program Program::simplify() {
             // Start by substituting the constants, because this will potentially erase some commands or even actions.
-            Program substitutedProgram = this->substituteConstants();
+            Program substitutedProgram = this->substituteConstantsFormulas();
             
             // As we possibly delete some commands and some actions might be dropped from modules altogether, we need to
             // maintain a list of actions that we need to remove in other modules. For example, if module A loses all [a]