(set-logic QF_BV)
(declare-fun x () (_ BitVec 32))
(declare-fun next_x () (_ BitVec 32))
(declare-fun n () (_ BitVec 32))
(declare-fun one () (_ BitVec 32))
(assert (= one (_ bv1 32)))
(assert (bvsge x n))
(assert (= next_x (bvadd x one)))
(push 1)
(assert (bvslt next_x n))
(set-info :status sat)
(check-sat)
(pop 1)

(push 1)
(assert (bvsge next_x n))
(set-info :status sat)
(check-sat)
(pop 1)