CI is unpredictably failing
chameco opened this issue · 1 comments
This can be seen clearly on the Nightly builds page, and is almost certainly a consequence of #1746.
It looks like not only the BLST job is inconsistent: in some jobs AWSLC times out.
In both cases it looks like a Z3 timeout, probably because we moved from Z3 4.8.10 to 4.8.14.
Sigh.
As a short-term fix, I think we should just include both z3-4.8.10 and z3-4.8.14 (with z3 being an alias for z3-4.8.14) in a what4-solvers bindist, and then we can manually copy z3-4.8.10 to z3 before running the AWSLC/BLST jobs.
Alternatively, we could try different, later versions of Z3 on those jobs to find one that doesn't exhibit the nondeterministic timeouts that z3-4.8.14 does, but that sounds like a tedious way to go about yet. Better yet would be to extract the SMT-LIB2 term that is causing the timeout so that we can test it on different Z3 versions without needing the run the full AWSLC/BLST jobs.