diff --git a/proofs/cbmc/poly_permute_bitrev_to_custom/poly_permute_bitrev_to_custom_harness.c b/proofs/cbmc/poly_permute_bitrev_to_custom/poly_permute_bitrev_to_custom_harness.c
index 21b726faa..c28158531 100644
--- a/proofs/cbmc/poly_permute_bitrev_to_custom/poly_permute_bitrev_to_custom_harness.c
+++ b/proofs/cbmc/poly_permute_bitrev_to_custom/poly_permute_bitrev_to_custom_harness.c
@@ -9,6 +9,6 @@ void mlk_poly_permute_bitrev_to_custom(int16_t data[MLKEM_N]);
 
 void harness(void)
 {
-  int16_t data[MLKEM_N];
+  int16_t *data;
   mlk_poly_permute_bitrev_to_custom(data);
 }
diff --git a/proofs/cbmc/poly_rej_uniform_x4/poly_rej_uniform_x4_harness.c b/proofs/cbmc/poly_rej_uniform_x4/poly_rej_uniform_x4_harness.c
index 847d2f80a..19a45b175 100644
--- a/proofs/cbmc/poly_rej_uniform_x4/poly_rej_uniform_x4_harness.c
+++ b/proofs/cbmc/poly_rej_uniform_x4/poly_rej_uniform_x4_harness.c
@@ -7,7 +7,7 @@
 
 void harness(void)
 {
-  mlk_poly out[4];
-  uint8_t seed[4][MLK_ALIGN_UP(MLKEM_SYMBYTES + 2)];
+  mlk_poly *out;
+  uint8_t(*seed)[MLK_ALIGN_UP(MLKEM_SYMBYTES + 2)];
   mlk_poly_rej_uniform_x4(out, seed);
 }