Meaning of (_ bv0 32), (_ bv1 16) ... in SMT2 benchmarks

Question

I noticed that is some SMT2 benchmarks, notations like (_ bv0 32), (_ bv16 32), ... are used like, for instance, in:

QF_FP/schanda/spark/zeros_consistent_2.smt2

http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_vdir.rev_xstrcoll_mtime.il.wp.smt2

http://rise4fun.com/Z3/e1s

However, this is no reference to such symbols in theories declarations:

http://smtlib.cs.uiowa.edu/theories.shtml

Any comment on that ? What is their meaning ?

Thanks !

Answer 1

(_ bv0 32) is a bitvector constant encoding the value 0 in 32 bits.

You can find the formal description in the Logic definition, under "Bitvector Constants" http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV