diff --git a/mldsa/mldsa_native.c b/mldsa/mldsa_native.c
index e20a82f2c..68f293305 100644
--- a/mldsa/mldsa_native.c
+++ b/mldsa/mldsa_native.c
@@ -252,7 +252,6 @@
 #undef MLD_NAMESPACE_KL
 #undef MLD_NAMESPACE_PREFIX
 #undef MLD_NAMESPACE_PREFIX_KL
-#undef MLD_UNION_OR_STRUCT
 #undef mld_memcpy
 #undef mld_memset
 /* mldsa/src/packing.h */
diff --git a/mldsa/mldsa_native.h b/mldsa/mldsa_native.h
index de2582d02..ce20056c8 100644
--- a/mldsa/mldsa_native.h
+++ b/mldsa/mldsa_native.h
@@ -913,20 +913,20 @@ int MLD_API_NAMESPACE(pk_from_sk)(
 /* check-magic: off */
 #if defined(MLD_API_LEGACY_CONFIG) || !defined(MLD_CONFIG_REDUCE_RAM)
 #define MLD_TOTAL_ALLOC_44_KEYPAIR_NO_PCT 41216
-#define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 56640
+#define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 48448
 #define MLD_TOTAL_ALLOC_44_PK_FROM_SK 45248
-#define MLD_TOTAL_ALLOC_44_SIGN 52896
-#define MLD_TOTAL_ALLOC_44_VERIFY 38816
+#define MLD_TOTAL_ALLOC_44_SIGN 44704
+#define MLD_TOTAL_ALLOC_44_VERIFY 34720
 #define MLD_TOTAL_ALLOC_65_KEYPAIR_NO_PCT 65792
-#define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 85856
+#define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 75616
 #define MLD_TOTAL_ALLOC_65_PK_FROM_SK 71872
-#define MLD_TOTAL_ALLOC_65_SIGN 80576
-#define MLD_TOTAL_ALLOC_65_VERIFY 62432
+#define MLD_TOTAL_ALLOC_65_SIGN 70336
+#define MLD_TOTAL_ALLOC_65_VERIFY 56288
 #define MLD_TOTAL_ALLOC_87_KEYPAIR_NO_PCT 104704
-#define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 130816
+#define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 116480
 #define MLD_TOTAL_ALLOC_87_PK_FROM_SK 112832
-#define MLD_TOTAL_ALLOC_87_SIGN 123584
-#define MLD_TOTAL_ALLOC_87_VERIFY 99552
+#define MLD_TOTAL_ALLOC_87_SIGN 109248
+#define MLD_TOTAL_ALLOC_87_VERIFY 91360
 #else /* MLD_API_LEGACY_CONFIG || !MLD_CONFIG_REDUCE_RAM */
 #define MLD_TOTAL_ALLOC_44_KEYPAIR_NO_PCT 28960
 #define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 28960
diff --git a/mldsa/mldsa_native_asm.S b/mldsa/mldsa_native_asm.S
index 36296bb5e..25fa78a29 100644
--- a/mldsa/mldsa_native_asm.S
+++ b/mldsa/mldsa_native_asm.S
@@ -255,7 +255,6 @@
 #undef MLD_NAMESPACE_KL
 #undef MLD_NAMESPACE_PREFIX
 #undef MLD_NAMESPACE_PREFIX_KL
-#undef MLD_UNION_OR_STRUCT
 #undef mld_memcpy
 #undef mld_memset
 /* mldsa/src/packing.h */
diff --git a/mldsa/src/common.h b/mldsa/src/common.h
index 899df9e3b..3dc8c33a0 100644
--- a/mldsa/src/common.h
+++ b/mldsa/src/common.h
@@ -290,19 +290,6 @@
 
 #endif /* MLD_CONFIG_CUSTOM_ALLOC_FREE */
 
-/*
- * We are facing severe CBMC performance issues when using unions.
- * As a temporary workaround, we use unions only when MLD_CONFIG_REDUCE_RAM is
- * set.
- * TODO: Remove the workaround once
- * https://github.com/diffblue/cbmc/issues/8813
- * is resolved
- */
-#if defined(MLD_CONFIG_REDUCE_RAM)
-#define MLD_UNION_OR_STRUCT union
-#else
-#define MLD_UNION_OR_STRUCT struct
-#endif
 
 /****************************** Error codes ***********************************/
 
diff --git a/mldsa/src/sign.c b/mldsa/src/sign.c
index 159ea7fbf..22fbf2c56 100644
--- a/mldsa/src/sign.c
+++ b/mldsa/src/sign.c
@@ -681,25 +681,19 @@ __contract__(
   unsigned int n;
   uint32_t w0_invalid, h_invalid;
   int ret;
-  /* TODO: Remove the following workaround for
-   * https://github.com/diffblue/cbmc/issues/8813 */
-  typedef MLD_UNION_OR_STRUCT
+  typedef union
   {
     mld_polyvecl y;
     mld_polyveck h;
-  }
-  yh_u;
+  } yh_u;
   mld_polyvecl *y;
   mld_polyveck *h;
 
-  /* TODO: Remove the following workaround for
-   * https://github.com/diffblue/cbmc/issues/8813 */
-  typedef MLD_UNION_OR_STRUCT
+  typedef union
   {
     mld_polyveck w1;
     mld_polyvecl tmp;
-  }
-  w1tmp_u;
+  } w1tmp_u;
   mld_polyveck *w1;
   mld_polyvecl *tmp;
 
