Jonathan Protzenko

These are the four files that the build is stuck on: ``` Hacl.Spec.BignumQ.Mul Vale.Curve25519.X64.FastMul Hacl.Spec.Poly1305.Equiv Vale.Curve25519.FastSqr_helpers ``` those are currently at 1h+ of Z3 time

Yeah that sounds reasonable, my only qualm is that I don't know how to go about debugging proof obligations that suddenly start taking 70+ minutes -- does the new z3...

But realistically, it would be nice to understand if there's new (non-intuitive) behavior that we need to be aware of for HACL*. As in: "these kinds of things used to...

Going to write down the failures here: - after four hours: ``` Failed after: 4:25:13 Full log is in obj/Hacl.Spec.Poly1305.Equiv.fst.checked.{out,err}, see excerpt below: * Error 19 at /Users/jonathan/Code/everest/hacl-star/code/poly1305/Hacl.Spec.Poly1305.Equiv.fst(183,9-183,56): - Assertion...

@gebner I looked at code/poly1305/Hacl.Spec.Poly1305.Equiv.fst in HACL* and the file has an rlimit of 50 -- why are we seeing failures after 4 hours? do you have any sense of...

My question is: the rlimit puts an upper bound on the "time budget" that z3 has. 50 is a very low rlimit that historically has corresponded to maybe a few...

> However, I believe we first need to reach the point where there is little to no proof performance regression. In particular, I see files now taking 45 minutes to...

@mtzguido did you end up making progress on this one? having to build z3 4.8.5 as part of the CI is becoming more and more painful maybe the behavior would...

wonderful, thanks Guido -- very eager to hear about the results

Do we still see a time explosion on the previously problematic files?