From acd6c5e9bef3234304cdf8b5b6bea4a170cf3c19 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 29 Aug 2017 17:13:37 +0200
Subject: [PATCH] fix for toIntegralVector

---
 src/storm/utility/vector.h | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h
index cb5789852..828ef1ed5 100644
--- a/src/storm/utility/vector.h
+++ b/src/storm/utility/vector.h
@@ -888,7 +888,7 @@ namespace storm {
                 if (occurringNonZeroNumbers.empty()) {
                     factor = storm::utility::one<ValueType>();
                 } else if (occurringNonZeroNumbers.size() == 1) {
-                    factor = storm::utility::one<ValueType>() / (*occurringNonZeroNumbers.begin());
+                    factor = *occurringNonZeroNumbers.begin();
                 } else {
                     // Obtain the least common multiple of the denominators of the occurring numbers.
                     // We can then multiply the numbers with the lcm to obtain integers.
@@ -912,8 +912,9 @@ namespace storm {
                 std::vector<TargetValueType> result;
                 result.reserve(vec.size());
                 for (auto const& v : vec) {
-                    result.push_back(storm::utility::convertNumber<TargetValueType, ValueType>(v / factor));
-                    STORM_LOG_ASSERT(storm::utility::isInteger(result.back()), "Resulting number '" << result.back() << "' is not integral.");
+                    ValueType vScaled = v / factor;
+                    STORM_LOG_ASSERT(storm::utility::isInteger(vScaled), "Resulting number '(" << v << ")/(" << factor << ") = " << vScaled << "' is not integral.");
+                    result.push_back(storm::utility::convertNumber<TargetValueType, ValueType>(vScaled));
                 }
                 return std::make_pair(std::move(result), std::move(factor));