diff --git a/.github/workflows/cbmc-update.yml b/.github/workflows/cbmc-update.yml
index 74d9caeb0fcf..5fe8a866c0e4 100644
--- a/.github/workflows/cbmc-update.yml
+++ b/.github/workflows/cbmc-update.yml
@@ -30,7 +30,7 @@ jobs:
         env:
           GH_TOKEN: ${{ github.token }}
         run: |
-          grep ^CBMC_VERSION kani-dependencies >> $GITHUB_ENV
+          grep ^CBMC_VERSION kani-dependencies | sed 's/"//g' >> $GITHUB_ENV
           CBMC_LATEST=$(gh -R diffblue/cbmc release list | grep Latest | awk '{print $1}' | cut -f2 -d-)
           echo "CBMC_LATEST=$CBMC_LATEST" >> $GITHUB_ENV
           # check whether the version has changed at all
@@ -47,8 +47,8 @@ jobs:
           elif ! git ls-remote --exit-code origin cbmc-$CBMC_LATEST ; then
             CBMC_LATEST_MAJOR=$(echo $CBMC_LATEST | cut -f1 -d.)
             CBMC_LATEST_MINOR=$(echo $CBMC_LATEST | cut -f2 -d.)
-            sed -i "s/^CBMC_MAJOR=.*/CBMC_MAJOR=\"$CBMC_MAJOR\"/" kani-dependencies
-            sed -i "s/^CBMC_MINOR=.*/CBMC_MINOR=\"$CBMC_MINOR\"/" kani-dependencies
+            sed -i "s/^CBMC_MAJOR=.*/CBMC_MAJOR=\"$CBMC_LATEST_MAJOR\"/" kani-dependencies
+            sed -i "s/^CBMC_MINOR=.*/CBMC_MINOR=\"$CBMC_LATEST_MINOR\"/" kani-dependencies
             sed -i "s/^CBMC_VERSION=.*/CBMC_VERSION=\"$CBMC_LATEST\"/" kani-dependencies
             git diff
             if ! ./scripts/kani-regression.sh ; then
@@ -79,7 +79,7 @@ jobs:
           token: ${{ github.token }}
           title: 'CBMC upgrade to ${{ env.CBMC_LATEST }} failed'
           body: >
-            Updating CBMC from ${{ evn.CBMC_VERSION }} to ${{ env.CBMC_LATEST }} failed.
+            Updating CBMC from ${{ env.CBMC_VERSION }} to ${{ env.CBMC_LATEST }} failed.
 
             The failed automated run
             [can be found here.](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }})
diff --git a/.github/workflows/toolchain-upgrade.yml b/.github/workflows/toolchain-upgrade.yml
index 8252bfb826e6..a4b95ea195f0 100644
--- a/.github/workflows/toolchain-upgrade.yml
+++ b/.github/workflows/toolchain-upgrade.yml
@@ -30,42 +30,11 @@ jobs:
         env:
           GH_TOKEN: ${{ github.token }}
         run: |
