diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index f99cc23aa..fd1db1421 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -479,7 +479,7 @@ namespace storm { } // Toplevel element will not fail (part of constraint 13) - constraints.push_back(std::make_shared(dft.getTopLevelIndex(), notFailed)); + constraints.push_back(std::make_shared(timePointVariables.at(dft.getTopLevelIndex()), notFailed)); constraints.back()->setDescription("Toplevel element should not fail"); }