Open A-Mehdi opened 1 year ago
- Yes
So do we have to change the defined macro MAX from 16 to 8? ALso I think MAX is a constant, not a non-determinitic input value from the environment, right?
We set MAX as 16 constant because of the overflow problem. If you try to access the left child of x[7], then you might access x[left(7)], which is x[14]. Please just let it be 16 constant, and think of it as an 8-length array.
We set MAX as 16 constant because of the overflow problem. If you try to access the left child of x[7], then you might access x[left(7)], which is x[14]. Please just let it be 16 constant, and think of it as an 8-length array.
But left child is already constrainted by (l<=h_size && x[l]>x[i]) so I think overflow would not happen?
It depends on your verification code.
I have two questions: