Trying to understand reason for "unknown" because of "incomplete quantifiers"

[maggesi]

Hello,

I have two scripts (they intend to prove a property of an abstract system of foraging ants, but this is irrelevant for my question).

• The first script is handled as I expect by Z3 (returns unsat).
  ant1.txt
• The second script returns "unknown" with the reason "incomplete quantifiers".
  ant2.txt

This surprises me, because both problems should be solved in the same logic (the first models a system with 1 ant, the second a system with 2 ants).

Thus, my question is: how can I understand why Z3 handles the first script but not the second one?

Thanks, in advance!

[maggesi]

Related question: how do I know which logic is automatically chosen by Z3?
Something like (get-info :used-logic) (which do not exists...)