From f0270304bbe1007880e3d63cbb955acdb10712e4 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 29 Jul 2024 12:33:02 +0200
Subject: [PATCH] Fixed accidentally discarding reward accumulations for
 cumulative reward formulas

---
 src/storm/logic/ExpressionSubstitutionVisitor.cpp | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/storm/logic/ExpressionSubstitutionVisitor.cpp b/src/storm/logic/ExpressionSubstitutionVisitor.cpp
index f31df2f309..52af363d14 100644
--- a/src/storm/logic/ExpressionSubstitutionVisitor.cpp
+++ b/src/storm/logic/ExpressionSubstitutionVisitor.cpp
@@ -90,9 +90,14 @@ boost::any ExpressionSubstitutionVisitor::visit(CumulativeRewardFormula const& f
         bounds.emplace_back(TimeBound(f.isBoundStrict(i), substitutionFunction(f.getBound(i))));
         timeBoundReferences.push_back(f.getTimeBoundReference(i));
     }
-    return std::static_pointer_cast<Formula>(std::make_shared<CumulativeRewardFormula>(bounds, timeBoundReferences));
+    boost::optional<RewardAccumulation> optionalRewardAccumulation;
+    if (f.hasRewardAccumulation()) {
+        optionalRewardAccumulation = f.getRewardAccumulation();
+    }
+    return std::static_pointer_cast<Formula>(std::make_shared<CumulativeRewardFormula>(bounds, timeBoundReferences, optionalRewardAccumulation));
 }
 
+
 boost::any ExpressionSubstitutionVisitor::visit(InstantaneousRewardFormula const& f, boost::any const& data) const {
     auto const& substitutionFunction = *boost::any_cast<std::function<storm::expressions::Expression(storm::expressions::Expression const&)> const*>(data);
     return std::static_pointer_cast<Formula>(std::make_shared<InstantaneousRewardFormula>(substitutionFunction(f.getBound()), f.getTimeBoundType()));