Why z3 return wrong result

Im learning about z3. Here is the code:

from z3 import *

x = BitVec("x", 32)
solver = Solver()
solver.add(x % 7 == 3)

if solver.check() == sat:
    print(solver.model())

The result i got x = 3205381361. But 3205381361 % 7 = 0. Why this happend, thanks

The main issue here is in overflow. When you say BitVec("x", 32) all that means is you have a string of 32 bits. There's no numerical value assigned to it. That is, you do not specify whether this should be treated as a signed number, or an unsigned number. (Note that this is a design choice, and one that is not the best in my opinion; but this is what z3 does.)

Signed and unsigned arithmetic are different operations on bit-vectors. (Sometimes they coincide, but not always.) Modulus is one of them where there's a difference. When you use %, z3 interprets that as a signed-modulus operation. So, when it prints 3205381361, that is extremely misleading: You need to interpret it as a signed 32-bit number. A signed 32-bit number has the range -(2^-31), 2^31-1. So, the number 3205381361 actually means -1089585935. (Confusing indeed: You can do a simple conversion by wrapping over 2^32, note that 3205381361 - 2^32 = -1089585935).

But now you can do the arithmetic as usual:

>>> (-1089585935) % 7
3

so it satisfies your equation.

How to "fix" this? Well, in a sense there's nothing to fix; just what you wrote didn't mean what you intended. You can use an Int if you want unbounded integers (by declaring x = Int("x")), and thus avoid the whole signed-unsigned business. (But that's not a panacea, because sometimes you really want to work with machine integers, when modeling actual computer programs for instance.)

Or you can say you only meant unsigned numbers by using URem instead:

from z3 import *

x = BitVec("x", 32)
solver = Solver()
solver.add(URem(x,7) == 3)

if solver.check() == sat:
   print(solver.model())

This prints:

[x = 4236335589]

which is probably what you were looking for int he first place.

The function URem is documented here: https://z3prover.github.io/api/html/namespacez3py.html#aec21d4855bd67ee88b5448d68c97a5d4

To sum up, if you're using bit-vectors, you need to be careful about your operations based on whether you want signed or unsigned semantics. See https://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV for a detailed list of operations. (Another common gotcha is comparisons, which also differ with signedness. See, for instance bvsle vs bvule in the link I provided.) z3py, unfortunately, conflates all these and unless you're careful which operation you're doing, you can get surprising (but still correct!) results.

Here's the motto to remember: In SMTLib bitvectors, operations are signed/unsigned, not the values. Which is the exact opposite of what most programming languages do, hence the constant confusion about it.

Actually, this solution is ok. Those are not regular integers, but integers that fit 32 bits (from 0 to 2^32 - 1) and operations made on them are all mod 2**32.

For this equation we look for integer x such that:

x % 7 == 3

which is equivalent to looking for integers x and k such that:

x = 7*k + 3

For x=3205381361 (your solution) we got k=4139312162:

(4139312162*7 + 3)%(2**32) == 3205381361

and hence

3205381361 % 7 == 3