diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 60f6976d6..06bfd1cca 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -566,10 +566,10 @@ namespace storm { // Child must be operational at time of claiming additionalC.push_back(std::make_shared(timeClaiming, timePointVariables.at(child->id()))); // No other spare claims this child - for (auto const& otherSpare : child->parents()) { - if (otherSpare->id() != spare->id()) { + for (auto const& parent : child->parents()) { + if (parent->isSpareGate() && parent->id() != spare->id()) { // Different spare - additionalC.push_back(std::make_shared(getClaimVariableIndex(otherSpare->id(), child->id()), notFailed)); + additionalC.push_back(std::make_shared(getClaimVariableIndex(parent->id(), child->id()), notFailed)); } } constraints.push_back(std::make_shared(leftC, std::make_shared(additionalC)));