FStar Huge verification freeze (performance regression)

Huge verification freeze (performance regression)

Open hacklex opened this issue 3 years ago • 2 comments

Here's an example extracted from my algebra library

FStar freezes for minutes before finally accepting the fraction field definition.

Aug 09 '22 20:08 hacklex

The issue with my algebra code is fixed (I avoided this freeze) -- but the issue with F* remains

Aug 10 '22 10:08 hacklex

Also, this is probably the same problem as mentioned here.

The fix @aseemr suggested didn't work btw.

Aug 10 '22 10:08 hacklex