PcaaWeightVectorChecker: Avoid division by zero bug (#653)

moves-rwth · Jan 14, 2025 · 4eaf6d6 · 4eaf6d6
1 parent 5823e1a
commit 4eaf6d6
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
@@ -513,7 +513,7 @@ void StandardPcaaWeightVectorChecker<SparseModelType>::unboundedIndividualPhase(
                         deterministicBackwardTransitions, storm::storage::BitVector(deterministicMatrix.getRowCount(), true), statesWithRewards);
 
                     // Compute the estimate for this objective
-                    if (!storm::utility::isZero(weightVector[objIndex])) {
+                    if (!storm::utility::isZero(weightVector[objIndex]) && !storm::utility::isZero(sumOfWeightsOfUncheckedObjectives)) {
                         objectiveResults[objIndex] = weightedSumOfUncheckedObjectives;
                         ValueType scalingFactor = storm::utility::one<ValueType>() / sumOfWeightsOfUncheckedObjectives;
                         if (storm::solver::minimize(obj.formula->getOptimalityType())) {