Nondeterministic blst test failure (Could not find declaration for "mulx_mont_sparse_256")

[RyanGlScott]

I've observed the CI nondeterministically fail to run the blst tests in two different spots (here and here). Here is the error message that occurred in both situations:

[23:33:48.604] Loading file "/saw-script/blst-verification/proof/x86/mulx_mont_256.saw"
[23:33:48.608] Finding symbol for "mulx_mont_sparse_256"
[23:33:48.610] Found symbol at address 0x1b4e0, building CFG
[23:33:48.636] Simulating function "mulx_mont_sparse_256" (at address 0x1b4e0)
[23:33:48.636] Examining specification to determine preconditions
[23:33:48.642] Stack trace:
"include" (/saw-script/blst-verification/proof/memory_safety.saw:18:1-18:8):
"include" (/saw-script/blst-verification/proof/x86.saw:29:1-29:8):
"verify_x86" (/saw-script/blst-verification/proof/x86/mulx_mont_256.saw:79:28-79:38):
"crucible_llvm_verify_x86" (/saw-script/blst-verification/proof/x86.saw:17:3-17:27):
Could not find declaration for "mulx_mont_sparse_256": Could not find declaration for function named `mulx_mont_sparse_256`.
Run SAW with --sim-verbose=3 to see all function names

Verification failed in proof/memory_safety.saw

[chameco]

@nano-o fixed this in GaloisInc/BLST-Verification@e15494b. We still need to update the ref in s2nTests/docker/blst.dockerfile, but after that this failure should no longer occur 😃

EDIT:
It might be slightly more effort to update to that commit, since it appears to change the build scripts to reference an absolute path that isn't present in our Docker environment. I'll work on getting this resolved today, hopefully.