The title says it all. I try to present -1 as the following: (_ bv-1 32), and z3 complains.
How do I present constraint such as 3x - 5y <= 10 in bit vector? For some reason, I do not want to use linear integer.
This is usually done via two's complement encoding. The short version is,
-x = flip(x) + 1
where flip(x) simply flips all the bits in x.