Top-level definition order highly impacts verification: Needs better solver profiling

I keep hitting strange regressions every time I update F* to its latest.
In commit `b590fde`:

```F#
module Test

open FStar.Mul

module L = FStar.Math.Lemmas

#reset-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 100"

private
let lemma_distr_5_0 u x1 x2 x3 x4 x5 : Lemma
(u * (x1 + x2 + x3 + x4 + x5)
== u * x1 + u * x2 + u * x3 + u * x4 + u * x5)
= ()

private
let lemma_distr_4_0 u x1 x2 x3 x4 : Lemma
(u * (x1 + x2 + x3 + x4)
== u * x1 + u * x2 + u * x3 + u * x4)
= ()
```
fails on `lemma_distr_4_0`. Changing the order of the lemmas makes it pass instantaneously.
It used to go through with a commit from last week.

Is the SMT encoding undergoing deep changes at the moment ? Should I stop updating F* for the time of out developments ? Or it is that I should build Z3 from its latest sources ? Thanks.