strange behavior with structs as member of parameterized object

[nano-o]

Hello, Ivy find a counter-example to the following invariant, which seems strange to me:

#lang ivy1.7

type pair_t = struct {
    x : bool,
    y : bool
}

type index

object obj(i:index) = {
    individual p:pair_t
    after init {
        p.x := false;
        p.y := false;
    }
    export action act1 = {
        require p.x = false;
        p.y := true;
    }
    export action act2 = {
        require p.y = false;
        p.x := true;
    }
    invariant ~(p.x & p.y)
}

[nano-o]

Using isolate obj instead of object obj seems to fix the problem.