Geringfügige Änderung führt zu "unbekannt" - bezogen auf Quantifizierer-Vorverarbeitung?

Question

Das folgende "minimale" Programm, destilliert von einem viel größeren Programm, wird erwartet,unsat zu ergeben (und tut). Das Auskommentieren des zusätzlichen Konjunktons im Quantifizierer AX-1 ändert jedoch das Ergebnis in unknown (in Z3 4.5.0 x64 unter Windows 10).

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

Die quantifier Instanziierung Statistiken zeigen, dass AX-2 in beiden Fällen instanziert wird, aber AX-1 wird nur instanziiert, wenn die zusätzliche conjunct ist nicht enthalten. Meine Annahme ist, dass im letzten Fall Z3 den Quantifizierer eliminiert, da die quantifizierte Variable nicht im Körper vorkommt.

Allerdings finde ich es überraschend, dass die Version mit der zusätzlichen conjunct - bei dem Z3 vermutlich nicht die quantifier beseitigen - Erträge unknown, da der Auslöser für die quantifier ((foo j)) sollte vorhanden sein.

Frage: Wird dieses Verhalten erwartet - und wenn ja, warum?

Answer 1

Bestätigt als Fehler, siehe Github issue 935.