采取这个简单的代码：
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()
这给了我：
[d = 8,
a = 4,
c = 64,
b = 8,
div0 = [(8, 4) -> 2, (256, 64) -> 4, else -> 1],
mod0 = [else -> 0]]
这是版本 4.8.12。
div0 和 mod0 行是什么意思？
请注意，在程序中直接调用 z3 不会为我产生此输出。我得到：
[b = 2, a = 1, c = 9, d = 1]
也许您正在向 z3 传递一些额外的参数来改变行为？
尽管如此，mod0和div0告诉你的是 z3 在构建模型时如何选择定义除以 0。例如：
div0 = [(8, 4) -> 2, (256, 64) -> 4, else -> 1],
8/4=2表示 z3 依赖于、256/64=4以及所有其他除法导致 的事实1；无论争论如何。您可能会觉得这很奇怪，但它避免了为整数除以 0 赋予含义的古老问题。在 SMTLib 中，该值保持未定义状态，这意味着求解器可以自由选择它想要的任何值，并且它告诉您它是1为此目的而选择的。当然，对于你的问题来说，这根本不重要，因为它发现的模型没有利用这个事实。
一般来说，您可以忽略div0/mod0赋值，除非 z3 为您提供了一个实际使用除以 的模型0。（也就是说，对于您的程序，您可以忽略它。）这是一个您不能忽略的示例：
[b = 2, a = 1, c = 9, d = 1]
该程序打印：
sat
[a = 3]
原因是z3可以自由选择，3 / 0因为5规格不足。这在http://smtlib.cs.uiowa.edu/theories-Reals.shtml中有解释：
由于在 SMT-LIB 逻辑中，所有函数符号都被解释为总
函数，因此 (/ t 0) 形式的项在实数的每个实例中都有
意义 。然而，该声明
对其价值没有施加任何限制。这特别意味着
- 对于每个实例理论 T 和
- 对于每个值 v（如 :values 属性中定义）和实数类封闭项 t，存在满足 (= v (/ t 0)) 的 T 模型。
（本文是关于s 的，但它也Real适用于s。）Int
长话短说：如果你得到一个模型，它用 0 做除法/模数，那么你需要注意 z3 如何选择在模型中定义div0和。mod0否则，您可以忽略这些分配。