deposit.smt2

(declare-rel beforeLoop ())
(declare-rel loopCond (Int Int))
(declare-rel loopBody (Int Int))
(declare-rel afterLoop ())
(declare-rel endFunction ())

(declare-var size Int)
(declare-var height Int)

(rule beforeLoop)

(rule (=>
    (and beforeLoop (> size 0) (<= size 4294967296))
    (loopCond size 0)
))  

(rule (=>
    (and (loopCond size height) (< height 32))
    (loopBody size height)
))  

(rule (=>
    (and (loopCond size height) (>= height 32))
    afterLoop
))

(rule (=>
    (and
        (loopBody size height)
        (= (mod size 2) 1)
    )
    endFunction
))  

(rule (=>
    (and
        (loopBody size height)
        (= (mod size 2) 0)
    )
    (loopCond (/ size 2) (+ height 1))
))

(query afterLoop :print-certificate true)