What does this output from Z3 mean?

Take this simple code:

from z3 import *
a, b, c, d =  Ints('a b c d')
s = Solver()
s.add(a>0)
s.add(b>1)
s.add(c>0)
s.add(d>0)
s.add(a*b - c*d< 20)
s.add(d/a+b/d > 2)
s.add((a*c)/(b*d) > 3)
s.check()
s.model()

This gives me:

[d = 8,
 a = 4,
 c = 64,
 b = 8,
 div0 = [(8, 4) -> 2, (256, 64) -> 4, else -> 1],
 mod0 = [else -> 0]]

This is in version 4.8.12.

What do the div0 and mod0 lines mean?

Solution

Note that a straightforward invocation of z3 on your program does not produce this output for me. I get:

[b = 2, a = 1, c = 9, d = 1]

Perhaps you're passing some extra arguments to z3 that changes the behavior?

Nonetheless, what mod0 and div0 are telling you is how z3 chose to define division by 0 when it constructed the model. For instance:

div0 = [(8, 4) -> 2, (256, 64) -> 4, else -> 1],

means z3 relied on the facts that 8/4=2, 256/64=4, and all other divisions result in 1; regardless of the arguments. You might find this odd, but it circumvents the age-old issue of giving a meaning to division-by 0 for integers. In SMTLib, this value remains undefined, meaning the solver is free to pick any value it wants, and it's telling you that it picked 1 for this purpose. Of course, for your problem, it did not matter at all, as the model it found did not make use of this fact.

In general, you can ignore the div0/mod0 assignments, unless z3 gives you a model that actually uses division by 0. (That is, for your program, you can just ignore it.) Here's an example where you cannot:

from z3 import *
a = Int('a')
s = Solver()
s.add(a > 2)
s.add(a / 0 == 5)
print(s.check())
print(s.model())

This program prints:

sat
[a = 3]

and the reason is because z3 is free to pick 3 / 0 to be 5 because of the underspecification. This is explained in http://smtlib.cs.uiowa.edu/theories-Reals.shtml:

Since in SMT-LIB logic all function symbols are interpreted as total
functions, terms of the form (/ t 0) are meaningful in every
instance of Reals. However, the declaration imposes no constraints
on their value. This means in particular that

for every instance theory T and

for every value v (as defined in the :values attribute) and closed term t of sort Real, there is a model of T that satisfies (= v (/ t 0)).

(This text is about Reals, but it applies to Ints as well.)

Long story short: If you get a model that does something funky with division/modulus by 0, then you need to pay attention to how z3 chose to define div0 and mod0 in the model. Otherwise, you can ignore these assignments.