build.sh: Use --remap-path-prefix

This ensures that full paths do not leak into MIR output.
GaloisInc · RyanGlScott · Jul 14, 2023 · Mar 2, 2023 · Mar 11, 2023 · Mar 16, 2023
commit 0be2b4a724eeea52ccc5f2c40a92bd1d57dda6c4
diff --git a/crux-mir/build.sh b/crux-mir/build.sh
diff --git a/crux-mir/test/symb_eval/alloc/out_of_bounds.good b/crux-mir/test/symb_eval/alloc/out_of_bounds.good
@@ -1,13 +1,13 @@
-test out_of_bounds/b521303c::crux_test[0]: FAILED
+test out_of_bounds/ca0644b7::crux_test[0]: FAILED
 
 failures:
 
----- out_of_bounds/b521303c::crux_test[0] counterexamples ----
+---- out_of_bounds/ca0644b7::crux_test[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux] test/symb_eval/alloc/out_of_bounds.rs:12:9: 12:24: error: in out_of_bounds/b521303c::crux_test[0]
+[Crux] test/symb_eval/alloc/out_of_bounds.rs:12:9: 12:24: error: in out_of_bounds/ca0644b7::crux_test[0]
 [Crux] vector index out of range: the length is 10 but the index is BV 12
 [Crux] Found counterexample for verification goal
-[Crux] test/symb_eval/alloc/out_of_bounds.rs:12:9: 12:24: error: in out_of_bounds/b521303c::crux_test[0]
+[Crux] test/symb_eval/alloc/out_of_bounds.rs:12:9: 12:24: error: in out_of_bounds/ca0644b7::crux_test[0]
 [Crux] attempted to read empty mux tree
 
 [Crux] Overall status: Invalid.
diff --git a/crux-mir/test/symb_eval/alloc/uninit_read.good b/crux-mir/test/symb_eval/alloc/uninit_read.good
@@ -1,13 +1,13 @@
-test uninit_read/e86da728::crux_test[0]: FAILED
+test uninit_read/851ea4ad::crux_test[0]: FAILED
 
 failures:
 
----- uninit_read/e86da728::crux_test[0] counterexamples ----
+---- uninit_read/851ea4ad::crux_test[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux] test/symb_eval/alloc/uninit_read.rs:9:9: 9:23: error: in uninit_read/e86da728::crux_test[0]
+[Crux] test/symb_eval/alloc/uninit_read.rs:9:9: 9:23: error: in uninit_read/851ea4ad::crux_test[0]
 [Crux] Attempted to read uninitialized vector index
 [Crux] Found counterexample for verification goal
-[Crux] test/symb_eval/alloc/uninit_read.rs:9:9: 9:23: error: in uninit_read/e86da728::crux_test[0]
+[Crux] test/symb_eval/alloc/uninit_read.rs:9:9: 9:23: error: in uninit_read/851ea4ad::crux_test[0]
 [Crux] attempted to read empty mux tree
 
 [Crux] Overall status: Invalid.
