diff --git a/libcrux/src/libcrux_hacl_glue.c b/libcrux/src/libcrux_hacl_glue.c
index 1df67914..471b3aff 100644
--- a/libcrux/src/libcrux_hacl_glue.c
+++ b/libcrux/src/libcrux_hacl_glue.c
@@ -1,15 +1,17 @@
 
+#include "libcrux_hacl_glue.h"
 #include "Hacl_Hash_SHA3_Scalar.h"
 #include "libcrux_kyber.h"
-#include "libcrux_hacl_glue.h"
 
 #ifdef HACL_CAN_COMPILE_VEC256
 #include "Hacl_Hash_SHA3_Simd256.h"
 #endif
 
-bool libcrux_platform_simd256_support(void) {
-    // TODO: Replace this with HACL platform support.
-    return false;
+bool
+libcrux_platform_simd256_support(void)
+{
+  // TODO: Replace this with HACL platform support.
+  return false;
 }
 
 inline void
@@ -31,21 +33,30 @@ libcrux_digest_shake128x4(size_t len,
                           Eurydice_slice input2,
                           Eurydice_slice input3)
 {
-#ifdef HACL_CAN_COMPILE_VEC256
-  Hacl_Hash_SHA3_Simd256_shake128(input0.len,
-                                  input0.ptr,
-                                  input1.ptr,
-                                  input2.ptr,
-                                  input3.ptr,
-                                  (uint32_t)len,
-                                  out);
-#else
   __uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t_
     out =
-      (__uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t_)
-  {
-    .fst = { 0 }, .snd = { 0 }, .thd = { 0 }, .f3 = { 0 }
-  };
+      (__uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t_){
+        .fst = { 0 }, .snd = { 0 }, .thd = { 0 }, .f3 = { 0 }
+      };
+#ifdef HACL_CAN_COMPILE_VEC256
+  if (libcrux_platform_simd256_support() == true) {
+    Hacl_SHA3_Vec256_shake128_vec256(input0.len,
+                                     input0.ptr,
+                                     input1.ptr,
+                                     input2.ptr,
+                                     input3.ptr,
+                                     (uint32_t)len,
+                                     out.fst,
+                                     out.snd,
+                                     out.thd,
+                                     out.f3);
+  } else {
+    Hacl_SHA3_shake128_hacl(input0.len, input0.ptr, (uint32_t)len, out.fst);
+    Hacl_SHA3_shake128_hacl(input1.len, input1.ptr, (uint32_t)len, out.snd);
+    Hacl_SHA3_shake128_hacl(input2.len, input2.ptr, (uint32_t)len, out.thd);
+    Hacl_SHA3_shake128_hacl(input3.len, input3.ptr, (uint32_t)len, out.f3);
+  }
+#else
   Hacl_Hash_SHA3_Scalar_shake128(
     input0.len, input0.ptr, (uint32_t)len, out.fst);
   Hacl_Hash_SHA3_Scalar_shake128(