Find SMT array write of a fixed size.

[andreistefanescu]

No description provided.

[kquick]

This fixed an issue for Amazon, but it fails on the s2n test, presumably due to available resources (memory, although it should be re-run to verify this). Amazon keeps rebasing this on top of their stuff to keep things working. Should we switch to internal runners to provide more memory because this just slipped us over the threshold, or is this a significant regression that needs addressing?

[kquick]

This has a crucible dependency: GaloisInc/crucible#1074

[RyanGlScott]

Another awslc CI timeout occurred in #2018, which has comparatively fewer changes. I wonder if the crucible submodule bump is the culprit?

[RyanGlScott]

On second thought, I don't think the crucible submodule bump has anything to do with it. In fact, the CI now passes after rebasing these changes on top of a more recent commit. I suspect that the CI was timing out earlier because, historically speaking, the awslc proofs job was very close to the timeout limit, and this PR timed out by falling on the wrong side of the limit due to an unlucky fluke. But now that we've rebased this, we can see that the awslc job finishes within 27 minutes, which is the same amount of time that the jobs takes on master. (SMT query caching coming in clutch here.)

This still isn't quite ready to land yet, as the crucible changes that this PR relies on haven't yet landed. But it's very close.

[RyanGlScott]

Superseded by #2037.