[Prover][Issue] An optimization issue

[junkil-park]

I am not exactly sure what the cause is, but think it may be related to an incorrect optimization.

Please examine the following example:

How to reproduce

module 0x42::loop_inv_2 {
    fun foo(i: u64) {
        assert!(i == 50, 0);
        let old_i = i;
        spec {
            assert old_i == 50;
        };
        while ({
            spec {
                invariant old_i <= i && i <= 100;
            };
            i < 100
        }) {
            spec {
                assert old_i == 50; // fail to prove
            };
            i = i + 1;
        };
        spec {
            assert i == 100;
        };
    }
}

In the example above, assert old_i == 50; // fail to prove fails. Looking at the generated boogie file, i and old_i seem to be treated as identical in the loop. So, when i is havoced in the loop, so is old_i effectively.

Expected output

Prover succeeds proving the example.