微小的变化会导致“未知”-与量词预处理相关？

Question

下面的“最小”程序是从一个大得多的程序中提取出来的，预计它会产生unsat (和to )。但是，去掉量词AX-1中的附加连词，结果将更改为unknown (在Windows10上的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 935号。