From e99e5bf6bfd66292b1acde051a7046bae83d716c Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Tue, 28 Nov 2017 15:56:50 +0100
Subject: [PATCH] Fixed typo leading to wrong variables in SMT encoding

---
 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 8704febe3..56e7671b5 100644
--- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
@@ -505,7 +505,7 @@ namespace storm {
                             tmpVars.push_back(varNames.size() - 1);
                             tmpTimePointVariables.push_back(varNames.size() - 1);
                             // AND over the selected children
-                            constraints.push_back(std::make_shared<IsMaximum>(tmpVars.at(i), combinationChildren));
+                            constraints.push_back(std::make_shared<IsMaximum>(timePointVariables.at(i), combinationChildren));
                             constraints.back()->setDescription("VOT gate " + element->name() + ": AND no. " + std::to_string(i));
                             // Generate next permutation
                             combination = nextBitPermutation(combination);