#lang ivy1.7

type t

relation p(X:t)

after init {
    p(X) := true
}

invariant p(X)

interpret t -> bv[1]

attribute method = mc