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

Jun Koi junkoi2004 at gmail.com
Tue Aug 23 22:29:06 EDT 2011


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


More information about the SMT-LIB mailing list