Unroll1

type t

relation p(X:t)

individual idx : t

action a(max:t)

object spec = {
    before a {
    idx := 0;
    while idx < max {
        assert p(idx);
        idx := idx + 1
    }
    }
}

interpret t -> bv[2]

export a

isolate iso = this