deposit_loop_mod_32.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 4294967295))
    (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)

Replaced mod 2 by slack variable. Still no progress.

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


(declare-var q1 Int)
(declare-var q2 Int)

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

(rule beforeLoop)

(rule
 (=>
  (and beforeLoop (> size 0) (<= size 4294967295))
  (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)
   (= (+ (* 2 q1) 1) size)
   )
  endFunction
  ))

(rule
 (=>
  (and
   (loopBody size height)
   (= (* 2 q2) size)
   )
  (loopCond (/ size 2) (+ height 1))
  ))

(query afterLoop :print-certificate true)