When set (the default) itauto is a complete but slow solver performing
backtracking.
When unset, itauto does not backtrack. This is done by ignoring the
sub-formulae that are so-called "implication clauses" and cannot be
turned into classic clauses.

Lia.v unset this option and defines a lia tactic:
Ltac lia := zify ; itauto (xlia zchecker).