The following "minimal" program, distilled from a much larger program, is expected to yield unsat (and does). However, uncommenting the additional conjunct in the quantifier AX-1 changes the result to unknown (in Z3 4.5.0 x64 on 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)
The quantifier instantiation statistics show that AX-2 is instantiated in both cases, but AX-1 is only instantiated if the additional conjunct is not included. My assumption is that in the latter case, Z3 eliminates the quantifier since the quantified variable doesn't occur in the body.
However, I find it surprising that the version with the additional conjunct - in which Z3 presumably doesn't eliminate the quantifier - yields unknown, since the trigger for the quantifier ((foo j)) should be available.
Question: Is this behaviour expected - and if so, why?
Confirmed as a bug, see Github issue 935.