z3：什麼可能是超時的原因

Question

z3中以下程序超時的原因可能是什麼？

http://rise4fun.com/Z3/pbEOw

(declare-const a Int) 
(declare-const a2 Int) 
(declare-const b Int) 
(assert (> b 0)) 
(assert (>= a a2)) 
(assert (< (div a b) (div a2 b))) 
(check-sat) 
(get-model) 

Answer 1

除法運算符的第二個操作數是一個變量。 這使得約束是非線性的，並且尋求令人滿意的非線性約束解釋通常不會終止（這也是一般不可判定的）。