Z3Py prove function returns wrong counterexample

I'm trying to using Z3Py prove function, but it seems to return an incorrect counterexample. What is the problem?? (Z3-4.7.1-x86-win, Python-2.7.15)

>>> import z3
>>> A = z3.BitVec('A', 8)
>>> B = z3.BitVec('B', 8)
>>> C = z3.BitVec('C', 8)
>>> z3.prove((A*B)/C == A*(B/C))
counterexample
[A = 67, B = 86, C = 2]
>>> ((67*86)%256)/2
65
>>> (67*(86/2))%256
65

Solution

Let's see what Z3 is doing:

import z3
A = z3.BitVec('A', 8)
B = z3.BitVec('B', 8)
C = z3.BitVec('C', 8)

s = z3.Solver()
s.add((A*B)/C == A*(B/C))
print s.sexpr()

When you run this script, you get:

$ python a.py
(declare-fun C () (_ BitVec 8))
(declare-fun B () (_ BitVec 8))
(declare-fun A () (_ BitVec 8))
(assert (= (bvsdiv (bvmul A B) C) (bvmul A (bvsdiv B C))))

Ah, it's using bvmul and bvsdiv over 8-bit vectors. Turns out multiplication doesn't matter for signed-unsigned, but division does. So, the mapping is actually done to map the result to the range -128 to 127 not to (as I suspect you might've expected) to 0 to 255.

So, if you do the math, the left-side reduces to -63, since the multiplication produces 5762, which gets mapped to -126 in signed-8-bit representation. Right-hand side, however, gets reduced to 65; thus giving you the legitimate counter-example.

To avoid this, you can either use good old Int type; or tell Python to not use signed division by using UDiv, see here: https://z3prover.github.io/api/html/namespacez3py.html#a64c02a843a4ac8781dd666a991797906

If you use UDiv, you can get a better counter-example:

>>> import z3
>>> A = z3.BitVec('A', 8)
>>> B = z3.BitVec('B', 8)
>>> C = z3.BitVec('C', 8)
>>> z3.prove(z3.UDiv(A*B, C) == A*z3.UDiv(B, C))
counterexample
[A = 95, B = 140, C = 41]
>>> ((95*140)%256/41)%256
5
>>> (95*((140/41)%256))%256
29

which is more along what you were expecting I suppose.