Add bool_to_Z

This MR adds bool_to_Z which has been used as Z_of_bool in both RefinedC and RustBelt. There is not much theory for it as most of the time one can reason about it by computation.