The solution to the minmax equation system becomes unique after eliminating end components.

src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp

@@ -199,6 +199,10 @@ namespace storm {
                             
                             // Eliminate the end components and remove the states that are not interesting (target or non-filter).
                             eliminateEndComponentsAndExtendedStatesUntilProbabilities(explicitRepresentation, solverRequirementsData, targetStates);
+                            
+                            // The solution becomes unique after end components have been eliminated.
+                            uniqueSolution = true;
+
                         } else {
                             // Then compute the vector that contains the one-step probabilities to a state with probability 1 for all
                             // maybe states.
@@ -571,6 +575,8 @@ namespace storm {
 
                             if (requirements.requiresNoEndComponents()) {
                                 eliminateEndComponentsAndTargetStatesReachabilityRewards(explicitRepresentation, solverRequirementsData, targetStates, requirements.requiresUpperBounds());
+                                // The solution becomes unique after end components have been eliminated.
+                                uniqueSolution = true;
                             } else {
                                 if (requirements.requiresValidInitialScheduler()) {
                                     // Compute a valid initial scheduler.

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@@ -441,6 +441,8 @@ namespace storm {
                         STORM_LOG_ASSERT(!result.hasUniqueSolution(), "The solver requires to eliminate the end components although the solution is already assumed to be unique.");
                         STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires it.");
                         result.eliminateEndComponents = true;
+                        // If end components have been eliminated we can assume a unique solution.
+                        result.uniqueSolution = true;
                         requirements.clearNoEndComponents();
                     }