`itauto lia` fails with "grounding a non evar-free term" anomaly

Require Import Lia ZArith.
Require Import Cdcl.Itauto.
Open Scope Z_scope.

Axiom width: Z.
Axiom word: Type.
Axiom w2z : word -> Z.
Axiom z2w : Z -> word.

Goal forall (left right : word) (xs : list word) (Lxs : nat)
    (v : nat) (x : list word) (x1 x2 x3 : word)
    (Lx : nat) (q0 q r r0 : Z),
  (w2z right - w2z left) mod 2 ^ width = 8 * Z.of_nat Lxs ->
  (w2z x2 - w2z x1) mod 2 ^ width = 8 * Z.of_nat Lx ->
  (w2z x2 - w2z x1) mod 2 ^ width <> 0 ->
  (forall default, w2z
    (if w2z (List.hd default (List.skipn (Z.to_nat q0) x)) <? w2z x3
     then z2w 1
     else z2w 0) <> 0) ->
  0 <= 8 * Z.of_nat Lx < 2 ^ width ->
  Z.of_nat Lx = Z.of_nat v ->
  0 <= Z.of_nat Lxs ->
  0 <= Z.of_nat Lx ->
  0 <= Z.of_nat v ->
  (2 ^ 4 <> 0 -> (w2z x2 - w2z x1) mod 2 ^ width = 2 ^ 4 * q + r) ->
  (0 < 2 ^ 4 -> 0 <= r < 2 ^ 4) ->
  (2 ^ 4 < 0 -> 2 ^ 4 < r <= 0) ->
  (8 mod 2 ^ width <> 0 ->
   ((w2z x1 +
     Z.shiftl
       (Z.shiftr ((w2z x2 - w2z x1) mod 2 ^ width) (4 mod 2 ^ width)
        mod 2 ^ width) (3 mod 2 ^ width) mod 2 ^ width) mod
    2 ^ width - w2z x1) mod 2 ^ width = 8 mod 2 ^ width * q0 + r0) ->
  (0 < 8 mod 2 ^ width -> 0 <= r0 < 8 mod 2 ^ width) ->
  (8 mod 2 ^ width < 0 -> 8 mod 2 ^ width < r0 <= 0) ->
  0 <= -8 * q + 8 * Z.of_nat Lx - 8 < 2 ^ width.
Proof.
  intros.
  evar (default: word).
  specialize (H2 default).
  subst default.

  (* lia succeeds fast no matter whether I clear H2 or not
  clear H2.
  lia.
  *)

  (* clear H2. *)
  itauto lia.
  (* Error: Anomaly "grounding a non evar-free term" Please report at http://coq.inria.fr/bugs/. *)

  (* If I uncomment `clear H2.`, it takes 9.688 secs and fails with
     Unable to unify "true" with "false". *)

Desired behavior: no matter whether I clear or don't clear H2, itauto lia should succeed fast.

• itauto version: 6791707c
• Coq version: https://github.com/fajb/coq/commit/10db7b18984e781e03da6589b3e163457a485648

mentioned in issue #4

closed with commit 75221106

This is a combination of three bugs - the fix may be partial.

1. The grounding a non evar-free term is avoided by ignoring evars.
2. The sluggishness was due to the multiple generation of the same arithmetic clause. They are now memoised.
3. The Unable to unify "true" with "false" was due to a too small fuel argument because of 2.

mentioned in issue #11 (closed)