微小的变化导致"unknown" - 与量词预处理有关？

Question

下面的"最小"程序，是从一个大得多的程序中提炼出来的，预计会产生 unsat(并且确实产生了)。但是，取消限定词AX-1中附加的连接词的注释会将结果更改为unknown(在Windows 10的Z3 4.5.0 x64中)。

(set-option :auto_config false)
(set-option :smt.mbqi false)
(declare-fun foo (Int) Bool)
(declare-const k Real)
(assert (forall ((i Int)) (!
  (and
    (< 0.0 k)
    ; (implies (<= 0 i) (< 0.0 k)) ;;; ---- uncomment this line ----
  )
  :pattern ((foo i))
  :qid |AX-1|)))
(assert (forall ((i Int)) (!
  (foo i)
  :pattern ((foo i))
  :qid |AX-2|)))
(declare-const j Int)
(assert (< j 0))
; (push) ;;; doesn't make a difference
(assert (not
  (ite
    (foo j)
    (< 0.0 k)
    false)))
; (set-option :smt.qi.profile true)
(check-sat)
; (get-info :all-statistics)
; (pop)

量词实例化统计表明，AX-2在两种情况下都被实例化，而AX-1只有在附加连词不包括时才被实例化。我的假设是，在后一种情况下，Z3消除了量词，因为量化变量没有出现在主体中。

然而，我发现带有附加连接词的版本(其中Z3可能没有消除量词)产生unknown，因为量词的触发器((foo j))应该是可用的。

问题:这种行为是预期的吗?如果是，为什么?

Answer 1

确认为bug，参见Github issue 935