Module `mach.bv` should provide purely bitvector-based pre-conditions
As a follow-up of issue #340 (closed), this issue calls for improvement in the pre-conditions of the function of the modules mach.bv.*
. Usage of functions to_int
and to_uint
are not convenient for provers with built-in BV support, hence bit-vector style formulas should be used instead. The book Hacker's Delight should provide good solutions.