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.
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.