
(enum status (ready busy))

(declare-const request Bool)
(declare-const status status)
(declare-const request_true Bool)

(assert (= status ready))

(assert (=> request
        (=> (not (= status busy))
            (exists ((request_true_prev Bool))
                (and request_true_prev
                     (not request_true)
                     (= status busy)
                     )
                )
            )
        )
)

(check-sat)