lia performance regression

[samuelgruetter]

Consider this lia goal:

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

Goal
  forall Y r0 r q q0 r1 q1 : Z,
  ~
  (131072 <= Y < 139264 \/
   268468224 <= Y < 268500992 \/ 268509184 <= Y < 268513280 \/ 268513280 <= Y < 268517376) ->
  131072 <= r0 < 139264 \/
  268468224 <= r0 < 268500992 \/ 268509184 <= r0 < 268513280 \/ 268513280 <= r0 < 268517376 ->
  r = 0 ->
  0 <= Y < 4294967296 ->
  (4 <> 0 -> r0 = 4 * q + r) ->
  (0 < 4 -> 0 <= r < 4) ->
  (4 < 0 -> 4 < r <= 0) ->
  (4 = 0 -> q = 0) ->
  (4 = 0 -> r = 0) ->
  (4294967296 <> 0 -> Y - r1 = 4294967296 * q0 + r0) ->
  (0 < 4294967296 -> 0 <= r0 < 4294967296) ->
  (4294967296 < 0 -> 4294967296 < r0 <= 0) ->
  (4294967296 = 0 -> q0 = 0) ->
  (4294967296 = 0 -> r0 = 0) ->
  (4294967296 <> 0 -> 2 = 4294967296 * q1 + r1) ->
  (0 < 4294967296 -> 0 <= r1 < 4294967296) ->
  (4294967296 < 0 -> 4294967296 < r1 <= 0) ->
  (4294967296 = 0 -> q1 = 0) -> (4294967296 = 0 -> r1 = 0) -> False.
Proof.
  intros.

  (* workaround by @thery *)
  repeat match goal with
	 | [ H : ?x -> _, H' : ?x -> _ |- _ ] =>
	   pose proof (fun u : x => conj (H u) (H' u)); clear H H' end.

  Timeout 60 Time lia.

Time Qed.

It used to have (close to) good performance in 8.9.0, but times out on Coq master:

Coq 8.9.0:

• with workaround: lia takes 20.55 secs, Qed takes 43.705 secs
• without workaround: timeout

Coq master of Nov 4:

• with workaround: timeout
• without workaround: timeout

For all tests, I first deleted .lia.cache and then ran coqc on the above file from the command line.

I'd be curious to know what caused this, but before I delve into a git bisect, maybe @fajb would have some intuition about what it could be?

[fajb]

I have no clue :(
With my current experimental version, PR #11047 it is instantaneous with thery's workaround.

[maximedenes]

Seems like it could be related to #11063.

[samuelgruetter]

For the record, here's the problem in the context of bedrock2: The build which succeeds in 8.9 and 8.10 but fails on master, and the commit which "fixed" (admitted) it (but also revealed the next problem).