diff --git a/libjade/crypto_kem/kyber_kyber768_avx2/kyber_kyber768_avx2.jazz b/libjade/crypto_kem/kyber_kyber768_avx2/kyber_kyber768_avx2.jazz
index 8323647..6ddd805 100644
--- a/libjade/crypto_kem/kyber_kyber768_avx2/kyber_kyber768_avx2.jazz
+++ b/libjade/crypto_kem/kyber_kyber768_avx2/kyber_kyber768_avx2.jazz
@@ -4769,7 +4769,11 @@ export fn jade_kem_kyber_kyber768_amd64_avx2_keypair(reg u64 public_key secret_k
 
   public_key = public_key;
   secret_key = secret_key;
-  stack_coins = #randombytes(stack_coins);
+  reg u64 num_bytes flag;
+  while {
+    flag = 0;
+    stack_coins, num_bytes = #randombytes(stack_coins, flag);
+  } (num_bytes != 2*KYBER_SYMBYTES)
   __crypto_kem_keypair_derand_jazz(public_key, secret_key, stack_coins);
   ?{}, r = #set0();
   return r;
@@ -4797,7 +4801,11 @@ export fn jade_kem_kyber_kyber768_amd64_avx2_enc(reg u64 ciphertext shared_secre
   ciphertext = ciphertext;
   shared_secret = shared_secret;
   public_key = public_key;
-  stack_coins = #randombytes(stack_coins);
+  reg u64 num_bytes flag;
+  while {
+    flag = 0;
+    stack_coins, num_bytes = #randombytes(stack_coins, flag);
+  } (num_bytes != KYBER_SYMBYTES)
   __crypto_kem_enc_derand_jazz(ciphertext, shared_secret, public_key, stack_coins);
   ?{}, r = #set0();
   return r;