Clearing up some confusion for going from bv to ints. Judging by the problems with the Z3 api this doesn't seem like a good route to go.