; define predicate for initial state: program counter is at 1
(define-fun initial ((pc Int) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool
  (= pc 1)
)
; define predicate to capture all possible transitions
(define-fun trans ((pc0 Int) (x0 (_ BitVec 32)) (y0 (_ BitVec 32)) (pc1 Int) (x1 (_ BitVec 32)) (y1 (_ BitVec 32))) Bool
  (or
    (and (= pc0 1) (= pc1 2))
    (and (= pc0 2) (= pc1 3) (= x1 #x00000001))
    (and (= pc0 3) (= pc1 4) (= x0 x1))
    (and (= pc0 4) (= pc1 5) (bvslt y0 #x00000064) (= x0 x1) (= y0 y1))
    (and (= pc0 5) (= pc1 6) (= y1 (bvadd y0 x0)) (= x0 x1))
    (and (= pc0 4) (= pc1 7) (not (bvslt y0 #x00000064)) (= x0 x1) (= y0 y1))
    (and (= pc0 6) (= pc1 4) (= x0 x1) (= y0 y1))
  )
)
; define predicate to capture violation: program counter is at 5 and addition overflows
(define-fun overflow ((pc Int) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool
  (and (= pc 5) (bvslt (bvadd y x) y))
)

; declare variables for 6 states
(declare-const pc0 Int)
(declare-const x0 (_ BitVec 32))
(declare-const y0 (_ BitVec 32))
(declare-const pc1 Int)
(declare-const x1 (_ BitVec 32))
(declare-const y1 (_ BitVec 32))
(declare-const pc2 Int)
(declare-const x2 (_ BitVec 32))
(declare-const y2 (_ BitVec 32))
(declare-const pc3 Int)
(declare-const x3 (_ BitVec 32))
(declare-const y3 (_ BitVec 32))
(declare-const pc4 Int)
(declare-const x4 (_ BitVec 32))
(declare-const y4 (_ BitVec 32))
(declare-const pc5 Int)
(declare-const x5 (_ BitVec 32))
(declare-const y5 (_ BitVec 32))
(declare-const r (_ BitVec 32))

; assert that (pc0,x0,y0) is initial state
(assert (initial pc0 x0 y0))
; assert that there are transitions from (pc0,x0,y0) to (pc5,x5,y5)
(assert (trans pc0 x0 y0 pc1 x1 y1))
(assert (trans pc1 x1 y1 pc2 x2 y2))
(assert (trans pc2 x2 y2 pc3 x3 y3))
(assert (trans pc3 x3 y3 pc4 x4 y4))
(assert (trans pc4 x4 y4 pc5 x5 y5))
; assert that there be a violation in one of the states
(assert
  (or
    (overflow pc0 x0 y0)
    (overflow pc1 x1 y1)
    (overflow pc2 x2 y2)
    (overflow pc3 x3 y3)
    (overflow pc4 x4 y4)
    (overflow pc5 x5 y5)
  )
)
(check-sat)
(get-model)