z3：一个公式及其否定是不可满足的

Question

一个公式及其否定都是不可满足的。

http://rise4fun.com/Z3/qJHD

(define-fun max1 ((x Int) (y Int)) Int
    (ite (< y x) x y))

(define-fun myMax ((a Int) (b Int)) Int
    (ite (< a b) (- b 1) 0))


(define-const f Bool 
(forall ((a Int) (b Int))
(=> (exists ((i Int)) (and (<= (+ a 1) i) (< i b)))
(= (myMax a b) (max1 a (myMax (+ a 1) b))))))

(assert f)
;(assert (not f))

(check-sat)

有人可以帮我理解吗？我期待他们中的一个人坐下来。 请注意，函数 max1 和 myMax 都已定义。

Answer 1

这是模块中的一个错误，它尝试使用傅里叶 Motzkin 消除来消除量化变量。现在将在 master 分支中检入一个修复程序。