Closed hajduakos closed 4 years ago
The problem here is the following: The type checker has a check whether an identifier that is a magic variable, is of type integer. If yes, it asserts that it has to be named "now"
and then reports a deprecation error to use block.timestamp
instead. So it seems like it is hardcoded that the only magic identifier of type int can be now
. However, we also have __verifier_idx_int
(see specs/SumPushPop.sol
), which causes the assertion to fail. A quick solution would be to turn the assertion into a condition: if we have an identifier which is a magic variable and it is an integer, then instead of asserting, we check if it is now
and if yes, report the deprecation. However, this would make a little modification in the type checker. A cleaner but more compex solution that I can imagine is to declare these __verifier_idx_XXX
variables similarly to the quantified variables, i.e., create a "regular" declaration (instead of a magic variable) and add it to the scope of the specification expression every time. What do you think @dddejan?
Simple solutions is probably best. We can figure out a better solution later.
Fixed it with the simple solution in a75b4a8226601480315a0ad462c8ffb9b7e83390
specs/SumPushPop.sol
gives