From 80fc8fb56ba5eaad73492d0a6d5b1149d701ec00 Mon Sep 17 00:00:00 2001
From: Alexander Bork <alexander.bork@rwth-aachen.de>
Date: Fri, 17 May 2019 13:30:34 +0200
Subject: [PATCH] Fix for error that checkbound may be large than number of
 Markovian states

---
 src/storm-dft/modelchecker/dft/DFTASFChecker.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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);