[SMT-LIB] BitVectors32

[Domagoj Babic]

Hi,

bv(0|1) are in the logic files, but where are bv<op>, op=(add|sub|...)
specified?

Also, I'm wondering about a couple of other related things:

1) My application requires a full set of integer operators (sdiv,
udiv, urem, mul...).
If I generate benchmarks in BitVec[32] format am I supposed to define the
operators, or I can just use bvsdiv, for instance?

2) Are theorem provers required to interpret all the operators? If not, how
do you compare (during the competition) theorem provers that handle
expensive operators as UIFs and those that handle them precisely?

Thx,
   Domagoj