(define x::int) (assert (>= x 1/2)) (assert (<= x 3/2)) (check)