How can I prove this C is_power_of_2 function using Frama-C?

Question

In a previous question I was asking for help writing a predicate to find if a number is a power of 2. This was a prelude to trying to prove the following C function:

static inline bool
is_power_of_2 (unsigned long v)
{
  return v && ((v & (v - 1)) == 0);
}

(This "trick" comes from here). Using the previous predicate I tried:

/*@
  ensures positive_power_of_2 (v) <==> \result == \true;
 */

but none of the various SMT solvers I'm using (alt-ergo, z3, gappa, cvc4) seem able to prove this.