Skip to content

Commit 1402d50

Browse files
remove unneccessary assume
1 parent 7e52e12 commit 1402d50

1 file changed

Lines changed: 0 additions & 1 deletion

File tree

library/core/src/num/dec2flt/decimal_seq.rs

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -190,7 +190,6 @@ impl DecimalSeq {
190190
} else if n == 0 {
191191
return;
192192
} else {
193-
kani::assume(read_index == self.num_digits);
194193
#[kani::loop_invariant(n > 0 && read_index <= self.num_digits + 64 - n.leading_zeros() as usize && read_index > 0)]
195194
while (n >> shift) == 0 {
196195
n *= 10;

0 commit comments

Comments
 (0)