相关疑难解决方法(0)

据我所知，z3 一般无法验证归纳证明。但我很好奇是否有一种方法可以让它检查一些简单的事情，例如：

; returns the same input list after iterating through each element
(declare-fun iterate ((List Int)) (List Int))

(declare-const l (List Int))

(assert (forall ((l (List Int)))
  (ite (= l nil)
    (= (iterate l) nil)
    (= (iterate l) (insert (head l) (iterate (tail l))))
  )
))

(assert (not (= l (iterate l))))
(check-sat)

现在它只是在我的机器上永远循环。