diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
index 0ed94401d..87cd93a17 100644
--- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
@@ -565,6 +565,7 @@ namespace storm {
         DFTASFChecker::checkFailsLeqWithEqNonMarkovianState(uint64_t checkbound, uint64_t nrNonMarkovian) {
             STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries");
             std::vector<uint64_t> markovianIndices;
+            checkbound = std::min<int>(checkbound, markovianVariables.size());
             // Get Markovian variable indices up until given timepoint
             for (uint64_t i = 0; i < checkbound; ++i) {
                 markovianIndices.push_back(markovianVariables.at(i));
@@ -576,7 +577,6 @@ namespace storm {
                     timePointVariables.at(dft.getTopLevelIndex()), checkbound);
             std::shared_ptr<storm::expressions::ExpressionManager> manager = solver->getManager().getSharedPointer();
             solver->add(tleFailedConstr->toExpression(varNames, manager));
-
             // Constraint that a given number of non-Markovian states are visited
             std::shared_ptr<SmtConstraint> nonMarkovianConstr = std::make_shared<FalseCountIsEqualConstant>(
                     markovianIndices, nrNonMarkovian);