[SMT-LIB] BitVectors32

[Christoph M. Wintersteiger]

Hi list members!

I have the following problem: The BitVectors32 theory defines these
basic functions:

- Constant symbols bv0 and bv1 of sort BitVec[32]
   [[bv0]] := \lambda x : [0...32). 0
   [[bv1]] := \lambda x : [0...32). if x = 0 then 1 else 0

However, some of the benchmarks seem to use this as if there was a
function bvX, e.g. QF_UFBV32/crafted/bb.smt wants bv7.

>From the declaration of bv0/bv1 I guess this used to be a definition of
the form bvX anyways. So: should I implement this as bv0/1 and wait for
the benchmark files to be fixed, or should I implement bvX and ignore
the theory definition? 

It would also be nice to know what does functions are supposed to do: Is
this kind of an ==0 as in C? or is this supposed to load a bitvector
with the binary representation of X?

Thanks,
Christoph