  There is increasing interest in applying verification tools to programs that
have bitvector operations. SMT solvers, which serve as a foundation for these
tools, have thus increased support for bitvector reasoning through bit-blasting
and linear arithmetic approximations. Still, verification tools are limited on
termination and LTL verification of bitvector programs. In this work, we show
that similar linear arithmetic approximation of bitvector operations can be
done at the source level through transformations. Specifically, we introduce
new paths that over-approximate bitvector operations with linear
conditions/constraints, increasing branching but allowing us to better exploit
the well-developed integer reasoning and interpolation of verification tools.
We present two sets of rules, namely rewriting rules and weakening rules, that
can be implemented as bitwise branching of program transformation, the
branching path can facilitate verification tools widen verification tasks over
bitvector programs. Our experiment shows this exploitation of integer reasoning
and interpolation enables competitive termination verification of bitvector
programs and leads to the first effective technique for LTL verification of
bitvector programs.
