(set-logic QF_BV) (declare-fun i () (_ BitVec 32)) (declare-fun n () (_ BitVec 32)) (declare-fun next_i () (_ BitVec 32)) (declare-fun b () (_ BitVec 1)) (declare-fun next_b () (_ BitVec 1)) (assert (not (= i (_ bv2147483647 32)))) (assert (= b (bvslt i n))) (assert (= next_i (bvadd i (_ bv1 32)))) (assert (= next_b (bvslt next_i n))) (assert (and (not b) next_b)) (check-sat) (exit)