Browse Source

BitVector: Fixed an issue with the move assignment operator. The 'other' BitVector was left in an invalid state.

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
commit
a728c01322
  1. 1
      src/storm/storage/BitVector.cpp

1
src/storm/storage/BitVector.cpp

@ -156,6 +156,7 @@ namespace storm {
// Only perform the assignment if the source and target are not identical. // Only perform the assignment if the source and target are not identical.
if (this != &other) { if (this != &other) {
bitCount = other.bitCount; bitCount = other.bitCount;
other.bitCount = 0;
if (this->buckets) { if (this->buckets) {
delete[] this->buckets; delete[] this->buckets;
} }

Loading…
Cancel
Save