Z3模式/触发器疑似Bug：版本间结果不一致问询

以下是测试用的SMT-LIB 2代码：

(set-option :print-success false)
(set-info :smt-lib-version 2.6)
(set-option :smt.AUTO_CONFIG false)
(set-option :smt.PHASE_SELECTION 0)
(set-option :smt.RESTART_STRATEGY 0)
(set-option :smt.RESTART_FACTOR 1.5)
(set-option :smt.ARITH.RANDOM_INITIAL_VALUE true)
(set-option :smt.CASE_SPLIT 3)
(set-option :smt.DELAY_UNITS true)
(set-option :NNF.SK_HACK true)
(set-option :smt.MBQI false)
(set-option :smt.QI.EAGER_THRESHOLD 100)
(set-option :smt.BV.REFLECT true)
(set-option :smt.qi.max_multi_patterns 1000)
(set-option :smt.mbqi false)
(set-option :model.compact false)
(set-option :model.v2 true)
(set-option :pp.bv_literals false)
; done setting options

(declare-sort Ref 0)
(declare-sort Field 0)
(declare-sort Mask 0)
(declare-fun select_mask (Mask Ref Field) Real)
(declare-fun zero_mask () Mask)
(declare-sort Heap 0)
(declare-fun length (Heap Ref) Int)
(declare-fun length* (Heap Ref) Int)
(declare-fun select_heap (Heap Ref Field) Ref)
(declare-fun next () Field)
(declare-fun null () Ref)
(declare-fun this () Ref)
(declare-fun mask () Mask)
(declare-fun store_mask (Mask Ref Field Real) Mask)
(assert (forall ( ( ?x0 Mask) ( ?x1 Ref) ( ?x2 Field) ( ?x3 Real)) (! (= (select_mask (store_mask ?x0 ?x1 ?x2 ?x3) ?x1 ?x2)  ?x3) :weight 0)))
(assert (forall ( ( ?x0 Mask) ( ?x1 Ref) ( ?y1 Ref) ( ?x2 Field) ( ?y2 Field) ( ?x3 Real)) (! (=> (or  (not (= ?x1 ?y1)) (not (= ?x2 ?y2))) (= (select_mask (store_mask ?x0 ?x1 ?x2 ?x3) ?y1 ?y2) (select_mask ?x0 ?y1 ?y2))) :weight 0)))
(assert (forall ((o_2 Ref) (f_4 Field) ) (! (= (select_mask zero_mask o_2 f_4) 0.0)
 :pattern ( (select_mask zero_mask o_2 f_4))
)))
(assert (forall ((heap Heap) (this Ref) ) (! (= (length heap this) (length* heap this))
 :pattern ( (length heap this))
)))
(assert (forall ((heap Heap) (this Ref) ) (! (= (length heap this) (ite (= (select_heap heap this next) null) 1 (+ 1 (length* heap (select_heap heap this next)))))
 :pattern ( (length heap this))
)))
(assert (not (= this null)))
(assert (= mask (store_mask zero_mask this next 1.0)))
(declare-fun heap () Heap)
(declare-fun valid-next () Field)
(push 1)
(set-info :boogie-vc-id test2)
(set-option :timeout 0)
(set-option :rlimit 0)
(assert
  (or (<= (select_mask mask this next) 0.0)
      (and (= (select_heap heap this next) this)
           (or (> 1.0 (select_mask zero_mask null valid-next))
               (and (<= 1.0 (select_mask zero_mask null valid-next))
                    (>= (length heap this) (length heap (select_heap heap this next))))))))
(check-sat)
(pop 1)

测试不同Z3版本后发现：

• Z3 4.8.6至4.8.9版本返回unknown
• Z3 4.8.10至4.9.1版本返回unsat

unsat的结果看起来是触发了length相关公理导致的，但如果按顺序处理析取项，Z3应该能找到无需触发length公理的部分模型（即满足(= (select_heap heap this next) this)且(> 1.0 (select_mask zero_mask null valid-next))），并返回unknown。想问这是Z3的Bug，还是Z3根本不保证析取项的处理顺序？

另外，移除代码中的push和pop语句后，所有测试过的Z3版本都返回unsat。

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