From d3952c82f6b3a8a845aa9210cce32e507b60a82e Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 26 Sep 2018 12:53:50 +0200 Subject: [PATCH] fix in variable information for unbounded variables --- src/storm/generator/VariableInformation.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/storm/generator/VariableInformation.cpp b/src/storm/generator/VariableInformation.cpp index 3bc1d7d8b..640989c43 100644 --- a/src/storm/generator/VariableInformation.cpp +++ b/src/storm/generator/VariableInformation.cpp @@ -164,12 +164,12 @@ namespace storm { if (variable.hasUpperBound()) { upperBound = variable.getUpperBound().evaluateAsInt(); } else { - upperBound = lowerBound + ((1u << reservedBitsForUnboundedVariables) - 1); + upperBound = lowerBound + ((1ll << reservedBitsForUnboundedVariables) - 1); } } else { STORM_LOG_THROW(variable.hasUpperBound(), storm::exceptions::WrongFormatException, "Bounded integer variable has neither a lower nor an upper bound."); upperBound = variable.getUpperBound().evaluateAsInt(); - lowerBound = upperBound - ((1u << reservedBitsForUnboundedVariables) - 1); + lowerBound = upperBound - ((1ll << reservedBitsForUnboundedVariables) - 1); } uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, global, !variable.hasLowerBound() || !variable.hasUpperBound()); @@ -178,8 +178,8 @@ namespace storm { } for (auto const& variable : variableSet.getUnboundedIntegerVariables()) { if (!variable.isTransient()) { - int64_t lowerBound = - (1u << (reservedBitsForUnboundedVariables - 1)); - int64_t upperBound = (1u << (reservedBitsForUnboundedVariables - 1)) - 1; + int64_t lowerBound = -(1ll << (reservedBitsForUnboundedVariables - 1)); + int64_t upperBound = (1ll << (reservedBitsForUnboundedVariables - 1)) - 1; integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, reservedBitsForUnboundedVariables, global, true); totalBitOffset += reservedBitsForUnboundedVariables; }