Added more functionality to the Z3 bindings for bitvectors. Started incorporating it into the constraint solver.