Trouble verifying "weakend" properties

[yav]

In the following model, sally successfully validates ok1, but returns unknown on ok2, which is the same as ok1 but or-ed with another boolean value.

(define-state-type
   S
   ( (ok1 Bool) (ok2 Bool) (x Int) (y Int) )
   ( (a Bool) )
)

(define-transition-system TS S
   (and
      (= x 1)
      (= y 2)
      (= ok1 true)
      (= ok2 true)
    )
   (and
      (= next.x state.y)
      (= next.y state.x)
      (= next.ok1     (not (= next.x next.y))         )
      (= next.ok2 (or (not (= next.x next.y)) input.a))
  )
)

(query TS ok1)
(query TS ok2)

>sally test1.sally --engine=kind
valid
unknown