How to check if a variable can be negative? about claripy HOT 5 CLOSED

That looks like it should work, but it seems more accurate to set a = claripy.BVV(0, 32). -1 is negative, after all.

from claripy.

I'm not sure if this approach is correct, but this is how I try to infer ranges of singed variables:
https://github.com/axt/angr-utils/blob/master/angrutils/expr.py

If you check the sat_negative function, what I do is to evaluate if the highest bit of the variable being one could be satisfied.

from claripy.

Can confirm that this approach is correct too. I have no idea what the performance looks like compared to the inequality method, but my suspicion is that z3 is more heavily optimized for inequalities than bit-extraction logic. I really wish we had someone on z3 to whom we can ask these questions, or at least someone with a background in SMT solving...

from claripy.

For bit-vectors, it wouldn't surprise me if the bit-extraction logic was better, in terms of Z3 being able to come up with simpler constraints internally for the actual solve, but I'm definitely as clueless about the inner workings of SMT solvers as the average bear.

from claripy.

I really wish we had someone on z3 to whom we can ask these questions, or at least someone with a background in SMT solving

Just open an issue on Z3Solver GitHub repo!

from claripy.