```java /** * Resizes the bit vector to have the given length. If the new length is larger than the current length, the * additional (most significant) bits are set the 'false'. If the new length is smaller than the current length, the * most significant bits are dropped. The BDDs for dropped bits, are {@link BDD#free freed}. */ ``` The method itself does this: ```java // Resize. BDD[] newBits = new BDD[length]; int min = Math.min(bits.length, length); System.arraycopy(bits, 0, newBits, 0, min); for (int i = min; i < length; i++) { newBits[i] = factory.zero(); } bits = newBits; ``` If `length < bits.length`, then some BDDs in `bits` are not copied. These BDDs are not freed, even though the description states they should be. Note that in practice we almost exclusively resize to a large length, so it shouldn't be a big issue. Still, it is wrong.