Simplify projections applied to casted literals in VCs
Function postconditions of the form result = x + 1
where result
and x
have type int32
results in verification conditions of the form:
int32'int result = int32'int x + int32'int (1:int32)
This PR is an attempt at simplifying it to int32'int result = int32'int x + 1
.
TODO: update obsoleted sessions