[SMT-LIB] BVDIV on Bitvector (SMTLIB2) ?

[Jun Koi]

hi,

in SMTLIB2, while we have most basic bitvector arithmetics, it seems
there is no support for bvdiv?
this is confirmed on Z3, which is fully compatible with SMTLIB2 from version 3.0

so do i need to implement bvdiv myself? if so, any body did that
before? any code to share, please?

also, where i can find information on QF_BV of SMTLIB2? for example,
to understand the syntax of bvxor, bvnot, ...etc

many thanks,
Jun