Z3多模型搜索：非增量方式有效，增量方式超时无结果

在使用Z3求解区间[0, 1]内多项式零点时，出现了与预期不符的求解表现：

初始问题定义与求解结果 #

问题的SMT-LIB代码如下：

(declare-fun perr () Real)
(assert
 (let (($x10 (<= perr 1.0)))
 (and (<= 0.0 perr) $x10)))
(assert
 (let ((?x64 (^ perr 8.0)))
 (let ((?x65 (* (- 9.0) ?x64)))
 (let ((?x59 (^ perr 6.0)))
 (let ((?x60 (* (- 4032.0) ?x59)))
 (let ((?x55 (^ perr 5.0)))
 (let ((?x56 (* 8064.0 ?x55)))
 (let ((?x51 (^ perr 4.0)))
 (let ((?x52 (* (- 10080.0) ?x51)))
 (let ((?x46 (^ perr 3.0)))
 (let ((?x47 (* 8064.0 ?x46)))
 (let ((?x41 (^ perr 2.0)))
 (let ((?x42 (* (- 4032.0) ?x41)))
 (let ((?x69 (* 1152.0 perr)))
 (let ((?x33 (^ perr 7.0)))
 (let ((?x34 (* 1152.0 ?x33)))
 (= (+ ?x34 ?x69 ?x42 ?x47 ?x52 ?x56 ?x60 ?x65) 144.0))))))))))))))))))
(check-sat)
(get-model)

执行后得到模型：

(
    (define-fun perr () Real
        (root-obj (+ (^ x 8) (* (- 128) (^ x 7)) (* 448 (^ x 6)) (* (- 896) (^ x 5)) (* 1120 (^ x 4)) (* (- 896) (^ x 3)) (* 448 (^ x 2)) (* (- 128) x) 16) 1))
)

非增量方式查询其他解 #

采用非增量方式，添加约束排除已得解，代码如下：

(declare-fun perr () Real)
(assert
 (let (($x10 (<= perr 1.0)))
 (and (<= 0.0 perr) $x10)))
(assert
 (let ((?x64 (^ perr 8.0)))
 (let ((?x65 (* (- 9.0) ?x64)))
 (let ((?x59 (^ perr 6.0)))
 (let ((?x60 (* (- 4032.0) ?x59)))
 (let ((?x55 (^ perr 5.0)))
 (let ((?x56 (* 8064.0 ?x55)))
 (let ((?x51 (^ perr 4.0)))
 (let ((?x52 (* (- 10080.0) ?x51)))
 (let ((?x46 (^ perr 3.0)))
 (let ((?x47 (* 8064.0 ?x46)))
 (let ((?x41 (^ perr 2.0)))
 (let ((?x42 (* (- 4032.0) ?x41)))
 (let ((?x69 (* 1152.0 perr)))
 (let ((?x33 (^ perr 7.0)))
 (let ((?x34 (* 1152.0 ?x33)))
 (= (+ ?x34 ?x69 ?x42 ?x47 ?x52 ?x56 ?x60 ?x65) 144.0))))))))))))))))))
(assert
 (not (= perr (root-obj (+ (^ x 8) (* (- 128) (^ x 7)) (* 448 (^ x 6)) (* (- 896) (^ x 5)) (* 1120 (^ x 4)) (* (- 896) (^ x 3)) (* 448 (^ x 2)) (* (- 128) x) 16) 1))))
(check-sat)

执行后返回unsat，说明区间内无其他解。

增量方式查询的异常表现 #

采用增量方式，先求解初始问题，再添加排除约束查询，代码如下：

(declare-fun perr () Real)
(assert
 (let (($x10 (<= perr 1.0)))
 (and (<= 0.0 perr) $x10)))
(assert
 (let ((?x64 (^ perr 8.0)))
 (let ((?x65 (* (- 9.0) ?x64)))
 (let ((?x59 (^ perr 6.0)))
 (let ((?x60 (* (- 4032.0) ?x59)))
 (let ((?x55 (^ perr 5.0)))
 (let ((?x56 (* 8064.0 ?x55)))
 (let ((?x51 (^ perr 4.0)))
 (let ((?x52 (* (- 10080.0) ?x51)))
 (let ((?x46 (^ perr 3.0)))
 (let ((?x47 (* 8064.0 ?x46)))
 (let ((?x41 (^ perr 2.0)))
 (let ((?x42 (* (- 4032.0) ?x41)))
 (let ((?x69 (* 1152.0 perr)))
 (let ((?x33 (^ perr 7.0)))
 (let ((?x34 (* 1152.0 ?x33)))
 (= (+ ?x34 ?x69 ?x42 ?x47 ?x52 ?x56 ?x60 ?x65) 144.0))))))))))))))))))
(check-sat)
(get-model)
(assert
 (not (= perr (root-obj (+ (^ x 8) (* (- 128) (^ x 7)) (* 448 (^ x 6)) (* (- 896) (^ x 5)) (* 1120 (^ x 4)) (* (- 896) (^ x 3)) (* 448 (^ x 2)) (* (- 128) x) 16) 1))))
(check-sat)

此时求解器无法返回unsat，出现超时。

疑问 #

推测可能是Z3在增量过程中生成的子句干扰了后续求解，但通常增量求解的表现应优于非增量方式，为何此处出现相反结果？

内容的提问来源于stack exchange，提问作者user3760874