We should add some check for this version of Z3. Otherwise, tests are going to fail for some users, and they will be clueless about why. Liquid.Fixpoint.Smt.Interface does version checks already.

Then it would be fine to skip the version check with a flag --skip-smt-version-check if the user wants to run an older version anyway.

I believe that was just a z3 bug so i don't know if it makes sense signaling to the user, and if we decide to do that we should probably check exactly from which version it's not going to loop forever, on Niki's pc the version was just slightly older than the CI's one

I'm assuming it is a z3 bug, indeed. I think you can drop this if you prefer. We can have an issue specifically for checking the z3 version.

My local version of z3 is 4.8.17.

I think an issue would be better

I'm realizing that if the pipeline is fed a single equality f = \x -> x with f local, it is not going to generate a rewrite for f. While I realize this is not the purpose of getCaseRewrites, I'm left wondering how to make a rewrite for it. Is this future work?

We could add that case is not going to create any problem in principle, it's the same thing as get equality being right biased it was thought as a way to extract equalities when performing dependant pattern matching on dependant inductive indexed types and in LH we generate constraint for those in a standard format (prop e = T e1 ... en) but I believe that in spirit of making the code more general as we did by removing the right bias we could also handle those cases

I checked if enabling --etabeta would have the effect of enabling extensionality, but this is not the case since there is one place in LH where the extensionality flag is used and etabeta is ignored.

I don't know what it is meant by the first sentence: "The eta-expansion rule subsumes the --extensionality flag".

To save time during typechecking,

Do you mean that extensionality makes etabeta noticeably slower?

It's meant as any theorem that is proved automatically by extensionality should also be automatically proved by eta beta, in practice the extensionality flag works this way:

If there is some proof { e1 = e2 } where e1 and e2 have type T_1 -> ... -> T_n -> T the extensionality flag rewrites the goal of the proof as { e1 x1 ... xn = e2 x1 ... xn } adding some "ghost" variables x1 ... xn to give a chance to ple to unfold any partially applied function in e1 and e2.

But now the unfolding of partially applied functions is also triggered by eta-expansion, actually is a more general mechanism as eta it works also when functions are used as an argument to some other function/constructor as eta expansion is type preserving but extensionality is not as adding the variables will change the type of the expression so adding the ghost variables there will create an ill typed term.

The suggestion to disable the extensionality flag is meant as: the extensionality flag is not going to automate any proof that is not already automated by etabeta so by enabling extensionality you are executing more code for nothing, is also not going to make PLE faster as we eta-expand everything also fully applied functions.

But we can easily not mention this if you think is only going to confuse the users

I made the note more explicit in e6dc9ac.

What do you think of that use of the extensionality flag in LH?

Should that place take into account etabeta as well?

I think that code is needed to take into account the fact that extensionality flag is changing the type of some expressions, thing that is not done by doing eta expansion, also the eta expansion is totally transparent to LH as it's actually done completely in LF so it shouldn't require any modification in LH