do not evaluate for loop iterator expr multiple times

[zeldovich]

Without this fix, trying to verify a simple program like:

        let m = HashSet::<u32>::new();
        for k in m.iter() {}

would lead to an error:

        error: loop invariant not satisfied
         --> bug.rs:9:9
          |
        9 |         for k in m.iter() {}
          |         ^^^^^^^^^^^^^^^^^^^^
          |         |
          |         at this loop exit
          |         failed this invariant

        verification results:: 1 verified, 1 errors
        error: aborting due to 1 previous error

but if m.iter() was instead an identifier, as in below, verification passed:

        let m = HashSet::<u32>::new();
        let m_iter = m.iter();
        for k in m_iter {}

This commit changes the for loop macro to avoid evaluating the iterator expression, such as m.iter() in the above example, multiple times, which makes the first example above verify just fine.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.