Betrachten Sie den folgenden SMT-LIB-Code:

(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|
)))

Versuch, dieses Axiom zu behauptenbar gilt, d. h.,

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

fails (Z3 4.3.2 - Build-Hashcode 47ac5c06333b):

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

Frage 1 Warum hat Z3 nur @ instanziierlimited-G doch keinslimited-F Nochbar (was würde die Behauptung beweisen)?

Frage 2 Kommentieren einer der (nutzlosen) Behauptungenfoo, limited-F oderlimited-G erlaubt Z3, die Behauptung zu beweisen - warum ist das so? (Je nachdem welche kommentiert sind, kann entweder nurbar oderbar undlimited-F werden instanziiert.)

Falls es mit dem beobachteten Verhalten zusammenhängt: Ich möchte @ setzsmt.case_split zu3 (meine Konfiguration folgt der von MSRs @ weggelassene Boogie Tool), aber Z3 gibt mirWARNING: auto configuration (option AUTO_CONFIG) must be disabled to use option CASE_SPLIT=3, 4 or 5, trotz der Tatsache dass(set-option :auto_config false).