diff --git a/nix/cbmc/default.nix b/nix/cbmc/default.nix
index c59aca03f..da51ae010 100644
--- a/nix/cbmc/default.nix
+++ b/nix/cbmc/default.nix
@@ -14,12 +14,12 @@ buildEnv {
   paths =
     builtins.attrValues {
       cbmc = cbmc.overrideAttrs (old: rec {
-        version = "6.4.1"; # remember to adjust this in ../flake.nix too
+        version = "d4757e2231b236ddd1d1933b4002a5aa4ca36db9"; # remember to adjust this in ../flake.nix too
         src = fetchFromGitHub {
-          owner = "diffblue";
+          owner = "remi-delmas-3000";
           repo = old.pname;
-          rev = "${old.pname}-${version}";
-          hash = "sha256-O8aZTW+Eylshl9bmm9GzbljWB0+cj2liZHs2uScERkM=";
+          rev = "contracts-obj-set--demonic";
+          hash = "sha256-FG6pTGlPpIwynsaMBgU1wdk7tZQllyImOKfHJjcjOJo";
         };
         patches = [
           ./0001-Do-not-download-sources-in-cmake.patch
diff --git a/proofs/cbmc/invntt_layer/Makefile b/proofs/cbmc/invntt_layer/Makefile
index fde0e1370..451209e78 100644
--- a/proofs/cbmc/invntt_layer/Makefile
+++ b/proofs/cbmc/invntt_layer/Makefile
@@ -27,6 +27,7 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
 
+CBMCFLAGS += --no-array-field-sensitivity --arrays-uf-always --slice-formula
 FUNCTION_NAME = invntt_layer
 
 # If this proof is found to consume huge amounts of RAM, you can set the