Рассмотрим следующий код SMT-LIB:

(set-option :auto_config false)
(set-option :smt.mbqi false)
; (set-option :smt.case_split 3)
(set-option :smt.qi.profile true)

(declare-const x Int)

(declare-fun trigF (Int Int Int) Bool)
(declare-fun trigF$ (Int Int Int) Bool)
(declare-fun trigG (Int) Bool)
(declare-fun trigG$ (Int) Bool)

; Essentially noise
(declare-const y Int)
(assert (!
  (not (= x y))
  :named foo
))

; Essentially noise
(assert (forall ((x Int) (y Int) (z Int)) (!
  (= (trigF$ x y z) (trigF x y z))
  :pattern ((trigF x y z))
  :qid |limited-F|
)))

; Essentially noise
(assert (forall ((x Int)) (!
  (= (trigG$ x) (trigG x))
  :pattern ((trigG x))
  :qid |limited-G|
)))

; This assumption is relevant
(assert (forall ((a Int) (b Int) (c Int)) (!
  (and
    (trigG a)
    (trigF a b c))
  :pattern ((trigF a b c))
  :qid |bar|
)))

Пытаясь утверждать эту аксиомуbar держит, т.е.

(push)
(assert (not (forall ((a Int) (b Int) (c Int))
  (and
    (trigG a)
    (trigF a b c)))))
(check-sat)
(pop)

не удается (Z3 4.3.2 - сборка хэш-кода 47ac5c06333b):

unknown
[quantifier_instances]  limited-G :      1 :   0 : 1

Вопрос 1: Почему Z3 только инстанцируетlimited-G но ниlimited-F ниbar (что бы доказать утверждение)?

Вопрос 2: Комментирование любого из (бесполезных) утвержденийfoo, limited-F или жеlimited-G позволяет Z3 доказать утверждение - почему это так? (В зависимости от того, какие комментарииbar или жеbar а такжеlimited-F создаются.)

В случае, если это связано с наблюдаемым поведением: я хотел бы установитьsmt.case_split в3 (моя конфигурация соответствует опущенной MSRбуги-вуги инструмент), но Z3 дает мнеWARNING: auto configuration (option AUTO_CONFIG) must be disabled to use option CASE_SPLIT=3, 4 or 5, несмотря на то, что(set-option :auto_config false).