Regressions with Gappa
I found some regression in why3 when I try to use Gappa 1.4.0 to prove some goals.
I join two gappa files that show the regression:
Gappa takes about 10s to return on the first file, and less than one second on the second file.
After investigations, it looks like the problem comes from the commit 05a7bc86 (MR !749 (merged)). In particular, the fact that the definitions of max_int
and max_real
are turned into lemmas really makes the proofs harder.