Z3 does not consider empty models. This is a standard assumption in first-order logic. For more details search "first-order logic empty models", you will get many links explaining the motivation for this convention. The wikipedia page for first-order logic has a brief description (section "Empty domains").
Moreover, we should not confuse []
with the empty model. It is just saying that for satisfying the input formulas, Z3 does not need to assign an interpretation to any uninterpreted symbol in the input formula. Z3 displays only the interpretation of symbols that are needed to satisfy the formula. For example, the formula [∃v : v = v]
does not contain any uninterpreted symbol, then Z3 just displays the empty assignment []
.