(define v1::(bitvector 32))
(define v2::(bitvector 32))
(define v3::(bitvector 32))

(assert (not(= v1 0x00000000)))
(assert (= v3 (bv-urem v2 v1)))
(assert (not (bv-lt v3 v1)))

(check)