From 004466b83f8552bb9d71d6369f30c5f0102e126c Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 13 Mar 2019 09:36:09 +0100
Subject: [PATCH] Fixed BitVector::full() for BitVectors with size 0
---
src/storm/storage/BitVector.cpp | 3 +++
src/storm/storage/BitVector.h | 1 +
2 files changed, 4 insertions(+)
diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp
index 18ac1feb3..616d2b424 100644
--- a/src/storm/storage/BitVector.cpp
+++ b/src/storm/storage/BitVector.cpp
@@ -566,6 +566,9 @@ namespace storm {
}
bool BitVector::full() const {
+ if (bitCount == 0) {
+ return true;
+ }
// Check that all buckets except the last one have all bits set.
uint64_t* last = buckets + bucketCount() - 1;
for (uint64_t const* it = buckets; it < last; ++it) {
diff --git a/src/storm/storage/BitVector.h b/src/storm/storage/BitVector.h
index 89d6ccad2..6fd4a79aa 100644
--- a/src/storm/storage/BitVector.h
+++ b/src/storm/storage/BitVector.h
@@ -417,6 +417,7 @@ namespace storm {
/*!
* Retrievs whether all bits are set in this bit vector.
+ * If the bit vector has size 0, this method always returns true.
*
* @return True iff all bits in the bit vector are set.
*/