What is the reason for the warning in Z3: "could not find a template for the quantifier (quantifier ID: k! 18)"

Question

I find the problem as shown in the following simple SMT-LIB program.

SMT-LIB Code:

(declare-fun isDigit (Int) Bool) (assert (forall ((x Int)) (=> (isDigit x) (and (>= x 0) (< x 10)) ) ) ) (assert (forall ((x Int)) (=> (and (>= x 12) (< x 15)) (exists ((y Int)) (and (>= y 1) (< y 6) (isHost (- xy)) ) ) ) ) ) (check-sat) (get-model) 

This gives the following warning:

 WARNING: failed to find a pattern for quantifier (quantifier id: k!18) sat ........ ........ 

I'm curious about the warning. I know something is missing, but I do not understand. Can someone help me on this?

Answer 1

Z3 uses different quantifier processing mechanisms (see Z3 manual ). One of these engines is based on pattern matching (E-Matching). Z3 tries to derive patterns for each quantitative formula. If he cannot find him, he will give a warning message. The user can also provide patterns for each quantifier. The manual shows how to do this. Id k!18 is the default identifier created by Z3. It is based on the line number (line 18 in your case). You can also provide your identifiers for quantifiers. The warning simply tells users that the E-matching mechanism will not be able to process the specified quantifier.