s2n proofs cannot be reproduced locally

[robdockins]

With GaloisInc/s2n checked out to hash eae05a158032468fa18de0d8a9132c310abaa4f8, I attempt the following interaction on OSX 10.15.5

$ export CLANG=/usr/local/Cellar/llvm\@7/7.1.0_1/bin/clang
$ export LLVMLINK=/usr/local/Cellar/llvm\@7/7.1.0_1/bin/llvm-link
$ make -C tests/saw

This eventually results in the following output:

[16:49:08.562] Proving correctness of s2n_advance_message
[16:49:09.147] Stack trace:
"prove_handshake_io_lowlevel" (/Users/rdockins/code/s2n/tests/saw/verify_cork_uncork.saw:23:1-23:28):
"crucible_llvm_verify" (/Users/rdockins/code/s2n/tests/saw/spec/handshake/handshake.saw:70:34-70:54):
"s2n_advance_message_spec" (/Users/rdockins/code/s2n/tests/saw/spec/handshake/handshake.saw:70:101-70:125):
"crucible_points_to" (/Users/rdockins/code/s2n/tests/saw/spec/handshake/handshake_io_lowlevel.saw:308:5-308:23):
types not memory-compatible:
<{ <{ i32, i32, [30 x i32] }>, <{ i32, i32, i32, i32, i32, i32, i32, [25 x i32] }>, [32 x i32], <{ [10 x i32], [22 x i32] }>, [32 x i32], [32 x i32], [32 x i32], <{ [11 x i32], [21 x i32] }>, [32 x i32], [32 x i32], [32 x i32], <{ [11 x i32], [21 x i32] }>, [32 x i32], [32 x i32], [32 x i32], <{ [12 x i32], [20 x i32] }>, [32 x i32], [32 x i32], [32 x i32], <{ [13 x i32], [19 x i32] }>, [32 x i32], [32 x i32], [32 x i32], <{ [14 x i32], [18 x i32] }>, [32 x i32], [32 x i32], [32 x i32], <{ [14 x i32], [18 x i32] }>, [32 x i32], [32 x i32], [32 x i32], <{ [15 x i32], [17 x i32] }>, [32 x i32], <{ [8 x i32], [24 x i32] }>, [32 x i32], <{ [11 x i32], [21 x i32] }>, [32 x i32], [32 x i32], [32 x i32], <{ [12 x i32], [20 x i32] }>, [32 x i32], [32 x i32], [32 x i32], <{ [12 x i32], [20 x i32] }>, [32 x i32], [32 x i32], [32 x i32], <{ [13 x i32], [19 x i32] }>, [32 x i32], [32 x i32], [32 x i32], <{ [14 x i32], [18 x i32] }>, [32 x i32], [32 x i32], [32 x i32], <{ [15 x i32], [17 x i32] }>, [32 x i32], [32 x i32], [32 x i32], <{ [15 x i32], [17 x i32] }>, [32 x i32], [32 x i32], [32 x i32], <{ [16 x i32], [16 x i32] }>, [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], <{ [12 x i32], [20 x i32] }>, [32 x i32], [32 x i32], [32 x i32], <{ [13 x i32], [19 x i32] }>, [32 x i32], [32 x i32], [32 x i32], <{ [13 x i32], [19 x i32] }>, [32 x i32], [32 x i32], [32 x i32], <{ [14 x i32], [18 x i32] }>, [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], [32 x i32], <{ [13 x i32], [19 x i32] }>, [32 x i32], [32 x i32], [32 x i32], <{ [14 x i32], [18 x i32] }>, [32 x i32], [32 x i32], [32 x i32], <{ [14 x i32], [18 x i32] }>, [32 x i32], [32 x i32], [32 x i32], <{ [15 x i32], [17 x i32] }>, [128 x [32 x i32]] }>
[256 x [32 x i32]]

Instead I expect to be able to run this script and locally test the proof still works outside the CI system.

[chameco]

Fixed in #823 - see #738.