CI is unpredictably failing

[chameco]

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.

[RyanGlScott]

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.

[sauclovian-g]

We need a comprehensive solution for solver versions.

[sauclovian-g]

(I have updated the labels accordingly)

[sauclovian-g]

There's already an issue for solver versions: #390. I don't think we need two, and the specific issue in here got handled. @RyanGlScott do you want to leave it open as a reminder to remove the prior hacks when we get a proper solution, or should we close it?

[RyanGlScott]

If I understand correctly, the "comprehensive solution" is to check to see if your solver's version number lies within a known range of supported solvers beforehand? If so, I would be fine with closing this issue in and dedicating #390 to the task of implementing that solution.

The what4-solvers hacks mentioned above are due to a different problem: different Z3 versions are very unpredictable in what SAW workloads they can support, and it's difficult to find a single version that works well on everything we want to do with SAW. Arguably, this is just as much of a toolchain issue than it is a SAW one. I wouldn't be opposed to opening a separate issue for the task of figuring out a Single Blessed Version™ of Z3 to use everywhere, although I'm not sure where we should open it. Maybe the what4-solvers issue tracker?

[mccleeary-galois]

If I understand correctly, the "comprehensive solution" is to check to see if your solver's version number lies within a known range of supported solvers beforehand? If so, I would be fine with closing this issue in and dedicating #390 to the task of implementing that solution.

The what4-solvers hacks mentioned above are due to a different problem: different Z3 versions are very unpredictable in what SAW workloads they can support, and it's difficult to find a single version that works well on everything we want to do with SAW. Arguably, this is just as much of a toolchain issue than it is a SAW one. I wouldn't be opposed to opening a separate issue for the task of figuring out a Single Blessed Version™ of Z3 to use everywhere, although I'm not sure where we should open it. Maybe the what4-solvers issue tracker?

I have been calling out what4-solvers in issues around this so I think it makes sense to have that be the source of "Single Blessed Version™ of Z3"

[sauclovian-g]

No, what I meant by a comprehensive solution is a robust way to have multiple version of the same solver on tap, and to be able to choose between them for proofs in a non-awful way.

I suppose that's more general than what's actually written in #390, in which case I suppose I ought to make a new issue (instead of repurposing this one) describing that more cogently, then close both of these.

I think there will be times when what4-solvers will need to ship two z3s, or two yicicies,or whatever.