From d62af9332b1c7e042b35f892f23238172ebb5e65 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Basg=C3=B6ze?= Date: Fri, 3 Apr 2020 15:25:10 +0200 Subject: [PATCH] Fix bitshift overflow The simple 1 is a 32bit integer literal on most machines leading to an overflow: 1<<32 == 0. Even on 64 bit machines. --- src/storm-dft/modelchecker/dft/DFTASFChecker.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 84e08d306..112f4d89d 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -255,7 +255,7 @@ namespace storm { // Construct selected children from combination std::vector combinationChildren; for (size_t j = 0; j < vot->nrChildren(); ++j) { - if (combination & (1 << j)) { + if (combination & (1ul << j)) { combinationChildren.push_back(childVarIndices.at(j)); } } @@ -270,7 +270,7 @@ namespace storm { // Generate next permutation combination = nextBitPermutation(combination); ++k; - } while (combination < (1 << vot->nrChildren()) && combination != 0); + } while (combination < (1ul << vot->nrChildren()) && combination != 0); // Constraint is OR over all possible combinations constraints.push_back(std::make_shared(timePointVariables.at(i), tmpVars));