You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copying from one slot to another should add a copy of every constraint that
includes the RHS of the assignment to the copy postcondition (with the RHS
renamed, in the constraint, to the new LHS slot).
In other words:
let int x = 10;
let int y = 11;
check lt(x,y); // postcond = { lt(x,y) }
let int z = x; // postcond = { lt(x,y), lt(z,y) }
Unless some horrible complications arise that make this impossible, I believe
the current rules permit this propagation to work.