diff --git a/crux-mir/test/symb_eval/alloc/valid_read.good b/crux-mir/test/symb_eval/alloc/valid_read.good
@@ -1,3 +1,3 @@
-test valid_read/f9c1ade1::crux_test[0]: returned 45, ok
+test valid_read/c82bffb5::crux_test[0]: returned 45, ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/alloc/zero_length.good b/crux-mir/test/symb_eval/alloc/zero_length.good
@@ -1,3 +1,3 @@
-test zero_length/94b92a2d::crux_test[0]: ok
+test zero_length/d9fb4927::crux_test[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/any/conditional.good b/crux-mir/test/symb_eval/any/conditional.good
@@ -1,3 +1,3 @@
-test conditional/84afefc9::crux_test[0]: ok
+test conditional/e22ae149::crux_test[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/any/downcast.good b/crux-mir/test/symb_eval/any/downcast.good
@@ -1,3 +1,3 @@
-test downcast/870d31b0::crux_test[0]: returned 1, ok
+test downcast/c8ce9e8e::crux_test[0]: returned 1, ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/array/basic.good b/crux-mir/test/symb_eval/array/basic.good
@@ -1,3 +1,3 @@
-test basic/bfb477c2::crux_test[0]: returned 3, ok
+test basic/a10c5e44::crux_test[0]: returned 3, ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/array/mux_slice.good b/crux-mir/test/symb_eval/array/mux_slice.good
@@ -1,3 +1,3 @@
-test mux_slice/fe5e891b::crux_test[0]: returned Symbolic BV, ok
+test mux_slice/df68b584::crux_test[0]: returned Symbolic BV, ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/array/slice.good b/crux-mir/test/symb_eval/array/slice.good
@@ -1,3 +1,3 @@
-test slice/ea2efd47::crux_test[0]: returned 5, ok
+test slice/ab67a8fd::crux_test[0]: returned 5, ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/array/slice_mut.good b/crux-mir/test/symb_eval/array/slice_mut.good
@@ -1,3 +1,3 @@
-test slice_mut/1361be29::crux_test[0]: returned 5, ok
+test slice_mut/cf0e1c49::crux_test[0]: returned 5, ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/bitvector/arith.good b/crux-mir/test/symb_eval/bitvector/arith.good
@@ -1,3 +1,3 @@
-test arith/382b0162::crux_test[0]: ok
+test arith/909ad774::crux_test[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/bitvector/cmp.good b/crux-mir/test/symb_eval/bitvector/cmp.good
@@ -1,3 +1,3 @@
-test cmp/a77f9ebc::crux_test[0]: ok
+test cmp/79f545fc::crux_test[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/bitvector/from_to.good b/crux-mir/test/symb_eval/bitvector/from_to.good
@@ -1,3 +1,3 @@
-test from_to/cecfc226::crux_test[0]: ok
+test from_to/81d915d3::crux_test[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/bitvector/leading_zeros.good b/crux-mir/test/symb_eval/bitvector/leading_zeros.good
@@ -1,3 +1,3 @@
-test leading_zeros/85b8f496::crux_test[0]: ok
+test leading_zeros/a181beeb::crux_test[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/bitvector/literals.good b/crux-mir/test/symb_eval/bitvector/literals.good
@@ -1,3 +1,3 @@
-test literals/06825ef9::crux_test[0]: ok
+test literals/9d6d8593::crux_test[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/bitvector/overflowing_sub.good b/crux-mir/test/symb_eval/bitvector/overflowing_sub.good
@@ -1,3 +1,3 @@
-test overflowing_sub/30a11e11::crux_test[0]: ok
+test overflowing_sub/d297e8c6::crux_test[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/bitvector/symbolic.good b/crux-mir/test/symb_eval/bitvector/symbolic.good
@@ -1,3 +1,3 @@
-test symbolic/d4690595::crux_test[0]: ok
+test symbolic/8802d91d::crux_test[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/bytes/extend_bytes.good b/crux-mir/test/symb_eval/bytes/extend_bytes.good
@@ -1,3 +1,3 @@
-test extend_bytes/fe7bcbf0::f[0]: ok
+test extend_bytes/724ff396::f[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/bytes/new.good b/crux-mir/test/symb_eval/bytes/new.good
@@ -1,3 +1,3 @@
-test new/dec1e542::f[0]: ok
+test new/7e2f4495::f[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/bytes/put_overflow.good b/crux-mir/test/symb_eval/bytes/put_overflow.good
@@ -1,10 +1,10 @@
-test put_overflow/3a1fbbbh::f[0]: FAILED
+test put_overflow/57f18178::f[0]: FAILED
 
 failures:
 
----- put_overflow/3a1fbbbh::f[0] counterexamples ----
+---- put_overflow/57f18178::f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux] internal: error: in bytes/3a1fbbbh::{{impl}}[4]::put_slice[0]
-[Crux] panicking::begin_panic, called from bytes/3a1fbbbh::{{impl}}[4]::put_slice[0]
+[Crux] internal: error: in bytes/c14f6c84::{impl#4}[0]::put_slice[0]
+[Crux] panicking::panic_fmt, called from bytes/c14f6c84::{impl#4}[0]::put_slice[0]
 
 [Crux] Overall status: Invalid.
diff --git a/crux-mir/test/symb_eval/concretize/array.good b/crux-mir/test/symb_eval/concretize/array.good
@@ -1,3 +1,3 @@
-test array/aa48835b::crux_test[0]: returned (1, 2, 3), ok
+test array/191383c3::crux_test[0]: returned (1, 2, 3), ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/concretize/assert_ok.good b/crux-mir/test/symb_eval/concretize/assert_ok.good
@@ -1,3 +1,3 @@
-test assert_ok/e60ec1ab::crux_test[0]: returned 1, ok
+test assert_ok/e20e387d::crux_test[0]: returned 1, ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/concretize/conc.good b/crux-mir/test/symb_eval/concretize/conc.good
@@ -1,3 +1,3 @@
-test conc/58237648::crux_test[0]: returned (1, 0), ok
+test conc/86e91a75::crux_test[0]: returned (1, 0), ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/concretize/no_conc.good b/crux-mir/test/symb_eval/concretize/no_conc.good
@@ -1,3 +1,3 @@
-test no_conc/46b8f4c7::crux_test[0]: returned (Symbolic BV, Symbolic BV), ok
+test no_conc/27ee0b55::crux_test[0]: returned (Symbolic BV, Symbolic BV), ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/crux/early_fail.good b/crux-mir/test/symb_eval/crux/early_fail.good
@@ -1,16 +1,16 @@
-test early_fail/3a1fbbbh::fail1[0]: FAILED
-test early_fail/3a1fbbbh::fail2[0]: FAILED
+test early_fail/233440b0::fail1[0]: FAILED
+test early_fail/233440b0::fail2[0]: FAILED
 
 failures:
 
----- early_fail/3a1fbbbh::fail1[0] counterexamples ----
+---- early_fail/233440b0::fail1[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux] internal: error: in early_fail/3a1fbbbh::fail1[0]
-[Crux] panicking::begin_panic, called from early_fail/3a1fbbbh::fail1[0]
+[Crux] internal: error: in early_fail/233440b0::fail1[0]
+[Crux] panicking::panic_fmt, called from early_fail/233440b0::fail1[0]
 
----- early_fail/3a1fbbbh::fail2[0] counterexamples ----
+---- early_fail/233440b0::fail2[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/crux/early_fail.rs:17:5: 17:30: error: in early_fail/3a1fbbbh::fail2[0]
+[Crux] ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/early_fail.rs:17:5: 17:29: error: in early_fail/233440b0::fail2[0]
 [Crux] MIR assertion at test/symb_eval/crux/early_fail.rs:17:5:
 [Crux] x == 0
 

diff --git a/crux-mir/test/symb_eval/crux/fail_return.good b/crux-mir/test/symb_eval/crux/fail_return.good
@@ -1,23 +1,23 @@
-test fail_return/3a1fbbbh::fail1[0]: returned Symbolic BV, FAILED
-test fail_return/3a1fbbbh::fail2[0]: returned 123, FAILED
+test fail_return/10c6efbb::fail1[0]: returned Symbolic BV, FAILED
+test fail_return/10c6efbb::fail2[0]: returned 123, FAILED
 
 failures:
 
----- fail_return/3a1fbbbh::fail1[0] counterexamples ----
+---- fail_return/10c6efbb::fail1[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux] test/symb_eval/crux/fail_return.rs:8:22: 8:27: error: in fail_return/3a1fbbbh::fail1[0]
-[Crux] attempt to add with overflow
+[Crux] test/symb_eval/crux/fail_return.rs:8:22: 8:27: error: in fail_return/10c6efbb::fail1[0]
+[Crux] attempt to compute `move _4 + const 1_u8`, which would overflow
 [Crux] Found counterexample for verification goal
-[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/crux/fail_return.rs:8:5: 8:33: error: in fail_return/3a1fbbbh::fail1[0]
+[Crux] ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/fail_return.rs:8:5: 8:32: error: in fail_return/10c6efbb::fail1[0]
 [Crux] MIR assertion at test/symb_eval/crux/fail_return.rs:8:5:
 [Crux] x + 1 > x
 
----- fail_return/3a1fbbbh::fail2[0] counterexamples ----
+---- fail_return/10c6efbb::fail2[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux] test/symb_eval/crux/fail_return.rs:15:22: 15:27: error: in fail_return/3a1fbbbh::fail2[0]
-[Crux] attempt to add with overflow
+[Crux] test/symb_eval/crux/fail_return.rs:15:22: 15:27: error: in fail_return/10c6efbb::fail2[0]
+[Crux] attempt to compute `move _5 + const 1_u8`, which would overflow
 [Crux] Found counterexample for verification goal
-[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/crux/fail_return.rs:15:5: 15:33: error: in fail_return/3a1fbbbh::fail2[0]
+[Crux] ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/fail_return.rs:15:5: 15:32: error: in fail_return/10c6efbb::fail2[0]
 [Crux] MIR assertion at test/symb_eval/crux/fail_return.rs:15:5:
 [Crux] x + 1 > x
 

diff --git a/crux-mir/test/symb_eval/crux/mixed_fail.good b/crux-mir/test/symb_eval/crux/mixed_fail.good
@@ -1,25 +1,25 @@
-test mixed_fail/3a1fbbbh::fail1[0]: FAILED
-test mixed_fail/3a1fbbbh::fail2[0]: FAILED
-test mixed_fail/3a1fbbbh::pass1[0]: ok
-test mixed_fail/3a1fbbbh::pass2[0]: ok
+test mixed_fail/0b094ced::fail1[0]: FAILED
+test mixed_fail/0b094ced::fail2[0]: FAILED
+test mixed_fail/0b094ced::pass1[0]: ok
+test mixed_fail/0b094ced::pass2[0]: ok
 
 failures:
 
----- mixed_fail/3a1fbbbh::fail1[0] counterexamples ----
+---- mixed_fail/0b094ced::fail1[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux] test/symb_eval/crux/mixed_fail.rs:8:22: 8:27: error: in mixed_fail/3a1fbbbh::fail1[0]
-[Crux] attempt to add with overflow
+[Crux] test/symb_eval/crux/mixed_fail.rs:8:22: 8:27: error: in mixed_fail/0b094ced::fail1[0]
+[Crux] attempt to compute `move _5 + const 1_u8`, which would overflow
 [Crux] Found counterexample for verification goal
-[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/crux/mixed_fail.rs:8:5: 8:33: error: in mixed_fail/3a1fbbbh::fail1[0]
+[Crux] ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/mixed_fail.rs:8:5: 8:32: error: in mixed_fail/0b094ced::fail1[0]
 [Crux] MIR assertion at test/symb_eval/crux/mixed_fail.rs:8:5:
 [Crux] x + 1 > x
 
----- mixed_fail/3a1fbbbh::fail2[0] counterexamples ----
+---- mixed_fail/0b094ced::fail2[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux] test/symb_eval/crux/mixed_fail.rs:14:22: 14:27: error: in mixed_fail/3a1fbbbh::fail2[0]
-[Crux] attempt to add with overflow
+[Crux] test/symb_eval/crux/mixed_fail.rs:14:22: 14:27: error: in mixed_fail/0b094ced::fail2[0]
+[Crux] attempt to compute `move _5 + const 2_u8`, which would overflow
 [Crux] Found counterexample for verification goal
-[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/crux/mixed_fail.rs:14:5: 14:33: error: in mixed_fail/3a1fbbbh::fail2[0]
+[Crux] ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/mixed_fail.rs:14:5: 14:32: error: in mixed_fail/0b094ced::fail2[0]
 [Crux] MIR assertion at test/symb_eval/crux/mixed_fail.rs:14:5:
 [Crux] x + 2 > x
 

diff --git a/crux-mir/test/symb_eval/crux/multi.good b/crux-mir/test/symb_eval/crux/multi.good
@@ -1,26 +1,26 @@
-test multi/3a1fbbbh::fail1[0]: FAILED
-test multi/3a1fbbbh::fail2[0]: FAILED
-test multi/3a1fbbbh::fail3[0]: FAILED
+test multi/017eda4c::fail1[0]: FAILED
+test multi/017eda4c::fail2[0]: FAILED
+test multi/017eda4c::fail3[0]: FAILED
 
 failures:
 
----- multi/3a1fbbbh::fail1[0] counterexamples ----
+---- multi/017eda4c::fail1[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux] test/symb_eval/crux/multi.rs:8:22: 8:27: error: in multi/3a1fbbbh::fail1[0]
-[Crux] attempt to add with overflow
+[Crux] test/symb_eval/crux/multi.rs:8:22: 8:27: error: in multi/017eda4c::fail1[0]
+[Crux] attempt to compute `move _5 + const 1_u8`, which would overflow
 [Crux] Found counterexample for verification goal
-[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/crux/multi.rs:8:5: 8:33: error: in multi/3a1fbbbh::fail1[0]
+[Crux] ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/multi.rs:8:5: 8:32: error: in multi/017eda4c::fail1[0]
 [Crux] MIR assertion at test/symb_eval/crux/multi.rs:8:5:
 [Crux] x + 1 > x
 
----- multi/3a1fbbbh::fail2[0] counterexamples ----
+---- multi/017eda4c::fail2[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux] internal: error: in multi/3a1fbbbh::fail2[0]
-[Crux] panicking::begin_panic, called from multi/3a1fbbbh::fail2[0]
+[Crux] internal: error: in multi/017eda4c::fail2[0]
+[Crux] panicking::panic_fmt, called from multi/017eda4c::fail2[0]
 
----- multi/3a1fbbbh::fail3[0] counterexamples ----
+---- multi/017eda4c::fail3[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/crux/multi.rs:20:5: 20:30: error: in multi/3a1fbbbh::assert_zero[0]
+[Crux] ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crux/multi.rs:20:5: 20:29: error: in multi/017eda4c::assert_zero[0]
 [Crux] MIR assertion at test/symb_eval/crux/multi.rs:20:5:
 [Crux] x == 0
 

diff --git a/crux-mir/test/symb_eval/crypto/bytes.good b/crux-mir/test/symb_eval/crypto/bytes.good
@@ -1,26 +1,26 @@
-test bytes/3a1fbbbh::f[0]: FAILED
+test bytes/0910acd4::f[0]: FAILED
 
 failures:
 
----- bytes/3a1fbbbh::f[0] counterexamples ----
+---- bytes/0910acd4::f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0]
+[Crux] ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:37: error: in bytes/0910acd4::f[0]
 [Crux] MIR assertion at test/symb_eval/crypto/bytes.rs:85:7:
 [Crux] a[i] == b[i]
 [Crux] Found counterexample for verification goal
-[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0]
+[Crux] ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:37: error: in bytes/0910acd4::f[0]
 [Crux] MIR assertion at test/symb_eval/crypto/bytes.rs:85:7:
 [Crux] a[i] == b[i]
 [Crux] Found counterexample for verification goal
-[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0]
+[Crux] ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:37: error: in bytes/0910acd4::f[0]
 [Crux] MIR assertion at test/symb_eval/crypto/bytes.rs:85:7:
 [Crux] a[i] == b[i]
 [Crux] Found counterexample for verification goal
-[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0]
+[Crux] ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:37: error: in bytes/0910acd4::f[0]
 [Crux] MIR assertion at test/symb_eval/crypto/bytes.rs:85:7:
 [Crux] a[i] == b[i]
 [Crux] Found counterexample for verification goal
-[Crux] ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0]
+[Crux] ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:37: error: in bytes/0910acd4::f[0]
 [Crux] MIR assertion at test/symb_eval/crypto/bytes.rs:85:7:
 [Crux] a[i] == b[i]
 

diff --git a/crux-mir/test/symb_eval/crypto/bytes2.good b/crux-mir/test/symb_eval/crypto/bytes2.good
@@ -1,3 +1,3 @@
-test bytes2/c529255b::f[0]: ok
+test bytes2/4bb09208::f[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/crypto/double.good b/crux-mir/test/symb_eval/crypto/double.good
@@ -1,3 +1,3 @@
-test double/e6e26f62::f[0]: ok
+test double/872a3d11::f[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/crypto/ffs.good b/crux-mir/test/symb_eval/crypto/ffs.good
@@ -1,3 +1,3 @@
-test ffs/12bb9465::f[0]: ok
+test ffs/fd27844b::f[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/enum/mux.good b/crux-mir/test/symb_eval/enum/mux.good
@@ -1,3 +1,3 @@
-test mux/e3e33eba::test[0]: ok
+test mux/48499f53::test[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/fnptr/mux.good b/crux-mir/test/symb_eval/fnptr/mux.good
@@ -1,3 +1,3 @@
-test mux/97bbb42d::crux_test[0]: returned 2, ok
+test mux/08dfe1f8::crux_test[0]: returned 2, ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/io/vec_write.good b/crux-mir/test/symb_eval/io/vec_write.good
@@ -1,3 +1,3 @@
-test vec_write/b46f4310::f[0]: ok
+test vec_write/ee788fed::f[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/mux/array.good b/crux-mir/test/symb_eval/mux/array.good
@@ -1,3 +1,3 @@
-test array/8d6b099f::crux_test[0]: returned Symbolic BV, ok
+test array/283f281e::crux_test[0]: returned Symbolic BV, ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/mux/array_mut.good b/crux-mir/test/symb_eval/mux/array_mut.good
@@ -1,3 +1,3 @@
-test array_mut/706b4322::crux_test[0]: returned Symbolic BV, ok
+test array_mut/78781ed1::crux_test[0]: returned Symbolic BV, ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir/test/symb_eval/num/checked_add.good b/crux-mir/test/symb_eval/num/checked_add.good
@@ -1,10 +1,10 @@
-test checked_add/b10d29cb::crux_test[0]: returned 44, FAILED
+test checked_add/00902a32::crux_test[0]: returned 44, FAILED
 
 failures:
 
----- checked_add/b10d29cb::crux_test[0] counterexamples ----
+---- checked_add/00902a32::crux_test[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux] test/symb_eval/num/checked_add.rs:6:5: 6:12: error: in checked_add/b10d29cb::crux_test[0]
+[Crux] test/symb_eval/num/checked_add.rs:6:5: 6:12: error: in checked_add/00902a32::crux_test[0]
 [Crux] attempt to compute `const 100_u8 + move _2`, which would overflow
 
 [Crux] Overall status: Invalid.