// check: VerificationError
// check: BorrowLocExistsBorrowError

module Tester {
    struct T{v: u64}

    public new(v: u64): V#Self.T  {
        return T{v: move(v)};
    }

    public update(t: &mut V#Self.T) {
        let vref: &mut u64;
        vref = &mut move(t).v;
        *move(vref) = 1;
        return;
    }

    public vref(this: &mut V#Self.T): &u64 {
        let r: &u64;
        r = &copy(this).v;
        release(move(this));
        return move(r);
    }
}

//! new-transaction

import {{default}}.Tester;

main() {
    let t: V#Tester.T;
    let tt: &mut V#Tester.T;
    let vref_before: &u64;
    let ref_t: &mut V#Tester.T;
    let vref_after: &u64;
    t = Tester.new(0);
    tt = &mut t;
    vref_before = Tester.vref(move(tt));
    assert(*copy(vref_before) == 0, 42);
    ref_t = &mut t;
    Tester.update(copy(ref_t));
    vref_after = Tester.vref(move(ref_t));
    assert(*move(vref_before) == 1, 42);
    assert(*move(vref_after) == 1, 42);
    return;
}