support for bitvectors in SMT backend and misc improvements