`lia` is fast but `itauto lia` gets stuck in non-lia work

Here's an example I isolated from bedrock2:

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

Unset Lia Cache.
Set Itauto Theory Time.

Ltac timing_lia := idtac "starting a lia call..."; time "lia" lia.

Goal forall instrMemSizeLg memSizeLg stack_size_in_bytes
            instrMemSizeBytes : Z,
 3 <= instrMemSizeLg <= 30 ->
 2 + instrMemSizeLg < memSizeLg <= 16 ->
 forall BPW : Z,
 stack_size_in_bytes mod BPW = 0 ->
 0 <= stack_size_in_bytes <= 2 ^ memSizeLg - instrMemSizeBytes ->
 forall (L2 : nat) (width : Z) (wordrep : Type)
   (w2z : wordrep -> Z) (z2w : Z -> wordrep),
 w2z (z2w 0) + Z.of_nat L2 <= w2z (z2w instrMemSizeBytes) ->
 0 <= Z.of_nat L2 ->
 Z.of_nat L2 <= instrMemSizeBytes ->
 instrMemSizeBytes <= 2 ^ memSizeLg - stack_size_in_bytes ->
 2 ^ memSizeLg - stack_size_in_bytes <= 2 ^ memSizeLg ->
 2 ^ memSizeLg < 2 ^ width ->
 instrMemSizeBytes = 2 ^ (2 + instrMemSizeLg) ->
 forall (z9 : Z) (L1 : nat),
 Z.of_nat L1 = z9 ->
 0 <= Z.of_nat L1 ->
 forall z2 : Z,
 0 < instrMemSizeBytes /\ z2 = instrMemSizeBytes \/
 instrMemSizeBytes <= 0 /\ z2 = 0 ->
 forall z3 : Z,
 0 < z2 - Z.of_nat L2 /\ z3 = z2 - Z.of_nat L2 \/
 z2 - Z.of_nat L2 <= 0 /\ z3 = 0 ->
 forall z4 : Z,
 0 < Z.of_nat L1 - Z.of_nat L2 /\ z4 = Z.of_nat L1 - Z.of_nat L2 \/
 Z.of_nat L1 - Z.of_nat L2 <= 0 /\ z4 = 0 ->
 forall z5 : Z,
 0 < z4 - z3 /\ z5 = z4 - z3 \/ z4 - z3 <= 0 /\ z5 = 0 ->
 forall z6 : Z,
 0 < 2 ^ memSizeLg - instrMemSizeBytes - stack_size_in_bytes /\
 z6 = 2 ^ memSizeLg - instrMemSizeBytes - stack_size_in_bytes \/
 2 ^ memSizeLg - instrMemSizeBytes - stack_size_in_bytes <= 0 /\
 z6 = 0 ->
 forall z7 : Z,
 z6 < z5 /\ z7 = z6 \/ z5 <= z6 /\ z7 = z5 ->
 forall z8 : Z,
 z3 < z4 /\ z8 = z3 \/ z4 <= z3 /\ z8 = z4 ->
 0 < 2 ^ memSizeLg /\ z9 = 2 ^ memSizeLg \/
 2 ^ memSizeLg <= 0 /\ z9 = 0 ->
 Z.of_nat L2 + z8 + z7 = 2 ^ memSizeLg - stack_size_in_bytes.
Proof.
  intros.
  (* Time lia. (* 0.565 secs *) *)
  itauto timing_lia.

It produces 168 lines of output, and then keeps computing without any more output. After several minutes, I aborted it, so I don't know how long it would run. The last few lines of output are

starting a lia call...
Tactic call lia ran for 0.006 secs (0.006u,0.s) (success)
starting a lia call...
Tactic call lia ran for 0.006 secs (0.006u,0.s) (success)
starting a lia call...
Tactic call lia ran for 0.006 secs (0.006u,0.s) (success)
starting a lia call...
Tactic call lia ran for 0.005 secs (0.005u,0.s) (success)
Debug: Theory running time 0.783

Each starting a lia call... line is followed by a Tactic call lia ran for line, so I assume that contrary to #13 (closed), here it gets stuck inside itauto code.

• Coq version: https://github.com/fajb/coq/commit/f1c016bcd964328f87d111346a981529a01d4f30
• itauto version: ff7ddd29

Update: I forgot to abort the build that was compiling the above goal in the full context of bedrock2, and it seems that there, this goal was solved in 13054.296 secs, which is more than 3.5 hours, but I guess that's more of a "fun fact" than "useful information"

Thanks for the report. With the latest coq / itauto, it is still slow : Finished transaction in 155.901 secs (154.88u,0.1s) (successful)

mentioned in issue #4

This isolated example now runs in 147.943 secs on my computer, but in the full context of bedrock2 (which has more hypotheses and larger subexpressions), it takes 693.509 secs, while lia solves it in 1.073 secs.

closed with commit 533c38f4

With 533c38f4, the running time is down to 3s (in isolation). Here, half of the time is spent generalising the propositional variables.

reopened

With 36ff4a86, < 1s

closed