(set-logic QF_BV)
(set-option :incremental true)
(declare-fun s0 () (_ BitVec 3))
(declare-fun zero () (_ BitVec 3))
(declare-fun one () (_ BitVec 3))
(declare-fun goal () (_ BitVec 3))
(declare-fun r1 () (_ BitVec 1))
(declare-fun e1 () (_ BitVec 1))
(declare-fun s1 () (_ BitVec 3))
(declare-fun r2 () (_ BitVec 1))
(declare-fun e2 () (_ BitVec 1))
(declare-fun s2 () (_ BitVec 3))
(declare-fun r3 () (_ BitVec 1))
(declare-fun e3 () (_ BitVec 1))
(declare-fun s3 () (_ BitVec 3))
(declare-fun r4 () (_ BitVec 1))
(declare-fun e4 () (_ BitVec 1))
(declare-fun s4 () (_ BitVec 3))
(declare-fun r5 () (_ BitVec 1))
(declare-fun e5 () (_ BitVec 1))
(declare-fun s5 () (_ BitVec 3))
(declare-fun r6 () (_ BitVec 1))
(declare-fun e6 () (_ BitVec 1))
(declare-fun s6 () (_ BitVec 3))
(declare-fun r7 () (_ BitVec 1))
(declare-fun e7 () (_ BitVec 1))
(declare-fun s7 () (_ BitVec 3))
(assert (= goal (_ bv7 3)))
(assert (= zero (_ bv0 3)))
(assert (= one (_ bv1 3)))
(assert (= s0 zero))
(push 1)
(assert (= s0 goal))
(check-sat)
(pop 1)

(assert (= s1 (ite (= r1 (_ bv1 1)) zero (ite (= e1 (_ bv1 1)) (bvadd s0 one) s0))))
(push 1)
(assert (= s1 goal))
(check-sat)
(pop 1)

(assert (= s2 (ite (= r2 (_ bv1 1)) zero (ite (= e2 (_ bv1 1)) (bvadd s1 one) s1))))
(push 1)
(assert (= s2 goal))
(check-sat)
(pop 1)

(assert (= s3 (ite (= r3 (_ bv1 1)) zero (ite (= e3 (_ bv1 1)) (bvadd s2 one) s2))))
(push 1)
(assert (= s3 goal))
(check-sat)
(pop 1)

(assert (= s4 (ite (= r4 (_ bv1 1)) zero (ite (= e4 (_ bv1 1)) (bvadd s3 one) s3))))
(push 1)
(assert (= s4 goal))
(check-sat)
(pop 1)

(assert (= s5 (ite (= r5 (_ bv1 1)) zero (ite (= e5 (_ bv1 1)) (bvadd s4 one) s4))))
(push 1)
(assert (= s5 goal))
(check-sat)
(pop 1)

(assert (= s6 (ite (= r6 (_ bv1 1)) zero (ite (= e6 (_ bv1 1)) (bvadd s5 one) s5))))
(push 1)
(assert (= s6 goal))
(check-sat)
(pop 1)

(assert (= s7 (ite (= r7 (_ bv1 1)) zero (ite (= e7 (_ bv1 1)) (bvadd s6 one) s6))))
(push 1)
(assert (= s7 goal))
(check-sat)
(pop 1)