Attribute Macro bitwise_proof
#[bitwise_proof]Expand description
This attribute indicates that the function need to be proved in “bitwise” mode, which means that Creusot will use the bitvector theory of SMT solvers.
#[bitwise_proof]This attribute indicates that the function need to be proved in “bitwise” mode, which means that Creusot will use the bitvector theory of SMT solvers.