1    (bvsmod s t) abbreviates
2      (let (?msb_s (extract[|m-1|:|m-1|] s))
3      (let (?msb_t (extract[|m-1|:|m-1|] t))
4      (ite (and (= ?msb_s bit0) (= ?msb_t bit0))
5           (bvurem s t)
6      (ite (and (= ?msb_s bit1) (= ?msb_t bit0))
7           (bvadd (bvneg (bvurem (bvneg s) t)) t)
8      (ite (and (= ?msb_s bit0) (= ?msb_t bit1))
9           (bvadd (bvurem s (bvneg t)) t)
10           (bvneg (bvurem (bvneg s) (bvneg t))))))))
11