-          current_toolchain_date=$(grep ^channel rust-toolchain.toml | sed 's/.*nightly-\(.*\)"/\1/')
-          echo "current_toolchain_date=$current_toolchain_date" >> $GITHUB_ENV
-          current_toolchain_epoch=$(date --date $current_toolchain_date +%s)
-          next_toolchain_date=$(date --date "@$(($current_toolchain_epoch + 86400))" +%Y-%m-%d)
-          echo "next_toolchain_date=$next_toolchain_date" >> $GITHUB_ENV
-          if gh issue list -S \
-              "Toolchain upgrade to nightly-$next_toolchain_date failed" \
-              --json number,title | grep title ; then
-            echo "next_step=none" >> $GITHUB_ENV
-          elif ! git ls-remote --exit-code origin toolchain-$next_toolchain_date ; then
-            echo "next_step=create_pr" >> $GITHUB_ENV
-            sed -i "/^channel/ s/$current_toolchain_date/$next_toolchain_date/" rust-toolchain.toml
-            git diff
-            git clone --filter=tree:0 https://github.com/rust-lang/rust rust.git
-            cd rust.git
-            current_toolchain_hash=$(curl https://static.rust-lang.org/dist/$current_toolchain_date/channel-rust-nightly-git-commit-hash.txt)
-            echo "current_toolchain_hash=$current_toolchain_hash" >> $GITHUB_ENV
-            next_toolchain_hash=$(curl https://static.rust-lang.org/dist/$next_toolchain_date/channel-rust-nightly-git-commit-hash.txt)
-            echo "next_toolchain_hash=$next_toolchain_hash" >> $GITHUB_ENV
-            EOF=$(dd if=/dev/urandom bs=15 count=1 status=none | base64)
-            echo "git_log<<$EOF" >> $GITHUB_ENV
-            git log --oneline $current_toolchain_hash..$next_toolchain_hash | \
-              sed 's#^#https://github.com/rust-lang/rust/commit/#' >> $GITHUB_ENV
-            echo "$EOF" >> $GITHUB_ENV
-            cd ..
-            rm -rf rust.git
-            if ! cargo build-dev ; then
-              echo "next_step=create_issue" >> $GITHUB_ENV
-            else
-              if ! ./scripts/kani-regression.sh ; then
-                echo "next_step=create_issue" >> $GITHUB_ENV
-              fi
-            fi
-          else
-            echo "next_step=none" >> $GITHUB_ENV
-          fi
+          source scripts/toolchain_update.sh
+
+      - name: Clean untracked files
+        run: git clean -f
+
       - name: Create Pull Request
         if: ${{ env.next_step == 'create_pr' }}
         uses: peter-evans/create-pull-request@v6
diff --git a/.gitignore b/.gitignore
index aae8f479aac9..a2defc0df119 100644
--- a/.gitignore
+++ b/.gitignore
@@ -48,6 +48,10 @@ no_llvm_build
 /tmp/
 # Created by default with `src/ci/docker/run.sh`
 /obj/
+# Created by kani-compiler
+*.rlib
+*.rmeta
+*.mir
 
 ## Temporary files
 *~
diff --git a/CHANGELOG.md b/CHANGELOG.md
index bd592b2f27a7..61e06601dfc3 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -4,6 +4,20 @@ This file contains notable changes (e.g. breaking changes, major changes, etc.)
 
 This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards.
 
+## [0.50.0]
+
+### Major Changes
+* Fix compilation issue with proc_macro2  (v1.0.80+) and Kani v0.49.0
+(https://github.com/model-checking/kani/issues/3138).
+
+### What's Changed
+* Implement valid value check for `write_bytes` by @celinval in
+https://github.com/model-checking/kani/pull/3108
+* Rust toolchain upgraded to 2024-04-15 by @tautschnig @celinval
+
+**Full Changelog**:
+https://github.com/model-checking/kani/compare/kani-0.49.0...kani-0.50.0
+
 ## [0.49.0]
 
 ### What's Changed
diff --git a/Cargo.lock b/Cargo.lock
index ae711d863430..627755fd91b3 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -73,9 +73,9 @@ dependencies = [
 
 [[package]]
 name = "anyhow"
-version = "1.0.81"
+version = "1.0.82"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0952808a6c2afd1aa8947271f3a60f1a6763c7b912d210184c5149b5cf147247"
+checksum = "f538837af36e6f6a9be0faa67f9a314f8119e4e4b5867c6ab40ed60360142519"
 
 [[package]]
 name = "autocfg"
@@ -97,7 +97,7 @@ checksum = "cf4b9d6a944f767f8e5e0db018570623c85f3d925ac718db4e06d0187adb21c1"
 
 [[package]]
 name = "build-kani"
-version = "0.49.0"
+version = "0.50.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
@@ -174,7 +174,7 @@ dependencies = [
  "heck 0.5.0",
  "proc-macro2",
  "quote",
- "syn 2.0.58",
+ "syn 2.0.60",
 ]
 
 [[package]]
@@ -233,7 +233,7 @@ dependencies = [
 
 [[package]]
 name = "cprover_bindings"
-version = "0.49.0"
+version = "0.50.0"
 dependencies = [
  "lazy_static",
  "linear-map",
@@ -295,9 +295,9 @@ dependencies = [
 
 [[package]]
 name = "either"
-version = "1.10.0"
+version = "1.11.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "11157ac094ffbdde99aa67b23417ebdd801842852b500e395a45a9c0aac03e4a"
+checksum = "a47c1c47d2f5964e29c61246e81db715514cd532db6b5116a25ea3c03d6780a2"
 
 [[package]]
 name = "encode_unicode"
@@ -338,9 +338,9 @@ dependencies = [
 
 [[package]]
 name = "getrandom"
-version = "0.2.13"
+version = "0.2.14"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a06fddc2749e0528d2813f95e050e87e52c8cbbae56223b9babf73b3e53b0cc6"
+checksum = "94b22e06ecb0110981051723910cbf0b5f5e09a2062dd7663334ee79a9d1286c"
 dependencies = [
  "cfg-if",
  "libc",
@@ -410,14 +410,14 @@ checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b"
 
 [[package]]
 name = "kani"
-version = "0.49.0"
+version = "0.50.0"
 dependencies = [
  "kani_macros",
 ]
 
 [[package]]
 name = "kani-compiler"
-version = "0.49.0"
+version = "0.50.0"
 dependencies = [
  "clap",
  "cprover_bindings",
@@ -438,7 +438,7 @@ dependencies = [
 
 [[package]]
 name = "kani-driver"
-version = "0.49.0"
+version = "0.50.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
@@ -466,7 +466,7 @@ dependencies = [
 
 [[package]]
 name = "kani-verifier"
-version = "0.49.0"
+version = "0.50.0"
 dependencies = [
  "anyhow",
  "home",
@@ -475,17 +475,17 @@ dependencies = [
 
 [[package]]
 name = "kani_macros"
-version = "0.49.0"
+version = "0.50.0"
 dependencies = [
  "proc-macro-error",
  "proc-macro2",
  "quote",
- "syn 2.0.58",
+ "syn 2.0.60",
 ]
 
 [[package]]
 name = "kani_metadata"
-version = "0.49.0"
+version = "0.50.0"
 dependencies = [
  "clap",
  "cprover_bindings",
@@ -571,9 +571,9 @@ dependencies = [
 
 [[package]]
 name = "num"
-version = "0.4.1"
+version = "0.4.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b05180d69e3da0e530ba2a1dae5110317e49e3b7f3d41be227dc5f92e49ee7af"
+checksum = "3135b08af27d103b0a51f2ae0f8632117b7b185ccf931445affa8df530576a41"
 dependencies = [
  "num-bigint",
  "num-complex",
@@ -733,18 +733,18 @@ dependencies = [
 
 [[package]]
 name = "proc-macro2"
-version = "1.0.79"
+version = "1.0.81"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e835ff2298f5721608eb1a980ecaee1aef2c132bf95ecc026a11b7bf3c01c02e"
+checksum = "3d1597b0c024618f09a9c3b8655b7e430397a36d23fdafec26d6965e9eec3eba"
 dependencies = [
  "unicode-ident",
 ]
 
 [[package]]
 name = "quote"
-version = "1.0.35"
+version = "1.0.36"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "291ec9ab5efd934aaf503a6466c5d5251535d108ee747472c3977cc5acc868ef"
+checksum = "0fa76aaf39101c457836aec0ce2316dbdc3ab723cdda1c6bd4e6ad4208acaca7"
 dependencies = [
  "proc-macro2",
 ]
@@ -860,9 +860,9 @@ checksum = "d626bb9dae77e28219937af045c257c28bfd3f69333c512553507f5f9798cb76"
 
 [[package]]
 name = "rustix"
-version = "0.38.32"
+version = "0.38.34"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "65e04861e65f21776e67888bfbea442b3642beaa0138fdb1dd7a84a52dffdb89"
+checksum = "70dc5ec042f7a43c4a73241207cecc9873a06d45debb38b329f8541d85c2730f"
 dependencies = [
  "bitflags 2.5.0",
  "errno",
@@ -909,29 +909,29 @@ dependencies = [
 
 [[package]]
 name = "serde"
-version = "1.0.197"
+version = "1.0.198"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3fb1c873e1b9b056a4dc4c0c198b24c3ffa059243875552b2bd0933b1aee4ce2"
+checksum = "9846a40c979031340571da2545a4e5b7c4163bdae79b301d5f86d03979451fcc"
 dependencies = [
  "serde_derive",
 ]
 
 [[package]]
 name = "serde_derive"
-version = "1.0.197"
+version = "1.0.198"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7eb0b34b42edc17f6b7cac84a52a1c5f0e1bb2227e997ca9011ea3dd34e8610b"
+checksum = "e88edab869b01783ba905e7d0153f9fc1a6505a96e4ad3018011eedb838566d9"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.58",
+ "syn 2.0.60",
 ]
 
 [[package]]
 name = "serde_json"
-version = "1.0.115"
+version = "1.0.116"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "12dc5c46daa8e9fdf4f5e71b6cf9a53f2487da0e86e55808e2d35539666497dd"
+checksum = "3e17db7126d17feb94eb3fad46bf1a96b034e8aacbc2e775fe81505f8b0b2813"
 dependencies = [
  "itoa",
  "ryu",
@@ -992,7 +992,7 @@ checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67"
 
 [[package]]
 name = "std"
-version = "0.49.0"
+version = "0.50.0"
 dependencies = [
  "kani",
 ]
@@ -1030,7 +1030,7 @@ dependencies = [
  "proc-macro2",
  "quote",
  "rustversion",
- "syn 2.0.58",
+ "syn 2.0.60",
 ]
 
 [[package]]
@@ -1045,9 +1045,9 @@ dependencies = [
 
 [[package]]
 name = "syn"
-version = "2.0.58"
+version = "2.0.60"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "44cfb93f38070beee36b3fef7d4f5a16f27751d94b187b666a5cc5e9b0d30687"
+checksum = "909518bc7b1c9b779f1bbf07f2929d35af9f0f37e47c6e9ef7f9dddc1e1821f3"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -1068,22 +1068,22 @@ dependencies = [
 
 [[package]]
 name = "thiserror"
-version = "1.0.58"
+version = "1.0.59"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "03468839009160513471e86a034bb2c5c0e4baae3b43f79ffc55c4a5427b3297"
+checksum = "f0126ad08bff79f29fc3ae6a55cc72352056dfff61e3ff8bb7129476d44b23aa"
 dependencies = [
  "thiserror-impl",
 ]
 
 [[package]]
 name = "thiserror-impl"
-version = "1.0.58"
+version = "1.0.59"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c61f3ba182994efc43764a46c018c347bc492c79f024e705f46567b418f6d4f7"
+checksum = "d1cd413b5d558b4c5bf3680e324a6fa5014e7b7c067a51e69dbdf47eb7148b66"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.58",
+ "syn 2.0.60",
 ]
 
 [[package]]
@@ -1119,9 +1119,9 @@ dependencies = [
 
 [[package]]
 name = "toml_edit"
-version = "0.22.9"
+version = "0.22.12"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8e40bb779c5187258fd7aad0eb68cb8706a0a81fa712fbea808ab43c4b8374c4"
+checksum = "d3328d4f68a705b2a4498da1d580585d39a6510f98318a2cec3018a7ec61ddef"
 dependencies = [
  "indexmap",
  "serde",
@@ -1149,7 +1149,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.58",
+ "syn 2.0.60",
 ]
 
 [[package]]
@@ -1315,7 +1315,7 @@ version = "0.52.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d"
 dependencies = [
- "windows-targets 0.52.4",
+ "windows-targets 0.52.5",
 ]
 
 [[package]]
@@ -1335,17 +1335,18 @@ dependencies = [
 
 [[package]]
 name = "windows-targets"
-version = "0.52.4"
+version = "0.52.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7dd37b7e5ab9018759f893a1952c9420d060016fc19a472b4bb20d1bdd694d1b"
+checksum = "6f0713a46559409d202e70e28227288446bf7841d3211583a4b53e3f6d96e7eb"
 dependencies = [
- "windows_aarch64_gnullvm 0.52.4",
- "windows_aarch64_msvc 0.52.4",
- "windows_i686_gnu 0.52.4",
- "windows_i686_msvc 0.52.4",
- "windows_x86_64_gnu 0.52.4",
- "windows_x86_64_gnullvm 0.52.4",
- "windows_x86_64_msvc 0.52.4",
+ "windows_aarch64_gnullvm 0.52.5",
+ "windows_aarch64_msvc 0.52.5",
+ "windows_i686_gnu 0.52.5",
+ "windows_i686_gnullvm",
+ "windows_i686_msvc 0.52.5",
+ "windows_x86_64_gnu 0.52.5",
+ "windows_x86_64_gnullvm 0.52.5",
+ "windows_x86_64_msvc 0.52.5",
 ]
 
 [[package]]
@@ -1356,9 +1357,9 @@ checksum = "2b38e32f0abccf9987a4e3079dfb67dcd799fb61361e53e2882c3cbaf0d905d8"
 
 [[package]]
 name = "windows_aarch64_gnullvm"
-version = "0.52.4"
+version = "0.52.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "bcf46cf4c365c6f2d1cc93ce535f2c8b244591df96ceee75d8e83deb70a9cac9"
+checksum = "7088eed71e8b8dda258ecc8bac5fb1153c5cffaf2578fc8ff5d61e23578d3263"
 
 [[package]]
 name = "windows_aarch64_msvc"
@@ -1368,9 +1369,9 @@ checksum = "dc35310971f3b2dbbf3f0690a219f40e2d9afcf64f9ab7cc1be722937c26b4bc"
 
 [[package]]
 name = "windows_aarch64_msvc"
-version = "0.52.4"
+version = "0.52.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "da9f259dd3bcf6990b55bffd094c4f7235817ba4ceebde8e6d11cd0c5633b675"
+checksum = "9985fd1504e250c615ca5f281c3f7a6da76213ebd5ccc9561496568a2752afb6"
 
 [[package]]
 name = "windows_i686_gnu"
@@ -1380,9 +1381,15 @@ checksum = "a75915e7def60c94dcef72200b9a8e58e5091744960da64ec734a6c6e9b3743e"
 
 [[package]]
 name = "windows_i686_gnu"
-version = "0.52.4"
+version = "0.52.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b474d8268f99e0995f25b9f095bc7434632601028cf86590aea5c8a5cb7801d3"
+checksum = "88ba073cf16d5372720ec942a8ccbf61626074c6d4dd2e745299726ce8b89670"
+
+[[package]]
+name = "windows_i686_gnullvm"
+version = "0.52.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "87f4261229030a858f36b459e748ae97545d6f1ec60e5e0d6a3d32e0dc232ee9"
 
 [[package]]
 name = "windows_i686_msvc"
@@ -1392,9 +1399,9 @@ checksum = "8f55c233f70c4b27f66c523580f78f1004e8b5a8b659e05a4eb49d4166cca406"
 
 [[package]]
 name = "windows_i686_msvc"
-version = "0.52.4"
+version = "0.52.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1515e9a29e5bed743cb4415a9ecf5dfca648ce85ee42e15873c3cd8610ff8e02"
+checksum = "db3c2bf3d13d5b658be73463284eaf12830ac9a26a90c717b7f771dfe97487bf"
 
 [[package]]
 name = "windows_x86_64_gnu"
@@ -1404,9 +1411,9 @@ checksum = "53d40abd2583d23e4718fddf1ebec84dbff8381c07cae67ff7768bbf19c6718e"
 
 [[package]]
 name = "windows_x86_64_gnu"
-version = "0.52.4"
+version = "0.52.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5eee091590e89cc02ad514ffe3ead9eb6b660aedca2183455434b93546371a03"
+checksum = "4e4246f76bdeff09eb48875a0fd3e2af6aada79d409d33011886d3e1581517d9"
 
 [[package]]
 name = "windows_x86_64_gnullvm"
@@ -1416,9 +1423,9 @@ checksum = "0b7b52767868a23d5bab768e390dc5f5c55825b6d30b86c844ff2dc7414044cc"
 
 [[package]]
 name = "windows_x86_64_gnullvm"
-version = "0.52.4"
+version = "0.52.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "77ca79f2451b49fa9e2af39f0747fe999fcda4f5e241b2898624dca97a1f2177"
+checksum = "852298e482cd67c356ddd9570386e2862b5673c85bd5f88df9ab6802b334c596"
 
 [[package]]
 name = "windows_x86_64_msvc"
@@ -1428,15 +1435,15 @@ checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538"
 
 [[package]]
 name = "windows_x86_64_msvc"
-version = "0.52.4"
+version = "0.52.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "32b752e52a2da0ddfbdbcc6fceadfeede4c939ed16d13e648833a61dfb611ed8"
+checksum = "bec47e5bfd1bff0eeaf6d8b485cc1074891a197ab4225d504cb7a1ab88b02bf0"
 
 [[package]]
 name = "winnow"
-version = "0.6.5"
+version = "0.6.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "dffa400e67ed5a4dd237983829e66475f0a4a26938c4b04c21baede6262215b8"
+checksum = "f0c976aaaa0e1f90dbb21e9587cdaf1d9679a1cde8875c0d6bd83ab96a208352"
 dependencies = [
  "memchr",
 ]
@@ -1464,5 +1471,5 @@ checksum = "9ce1b18ccd8e73a9321186f97e46f9f04b778851177567b1975109d26a08d2a6"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.58",
+ "syn 2.0.60",
 ]
diff --git a/Cargo.toml b/Cargo.toml
index e271a3650c03..93affb02856f 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-verifier"
-version = "0.49.0"
+version = "0.50.0"
 edition = "2021"
 description = "A bit-precise model checker for Rust."
 readme = "README.md"
diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml
index ed0e57847e71..d199558ff16a 100644
--- a/cprover_bindings/Cargo.toml
+++ b/cprover_bindings/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "cprover_bindings"
-version = "0.49.0"
+version = "0.50.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs
index 28f8afb4fae7..9f97e7a0a599 100644
--- a/cprover_bindings/src/goto_program/expr.rs
+++ b/cprover_bindings/src/goto_program/expr.rs
@@ -389,6 +389,7 @@ impl Expr {
             source.is_integer() || source.is_pointer() || source.is_bool()
         } else if target.is_integer() {
             source.is_c_bool()
+                || source.is_bool()
                 || source.is_integer()
                 || source.is_floating_point()
                 || source.is_pointer()
diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml
index ffc508e90866..244172715056 100644
--- a/kani-compiler/Cargo.toml
+++ b/kani-compiler/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-compiler"
-version = "0.49.0"
+version = "0.50.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
index a16dd616e7c0..9e785910ea0f 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -292,6 +292,11 @@ impl<'tcx> GotocCtx<'tcx> {
                             "element of {parent_ty:?} is not accessed via field projection"
                         )
                     }
+                    TyKind::RigidTy(RigidTy::Pat(..)) => {
+                        // See https://github.com/rust-lang/types-team/issues/126
+                        // for what is currently supported.
+                        unreachable!("projection inside a pattern is not supported, only transmute")
+                    }
                 }
             }
             // if we fall here, then we are handling an enum
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index 74622d41ed50..cb78163fe99b 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -20,6 +20,7 @@ use num::bigint::BigInt;
 use rustc_middle::ty::{TyCtxt, VtblEntry};
 use rustc_smir::rustc_internal;
 use rustc_target::abi::{FieldsShape, TagEncoding, Variants};
+use stable_mir::abi::{Primitive, Scalar, ValueAbi};
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{
     AggregateKind, BinOp, CastKind, NullOp, Operand, Place, PointerCoercion, Rvalue, UnOp,
@@ -32,9 +33,11 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_comparison(&mut self, op: &BinOp, e1: &Operand, e2: &Operand) -> Expr {
         let left_op = self.codegen_operand_stable(e1);
         let right_op = self.codegen_operand_stable(e2);
-        let is_float =
-            matches!(self.operand_ty_stable(e1).kind(), TyKind::RigidTy(RigidTy::Float(..)));
-        comparison_expr(op, left_op, right_op, is_float)
+        let left_ty = self.operand_ty_stable(e1);
+        let right_ty = self.operand_ty_stable(e2);
+        let res_ty = op.ty(left_ty, right_ty);
+        let is_float = matches!(left_ty.kind(), TyKind::RigidTy(RigidTy::Float(..)));
+        self.comparison_expr(op, left_op, right_op, res_ty, is_float)
     }
 
     /// This function codegen comparison for fat pointers.
@@ -72,16 +75,18 @@ impl<'tcx> GotocCtx<'tcx> {
             Expr::statement_expression(body, ret_type).with_location(loc)
         } else {
             // Compare data pointer.
+            let res_ty = op.ty(left_typ, right_typ);
             let left_ptr = self.codegen_operand_stable(left_op);
             let left_data = left_ptr.clone().member("data", &self.symbol_table);
             let right_ptr = self.codegen_operand_stable(right_op);
             let right_data = right_ptr.clone().member("data", &self.symbol_table);
-            let data_cmp = comparison_expr(op, left_data.clone(), right_data.clone(), false);
+            let data_cmp =
+                self.comparison_expr(op, left_data.clone(), right_data.clone(), res_ty, false);
 
             // Compare the slice metadata (this logic could be adapted to compare vtable if needed).
             let left_len = left_ptr.member("len", &self.symbol_table);
             let right_len = right_ptr.member("len", &self.symbol_table);
-            let metadata_cmp = comparison_expr(op, left_len, right_len, false);
+            let metadata_cmp = self.comparison_expr(op, left_len, right_len, res_ty, false);
 
             // Join the results.
             // https://github.com/rust-lang/rust/pull/29781
@@ -93,10 +98,20 @@ impl<'tcx> GotocCtx<'tcx> {
                 // If data is different, only compare data.
                 // If data is equal, apply operator to metadata.
                 BinOp::Lt | BinOp::Le | BinOp::Ge | BinOp::Gt => {
-                    let data_eq =
-                        comparison_expr(&BinOp::Eq, left_data.clone(), right_data.clone(), false);
-                    let data_strict_comp =
-                        comparison_expr(&get_strict_operator(op), left_data, right_data, false);
+                    let data_eq = self.comparison_expr(
+                        &BinOp::Eq,
+                        left_data.clone(),
+                        right_data.clone(),
+                        res_ty,
+                        false,
+                    );
+                    let data_strict_comp = self.comparison_expr(
+                        &get_strict_operator(op),
+                        left_data,
+                        right_data,
+                        res_ty,
+                        false,
+                    );
                     data_strict_comp.or(data_eq.and(metadata_cmp))
                 }
                 _ => unreachable!("Unexpected operator {:?}", op),
@@ -376,7 +391,7 @@ impl<'tcx> GotocCtx<'tcx> {
             BinOp::BitXor | BinOp::BitAnd | BinOp::BitOr => {
                 self.codegen_unchecked_scalar_binop(op, e1, e2)
             }
-            BinOp::Eq | BinOp::Lt | BinOp::Le | BinOp::Ne | BinOp::Ge | BinOp::Gt => {
+            BinOp::Eq | BinOp::Lt | BinOp::Le | BinOp::Ne | BinOp::Ge | BinOp::Gt | BinOp::Cmp => {
                 let op_ty = self.operand_ty_stable(e1);
                 if self.is_fat_pointer_stable(op_ty) {
                     self.codegen_comparison_fat_ptr(op, e1, e2, loc)
@@ -681,7 +696,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 | CastKind::FnPtrToPtr
                 | CastKind::PtrToPtr
                 | CastKind::PointerExposeAddress
-                | CastKind::PointerFromExposedAddress,
+                | CastKind::PointerWithExposedProvenance,
                 e,
                 t,
             ) => self.codegen_misc_cast(e, *t),
@@ -1260,7 +1275,7 @@ impl<'tcx> GotocCtx<'tcx> {
     fn check_vtable_size(&mut self, operand_type: Ty, vt_size: Expr) -> Stmt {
         // Check against the size we get from the layout from the what we
         // get constructing a value of that type
-        let ty: Type = self.codegen_ty_stable(operand_type);
+        let ty = self.codegen_ty_stable(operand_type);
         let codegen_size = ty.sizeof(&self.symbol_table);
         assert_eq!(vt_size.int_constant_value().unwrap(), BigInt::from(codegen_size));
 
@@ -1423,6 +1438,65 @@ impl<'tcx> GotocCtx<'tcx> {
             }
         }
     }
+
+    fn comparison_expr(
+        &mut self,
+        op: &BinOp,
+        left: Expr,
+        right: Expr,
+        res_ty: Ty,
+        is_float: bool,
+    ) -> Expr {
+        match op {
+            BinOp::Eq => {
+                if is_float {
+                    left.feq(right)
+                } else {
+                    left.eq(right)
+                }
+            }
+            BinOp::Lt => left.lt(right),
+            BinOp::Le => left.le(right),
+            BinOp::Ne => {
+                if is_float {
+                    left.fneq(right)
+                } else {
+                    left.neq(right)
+                }
+            }
+            BinOp::Ge => left.ge(right),
+            BinOp::Gt => left.gt(right),
+            BinOp::Cmp => {
+                // Implement https://doc.rust-lang.org/core/cmp/trait.Ord.html as done in cranelift,
+                // i.e., (left > right) - (left < right)
+                // Return value is the Ordering enumeration:
+                // ```
+                // #[repr(i8)]
+                // pub enum Ordering {
+                //     Less = -1,
+                //     Equal = 0,
+                //     Greater = 1,
+                // }
+                // ```
+                let res_typ = self.codegen_ty_stable(res_ty);
+                let ValueAbi::Scalar(Scalar::Initialized { value, valid_range }) =
+                    res_ty.layout().unwrap().shape().abi
+                else {
+                    unreachable!("Unexpected layout")
+                };
+                assert_eq!(valid_range.start, -1i8 as u8 as u128);
+                assert_eq!(valid_range.end, 1);
+                let Primitive::Int { length, signed: true } = value else { unreachable!() };
+                let scalar_typ = Type::signed_int(length.bits());
+                left.clone()
+                    .gt(right.clone())
+                    .cast_to(scalar_typ.clone())
+                    .sub(left.lt(right).cast_to(scalar_typ))
+                    .transmute_to(res_typ, &self.symbol_table)
+            }
+            _ => unreachable!(),
+        }
+    }
 }
 
 /// Perform a wrapping subtraction of an Expr with a constant "expr - constant"
@@ -1445,30 +1519,6 @@ fn wrapping_sub(expr: &Expr, constant: u64) -> Expr {
     }
 }
 
-fn comparison_expr(op: &BinOp, left: Expr, right: Expr, is_float: bool) -> Expr {
-    match op {
-        BinOp::Eq => {
-            if is_float {
-                left.feq(right)
-            } else {
-                left.eq(right)
-            }
-        }
-        BinOp::Lt => left.lt(right),
-        BinOp::Le => left.le(right),
-        BinOp::Ne => {
-            if is_float {
-                left.fneq(right)
-            } else {
-                left.neq(right)
-            }
-        }
-        BinOp::Ge => left.ge(right),
-        BinOp::Gt => left.gt(right),
-        _ => unreachable!(),
-    }
-}
-
 /// Remove the equality from an operator. Translates `<=` to `<` and `>=` to `>`
 fn get_strict_operator(op: &BinOp) -> BinOp {
     match op {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index b5ccf1a83716..64c36dd76cfb 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -595,6 +595,13 @@ impl<'tcx> GotocCtx<'tcx> {
                     )
                 }
             }
+            // This object has the same layout as base. For now, translate this into `(base)`.
+            // The only difference is the niche.
+            ty::Pat(base_ty, ..) => {
+                self.ensure_struct(self.ty_mangled_name(ty), self.ty_pretty_name(ty), |tcx, _| {
+                    tcx.codegen_ty_tuple_like(ty, vec![*base_ty])
+                })
+            }
             ty::Alias(..) => {
                 unreachable!("Type should've been normalized already")
             }
@@ -995,6 +1002,7 @@ impl<'tcx> GotocCtx<'tcx> {
             | ty::Int(_)
             | ty::RawPtr(_, _)
             | ty::Ref(..)
+            | ty::Pat(..)
             | ty::Tuple(_)
             | ty::Uint(_) => self.codegen_ty(pointee_type).to_pointer(),
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
index 3a6501d544d8..095f907228a4 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
@@ -137,7 +137,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
     // Generate a Symbol Expression representing a function variable from the MIR
     pub fn gen_function_local_variable(&mut self, c: u64, fname: &str, t: Type) -> Symbol {
-        self.gen_stack_variable(c, fname, "var", t, Location::none(), false)
+        self.gen_stack_variable(c, fname, "var", t, Location::none())
     }
 
     /// Given a counter `c` a function name `fname, and a prefix `prefix`, generates a new function local variable
@@ -149,11 +149,10 @@ impl<'tcx> GotocCtx<'tcx> {
         prefix: &str,
         t: Type,
         loc: Location,
-        is_param: bool,
     ) -> Symbol {
         let base_name = format!("{prefix}_{c}");
         let name = format!("{fname}::1::{base_name}");
-        let symbol = Symbol::variable(name, base_name, t, loc).with_is_parameter(is_param);
+        let symbol = Symbol::variable(name, base_name, t, loc);
         self.symbol_table.insert(symbol.clone());
         symbol
     }
@@ -167,8 +166,7 @@ impl<'tcx> GotocCtx<'tcx> {
         loc: Location,
     ) -> (Expr, Stmt) {
         let c = self.current_fn_mut().get_and_incr_counter();
-        let var =
-            self.gen_stack_variable(c, &self.current_fn().name(), "temp", t, loc, false).to_expr();
+        let var = self.gen_stack_variable(c, &self.current_fn().name(), "temp", t, loc).to_expr();
         let value = value.or_else(|| self.codegen_default_initializer(&var));
         let decl = Stmt::decl(var.clone(), value, loc);
         (var, decl)
diff --git a/kani-compiler/src/kani_middle/stubbing/annotations.rs b/kani-compiler/src/kani_middle/stubbing/annotations.rs
index 52b994ab97d2..26e508707207 100644
--- a/kani-compiler/src/kani_middle/stubbing/annotations.rs
+++ b/kani-compiler/src/kani_middle/stubbing/annotations.rs
@@ -56,7 +56,7 @@ pub fn update_stub_mapping(
                         "duplicate stub mapping: {} mapped to {} and {}",
                         tcx.def_path_str(orig_id),
                         tcx.def_path_str(stub_id),
-                        tcx.def_path_str(tcx.def_path_hash_to_def_id(other, &mut || panic!()))
+                        tcx.def_path_str(tcx.def_path_hash_to_def_id(other, &()))
                     ),
                 );
             }
diff --git a/kani-compiler/src/kani_middle/stubbing/transform.rs b/kani-compiler/src/kani_middle/stubbing/transform.rs
index 16c46990bc6f..f101a6009907 100644
--- a/kani-compiler/src/kani_middle/stubbing/transform.rs
+++ b/kani-compiler/src/kani_middle/stubbing/transform.rs
@@ -234,7 +234,7 @@ fn deserialize_mapping(tcx: TyCtxt, val: &str) -> HashMap<DefId, DefId> {
     type Item = (u64, u64);
     let item_to_def_id = |item: Item| -> DefId {
         let hash = DefPathHash(Fingerprint::new(item.0, item.1));
-        tcx.def_path_hash_to_def_id(hash, &mut || panic!())
+        tcx.def_path_hash_to_def_id(hash, &())
     };
     let pairs: Vec<(Item, Item)> = serde_json::from_str(val).unwrap();
     let mut m = HashMap::default();
diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs
index a620dfabb72e..d62b5807319e 100644
--- a/kani-compiler/src/kani_middle/transform/check_values.rs
+++ b/kani-compiler/src/kani_middle/transform/check_values.rs
@@ -631,7 +631,7 @@ impl<'a> MirVisitor for CheckValueVisitor<'a> {
                     ty: (rvalue.ty(self.locals).unwrap()),
                 }),
                 CastKind::PointerExposeAddress
-                | CastKind::PointerFromExposedAddress
+                | CastKind::PointerWithExposedProvenance
                 | CastKind::PointerCoercion(_)
                 | CastKind::IntToInt
                 | CastKind::FloatToInt
@@ -898,6 +898,12 @@ fn ty_validity_per_offset(
                         }
                     }
                 }
+                RigidTy::Pat(base_ty, ..) => {
+                    // This is similar to a structure with one field and with niche defined.
+                    let mut pat_validity = ty_req();
+                    pat_validity.append(&mut ty_validity_per_offset(machine_info, *base_ty, 0)?);
+                    Ok(pat_validity)
+                }
                 RigidTy::Tuple(tys) => {
                     let mut tuple_validity = vec![];
                     for idx in layout.fields.fields_by_offset_order() {
diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml
index 3a476922a838..ab83c2202bc9 100644
--- a/kani-driver/Cargo.toml
+++ b/kani-driver/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-driver"
-version = "0.49.0"
+version = "0.50.0"
 edition = "2021"
 description = "Build a project with Kani and run all proof harnesses"
 license = "MIT OR Apache-2.0"
diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml
index 582c20c7bd9f..7936d943556b 100644
--- a/kani_metadata/Cargo.toml
+++ b/kani_metadata/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani_metadata"
-version = "0.49.0"
+version = "0.50.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml
index b87536740fcd..97952dd7ab9e 100644
--- a/library/kani/Cargo.toml
+++ b/library/kani/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani"
-version = "0.49.0"
+version = "0.50.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs
index 203eae2229c4..43062ebed6a1 100644
--- a/library/kani/src/mem.rs
+++ b/library/kani/src/mem.rs
@@ -44,7 +44,7 @@ use std::ptr::{DynMetadata, NonNull, Pointee};
 /// Note that an unaligned pointer is still considered valid.
 ///
 /// TODO: Kani should automatically add those checks when a de-reference happens.
-/// https://github.com/model-checking/kani/issues/2975
+/// <https://github.com/model-checking/kani/issues/2975>
 ///
 /// This function will either panic or return `true`. This is to make it easier to use it in
 /// contracts.
diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml
index fe4279fc4366..a54fb44d8b6c 100644
--- a/library/kani_macros/Cargo.toml
+++ b/library/kani_macros/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani_macros"
-version = "0.49.0"
+version = "0.50.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml
index 05f5b4de5635..6f9a380fc584 100644
--- a/library/std/Cargo.toml
+++ b/library/std/Cargo.toml
@@ -5,7 +5,7 @@
 # Note: this package is intentionally named std to make sure the names of
 # standard library symbols are preserved
 name = "std"
-version = "0.49.0"
+version = "0.50.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/rfc/src/rfcs/0003-cover-statement.md b/rfc/src/rfcs/0003-cover-statement.md
index 6839af22f929..de452654392b 100644
--- a/rfc/src/rfcs/0003-cover-statement.md
+++ b/rfc/src/rfcs/0003-cover-statement.md
@@ -1,8 +1,8 @@
 - **Feature Name:** Cover statement (`cover-statement`)
 - **Feature Request Issue:** <https://github.com/model-checking/kani/issues/696>
 - **RFC PR:** <https://github.com/model-checking/kani/pull/1906>
-- **Status:** Unstable
-- **Version:** 1
+- **Status:** Stable
+- **Version:** 2
 
 -------------------
 
@@ -138,8 +138,12 @@ However, if the condition can indeed be covered, verification would fail due to
 
 ## Open questions
 
-Should we allow format arguments in the macro, e.g. `kani::cover!(x > y, "{} can be greater than {}", x, y)`?
-Users may expect this to be supported since the macro looks similar to the `assert` macro, but Kani doesn't include the formatted string in the message description, since it's not available at compile time.
+- ~Should we allow format arguments in the macro, e.g. `kani::cover!(x > y, "{} can be greater than {}", x, y)`?
+Users may expect this to be supported since the macro looks similar to the `assert` macro, but Kani doesn't include the formatted string in the message description, since it's not available at compile time.~
+  - For now, this macro will not accept format arguments, since this
+    is not well handled by Kani.
+    This is an extesion to this API that can be easily added later on if Kani
+    ever supports runtime formatting.
 
 ## Other Considerations
 
diff --git a/rfc/src/rfcs/0009-function-contracts.md b/rfc/src/rfcs/0009-function-contracts.md
index e26592080822..dae805a7db72 100644
--- a/rfc/src/rfcs/0009-function-contracts.md
+++ b/rfc/src/rfcs/0009-function-contracts.md
@@ -1,8 +1,8 @@
 - **Feature Name:** Function Contracts
 - **Feature Request Issue:** [#2652](https://github.com/model-checking/kani/issues/2652) and [Milestone](https://github.com/model-checking/kani/milestone/31)
 - **RFC PR:** [#2620](https://github.com/model-checking/kani/pull/2620)
-- **Status:** Under Review 
-- **Version:** 0
+- **Status:** Unstable
+- **Version:** 1
 - **Proof-of-concept:** [features/contracts](https://github.com/model-checking/kani/tree/features/contracts)
 - **Feature Gate:** `-Zfunction-contracts`, enforced by compile time error[^gate]
 
@@ -893,4 +893,5 @@ times larger than what they expect the function will touch).
 
 [^stubcheck]: Kani cannot report the occurrence of a contract function to check
     in abstracted functions as errors, because the mechanism is needed to verify
-    mutually recursive functions.
\ No newline at end of file
+    mutually recursive functions.
+
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 1ee76e0f92f1..70848743b686 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-04-02"
+channel = "nightly-2024-04-21"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/scripts/build-docs.sh b/scripts/build-docs.sh
index cd40a2edabad..2e2c10b052f6 100755
--- a/scripts/build-docs.sh
+++ b/scripts/build-docs.sh
@@ -28,8 +28,10 @@ else
       curl -sSL -o "$FILE" "$URL"
       echo "$EXPECTED_HASH $FILE" | sha256sum -c -
       tar zxf $FILE
+      MDBOOK=${SCRIPT_DIR}/mdbook
+  else
+      MDBOOK=mdbook
   fi
-  MDBOOK=${SCRIPT_DIR}/mdbook
 fi
 
 KANI_DIR=$SCRIPT_DIR/..
diff --git a/scripts/toolchain_update.sh b/scripts/toolchain_update.sh
new file mode 100755
index 000000000000..856c346e542c
--- /dev/null
+++ b/scripts/toolchain_update.sh
@@ -0,0 +1,65 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# This script is part of our CI nightly job to bump the toolchain version.
+# It will potentially update the rust-toolchain.toml file, and run the
+# regression.
+#
+# In order to manually run this script, you will need to do the following:
+#
+# 1. Set $GITHUB_ENV to point to an output file.
+# 2. Install and configure GitHub CLI
+
+set -eu
+
+current_toolchain_date=$(grep ^channel rust-toolchain.toml | sed 's/.*nightly-\(.*\)"/\1/')
+echo "current_toolchain_date=$current_toolchain_date" >> $GITHUB_ENV
+
+current_toolchain_epoch=$(date --date $current_toolchain_date +%s)
+next_toolchain_date=$(date --date "@$(($current_toolchain_epoch + 86400))" +%Y-%m-%d)
+echo "next_toolchain_date=$next_toolchain_date" >> $GITHUB_ENV
+
+echo "------ Start upgrade ------"
+echo "- current: ${current_toolchain_date}"
+echo "- next: ${next_toolchain_date}"
+echo "---------------------------"
+
+if gh issue list -S \
+  "Toolchain upgrade to nightly-$next_toolchain_date failed" \
+  --json number,title | grep title
+then
+  echo "Skip update: Found existing issue"
+  echo "next_step=none" >> $GITHUB_ENV
+elif ! git ls-remote --exit-code origin toolchain-$next_toolchain_date
+then
+  echo "next_step=create_pr" >> $GITHUB_ENV
+
+  # Modify rust-toolchain file
+  sed -i "/^channel/ s/$current_toolchain_date/$next_toolchain_date/" rust-toolchain.toml
+
+  git diff
+  git clone --filter=tree:0 https://github.com/rust-lang/rust rust.git
+  cd rust.git
+  current_toolchain_hash=$(curl https://static.rust-lang.org/dist/$current_toolchain_date/channel-rust-nightly-git-commit-hash.txt)
+  echo "current_toolchain_hash=$current_toolchain_hash" >> $GITHUB_ENV
+
+  next_toolchain_hash=$(curl https://static.rust-lang.org/dist/$next_toolchain_date/channel-rust-nightly-git-commit-hash.txt)
+  echo "next_toolchain_hash=$next_toolchain_hash" >> $GITHUB_ENV
+
+  EOF=$(dd if=/dev/urandom bs=15 count=1 status=none | base64)
+  echo "git_log<<$EOF" >> $GITHUB_ENV
+
+  git log --oneline $current_toolchain_hash..$next_toolchain_hash | \
+    sed 's#^#https://github.com/rust-lang/rust/commit/#' >> $GITHUB_ENV
+  echo "$EOF" >> $GITHUB_ENV
+
+  cd ..
+  rm -rf rust.git
+  if ! ./scripts/kani-regression.sh ; then
+    echo "next_step=create_issue" >> $GITHUB_ENV
+  fi
+else
+  echo "Skip update: Found existing branch"
+  echo "next_step=none" >> $GITHUB_ENV
+fi
diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic
index 2d5e891f3fdc..9730578c0d56 160000
--- a/tests/perf/s2n-quic
+++ b/tests/perf/s2n-quic
@@ -1 +1 @@
-Subproject commit 2d5e891f3fdc8a88b2d457baceedea5751efaa0d
+Subproject commit 9730578c0d562d80bbbe663161b3a5408ed3116c
diff --git a/tools/benchcomp/benchcomp/visualizers/__init__.py b/tools/benchcomp/benchcomp/visualizers/__init__.py
index 8de4a9f130b6..1452488c76b1 100644
--- a/tools/benchcomp/benchcomp/visualizers/__init__.py
+++ b/tools/benchcomp/benchcomp/visualizers/__init__.py
@@ -358,7 +358,20 @@ def _add_extra_columns(self, metrics):
             for bench, variants in benches.items():
                 tmp_variants = dict(variants)
                 for column in columns:
-                    variants[column["column_name"]] = column["text"](tmp_variants)
+                    if "column_name" not in column:
+                        logging.error(
+                            "A column specification for metric %s did not "
+                            "contain a column_name field. Each column should "
+                            "have a column name and column text", metric)
+                        sys.exit(1)
+                    try:
+                        variants[column["column_name"]] = column["text"](tmp_variants)
+                    except BaseException:
+                        # This may be reached when evaluating the column text
+                        # throws an exception. The column text is written in a
+                        # YAML file and is typically a simple lambda so can't
+                        # contain sophisticated error handling.
+                        variants[column["column_name"]] = "**ERROR**"
 
 
     @staticmethod
diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml
index 525c060232a7..eabb396e0923 100644
--- a/tools/build-kani/Cargo.toml
+++ b/tools/build-kani/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "build-kani"
-version = "0.49.0"
+version = "0.50.0"
 edition = "2021"
 description = "Builds Kani, Sysroot and release bundle."
 license = "MIT OR Apache-2.0"