#lang ivy1.7
type t
relation p(X:t)
after init {
p(X) := true
}
invariant p(X)
interpret t -> bv[1]
attribute method = mc