(in a0 a1 a2 a3 a4 a5 a6 a7 b0 b1 b2 b3 b4 b5 b6 b7)
(out res ca0 ca1 ca2 ca3 ca4 ca5 ca6 ca7 cb0 cb1 cb2 cb3 cb4 cb5 cb6 cb7)
(verify res b0 b1 b2 b3 b4 b5 b6 b7)
(program
(= ca0 (* a0 (+ a0 250)))
(= ca1 (* a1 (+ a1 250)))
(= ca2 (* a2 (+ a2 250)))
(= ca3 (* a3 (+ a3 250)))
(= ca4 (* a4 (+ a4 250)))
(= ca5 (* a5 (+ a5 250)))
(= ca6 (* a6 (+ a6 250)))
(= ca7 (* a7 (+ a7 250)))
(= cb0 (* b0 (+ b0 250)))
(= cb1 (* b1 (+ b1 250)))
(= cb2 (* b2 (+ b2 250)))
(= cb3 (* b3 (+ b3 250)))
(= cb4 (* b4 (+ b4 250)))
(= cb5 (* b5 (+ b5 250)))
(= cb6 (* b6 (+ b6 250)))
(= cb7 (* b7 (+ b7 250)))
(= diff0 (* (+ a0 (* 250 b0)) (+ a0 (* 250 b0))))
(= diff1 (* (+ a1 (* 250 b1)) (+ a1 (* 250 b1))))
(= diff2 (* (+ a2 (* 250 b2)) (+ a2 (* 250 b2))))
(= diff3 (* (+ a3 (* 250 b3)) (+ a3 (* 250 b3))))
(= diff4 (* (+ a4 (* 250 b4)) (+ a4 (* 250 b4))))
(= diff5 (* (+ a5 (* 250 b5)) (+ a5 (* 250 b5))))
(= diff6 (* (+ a6 (* 250 b6)) (+ a6 (* 250 b6))))
(= diff7 (* (+ a7 (* 250 b7)) (+ a7 (* 250 b7))))
(= acc7 (* 1 diff7))
(= acc_i6 (* acc7 diff6))
(= acc6 (* 1 (+ acc7 diff6 (* 250 acc_i6))))
(= acc_i5 (* acc6 diff5))
(= acc5 (* 1 (+ acc6 diff5 (* 250 acc_i5))))
(= acc_i4 (* acc5 diff4))
(= acc4 (* 1 (+ acc5 diff4 (* 250 acc_i4))))
(= acc_i3 (* acc4 diff3))
(= acc3 (* 1 (+ acc4 diff3 (* 250 acc_i3))))
(= acc_i2 (* acc3 diff2))
(= acc2 (* 1 (+ acc3 diff2 (* 250 acc_i2))))
(= acc_i1 (* acc2 diff1))
(= acc1 (* 1 (+ acc2 diff1 (* 250 acc_i1))))
(= acc_i0 (* acc1 diff0))
(= acc0 (* 1 (+ acc1 diff0 (* 250 acc_i0))))
(= fdiff7 (* 1 acc7))
(= fdiff6 (* (+ acc7 (* 250 acc6)) (+ acc7 (* 250 acc6))))
(= fdiff5 (* (+ acc6 (* 250 acc5)) (+ acc6 (* 250 acc5))))
(= fdiff4 (* (+ acc5 (* 250 acc4)) (+ acc5 (* 250 acc4))))
(= fdiff3 (* (+ acc4 (* 250 acc3)) (+ acc4 (* 250 acc3))))
(= fdiff2 (* (+ acc3 (* 250 acc2)) (+ acc3 (* 250 acc2))))
(= fdiff1 (* (+ acc2 (* 250 acc1)) (+ acc2 (* 250 acc1))))
(= fdiff0 (* (+ acc1 (* 250 acc0)) (+ acc1 (* 250 acc0))))
(= chka0 (* a0 fdiff0))
(= chka1 (* a1 fdiff1))
(= chka2 (* a2 fdiff2))
(= chka3 (* a3 fdiff3))
(= chka4 (* a4 fdiff4))
(= chka5 (* a5 fdiff5))
(= chka6 (* a6 fdiff6))
(= chka7 (* a7 fdiff7))
(= res7 (* 1 chka7))
(= res_i6 (* res7 chka6))
(= res6 (* 1 (+ res7 chka6 (* 250 res_i6))))
(= res_i5 (* res6 chka5))
(= res5 (* 1 (+ res6 chka5 (* 250 res_i5))))
(= res_i4 (* res5 chka4))
(= res4 (* 1 (+ res5 chka4 (* 250 res_i4))))
(= res_i3 (* res4 chka3))
(= res3 (* 1 (+ res4 chka3 (* 250 res_i3))))
(= res_i2 (* res3 chka2))
(= res2 (* 1 (+ res3 chka2 (* 250 res_i2))))
(= res_i1 (* res2 chka1))
(= res1 (* 1 (+ res2 chka1 (* 250 res_i1))))
(= res_i (* res1 chka0))
(= res (* 1 (+ res1 chka0 (* 250 res_i)))))