Fix purification

[fpoli]

The purify_vars pass does not correctly havoc the variables that it purified in a loop. That is, while replacing a usize(_2) with _2: Int it removes acc(usize(_2), write) from exhale statements without generating an havoc statement. The encode_unsigned_num_constraint=true and check_overflows=false combination is required to expose this encoding bug.

In the following example, the bug hides that the precondition of next might fail:

use prusti_contracts::*;

struct IterRange {
    from: usize,
    to: usize,
}

#[requires(iter.from < iter.to)] // Wrong, should be `<=`
#[ensures(iter.to == old(iter.to))]
#[ensures(old(iter.from < iter.to) ==> iter.from == old(iter.from) + 1)]
#[ensures(old(iter.from < iter.to) == matches!(result, Some(_)))]
#[ensures(old(iter.from == iter.to) == matches!(result, None))]
fn next(iter: &mut IterRange) -> Option<usize> {
    assert!(iter.from < iter.to);
    if iter.from < iter.to {
        let v = iter.from;
        iter.from = v + 1;
        Some(v)
    } else {
        None
    }
}

fn main() {
    let mut iter = IterRange { from: 0, to: 10 };
    let mut i = 0;
    loop {
        body_invariant!(i == iter.from && iter.from <= iter.to && iter.to == 10);
        match next(&mut iter) { // Expected: precondition might not hold
            Some(_) => {}
            None => break,
        }
        i += 1;
    }
    assert!(i == 10);
}