diff --git a/src/storm/storage/jani/ArrayEliminator.cpp b/src/storm/storage/jani/ArrayEliminator.cpp index 58379cfc4..cd78f95ca 100644 --- a/src/storm/storage/jani/ArrayEliminator.cpp +++ b/src/storm/storage/jani/ArrayEliminator.cpp @@ -668,12 +668,16 @@ namespace storm { } ArrayEliminatorData ArrayEliminator::eliminate(Model& model, bool keepNonTrivialArrayAccess) { - auto sizes = detail::MaxArraySizeDeterminer().getMaxSizes(model); - ArrayEliminatorData result = detail::ArrayVariableReplacer(model.getExpressionManager(), keepNonTrivialArrayAccess, sizes).replace(model); - if (!keepNonTrivialArrayAccess) { - model.getModelFeatures().remove(ModelFeature::Arrays); + ArrayEliminatorData result; + // Only perform actions if there actually are arrays. + if (model.getModelFeatures().hasArrays()) { + auto sizes = detail::MaxArraySizeDeterminer().getMaxSizes(model); + result = detail::ArrayVariableReplacer(model.getExpressionManager(), keepNonTrivialArrayAccess, sizes).replace(model); + if (!keepNonTrivialArrayAccess) { + model.getModelFeatures().remove(ModelFeature::Arrays); + } + model.finalize(); } - model.finalize(); STORM_LOG_ASSERT(!containsArrayExpression(model), "the model still contains array expressions."); return result; } diff --git a/src/storm/storage/jani/FunctionEliminator.cpp b/src/storm/storage/jani/FunctionEliminator.cpp index 50d5deb95..ed2784d10 100644 --- a/src/storm/storage/jani/FunctionEliminator.cpp +++ b/src/storm/storage/jani/FunctionEliminator.cpp @@ -394,7 +394,10 @@ namespace storm { void eliminateFunctions(Model& model, std::vector& properties) { - detail::FunctionEliminatorTraverser().eliminate(model, properties); + // Only perform actions if there actually are functions. + if (model.getModelFeatures().hasFunctions()) { + detail::FunctionEliminatorTraverser().eliminate(model, properties); + } STORM_LOG_ASSERT(!containsFunctionCallExpression(model), "The model still seems to contain function calls."); }