Z3 返回未知，用于涉及整数除法的简单查询

Question

下面是一个简单的 Z3 查询，涉及整数除法（即非线性运算）：

(declare-const a01 Int)
(declare-const a02 Int)
(assert(or (= (/ a01 a02) 2) (= (/ a02 a01) 2)))
(assert( > a01 0))
(assert( > a02 0))
(check-sat)

Z3 在尝试解决此查询时返回未知。我知道非线性整数算术是不可判定的，但我仍然希望 Z3 在实践中不那么脆弱。

如果我缺少一些可以为 Z3 设置的明显参数以帮助它解决此类查询，请告诉我。我正在使用Z3 4.4.1，我也尝试了rise4fun上的版本。谢谢！

Answer 1

使用 div 而不是 / 。

(declare-const a01 Int)
(declare-const a02 Int)
(assert(or (= (div a01 a02) 2) (= (div a02 a01) 2)))
(assert( > a01 0))
(assert( > a02 0))
(check-sat)