(define x1::int) (define x2::int) (assert (<= x1 0)) (assert (>= x2 0)) (assert (= x1 (+ x2 1)))