/*@
predicate positive_power_of_2 (integer i) =
i > 0 &&
(i == 1 || ((i & 1) == 0 && positive_power_of_2 (i >> 1)));
lemma positive_power_of_2 (1);
lemma positive_power_of_2 (2);
lemma positive_power_of_2 (4);
lemma !positive_power_of_2 (7);
*/
https://stackoverflow.com/questions/64268418/how-do-i-write-an-is-power-of-2-predicate-in-acsl