[SMT-LIB] new bitvector theories/logics

Domagoj Babic babic.domagoj at gmail.com
Thu May 10 23:02:05 EDT 2007


Hi Clark,

Thx for accepting my suggestion about naming comparison operators bv(u|s)xx,
that's much more consistent.

Question: Are you also planning to rename div & rem operators:

bvdiv -> bvudiv
bvsdiv stays the same
bvrem -> bvurem
bvsrem stays the same

These additional renamings would make the theory more consistent.

Domagoj Babic


More information about the SMT-LIB mailing list