@@ -1078,14 +1072,11 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen,
 {
   int ret, cmp;
 
-  /* TODO: Remove the following workaround for
-   * https://github.com/diffblue/cbmc/issues/8813 */
-  typedef MLD_UNION_OR_STRUCT
+  typedef union
   {
     mld_polyveck t1;
     mld_polyveck w1;
-  }
-  t1w1_u;
+  } t1w1_u;
   mld_polyveck *t1;
   mld_polyveck *w1;
 
diff --git a/nix/cbmc/0002-Do-not-download-sources-in-cmake.patch b/nix/cbmc/0002-Do-not-download-sources-in-cmake.patch
new file mode 100644
index 000000000..89456d8ae
--- /dev/null
+++ b/nix/cbmc/0002-Do-not-download-sources-in-cmake.patch
@@ -0,0 +1,53 @@
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+From c6b6438d3c87ce000b4e80b2eda2389e9473d24c Mon Sep 17 00:00:00 2001
+From: wxt <3264117476@qq.com>
+Date: Mon, 11 Nov 2024 11:35:03 +0800
+Subject: [PATCH] Do not download sources in cmake
+
+---
+ src/solvers/CMakeLists.txt | 9 +++------
+ 1 file changed, 3 insertions(+), 6 deletions(-)
+
+diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt
+index ab8d111..d7165e2 100644
+--- a/src/solvers/CMakeLists.txt
++++ b/src/solvers/CMakeLists.txt
+@@ -102,10 +102,9 @@ foreach(SOLVER ${sat_impl})
+         message(STATUS "Building solvers with glucose")
+
+         download_project(PROJ glucose
+-            URL https://github.com/BrunoDutertre/glucose-syrup/archive/0bb2afd3b9baace6981cbb8b4a1c7683c44968b7.tar.gz
++            SOURCE_DIR @srcglucose@
+             PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/glucose-syrup-patch
+             COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/scripts/glucose_CMakeLists.txt CMakeLists.txt
+-            URL_MD5 7c539c62c248b74210aef7414787323a
+         )
+
+         add_subdirectory(${glucose_SOURCE_DIR} ${glucose_BINARY_DIR})
+@@ -121,11 +120,10 @@ foreach(SOLVER ${sat_impl})
+         message(STATUS "Building solvers with cadical")
+
+         download_project(PROJ cadical
+-            URL https://github.com/arminbiere/cadical/archive/rel-3.0.0.tar.gz
++            SOURCE_DIR @srccadical@
+             PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-3.0.0-patch
+             COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/scripts/cadical_CMakeLists.txt CMakeLists.txt
+             COMMAND ./configure
+-            URL_HASH SHA256=282b1c9422fde8631cb721b86450ae94df4e8de0545c17a69a301aaa4bf92fcf
+         )
+
+         add_subdirectory(${cadical_SOURCE_DIR} ${cadical_BINARY_DIR})
+@@ -144,10 +142,9 @@ foreach(SOLVER ${sat_impl})
+         message(STATUS "Building with IPASIR solver linking against: CaDiCaL")
+
+         download_project(PROJ cadical
+-            URL https://github.com/arminbiere/cadical/archive/rel-3.0.0.tar.gz
++            SOURCE_DIR @srccadical@
+             PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-3.0.0-patch
+             COMMAND ./configure
+-            URL_HASH SHA256=282b1c9422fde8631cb721b86450ae94df4e8de0545c17a69a301aaa4bf92fcf
+         )
+
+         message(STATUS "Building CaDiCaL")
+--
+2.47.0
diff --git a/nix/cbmc/default.nix b/nix/cbmc/default.nix
index 4ff8db1a9..9665dca65 100644
--- a/nix/cbmc/default.nix
+++ b/nix/cbmc/default.nix
@@ -21,10 +21,18 @@ buildEnv {
       cbmc = cbmc.overrideAttrs (old: rec {
         version = "6.8.0";
         src = fetchFromGitHub {
-          owner = "diffblue";
+          owner = "tautschnig";
           repo = "cbmc";
-          hash = "sha256-PT6AYiwkplCeyMREZnGZA0BKl4ZESRC02/9ibKg7mYU=";
-          tag = "cbmc-6.8.0";
+          hash = "sha256-8ou+8ucabQy+IAfW/WeCU7Zv4u1uZknrMwtecY9UDcs=";
+          rev = "f2244fd6ea6068ba0493280942538bad9c0f2367";
+        };
+        srccadical = cadical.src; # 3.0.0 from nixpkgs-unstable
+        patches = [
+          (builtins.elemAt old.patches 0) # cudd patch from nixpkgs
+          ./0002-Do-not-download-sources-in-cmake.patch # cadical 3.0.0
+        ];
+        env = old.env // {
+          NIX_CFLAGS_COMPILE = (old.env.NIX_CFLAGS_COMPILE or "") + " -Wno-error=switch-enum";
         };
       });
       litani = callPackage ./litani.nix { }; # 1.29.0
@@ -40,7 +48,7 @@ buildEnv {
       });
 
       inherit
-        cadical# 2.2.0
+        cadical# 3.0.0
         bitwuzla# 0.8.2
         ninja; # 1.13.2
     };