## Issue

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)aremeaningful 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 `Real`

s, but it applies to `Int`

s 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.

Answered By – alias

**This Answer collected from stackoverflow, is licensed under cc by-sa 2.5 , cc by-sa 3.0 and cc by-sa 4.0 **