z3 giving a surprising answer

Question

I tried this:

import z3
n,x,y,z = z3.Ints('n x y z')
s = z3.Solver()
s.add(4/n==1/x+1/y+1/z)
s.add(x>0)
s.add(n>0)
s.add(y>0)
s.add(z>0)
s.check()
s.model()

and I get:

[x = 1, n = 2, z = 3, y = 1, div0 = [(1, 1) → 1, (4, 2) → 2, else → 0], mod0 = [(1, 3) → 1, else → 0]]

But 4/2 does not equal 1/1+1/1+1/3.

What am I doing wrong?

Answer 1

You've declared n, x, y, z as integers. So division is done as an integer, giving you 1/1 = 1 and 1/3 = 0; hence satisfying the equality 2=2.

The obvious thing to do is to use Real values for this problem. Changing the declaration to:

n,x,y,z = z3.Reals('n x y z')

produces:

[z = 1, y = 1, n = 4/3, x = 1]

which does satisfy the equation you posed trivially.

In case you actually do want n, x, y, z to be integers; then you should convert them to reals before you divide, like this:

import z3
n,x,y,z = z3.Ints('n x y z')
s = z3.Solver()
s.add(4/z3.ToReal(n)==1/z3.ToReal(x)+1/z3.ToReal(y)+1/z3.ToReal(z))
s.add(x>0)
s.add(n>0)
s.add(y>0)
s.add(z>0)
print(s.check())
print(s.model())

This prints:

sat
[n = 4, x = 3, z = 3, y = 3]

again satisfying your constraints.