diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index d8cb0fc2bb2d..5d4b5b9a4e0d 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -31,27 +31,6 @@ jobs:
       - name: Execute Kani regression
         run: ./scripts/kani-regression.sh
 
-  write-json-symtab-regression:
-    runs-on: ubuntu-20.04
-    steps:
-      - name: Checkout Kani
-        uses: actions/checkout@v4
-
-      - name: Setup Kani Dependencies
-        uses: ./.github/actions/setup
-        with:
-          os: ubuntu-20.04
-
-      - name: Build Kani
-        run: cargo build-dev -- --features write_json_symtab
-
-      - name: Run tests
-        run: |
-          cargo run -p compiletest --quiet -- --suite kani --mode kani --quiet --no-fail-fast
-          cargo run -p compiletest --quiet -- --suite expected --mode expected --quiet --no-fail-fast
-          cargo run -p compiletest --quiet -- --suite cargo-kani --mode cargo-kani --quiet --no-fail-fast
-
-
   benchcomp-tests:
     runs-on: ubuntu-20.04
     steps:
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index ad2e339f19e1..36aee463061a 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -272,7 +272,7 @@ jobs:
       - name: Run tests
         # TODO: Customize compiletest to run custom kani. For now, just run a few cargo kani tests.
         run: |
-          for dir in simple-lib simple-visualize build-rs-works simple-kissat; do
+          for dir in simple-lib build-rs-works simple-kissat; do
             >&2 echo "Running test $dir"
             pushd tests/cargo-kani/$dir
             cargo kani
@@ -312,7 +312,7 @@ jobs:
 
       - name: Run installed tests
         run: |
-          for dir in simple-lib simple-visualize build-rs-works simple-kissat; do
+          for dir in simple-lib build-rs-works simple-kissat; do
             >&2 echo "Running test $dir"
             docker run -v /var/run/docker.sock:/var/run/docker.sock \
               -w /tmp/kani/tests/cargo-kani/$dir kani-18-04 cargo kani
diff --git a/.github/workflows/verify-std-check.yml b/.github/workflows/verify-std-check.yml
index 6935b2bb4073..3efdacc2cb85 100644
--- a/.github/workflows/verify-std-check.yml
+++ b/.github/workflows/verify-std-check.yml
@@ -59,7 +59,7 @@ jobs:
         continue-on-error: true
         run: |
           kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
-            -Z mem-predicates
+            -Z mem-predicates -Z loop-contracts --enable-unstable --cbmc-args --object-bits 12
 
       # If the head failed, check if it's a new failure.
       - name: Checkout base
@@ -77,7 +77,7 @@ jobs:
         continue-on-error: true
         run: |
           kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
-            -Z mem-predicates
+            -Z mem-predicates -Z loop-contracts --enable-unstable --cbmc-args --object-bits 12
 
       - name: Compare PR results
         if: steps.check-head.outcome != 'success' && steps.check-head.outcome != steps.check-base.outcome
diff --git a/Cargo.lock b/Cargo.lock
index cddd59917d64..1c1d3b6458e0 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -2,6 +2,21 @@
 # It is not intended for manual editing.
 version = 4
 
+[[package]]
+name = "addr2line"
+version = "0.24.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dfbe277e56a376000877090da837660b4427aad530e3028d44e0bffe4f89a1c1"
+dependencies = [
+ "gimli",
+]
+
+[[package]]
+name = "adler2"
+version = "2.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "512761e0bb2578dd7380c6baaa0f4ce03e84f95e960231d1dec8bf4d7d6e2627"
+
 [[package]]
 name = "ahash"
 version = "0.8.11"
@@ -26,9 +41,9 @@ dependencies = [
 
 [[package]]
 name = "anstream"
-version = "0.6.15"
+version = "0.6.18"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "64e15c1ab1f89faffbf04a634d5e1962e9074f2741eef6d97f3c4e322426d526"
+checksum = "8acc5369981196006228e28809f761875c0327210a891e941f4c683b3a99529b"
 dependencies = [
  "anstyle",
  "anstyle-parse",
@@ -41,43 +56,43 @@ dependencies = [
 
 [[package]]
 name = "anstyle"
-version = "1.0.8"
+version = "1.0.10"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1bec1de6f59aedf83baf9ff929c98f2ad654b97c9510f4e70cf6f661d49fd5b1"
+checksum = "55cc3b69f167a1ef2e161439aa98aed94e6028e5f9a59be9a6ffb47aef1651f9"
 
 [[package]]
 name = "anstyle-parse"
-version = "0.2.5"
+version = "0.2.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "eb47de1e80c2b463c735db5b217a0ddc39d612e7ac9e2e96a5aed1f57616c1cb"
+checksum = "3b2d16507662817a6a20a9ea92df6652ee4f94f914589377d69f3b21bc5798a9"
 dependencies = [
  "utf8parse",
 ]
 
 [[package]]
 name = "anstyle-query"
-version = "1.1.1"
+version = "1.1.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6d36fc52c7f6c869915e99412912f22093507da8d9e942ceaf66fe4b7c14422a"
+checksum = "79947af37f4177cfead1110013d678905c37501914fba0efea834c3fe9a8d60c"
 dependencies = [
- "windows-sys 0.52.0",
+ "windows-sys 0.59.0",
 ]
 
 [[package]]
 name = "anstyle-wincon"
-version = "3.0.4"
+version = "3.0.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5bf74e1b6e971609db8ca7a9ce79fd5768ab6ae46441c572e46cf596f59e57f8"
+checksum = "2109dbce0e72be3ec00bed26e6a7479ca384ad226efdd66db8fa2e3a38c83125"
 dependencies = [
  "anstyle",
- "windows-sys 0.52.0",
+ "windows-sys 0.59.0",
 ]
 
 [[package]]
 name = "anyhow"
-version = "1.0.89"
+version = "1.0.93"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "86fdf8605db99b54d3cd748a44c6d04df638eb5dafb219b135d0149bd0db01f6"
+checksum = "4c95c10ba0b00a02636238b814946408b1322d5ac4760326e6fb8ec956d85775"
 
 [[package]]
 name = "arrayvec"
@@ -113,20 +128,32 @@ version = "1.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "ace50bade8e6234aa140d9a2f552bbee1db4d353f69b8217bc503490fc1a9f26"
 
+[[package]]
+name = "backtrace"
+version = "0.3.74"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8d82cb332cdfaed17ae235a638438ac4d4839913cc2af585c3c6746e8f8bee1a"
+dependencies = [
+ "addr2line",
+ "cfg-if",
+ "libc",
+ "miniz_oxide",
+ "object",
+ "rustc-demangle",
+ "windows-targets 0.52.6",
+]
+
 [[package]]
 name = "bitflags"
-version = "2.6.0"
+version = "1.3.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de"
+checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a"
 
 [[package]]
-name = "bitmaps"
-version = "2.1.0"
+name = "bitflags"
+version = "2.6.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "031043d04099746d8db04daf1fa424b2bc8bd69d92b25962dcde24da39ab64a2"
-dependencies = [
- "typenum",
-]
+checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de"
 
 [[package]]
 name = "brownstone"
@@ -164,6 +191,12 @@ version = "1.5.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "1fd0f2584146f6f2ef48085050886acf353beff7305ebd1ae69500e27c67f64b"
 
+[[package]]
+name = "bytes"
+version = "1.8.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9ac0150caa2ae65ca5bd83f25c7de183dea78d4d366469f148435e2acfbad0da"
+
 [[package]]
 name = "camino"
 version = "1.1.9"
@@ -198,9 +231,9 @@ dependencies = [
 
 [[package]]
 name = "cc"
-version = "1.1.30"
+version = "1.1.37"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b16803a61b81d9eabb7eae2588776c4c1e584b738ede45fdbb4c972cec1e9945"
+checksum = "40545c26d092346d8a8dab71ee48e7685a7a9cba76e634790c215b41a4a7b4cf"
 dependencies = [
  "shlex",
 ]
@@ -213,7 +246,7 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
 
 [[package]]
 name = "charon"
-version = "0.1.36"
+version = "0.1.45"
 dependencies = [
  "anyhow",
  "assert_cmd",
@@ -224,7 +257,6 @@ dependencies = [
  "derive-visitor",
  "env_logger",
  "hashlink",
- "im",
  "index_vec",
  "indoc",
  "itertools 0.13.0",
@@ -236,6 +268,7 @@ dependencies = [
  "petgraph",
  "pretty",
  "regex",
+ "rustc_apfloat",
  "rustc_version",
  "serde",
  "serde-map-to-array",
@@ -246,7 +279,7 @@ dependencies = [
  "toml",
  "tracing",
  "tracing-subscriber",
- "tracing-tree 0.3.1",
+ "tracing-tree 0.4.0 (git+https://github.com/Nadrieril/tracing-tree)",
  "which",
 ]
 
@@ -281,7 +314,7 @@ dependencies = [
  "heck",
  "proc-macro2",
  "quote",
- "syn 2.0.79",
+ "syn 2.0.87",
 ]
 
 [[package]]
@@ -292,9 +325,9 @@ checksum = "1462739cb27611015575c0c11df5df7601141071f07518d56fcc1be504cbec97"
 
 [[package]]
 name = "colorchoice"
-version = "1.0.2"
+version = "1.0.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d3fd119d74b830634cea2a0f58bbd0d54540518a14397557951e79340abc28c0"
+checksum = "5b63caa9aa9397e2d9480a9b13673856c78d8ac123288526c37d7839f2a86990"
 
 [[package]]
 name = "colored"
@@ -418,7 +451,7 @@ version = "0.27.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "f476fe445d41c9e991fd07515a6f463074b782242ccf4a5b7b1d1012e70824df"
 dependencies = [
- "bitflags",
+ "bitflags 2.6.0",
  "crossterm_winapi",
  "libc",
  "parking_lot",
@@ -436,9 +469,9 @@ dependencies = [
 
 [[package]]
 name = "csv"
-version = "1.3.0"
+version = "1.3.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ac574ff4d437a7b5ad237ef331c17ccca63c46479e5b5453eb8e10bb99a759fe"
+checksum = "acdc4883a9c96732e4733212c01447ebd805833b7275a73ca3ee080fd77afdaf"
 dependencies = [
  "csv-core",
  "itoa",
@@ -562,9 +595,9 @@ dependencies = [
 
 [[package]]
 name = "fastrand"
-version = "2.1.1"
+version = "2.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e8c02a5121d4ea3eb16a80748c74f5549a5665e4c21333c6098f283870fbdea6"
+checksum = "486f806e73c5707928240ddc295403b1b93c96a02038563881c4a2fd84b81ac4"
 
 [[package]]
 name = "fixedbitset"
@@ -592,6 +625,12 @@ dependencies = [
  "wasi",
 ]
 
+[[package]]
+name = "gimli"
+version = "0.31.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "07e28edb80900c19c28f1072f2e8aeca7fa06b23cd4169cefe1af5aa3260783f"
+
 [[package]]
 name = "glob"
 version = "0.3.1"
@@ -620,9 +659,9 @@ dependencies = [
 
 [[package]]
 name = "hashbrown"
-version = "0.15.0"
+version = "0.15.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1e087f84d4f86bf4b218b927129862374b72199ae7d8657835f1e89000eea4fb"
+checksum = "3a9bfc1af68b1726ea47d3d5109de126281def866b33970e10fbab11b5dafab3"
 
 [[package]]
 name = "hashlink"
@@ -640,6 +679,12 @@ version = "0.5.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea"
 
+[[package]]
+name = "hermit-abi"
+version = "0.3.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d231dfb89cfffdbc30e7fc41579ed6066ad03abda9e567ccafae602b97ec5024"
+
 [[package]]
 name = "home"
 version = "0.5.9"
@@ -655,20 +700,6 @@ version = "2.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4"
 
-[[package]]
-name = "im"
-version = "15.1.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d0acd33ff0285af998aaf9b57342af478078f53492322fafc47450e09397e0e9"
-dependencies = [
- "bitmaps",
- "rand_core",
- "rand_xoshiro",
- "sized-chunks",
- "typenum",
- "version_check",
-]
-
 [[package]]
 name = "indent_write"
 version = "2.2.0"
@@ -691,7 +722,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "707907fe3c25f5424cce2cb7e1cbcafee6bdbe735ca90ef77c29e84591e5b9da"
 dependencies = [
  "equivalent",
- "hashbrown 0.15.0",
+ "hashbrown 0.15.1",
 ]
 
 [[package]]
@@ -763,10 +794,10 @@ dependencies = [
  "shell-words",
  "strum",
  "strum_macros",
- "syn 2.0.79",
+ "syn 2.0.87",
  "tracing",
  "tracing-subscriber",
- "tracing-tree 0.4.0",
+ "tracing-tree 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)",
 ]
 
 [[package]]
@@ -807,6 +838,7 @@ dependencies = [
  "strum_macros",
  "tempfile",
  "time",
+ "tokio",
  "toml",
  "tracing",
  "tracing-subscriber",
@@ -836,7 +868,7 @@ dependencies = [
  "proc-macro-error2",
  "proc-macro2",
  "quote",
- "syn 2.0.79",
+ "syn 2.0.87",
 ]
 
 [[package]]
@@ -858,9 +890,9 @@ checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe"
 
 [[package]]
 name = "libc"
-version = "0.2.159"
+version = "0.2.162"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "561d97a539a36e26a9a5fad1ea11a3039a67714694aaa379433e580854bc3dc5"
+checksum = "18d287de67fe55fd7e1581fe933d965a5a9477b38e949cfa9f8574ef01506398"
 
 [[package]]
 name = "linear-map"
@@ -900,7 +932,7 @@ version = "0.1.0"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.79",
+ "syn 2.0.87",
 ]
 
 [[package]]
@@ -930,6 +962,27 @@ version = "0.2.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a"
 
+[[package]]
+name = "miniz_oxide"
+version = "0.8.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e2d80299ef12ff69b16a84bb182e3b9df68b5a91574d3d4fa6e41b65deec4df1"
+dependencies = [
+ "adler2",
+]
+
+[[package]]
+name = "mio"
+version = "1.0.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "80e04d1dcff3aae0704555fe5fee3bcfaf3d1fdf8a7e521d5b9d2b42acb52cec"
+dependencies = [
+ "hermit-abi",
+ "libc",
+ "wasi",
+ "windows-sys 0.52.0",
+]
+
 [[package]]
 name = "nom"
 version = "7.1.3"
@@ -1051,6 +1104,24 @@ dependencies = [
  "autocfg",
 ]
 
+[[package]]
+name = "num_threads"
+version = "0.1.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5c7398b9c8b70908f6371f47ed36737907c87c52af34c268fed0bf0ceb92ead9"
+dependencies = [
+ "libc",
+]
+
+[[package]]
+name = "object"
+version = "0.36.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "aedf0a2d09c573ed1d8d85b30c119153926a2b36dce0ab28322c09a117a4683e"
+dependencies = [
+ "memchr",
+]
+
 [[package]]
 name = "once_cell"
 version = "1.20.2"
@@ -1114,9 +1185,9 @@ dependencies = [
 
 [[package]]
 name = "pin-project-lite"
-version = "0.2.14"
+version = "0.2.15"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "bda66fc9667c18cb2758a2ac84d1167245054bcf85d5d1aaa6923f45801bdd02"
+checksum = "915a1e146535de9163f3987b8944ed8cf49a18bb0056bcebcdcece385cece4ff"
 
 [[package]]
 name = "powerfmt"
@@ -1190,14 +1261,14 @@ dependencies = [
  "proc-macro-error-attr2",
  "proc-macro2",
  "quote",
- "syn 2.0.79",
+ "syn 2.0.87",
 ]
 
 [[package]]
 name = "proc-macro2"
-version = "1.0.87"
+version = "1.0.89"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b3e4daa0dcf6feba26f985457cdf104d4b4256fc5a09547140f3631bb076b19a"
+checksum = "f139b0662de085916d1fb67d2b4169d1addddda1919e696f3252b740b629986e"
 dependencies = [
  "unicode-ident",
 ]
@@ -1250,15 +1321,6 @@ dependencies = [
  "getrandom",
 ]
 
-[[package]]
-name = "rand_xoshiro"
-version = "0.6.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6f97cdb2a36ed4183de61b2f824cc45c9f1037f28afe0a322e9fff4c108b5aaa"
-dependencies = [
- "rand_core",
-]
-
 [[package]]
 name = "rayon"
 version = "1.10.0"
@@ -1285,14 +1347,14 @@ version = "0.5.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "9b6dfecf2c74bce2466cabf93f6664d6998a69eb21e39f4207930065b27b771f"
 dependencies = [
- "bitflags",
+ "bitflags 2.6.0",
 ]
 
 [[package]]
 name = "regex"
-version = "1.11.0"
+version = "1.11.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "38200e5ee88914975b69f657f0801b6f6dccafd44fd9326302a4aaeecfacb1d8"
+checksum = "b544ef1b4eac5dc2db33ea63606ae9ffcfac26c1416a2806ae0bf5f56b201191"
 dependencies = [
  "aho-corasick",
  "memchr",
@@ -1338,6 +1400,16 @@ version = "0.1.24"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "719b953e2095829ee67db738b3bfa9fa368c94900df327b3f07fe6e794d2fe1f"
 
+[[package]]
+name = "rustc_apfloat"
+version = "0.2.1+llvm-462a31f5a5ab"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "886d94c63c812a8037c4faca2607453a0fa4cf82f734665266876b022244543f"
+dependencies = [
+ "bitflags 1.3.2",
+ "smallvec",
+]
+
 [[package]]
 name = "rustc_version"
 version = "0.4.1"
@@ -1349,11 +1421,11 @@ dependencies = [
 
 [[package]]
 name = "rustix"
-version = "0.38.37"
+version = "0.38.40"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8acb788b847c24f28525660c4d7758620a7210875711f79e7f663cc152726811"
+checksum = "99e4ea3e1cdc4b559b8e5650f9c8e5998e3e5c1343b4eaf034565f32318d63c0"
 dependencies = [
- "bitflags",
+ "bitflags 2.6.0",
  "errno",
  "libc",
  "linux-raw-sys",
@@ -1362,9 +1434,9 @@ dependencies = [
 
 [[package]]
 name = "rustversion"
-version = "1.0.17"
+version = "1.0.18"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "955d28af4278de8121b7ebeb796b6a45735dc01436d898801014aced2773a3d6"
+checksum = "0e819f2bc632f285be6d7cd36e25940d45b2391dd6d9b939e79de557f7014248"
 
 [[package]]
 name = "ryu"
@@ -1410,9 +1482,9 @@ dependencies = [
 
 [[package]]
 name = "serde"
-version = "1.0.210"
+version = "1.0.214"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c8e3592472072e6e22e0a54d5904d9febf8508f65fb8552499a1abc7d1078c3a"
+checksum = "f55c3193aca71c12ad7890f1785d2b73e1b9f63a0bbc353c08ef26fe03fc56b5"
 dependencies = [
  "serde_derive",
 ]
@@ -1428,20 +1500,20 @@ dependencies = [
 
 [[package]]
 name = "serde_derive"
-version = "1.0.210"
+version = "1.0.214"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "243902eda00fad750862fc144cea25caca5e20d615af0a81bee94ca738f1df1f"
+checksum = "de523f781f095e28fa605cdce0f8307e451cc0fd14e2eb4cd2e98a355b147766"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.79",
+ "syn 2.0.87",
 ]
 
 [[package]]
 name = "serde_json"
-version = "1.0.128"
+version = "1.0.132"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6ff5456707a1de34e7e37f2a6fd3d3f808c318259cbd01ab6377795054b483d8"
+checksum = "d726bfaff4b320266d395898905d0eba0345aae23b54aee3a737e260fd46db03"
 dependencies = [
  "indexmap",
  "itoa",
@@ -1513,13 +1585,12 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64"
 
 [[package]]
-name = "sized-chunks"
-version = "0.6.5"
+name = "signal-hook-registry"
+version = "1.4.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "16d69225bde7a69b235da73377861095455d298f2b970996eec25ddbb42b3d1e"
+checksum = "a9e9e0b4211b72e7b8b6e85c807d36c212bdb33ea8587f7569562a84df5465b1"
 dependencies = [
- "bitmaps",
- "typenum",
+ "libc",
 ]
 
 [[package]]
@@ -1581,7 +1652,7 @@ dependencies = [
  "proc-macro2",
  "quote",
  "rustversion",
- "syn 2.0.79",
+ "syn 2.0.87",
 ]
 
 [[package]]
@@ -1597,9 +1668,9 @@ dependencies = [
 
 [[package]]
 name = "syn"
-version = "2.0.79"
+version = "2.0.87"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "89132cd0bf050864e1d38dc3bbc07a0eb8e7530af26344d3d2bbbef83499f590"
+checksum = "25aa4ce346d03a6dcd68dd8b4010bcb74e54e62c90c573f394c46eae99aba32d"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -1614,9 +1685,9 @@ checksum = "f764005d11ee5f36500a149ace24e00e3da98b0158b3e2d53a7495660d3f4d60"
 
 [[package]]
 name = "tempfile"
-version = "3.13.0"
+version = "3.14.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f0f2c9fc62d0beef6951ccffd757e241266a2c833136efbe35af6cd2567dca5b"
+checksum = "28cce251fcbc87fac86a866eeb0d6c2d536fc16d06f184bb61aeae11aa4cee0c"
 dependencies = [
  "cfg-if",
  "fastrand",
@@ -1633,22 +1704,22 @@ checksum = "3369f5ac52d5eb6ab48c6b4ffdc8efbcad6b89c765749064ba298f2c68a16a76"
 
 [[package]]
 name = "thiserror"
-version = "1.0.64"
+version = "1.0.69"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d50af8abc119fb8bb6dbabcfa89656f46f84aa0ac7688088608076ad2b459a84"
+checksum = "b6aaf5339b578ea85b50e080feb250a3e8ae8cfcdff9a461c9ec2904bc923f52"
 dependencies = [
  "thiserror-impl",
 ]
 
 [[package]]
 name = "thiserror-impl"
-version = "1.0.64"
+version = "1.0.69"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "08904e7672f5eb876eaaf87e0ce17857500934f4981c4a0ab2b4aa98baac7fc3"
+checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.79",
+ "syn 2.0.87",
 ]
 
 [[package]]
@@ -1669,7 +1740,9 @@ checksum = "5dfd88e563464686c916c7e46e623e520ddc6d79fa6641390f2e3fa86e83e885"
 dependencies = [
  "deranged",
  "itoa",
+ "libc",
  "num-conv",
+ "num_threads",
  "powerfmt",
  "serde",
  "time-core",
@@ -1692,6 +1765,21 @@ dependencies = [
  "time-core",
 ]
 
+[[package]]
+name = "tokio"
+version = "1.41.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "22cfb5bee7a6a52939ca9224d6ac897bb669134078daa8735560897f69de4d33"
+dependencies = [
+ "backtrace",
+ "bytes",
+ "libc",
+ "mio",
+ "pin-project-lite",
+ "signal-hook-registry",
+ "windows-sys 0.52.0",
+]
+
 [[package]]
 name = "toml"
 version = "0.8.19"
@@ -1745,7 +1833,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.79",
+ "syn 2.0.87",
 ]
 
 [[package]]
@@ -1803,9 +1891,9 @@ dependencies = [
 
 [[package]]
 name = "tracing-tree"
-version = "0.3.1"
+version = "0.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b56c62d2c80033cb36fae448730a2f2ef99410fe3ecbffc916681a32f6807dbe"
+checksum = "f459ca79f1b0d5f71c54ddfde6debfc59c8b6eeb46808ae492077f739dc7b49c"
 dependencies = [
  "nu-ansi-term 0.50.1",
  "tracing-core",
@@ -1816,10 +1904,10 @@ dependencies = [
 [[package]]
 name = "tracing-tree"
 version = "0.4.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f459ca79f1b0d5f71c54ddfde6debfc59c8b6eeb46808ae492077f739dc7b49c"
+source = "git+https://github.com/Nadrieril/tracing-tree#841286bfffd3c2200810244506cd127013dbeff9"
 dependencies = [
  "nu-ansi-term 0.50.1",
+ "time",
  "tracing-core",
  "tracing-log",
  "tracing-subscriber",
@@ -1859,12 +1947,6 @@ version = "2.0.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "6af6ae20167a9ece4bcb41af5b80f8a1f1df981f6391189ce00fd257af04126a"
 
-[[package]]
-name = "typenum"
-version = "1.17.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "42ff0bf0c66b8238c6f3b578df37d0b7848e55df8577b3f74f92a69acceeb825"
-
 [[package]]
 name = "unicode-ident"
 version = "1.0.13"
@@ -2156,5 +2238,5 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.79",
+ "syn 2.0.87",
 ]
diff --git a/charon b/charon
index cdc1dcde447a..2193aa00fd89 160000
--- a/charon
+++ b/charon
@@ -1 +1 @@
-Subproject commit cdc1dcde447a50cbc20336c79b21b42ac977b7fd
+Subproject commit 2193aa00fd89e991226ada10d8a8f66e0594f212
diff --git a/deny.toml b/deny.toml
index 9866397b4655..743f6965e2f5 100644
--- a/deny.toml
+++ b/deny.toml
@@ -1,6 +1,12 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
+[graph]
+# derivative is marked as unmaintained by RUSTSEC but still used in
+# Charon. We exclude it from the deny check until derivative is replaced
+# from Charon (https://github.com/AeneasVerif/charon/pull/459).
+exclude = ["derivative"]
+
 # This section is considered when running `cargo deny check advisories`
 # More documentation for the advisories section can be found here:
 # https://embarkstudios.github.io/cargo-deny/checks/advisories/cfg.html
@@ -23,6 +29,7 @@ confidence-threshold = 0.8
 # All these exceptions should probably appear in: tools/build-kani/license-notes.txt
 exceptions = [
     { name = "unicode-ident", allow=["Unicode-DFS-2016"] },
+    { name = "rustc_apfloat", allow=["Apache-2.0 WITH LLVM-exception"] },
 ]
 
 [licenses.private]
@@ -42,3 +49,4 @@ wildcards = "allow"
 unknown-registry = "deny"
 unknown-git = "deny"
 allow-registry = ["https://github.com/rust-lang/crates.io-index"]
+allow-git = ["https://github.com/Nadrieril/tracing-tree"]
diff --git a/docs/src/build-from-source.md b/docs/src/build-from-source.md
index 01860f5f37e4..253fcf351073 100644
--- a/docs/src/build-from-source.md
+++ b/docs/src/build-from-source.md
@@ -12,8 +12,7 @@ In general, the following dependencies are required to build Kani from source.
 
 1. Cargo installed via [rustup](https://rustup.rs/)
 2. [CBMC](https://github.com/diffblue/cbmc) (latest release)
-3. [CBMC Viewer](https://github.com/awslabs/aws-viewer-for-cbmc) (latest release)
-4. [Kissat](https://github.com/arminbiere/kissat) (Release 3.1.1)
+3. [Kissat](https://github.com/arminbiere/kissat) (Release 3.1.1)
 
 Kani has been tested in [Ubuntu](#install-dependencies-on-ubuntu) and [macOS](##install-dependencies-on-macos) platforms.
 
diff --git a/docs/src/install-guide.md b/docs/src/install-guide.md
index 776209987ba1..d64ad3c89ce0 100644
--- a/docs/src/install-guide.md
+++ b/docs/src/install-guide.md
@@ -16,7 +16,6 @@ The following must already be installed:
 
 * **Python version 3.7 or newer** and the package installer `pip`.
 * Rust 1.58 or newer installed via `rustup`.
-* `ctags` is required for Kani's `--visualize` option to work correctly. [Universal ctags](https://ctags.io/) is recommended.
 
 ## Installing the latest version
 
diff --git a/docs/src/reference/experimental/coverage.md b/docs/src/reference/experimental/coverage.md
index 5e536b3992b6..aa7aa576886a 100644
--- a/docs/src/reference/experimental/coverage.md
+++ b/docs/src/reference/experimental/coverage.md
@@ -14,7 +14,7 @@ Fortunately, Kani is able to report a coverage metric for each proof harness.
 In the `first-steps-v2` directory, try running:
 
 ```
-cargo kani --coverage -Z line-coverage --harness verify_success
+cargo kani --coverage -Z source-coverage --harness verify_success
 ```
 
 which verifies the harness, then prints coverage information for each line.
diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md
index ce3c9fc1b7a2..a9e2740836e5 100644
--- a/docs/src/rust-feature-support/intrinsics.md
+++ b/docs/src/rust-feature-support/intrinsics.md
@@ -156,7 +156,7 @@ fabsf32 | Yes | |
 fabsf64 | Yes | |
 fadd_fast | Yes | |
 fdiv_fast | Partial | [#809](https://github.com/model-checking/kani/issues/809) |
-float_to_int_unchecked | No | |
+float_to_int_unchecked | Partial | [#3629](https://github.com/model-checking/kani/issues/3629) |
 floorf32 | Yes | |
 floorf64 | Yes | |
 fmaf32 | Partial | Results are overapproximated |
diff --git a/docs/src/tutorial-real-code.md b/docs/src/tutorial-real-code.md
index 3dd216cd6258..099294ac35eb 100644
--- a/docs/src/tutorial-real-code.md
+++ b/docs/src/tutorial-real-code.md
@@ -74,7 +74,7 @@ A first proof will likely start in the following form:
 Running Kani on this simple starting point will help figure out:
 
 1. What unexpected constraints might be needed on your inputs (using `kani::assume`) to avoid "expected" failures.
-2. Whether you're over-constrained. Check the coverage report using `--coverage -Z line-coverage`. Ideally you'd see 100% coverage, and if not, it's usually because you've assumed too much (thus over-constraining the inputs).
+2. Whether you're over-constrained. Check the coverage report using `--coverage -Z source-coverage`. Ideally you'd see 100% coverage, and if not, it's usually because you've assumed too much (thus over-constraining the inputs).
 3. Whether Kani will support all the Rust features involved.
 4. Whether you've started with a tractable problem.
 (Remember to try setting `#[kani::unwind(1)]` to force early termination and work up from there.)
diff --git a/docs/src/usage.md b/docs/src/usage.md
index aaa5d3fa234c..60592aa56c9a 100644
--- a/docs/src/usage.md
+++ b/docs/src/usage.md
@@ -28,8 +28,6 @@ Common to both `kani` and `cargo kani` are many command-line flags:
  If used with `print`, Kani will only print the unit test to stdout.
  If used with `inplace`, Kani will automatically add the unit test to the user's source code, next to the proof harness. For more detailed instructions, see the [concrete playback](./experimental/concrete-playback.md) section.
 
- * `--visualize`: _Experimental_, `--enable-unstable` feature that generates an HTML report providing traces (i.e., counterexamples) for each failure found by Kani.
-
  * `--tests`: Build in "[test mode](https://doc.rust-lang.org/rustc/tests/index.html)", i.e. with `cfg(test)` set and `dev-dependencies` available (when using `cargo kani`).
 
  * `--harness <name>`: By default, Kani checks all proof harnesses it finds.
diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml
index 7b17e6073bb3..9f084da7b962 100644
--- a/kani-compiler/Cargo.toml
+++ b/kani-compiler/Cargo.toml
@@ -31,10 +31,9 @@ tracing-tree = "0.4.0"
 
 # Future proofing: enable backend dependencies using feature.
 [features]
-default = ['aeneas', 'cprover']
-aeneas = ['charon']
+default = ['cprover', 'llbc']
+llbc = ['charon']
 cprover = ['cbmc', 'num', 'serde']
-write_json_symtab = []
 
 [package.metadata.rust-analyzer]
 # This package uses rustc crates.
diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs
index b5b799321cf3..fee2521f4908 100644
--- a/kani-compiler/src/args.rs
+++ b/kani-compiler/src/args.rs
@@ -7,15 +7,15 @@ use tracing_subscriber::filter::Directive;
 #[derive(Debug, Default, Display, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)]
 #[strum(serialize_all = "snake_case")]
 pub enum BackendOption {
-    /// Aeneas (LLBC) backend
-    #[cfg(feature = "aeneas")]
-    Aeneas,
-
     /// CProver (Goto) backend
     #[cfg(feature = "cprover")]
     #[strum(serialize = "cprover")]
     #[default]
     CProver,
+
+    /// LLBC backend (Aeneas's IR)
+    #[cfg(feature = "llbc")]
+    Llbc,
 }
 
 #[derive(Debug, Default, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)]
@@ -51,11 +51,6 @@ pub struct Arguments {
     /// Option used for suppressing global ASM error.
     #[clap(long)]
     pub ignore_global_asm: bool,
-    #[clap(long)]
-    /// Option used to write JSON symbol tables instead of GOTO binaries.
-    ///
-    /// When set, instructs the compiler to produce the symbol table for CBMC in JSON format and use symtab2gb.
-    pub write_json_symtab: bool,
     /// Option name used to select which reachability analysis to perform.
     #[clap(long = "reachability", default_value = "none")]
     pub reachability_analysis: ReachabilityType,
@@ -87,7 +82,7 @@ pub struct Arguments {
     /// Option name used to select which backend to use.
     #[clap(long = "backend", default_value_t = BackendOption::CProver)]
     pub backend: BackendOption,
-    /// Print the final LLBC file to stdout. This requires `-Zaeneas`.
+    /// Print the final LLBC file to stdout.
     #[clap(long)]
     pub print_llbc: bool,
 }
diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs
index f9922f237bd5..9f4365b194b2 100644
--- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs
@@ -12,7 +12,7 @@ use crate::kani_middle::provide;
 use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_items};
 use crate::kani_middle::transform::{BodyTransformation, GlobalPasses};
 use crate::kani_queries::QueryDb;
-use charon_lib::ast::TranslatedCrate;
+use charon_lib::ast::{AnyTransId, TranslatedCrate};
 use charon_lib::errors::ErrorCtx;
 use charon_lib::transform::TransformCtx;
 use charon_lib::transform::ctx::TransformOptions;
@@ -24,7 +24,7 @@ use rustc_codegen_ssa::back::archive::{
 use rustc_codegen_ssa::back::link::link_binary;
 use rustc_codegen_ssa::traits::CodegenBackend;
 use rustc_codegen_ssa::{CodegenResults, CrateInfo};
-use rustc_data_structures::fx::FxIndexMap;
+use rustc_data_structures::fx::{FxHashMap, FxIndexMap};
 use rustc_errors::{DEFAULT_LOCALE_RESOURCE, ErrorGuaranteed};
 use rustc_hir::def_id::{DefId as InternalDefId, LOCAL_CRATE};
 use rustc_metadata::EncodedMetadata;
@@ -106,13 +106,19 @@ impl LlbcCodegenBackend {
 
         // Create a Charon transformation context that will be populated with translation results
         let mut ccx = create_charon_transformation_context(tcx);
+        let mut id_map: FxHashMap<DefId, AnyTransId> = FxHashMap::default();
 
         // Translate all the items
         for item in &items {
             match item {
                 MonoItem::Fn(instance) => {
-                    let mut fcx =
-                        Context::new(tcx, *instance, &mut ccx.translated, &mut ccx.errors);
+                    let mut fcx = Context::new(
+                        tcx,
+                        *instance,
+                        &mut ccx.translated,
+                        &mut id_map,
+                        &mut ccx.errors,
+                    );
                     let _ = fcx.translate();
                 }
                 MonoItem::Static(_def) => todo!(),
@@ -140,7 +146,7 @@ impl LlbcCodegenBackend {
 
         // Run the micro-passes that clean up bodies.
         for pass in charon_lib::transform::ULLBC_PASSES.iter() {
-            pass.transform_ctx(&mut ccx)
+            pass.run(&mut ccx)
         }
 
         // # Go from ULLBC to LLBC (Low-Level Borrow Calculus) by reconstructing
@@ -151,7 +157,7 @@ impl LlbcCodegenBackend {
 
         // Run the micro-passes that clean up bodies.
         for pass in charon_lib::transform::LLBC_PASSES.iter() {
-            pass.transform_ctx(&mut ccx)
+            pass.run(&mut ccx)
         }
 
         // Print the LLBC if requested. This is useful for expected tests.
@@ -161,8 +167,10 @@ impl LlbcCodegenBackend {
             debug!("# Final LLBC before serialization:\n\n{}\n", ccx);
         }
 
-        // Display an error report about the external dependencies, if necessary
-        ccx.errors.report_external_deps_errors();
+        // TODO: display an error report about the external dependencies, if necessary
+        if ccx.errors.error_count > 0 {
+            todo!()
+        }
 
         let crate_data: charon_lib::export::CrateData = charon_lib::export::CrateData::new(&ccx);
 
@@ -393,18 +401,20 @@ fn create_charon_transformation_context(tcx: TyCtxt) -> TransformCtx {
     let options = TransformOptions {
         no_code_duplication: false,
         hide_marker_traits: false,
+        no_merge_goto_chains: false,
         item_opacities: Vec::new(),
     };
     let crate_name = tcx.crate_name(LOCAL_CRATE).as_str().into();
     let translated = TranslatedCrate { crate_name, ..TranslatedCrate::default() };
     let errors = ErrorCtx {
         continue_on_failure: true,
-        errors_as_warnings: false,
-        dcx: tcx.dcx(),
-        decls_with_errors: HashSet::new(),
+        error_on_warnings: false,
+        dcx: &(),
+        external_decls_with_errors: HashSet::new(),
         ignored_failed_decls: HashSet::new(),
-        dep_sources: HashMap::new(),
+        external_dep_sources: HashMap::new(),
         def_id: None,
+        def_id_is_local: true,
         error_count: 0,
     };
     TransformCtx { options, translated, errors }
diff --git a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs
index 62462915480e..35e4d137229d 100644
--- a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs
+++ b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs
@@ -16,7 +16,8 @@ use charon_lib::ast::Rvalue as CharonRvalue;
 use charon_lib::ast::Span as CharonSpan;
 use charon_lib::ast::meta::{AttrInfo, Loc, RawSpan};
 use charon_lib::ast::types::Ty as CharonTy;
-use charon_lib::ast::{AbortKind, Body as CharonBody, Var, VarId, make_locals_generator};
+use charon_lib::ast::types::TyKind as CharonTyKind;
+use charon_lib::ast::{AbortKind, Body as CharonBody, Var, VarId};
 use charon_lib::ast::{
     AnyTransId, Assert, BodyId, BuiltinTy, Disambiguator, FileName, FunDecl, FunSig, GenericArgs,
     GenericParams, IntegerTy, ItemKind, ItemMeta, ItemOpacity, Literal, LiteralTy, Name, Opaque,
@@ -30,7 +31,7 @@ use charon_lib::ast::{
 use charon_lib::ast::{
     BorrowKind as CharonBorrowKind, ConstantExpr, Operand as CharonOperand, UnOp,
 };
-use charon_lib::common::Error;
+use charon_lib::errors::Error;
 use charon_lib::errors::ErrorCtx;
 use charon_lib::ids::Vector;
 use charon_lib::ullbc_ast::{
@@ -39,14 +40,15 @@ use charon_lib::ullbc_ast::{
     Terminator as CharonTerminator,
 };
 use charon_lib::{error_assert, error_or_panic};
-use rustc_errors::MultiSpan;
+use rustc_data_structures::fx::FxHashMap;
 use rustc_middle::ty::TyCtxt;
 use rustc_smir::rustc_internal;
-use rustc_span::def_id::DefId as InternalDefId;
 use stable_mir::abi::PassMode;
+use stable_mir::mir::VarDebugInfoContents;
 use stable_mir::mir::mono::Instance;
+use stable_mir::mir::mono::InstanceDef;
 use stable_mir::mir::{
-    BasicBlock, BinOp, Body, BorrowKind, CastKind, ConstOperand, Mutability, Operand, Place,
+    BasicBlock, BinOp, Body, BorrowKind, CastKind, ConstOperand, Local, Mutability, Operand, Place,
     ProjectionElem, Rvalue, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind,
 };
 use stable_mir::ty::{
@@ -63,7 +65,9 @@ pub struct Context<'a, 'tcx> {
     tcx: TyCtxt<'tcx>,
     instance: Instance,
     translated: &'a mut TranslatedCrate,
+    id_map: &'a mut FxHashMap<DefId, AnyTransId>,
     errors: &'a mut ErrorCtx<'tcx>,
+    local_names: FxHashMap<Local, String>,
 }
 
 impl<'a, 'tcx> Context<'a, 'tcx> {
@@ -73,16 +77,27 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         tcx: TyCtxt<'tcx>,
         instance: Instance,
         translated: &'a mut TranslatedCrate,
+        id_map: &'a mut FxHashMap<DefId, AnyTransId>,
         errors: &'a mut ErrorCtx<'tcx>,
     ) -> Self {
-        Self { tcx, instance, translated, errors }
+        let mut local_names = FxHashMap::default();
+        // populate names of locals
+        for info in instance.body().unwrap().var_debug_info {
+            if let VarDebugInfoContents::Place(p) = info.value {
+                if p.projection.is_empty() {
+                    local_names.insert(p.local, info.name);
+                }
+            }
+        }
+
+        Self { tcx, instance, translated, id_map, errors, local_names }
     }
 
     fn tcx(&self) -> TyCtxt<'tcx> {
         self.tcx
     }
 
-    fn span_err<S: Into<MultiSpan>>(&mut self, span: S, msg: &str) {
+    fn span_err(&mut self, span: CharonSpan, msg: &str) {
         self.errors.span_err(span, msg);
     }
 
@@ -92,13 +107,10 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
 
     /// Perform the translation
     pub fn translate(&mut self) -> Result<(), ()> {
-        // Charon's `id_map` is in terms of internal `DefId`
-        let def_id = rustc_internal::internal(self.tcx(), self.instance.def.def_id());
-
         // TODO: might want to populate `errors.dep_sources` to help with
         // debugging
 
-        let fid = self.register_fun_decl_id(def_id);
+        let fid = self.register_fun_decl_id(self.instance.def.def_id());
 
         let item_meta = match self.translate_item_meta_from_rid(self.instance) {
             Ok(item_meta) => item_meta,
@@ -115,14 +127,8 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             }
         };
 
-        let fun_decl = FunDecl {
-            def_id: fid,
-            rust_id: def_id,
-            item_meta,
-            signature,
-            kind: ItemKind::Regular,
-            body: Ok(body),
-        };
+        let fun_decl =
+            FunDecl { def_id: fid, item_meta, signature, kind: ItemKind::Regular, body: Ok(body) };
 
         self.translated.fun_decls.set_slot(fid, fun_decl);
 
@@ -130,24 +136,26 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
     }
 
     /// Get or create a `FunDeclId` for the given function
-    fn register_fun_decl_id(&mut self, def_id: InternalDefId) -> FunDeclId {
-        let tid = match self.translated.id_map.get(&def_id) {
+    fn register_fun_decl_id(&mut self, def_id: DefId) -> FunDeclId {
+        debug!("register_fun_decl_id: {:?}", def_id);
+        let tid = match self.id_map.get(&def_id) {
             Some(tid) => *tid,
             None => {
+                debug!("***Not found!");
                 let tid = AnyTransId::Fun(self.translated.fun_decls.reserve_slot());
-                self.translated.id_map.insert(def_id, tid);
-                self.translated.reverse_id_map.insert(tid, def_id);
+                self.id_map.insert(def_id, tid);
                 self.translated.all_ids.insert(tid);
                 tid
             }
         };
-        *tid.as_fun()
+        debug!("register_fun_decl_id: {:?}", self.id_map);
+        tid.try_into().unwrap()
     }
 
     /// Compute the meta information for a Rust item identified by its id.
     fn translate_item_meta_from_rid(&mut self, instance: Instance) -> Result<ItemMeta, Error> {
         let span = self.translate_instance_span(instance);
-        let name = self.def_id_to_name(instance.def.def_id())?;
+        let name = self.def_to_name(instance.def)?;
         // TODO: populate the source text
         let source_text = None;
         // TODO: populate the attribute info
@@ -168,11 +176,12 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
     /// Retrieve an item name from a [DefId].
     /// This function is adapted from Charon:
     /// https://github.com/AeneasVerif/charon/blob/53530427db2941ce784201e64086766504bc5642/charon/src/bin/charon-driver/translate/translate_ctx.rs#L344
-    fn def_id_to_name(&mut self, def_id: DefId) -> Result<Name, Error> {
+    fn def_to_name(&mut self, def: InstanceDef) -> Result<Name, Error> {
+        let def_id = def.def_id();
         trace!("{:?}", def_id);
-        let def_id = rustc_internal::internal(self.tcx(), def_id);
         let tcx = self.tcx();
-        let span = tcx.def_span(def_id);
+        let span: CharonSpan = self.translate_span(def.span());
+        let def_id = rustc_internal::internal(self.tcx(), def_id);
 
         // We have to be a bit careful when retrieving names from def ids. For instance,
         // due to reexports, [`TyCtxt::def_path_str`](TyCtxt::def_path_str) might give
@@ -328,7 +337,6 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             file_id,
             beg: Loc { line: lineinfo.start_line, col: lineinfo.start_col },
             end: Loc { line: lineinfo.end_line, col: lineinfo.end_col },
-            rust_span_data: rustc_internal::internal(self.tcx(), span).data(),
         };
 
         // TODO: populate `generated_from_span` info
@@ -392,7 +400,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         let body: BodyContents =
             mir_body.blocks.iter().map(|bb| self.translate_block(bb)).collect();
 
-        let body_expr = ExprBody { span, arg_count, locals, body };
+        let body_expr = ExprBody { span, arg_count, locals, body, comments: Vec::new() };
         CharonBody::Unstructured(body_expr)
     }
 
@@ -411,12 +419,16 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
     fn translate_rigid_ty(&self, rigid_ty: RigidTy) -> CharonTy {
         debug!("translate_rigid_ty: {rigid_ty:?}");
         match rigid_ty {
-            RigidTy::Bool => CharonTy::Literal(LiteralTy::Bool),
-            RigidTy::Char => CharonTy::Literal(LiteralTy::Char),
-            RigidTy::Int(it) => CharonTy::Literal(LiteralTy::Integer(translate_int_ty(it))),
-            RigidTy::Uint(uit) => CharonTy::Literal(LiteralTy::Integer(translate_uint_ty(uit))),
-            RigidTy::Never => CharonTy::Never,
-            RigidTy::Str => CharonTy::Adt(
+            RigidTy::Bool => CharonTy::new(CharonTyKind::Literal(LiteralTy::Bool)),
+            RigidTy::Char => CharonTy::new(CharonTyKind::Literal(LiteralTy::Char)),
+            RigidTy::Int(it) => {
+                CharonTy::new(CharonTyKind::Literal(LiteralTy::Integer(translate_int_ty(it))))
+            }
+            RigidTy::Uint(uit) => {
+                CharonTy::new(CharonTyKind::Literal(LiteralTy::Integer(translate_uint_ty(uit))))
+            }
+            RigidTy::Never => CharonTy::new(CharonTyKind::Never),
+            RigidTy::Str => CharonTy::new(CharonTyKind::Adt(
                 TypeId::Builtin(BuiltinTy::Str),
                 // TODO: find out whether any of the information below should be
                 // populated for strings
@@ -426,15 +438,15 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                     const_generics: Vector::new(),
                     trait_refs: Vector::new(),
                 },
-            ),
-            RigidTy::Ref(region, ty, mutability) => CharonTy::Ref(
+            )),
+            RigidTy::Ref(region, ty, mutability) => CharonTy::new(CharonTyKind::Ref(
                 self.translate_region(region),
-                Box::new(self.translate_ty(ty)),
+                self.translate_ty(ty),
                 match mutability {
                     Mutability::Mut => RefKind::Mut,
                     Mutability::Not => RefKind::Shared,
                 },
-            ),
+            )),
             RigidTy::Tuple(ty) => {
                 let types = ty.iter().map(|ty| self.translate_ty(*ty)).collect();
                 // TODO: find out if any of the information below is needed
@@ -444,7 +456,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                     const_generics: Vector::new(),
                     trait_refs: Vector::new(),
                 };
-                CharonTy::Adt(TypeId::Tuple, generic_args)
+                CharonTy::new(CharonTyKind::Adt(TypeId::Tuple, generic_args))
             }
             RigidTy::FnDef(def_id, args) => {
                 if !args.0.is_empty() {
@@ -454,7 +466,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                 let inputs = sig.inputs().iter().map(|ty| self.translate_ty(*ty)).collect();
                 let output = self.translate_ty(sig.output());
                 // TODO: populate regions?
-                CharonTy::Arrow(Vector::new(), inputs, Box::new(output))
+                CharonTy::new(CharonTyKind::Arrow(Vector::new(), inputs, output))
             }
             _ => todo!(),
         }
@@ -466,19 +478,21 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         // - the input arguments
         // - the remaining locals, used for the intermediate computations
         let mut locals = Vector::new();
-        {
-            let mut add_variable = make_locals_generator(&mut locals);
-            mir_body.local_decls().for_each(|(_, local)| {
-                add_variable(self.translate_ty(local.ty));
-            });
-        }
+        mir_body.local_decls().for_each(|(local, local_decl)| {
+            let ty = self.translate_ty(local_decl.ty);
+            let name = self.local_names.get(&local);
+            locals.push_with(|index| Var { index, name: name.cloned(), ty });
+        });
         locals
     }
 
     fn translate_block(&mut self, bb: &BasicBlock) -> BlockData {
-        let statements =
+        let mut statements: Vec<CharonStatement> =
             bb.statements.iter().filter_map(|stmt| self.translate_statement(stmt)).collect();
-        let terminator = self.translate_terminator(&bb.terminator);
+        let (statement, terminator) = self.translate_terminator(&bb.terminator);
+        if let Some(statement) = statement {
+            statements.push(statement);
+        }
         BlockData { statements, terminator }
     }
 
@@ -508,21 +522,27 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         None
     }
 
-    fn translate_terminator(&mut self, terminator: &Terminator) -> CharonTerminator {
+    fn translate_terminator(
+        &mut self,
+        terminator: &Terminator,
+    ) -> (Option<CharonStatement>, CharonTerminator) {
         let span = self.translate_span(terminator.span);
-        let content = match &terminator.kind {
-            TerminatorKind::Return => RawTerminator::Return,
+        let (statement, terminator) = match &terminator.kind {
+            TerminatorKind::Return => (None, RawTerminator::Return),
             TerminatorKind::Goto { target } => {
-                RawTerminator::Goto { target: BlockId::from_usize(*target) }
+                (None, RawTerminator::Goto { target: BlockId::from_usize(*target) })
+            }
+            TerminatorKind::Unreachable => {
+                (None, RawTerminator::Abort(AbortKind::UndefinedBehavior))
+            }
+            TerminatorKind::Drop { place, target, .. } => {
+                (Some(RawStatement::Drop(self.translate_place(&place))), RawTerminator::Goto {
+                    target: BlockId::from_usize(*target),
+                })
             }
-            TerminatorKind::Unreachable => RawTerminator::Abort(AbortKind::UndefinedBehavior),
-            TerminatorKind::Drop { place, target, .. } => RawTerminator::Drop {
-                place: self.translate_place(&place),
-                target: BlockId::from_usize(*target),
-            },
             TerminatorKind::SwitchInt { discr, targets } => {
                 let (discr, targets) = self.translate_switch_targets(discr, targets);
-                RawTerminator::Switch { discr, targets }
+                (None, RawTerminator::Switch { discr, targets })
             }
             TerminatorKind::Call { func, args, destination, target, .. } => {
                 debug!("translate_call: {func:?} {args:?} {destination:?} {target:?}");
@@ -530,7 +550,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                 let fn_ptr = match fn_ty.kind() {
                     TyKind::RigidTy(RigidTy::FnDef(def, args)) => {
                         let instance = Instance::resolve(def, &args).unwrap();
-                        let def_id = rustc_internal::internal(self.tcx(), instance.def.def_id());
+                        let def_id = instance.def.def_id();
                         let fid = self.register_fun_decl_id(def_id);
                         FnPtr {
                             func: FunIdOrTraitMethodRef::Fun(FunId::Regular(fid)),
@@ -555,17 +575,23 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                     args: args.iter().map(|arg| self.translate_operand(arg)).collect(),
                     dest: self.translate_place(destination),
                 };
-                RawTerminator::Call { call, target: target.map(BlockId::from_usize) }
-            }
-            TerminatorKind::Assert { cond, expected, msg: _, target, .. } => {
-                RawTerminator::Assert {
-                    assert: Assert { cond: self.translate_operand(cond), expected: *expected },
-                    target: BlockId::from_usize(*target),
-                }
+                (Some(RawStatement::Call(call)), RawTerminator::Goto {
+                    target: BlockId::from_usize(target.unwrap()),
+                })
             }
+            TerminatorKind::Assert { cond, expected, msg: _, target, .. } => (
+                Some(RawStatement::Assert(Assert {
+                    cond: self.translate_operand(cond),
+                    expected: *expected,
+                })),
+                RawTerminator::Goto { target: BlockId::from_usize(*target) },
+            ),
             _ => todo!(),
         };
-        CharonTerminator { span, content }
+        (
+            statement.map(|statement| CharonStatement { span, content: statement }),
+            CharonTerminator { span, content: terminator },
+        )
     }
 
     fn translate_place(&self, place: &Place) -> CharonPlace {
@@ -695,7 +721,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                 if value == 0 { (targets.otherwise(), bb) } else { (bb, targets.otherwise()) };
             CharonSwitchTargets::If(BlockId::from_usize(then_bb), BlockId::from_usize(else_bb))
         } else {
-            let CharonTy::Literal(LiteralTy::Integer(int_ty)) = charon_ty else {
+            let CharonTyKind::Literal(LiteralTy::Integer(int_ty)) = charon_ty.kind() else {
                 panic!("Expected integer type for switch discriminant");
             };
             let branches = targets
@@ -719,7 +745,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                 })
                 .collect();
             let otherwise = BlockId::from_usize(targets.otherwise());
-            CharonSwitchTargets::SwitchInt(int_ty, branches, otherwise)
+            CharonSwitchTargets::SwitchInt(*int_ty, branches, otherwise)
         };
         (discr, switch_targets)
     }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index ef0468cd6cc5..3a72fd45fa35 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -373,6 +373,14 @@ impl GotocCtx<'_> {
                 let binop_stmt = codegen_intrinsic_binop!(div);
                 self.add_finite_args_checks(intrinsic_str, fargs_clone, binop_stmt, span)
             }
+            Intrinsic::FloatToIntUnchecked => self.codegen_float_to_int_unchecked(
+                intrinsic_str,
+                fargs.remove(0),
+                farg_types[0],
+                place,
+                ret_ty,
+                loc,
+            ),
             Intrinsic::FloorF32 => codegen_simple_intrinsic!(Floorf),
             Intrinsic::FloorF64 => codegen_simple_intrinsic!(Floor),
             Intrinsic::FmafF32 => codegen_simple_intrinsic!(Fmaf),
@@ -711,7 +719,7 @@ impl GotocCtx<'_> {
 
         // For all intrinsics we first check `is_uninhabited` to give a more
         // precise error message
-        if layout.abi.is_uninhabited() {
+        if layout.is_uninhabited() {
             return self.codegen_fatal_error(
                 PropertyClass::SafetyCheck,
                 &format!(
@@ -1907,6 +1915,57 @@ impl GotocCtx<'_> {
             Stmt::block(vec![non_overlapping_stmt, assign_to_t, assign_to_y, assign_to_x], loc)
         }
     }
+
+    /// Checks that the floating-point value is:
+    ///     1. Finite (i.e. neither infinite nor NaN)
+    ///     2. Its truncated value is in range of the target integer
+    /// then performs the cast to the target type
+    pub fn codegen_float_to_int_unchecked(
+        &mut self,
+        intrinsic: &str,
+        expr: Expr,
+        ty: Ty,
+        place: &Place,
+        res_ty: Ty,
+        loc: Location,
+    ) -> Stmt {
+        let finite_check = self.codegen_assert_assume(
+            expr.clone().is_finite(),
+            PropertyClass::ArithmeticOverflow,
+            format!("{intrinsic}: attempt to convert a non-finite value to an integer").as_str(),
+            loc,
+        );
+
+        assert!(res_ty.kind().is_integral());
+        assert!(ty.kind().is_float());
+        let TyKind::RigidTy(integral_ty) = res_ty.kind() else {
+            panic!(
+                "Expected intrinsic `{}` type to be `RigidTy`, but found: `{:?}`",
+                intrinsic, res_ty
+            );
+        };
+        let TyKind::RigidTy(RigidTy::Float(float_type)) = ty.kind() else {
+            panic!("Expected intrinsic `{}` type to be `Float`, but found: `{:?}`", intrinsic, ty);
+        };
+        let mm = self.symbol_table.machine_model();
+        let in_range = utils::codegen_in_range_expr(&expr, float_type, integral_ty, mm);
+
+        let range_check = self.codegen_assert_assume(
+            in_range,
+            PropertyClass::ArithmeticOverflow,
+            format!("{intrinsic}: attempt to convert a value out of range of the target integer")
+                .as_str(),
+            loc,
+        );
+
+        let int_type = self.codegen_ty_stable(res_ty);
+        let cast = expr.cast_to(int_type);
+
+        Stmt::block(
+            vec![finite_check, range_check, self.codegen_expr_to_place_stable(place, cast, loc)],
+            loc,
+        )
+    }
 }
 
 fn instance_args(instance: &Instance) -> GenericArgs {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index 779874f2ff77..7f578940d98e 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -726,6 +726,17 @@ impl GotocCtx<'_> {
                             dynamic_fat_ptr(typ, data_cast, vtable_expr, &self.symbol_table)
                         }
                     }
+                    TyKind::RigidTy(RigidTy::Dynamic(..)) => {
+                        let pointee_goto_typ = self.codegen_ty_stable(pointee_ty);
+                        let data_cast =
+                            data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) });
+                        let meta = self.codegen_operand_stable(&operands[1]);
+                        let vtable_expr = meta
+                            .member("_vtable_ptr", &self.symbol_table)
+                            .member("pointer", &self.symbol_table)
+                            .cast_to(typ.lookup_field_type("vtable", &self.symbol_table).unwrap());
+                        dynamic_fat_ptr(typ, data_cast, vtable_expr, &self.symbol_table)
+                    }
                     _ => {
                         let pointee_goto_typ = self.codegen_ty_stable(pointee_ty);
                         data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) })
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index 06233a52b833..cc7f3655f51f 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -18,8 +18,8 @@ use rustc_middle::ty::{List, TypeFoldable};
 use rustc_smir::rustc_internal;
 use rustc_span::def_id::DefId;
 use rustc_target::abi::{
-    Abi::Vector, FieldIdx, FieldsShape, Float, Integer, LayoutS, Primitive, Size, TagEncoding,
-    TyAndLayout, VariantIdx, Variants,
+    BackendRepr::Vector, FieldIdx, FieldsShape, Float, Integer, LayoutData, Primitive, Size,
+    TagEncoding, TyAndLayout, VariantIdx, Variants,
 };
 use stable_mir::abi::{ArgAbi, FnAbi, PassMode};
 use stable_mir::mir::Body;
@@ -675,7 +675,7 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_alignment_padding(
         &self,
         size: Size,
-        layout: &LayoutS<FieldIdx, VariantIdx>,
+        layout: &LayoutData<FieldIdx, VariantIdx>,
         idx: usize,
     ) -> Option<DatatypeComponent> {
         let align = Size::from_bits(layout.align.abi.bits());
@@ -700,7 +700,7 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_struct_fields(
         &mut self,
         flds: Vec<(String, Ty<'tcx>)>,
-        layout: &LayoutS<FieldIdx, VariantIdx>,
+        layout: &LayoutData<FieldIdx, VariantIdx>,
         initial_offset: Size,
     ) -> Vec<DatatypeComponent> {
         match &layout.fields {
@@ -1112,7 +1112,7 @@ impl<'tcx> GotocCtx<'tcx> {
         &mut self,
         variant: &VariantDef,
         subst: &'tcx GenericArgsRef<'tcx>,
-        layout: &LayoutS<FieldIdx, VariantIdx>,
+        layout: &LayoutData<FieldIdx, VariantIdx>,
         initial_offset: Size,
     ) -> Vec<DatatypeComponent> {
         let flds: Vec<_> =
@@ -1251,7 +1251,7 @@ impl<'tcx> GotocCtx<'tcx> {
                             // https://github.com/rust-lang/rust/blob/e60ebb2f2c1facba87e7971798f3cbdfd309cd23/compiler/rustc_session/src/code_stats.rs#L166
                             let max_variant_size = variants
                                 .iter()
-                                .map(|l: &LayoutS<FieldIdx, VariantIdx>| l.size)
+                                .map(|l: &LayoutData<FieldIdx, VariantIdx>| l.size)
                                 .max()
                                 .unwrap();
                             let max_variant_size = std::cmp::max(max_variant_size, discr_offset);
@@ -1298,7 +1298,7 @@ impl<'tcx> GotocCtx<'tcx> {
         ty: Ty<'tcx>,
         adtdef: &'tcx AdtDef,
         subst: &'tcx GenericArgsRef<'tcx>,
-        variants: &IndexVec<VariantIdx, LayoutS<FieldIdx, VariantIdx>>,
+        variants: &IndexVec<VariantIdx, LayoutData<FieldIdx, VariantIdx>>,
     ) -> Type {
         let non_zst_count = variants.iter().filter(|layout| layout.size.bytes() > 0).count();
         let mangled_name = self.ty_mangled_name(ty);
@@ -1317,7 +1317,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
     pub(crate) fn variant_min_offset(
         &self,
-        variants: &IndexVec<VariantIdx, LayoutS<FieldIdx, VariantIdx>>,
+        variants: &IndexVec<VariantIdx, LayoutData<FieldIdx, VariantIdx>>,
     ) -> Option<Size> {
         variants
             .iter()
@@ -1407,7 +1407,7 @@ impl<'tcx> GotocCtx<'tcx> {
         pretty_name: InternedString,
         def: &'tcx AdtDef,
         subst: &'tcx GenericArgsRef<'tcx>,
-        layouts: &IndexVec<VariantIdx, LayoutS<FieldIdx, VariantIdx>>,
+        layouts: &IndexVec<VariantIdx, LayoutData<FieldIdx, VariantIdx>>,
         initial_offset: Size,
     ) -> Vec<DatatypeComponent> {
         def.variants()
@@ -1439,7 +1439,7 @@ impl<'tcx> GotocCtx<'tcx> {
         pretty_name: InternedString,
         case: &VariantDef,
         subst: &'tcx GenericArgsRef<'tcx>,
-        variant: &LayoutS<FieldIdx, VariantIdx>,
+        variant: &LayoutData<FieldIdx, VariantIdx>,
         initial_offset: Size,
     ) -> Type {
         let case_name = format!("{name}::{}", case.name);
@@ -1451,7 +1451,7 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     fn codegen_vector(&mut self, ty: Ty<'tcx>) -> Type {
-        let layout = &self.layout_of(ty).layout.abi();
+        let layout = &self.layout_of(ty).layout.backend_repr();
         debug! {"handling simd with layout {:?}", layout};
 
         let (element, size) = match layout {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
index cef6aa58b9b7..6e07390940fe 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -46,15 +46,13 @@ use stable_mir::mir::mono::{Instance, MonoItem};
 use stable_mir::{CrateDef, DefId};
 use std::any::Any;
 use std::collections::BTreeMap;
-use std::ffi::OsString;
 use std::fmt::Write;
 use std::fs::File;
 use std::io::BufWriter;
-use std::path::{Path, PathBuf};
-use std::process::Command;
+use std::path::Path;
 use std::sync::{Arc, Mutex};
 use std::time::Instant;
-use tracing::{debug, error, info};
+use tracing::{debug, info};
 
 pub type UnsupportedConstructs = FxHashMap<InternedString, Vec<Location>>;
 
@@ -204,12 +202,7 @@ impl GotocCodegenBackend {
         if !tcx.sess.opts.unstable_opts.no_codegen && tcx.sess.opts.output_types.should_codegen() {
             let pretty = self.queries.lock().unwrap().args().output_pretty_json;
             write_file(&symtab_goto, ArtifactType::PrettyNameMap, &pretty_name_map, pretty);
-            if gcx.queries.args().write_json_symtab {
-                write_file(&symtab_goto, ArtifactType::SymTab, &gcx.symbol_table, pretty);
-                symbol_table_to_gotoc(&tcx, &symtab_goto);
-            } else {
-                write_goto_binary_file(symtab_goto, &gcx.symbol_table);
-            }
+            write_goto_binary_file(symtab_goto, &gcx.symbol_table);
             write_file(&symtab_goto, ArtifactType::TypeMap, &type_map, pretty);
             // If they exist, write out vtable virtual call function pointer restrictions
             if let Some(restrictions) = vtable_restrictions {
@@ -270,6 +263,7 @@ impl CodegenBackend for GotocCodegenBackend {
                 ReachabilityType::Harnesses => {
                     let mut units = CodegenUnits::new(&queries, tcx);
                     let mut modifies_instances = vec![];
+                    let mut loop_contracts_instances = vec![];
                     // Cross-crate collecting of all items that are reachable from the crate harnesses.
                     for unit in units.iter() {
                         // We reset the body cache for now because each codegen unit has different
@@ -287,6 +281,9 @@ impl CodegenBackend for GotocCodegenBackend {
                                 contract_metadata,
                                 transformer,
                             );
+                            if gcx.has_loop_contracts {
+                                loop_contracts_instances.push(*harness);
+                            }
                             results.extend(gcx, items, None);
                             if let Some(assigns_contract) = contract_info {
                                 modifies_instances.push((*harness, assigns_contract));
@@ -294,6 +291,7 @@ impl CodegenBackend for GotocCodegenBackend {
                         }
                     }
                     units.store_modifies(&modifies_instances);
+                    units.store_loop_contracts(&loop_contracts_instances);
                     units.write_metadata(&queries, tcx);
                 }
                 ReachabilityType::Tests => {
@@ -545,40 +543,6 @@ fn codegen_results(
     ))
 }
 
-fn symbol_table_to_gotoc(tcx: &TyCtxt, base_path: &Path) -> PathBuf {
-    let output_filename = base_path.to_path_buf();
-    let input_filename = convert_type(base_path, ArtifactType::SymTabGoto, ArtifactType::SymTab);
-
-    let args = vec![
-        input_filename.clone().into_os_string(),
-        "--out".into(),
-        OsString::from(output_filename.as_os_str()),
-    ];
-    // TODO get symtab2gb path from self
-    let mut cmd = Command::new("symtab2gb");
-    cmd.args(args);
-    info!("[Kani] Running: `{:?} {:?}`", cmd.get_program(), cmd.get_args());
-
-    let result = with_timer(
-        || {
-            cmd.output()
-                .expect(&format!("Failed to generate goto model for {}", input_filename.display()))
-        },
-        "symtab2gb",
-    );
-    if !result.status.success() {
-        error!("Symtab error output:\n{}", String::from_utf8_lossy(&result.stderr));
-        error!("Symtab output:\n{}", String::from_utf8_lossy(&result.stdout));
-        let err_msg = format!(
-            "Failed to generate goto model:\n\tsymtab2gb failed on file {}.",
-            input_filename.display()
-        );
-        tcx.dcx().err(err_msg);
-        tcx.dcx().abort_if_errors();
-    };
-    output_filename
-}
-
 pub fn write_file<T>(base_path: &Path, file_type: ArtifactType, source: &T, pretty: bool)
 where
     T: serde::Serialize,
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 176268022f34..6fd9da651002 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
@@ -74,6 +74,8 @@ pub struct GotocCtx<'tcx> {
     pub concurrent_constructs: UnsupportedConstructs,
     /// The body transformation agent.
     pub transformer: BodyTransformation,
+    /// If there exist some usage of loop contracts int context.
+    pub has_loop_contracts: bool,
 }
 
 /// Constructor
@@ -103,6 +105,7 @@ impl<'tcx> GotocCtx<'tcx> {
             unsupported_constructs: FxHashMap::default(),
             concurrent_constructs: FxHashMap::default(),
             transformer,
+            has_loop_contracts: false,
         }
     }
 }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
index 8675d3fad3f3..74c39c45ed74 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
@@ -567,15 +567,52 @@ impl GotocHook for LoopInvariantRegister {
         gcx: &mut GotocCtx,
         instance: Instance,
         fargs: Vec<Expr>,
-        _assign_to: &Place,
+        assign_to: &Place,
         target: Option<BasicBlockIdx>,
         span: Span,
     ) -> Stmt {
         let loc = gcx.codegen_span_stable(span);
         let func_exp = gcx.codegen_func_expr(instance, loc);
 
-        Stmt::goto(bb_label(target.unwrap()), loc)
-            .with_loop_contracts(func_exp.call(fargs).cast_to(Type::CInteger(CIntType::Bool)))
+        gcx.has_loop_contracts = true;
+
+        if gcx.queries.args().unstable_features.contains(&"loop-contracts".to_string()) {
+            // When loop-contracts is enabled, codegen
+            // free(0)
+            // goto target --- with loop contracts annotated.
+
+            // Add `free(0)` to make sure the body of `free` won't be dropped to
+            // satisfy the requirement of DFCC.
+            Stmt::block(
+                vec![
+                    BuiltinFn::Free
+                        .call(vec![Expr::pointer_constant(0, Type::void_pointer())], loc)
+                        .as_stmt(loc),
+                    Stmt::goto(bb_label(target.unwrap()), loc).with_loop_contracts(
+                        func_exp.call(fargs).cast_to(Type::CInteger(CIntType::Bool)),
+                    ),
+                ],
+                loc,
+            )
+        } else {
+            // When loop-contracts is not enabled, codegen
+            // assign_to = true
+            // goto target
+            Stmt::block(
+                vec![
+                    unwrap_or_return_codegen_unimplemented_stmt!(
+                        gcx,
+                        gcx.codegen_place_stable(assign_to, loc)
+                    )
+                    .goto_expr
+                    .assign(Expr::c_true(), loc),
+                    Stmt::goto(bb_label(target.unwrap()), loc).with_loop_contracts(
+                        func_exp.call(fargs).cast_to(Type::CInteger(CIntType::Bool)),
+                    ),
+                ],
+                loc,
+            )
+        }
     }
 }
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs
new file mode 100644
index 000000000000..a50353b7c96d
--- /dev/null
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs
@@ -0,0 +1,435 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This module contains utilities related to floating-point types
+
+use cbmc::{MachineModel, goto_program::Expr};
+use stable_mir::ty::{FloatTy, IntTy, RigidTy, UintTy};
+
+/// This function creates a boolean expression that the given `float_expr` when truncated is in the range of `integral_ty`.
+///
+/// The expression it generates is in the form:
+///
+///     `float_expr > lower_bound && float_expr < upper_bound`
+///
+/// i.e., the comparison is performed in terms of floats
+///
+/// Generally, the lower bound for an integral type is `MIN - 1` and the upper bound is `MAX + 1`.
+/// For example, for `i16`, the lower bound is `i16::MIN - 1` (-32769) and the upper bound is `i16::MAX + 1` (32768)
+/// Similarly, for `u8`, the lower bound is `u8::MIN - 1` (-1) and the upper bound is `u8::MAX + 1` (256)
+///
+/// However, due to the floating-point imprecision, not every value has a representation.
+/// For example, while `i16::MIN - 1` (-32769) and `u8::MAX + 1` (256) can be accurately represented as `f32` and `f64`,
+/// `i32::MIN - 1` (-2147483649) cannot be represented in `f32` (the closest `f32` value is -2147483648).
+/// See https://www.h-schmidt.net/FloatConverter/IEEE754.html
+///
+/// If we were to just use `MIN - 1`, the resulting expression may exclude values that are actually in range.
+/// For example, `float_expr > ((i32::MIN - 1) as f32)` would expand to `float_expr > -2147483649 as f32` which
+/// would result in `float_expr > -2147483648.0`. This expression incorrectly exlcudes a valid `i32`
+/// value: `i32::MIN` = -2147483648.
+///
+/// Thus, to determine the lower bound, we need to find the **largest** floating-point value that is
+/// less than or equal to `MIN - 1`.
+/// For example, for `i32`, the largest such value is `-2147483904.0`
+/// Similarly, to determine the upper bound, we need to find the smallest floating-point value that is
+/// greater than or equal to `MAX + 1`.
+///
+/// An alternative approach would be to perform the float-to-int cast with a wider integer and
+/// then check if the wider integer value is in the range of the narrower integer value.
+/// This seems to be the approach used in MIRI:
+/// https://github.com/rust-lang/rust/blob/096277e989d6de11c3077472fc05778e261e7b8e/src/tools/miri/src/helpers.rs#L1003
+/// but it's not clear what it does for `i128` and `u128`.
+pub fn codegen_in_range_expr(
+    float_expr: &Expr,
+    float_ty: FloatTy,
+    integral_ty: RigidTy,
+    mm: &MachineModel,
+) -> Expr {
+    match float_ty {
+        FloatTy::F32 => {
+            let (lower, upper) = get_bounds_f32(integral_ty, mm);
+            let mut in_range = Expr::bool_true();
+            // Avoid unnecessary comparison against -∞ or ∞
+            if lower != f32::NEG_INFINITY {
+                in_range = in_range.and(float_expr.clone().gt(Expr::float_constant(lower)));
+            }
+            if upper != f32::INFINITY {
+                in_range = in_range.and(float_expr.clone().lt(Expr::float_constant(upper)));
+            }
+            in_range
+        }
+        FloatTy::F64 => {
+            let (lower, upper) = get_bounds_f64(integral_ty, mm);
+            let mut in_range = Expr::bool_true();
+            if lower != f64::NEG_INFINITY {
+                in_range = in_range.and(float_expr.clone().gt(Expr::double_constant(lower)));
+            }
+            if upper != f64::INFINITY {
+                in_range = in_range.and(float_expr.clone().lt(Expr::double_constant(upper)));
+            }
+            in_range
+        }
+        _ => unimplemented!(),
+    }
+}
+
+const F32_I8_LOWER: [u8; 4] = [0x00, 0x00, 0x01, 0xC3]; // -129.0
+const F32_I8_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x43]; // 128.0
+const F32_I16_LOWER: [u8; 4] = [0x00, 0x01, 0x00, 0xC7]; // -32769.0
+const F32_I16_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x47]; // 32768.0
+const F32_I32_LOWER: [u8; 4] = [0x01, 0x00, 0x00, 0xCF]; // -2147483904.0
+const F32_I32_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x4F]; // 2147483648.0
+const F32_I64_LOWER: [u8; 4] = [0x01, 0x00, 0x00, 0xDF]; // -9223373136366403584.0
+const F32_I64_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x5F]; // 9223372036854775808.0
+// The next value is determined manually and not via test:
+const F32_I128_LOWER: [u8; 4] = [0x01, 0x00, 0x00, 0xFF]; // -170141203742878835383357727663135391744.0
+const F32_I128_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x7F]; // 170141183460469231731687303715884105728.0
+
+const F64_I8_LOWER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x20, 0x60, 0xC0]; // -129.0
+const F64_I8_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x60, 0x40]; // 128.0
+const F64_I16_LOWER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x20, 0x00, 0xE0, 0xC0]; // -32769.0
+const F64_I16_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0x40]; // 32768.0
+const F64_I32_LOWER: [u8; 8] = [0x00, 0x00, 0x20, 0x00, 0x00, 0x00, 0xE0, 0xC1]; // -2147483649.0
+const F64_I32_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0x41]; // 2147483648.0
+const F64_I64_LOWER: [u8; 8] = [0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0xC3]; // -9223372036854777856.0
+const F64_I64_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0x43]; // 9223372036854775808.0
+// The next value is determined manually and not via test:
+const F64_I128_LOWER: [u8; 8] = [0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0xC7]; // -170141183460469269510619166673045815296.0
+const F64_I128_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0x47]; // 170141183460469231731687303715884105728.0
+
+const F32_U_LOWER: [u8; 4] = [0x00, 0x00, 0x80, 0xBF]; // -1.0
+const F32_U8_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x43]; // 256.0
+const F32_U16_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x47]; // 65536.0
+const F32_U32_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x4F]; // 4294967296.0
+const F32_U64_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x5F]; // 18446744073709551616.0
+// The largest f32 value fits in a u128, so there is no upper bound
+const F32_U128_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x7F]; // inf
+
+const F64_U_LOWER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0xBF]; // -1.0
+const F64_U8_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x70, 0x40]; // 256.0
+const F64_U16_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x40]; // 65536.0
+const F64_U32_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x41]; // 4294967296.0
+const F64_U64_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x43]; // 18446744073709551616.0
+const F64_U128_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x47]; // 340282366920938463463374607431768211456.0
+
+/// upper is the smallest `f32` that after truncation is strictly larger than i<N>::MAX or u<N>::MAX
+/// lower is the largest `f32` that after truncation is strictly smaller than i<N>::MIN or u<N>::MIN
+///
+/// For example, for `u8`, upper is 256.0 because the previous f32 (i.e.
+/// `256_f32.next_down()` which is 255.9999847412109375) when truncated is 255.0,
+/// which is not strictly larger than `u8::MAX`
+///
+/// For `i16`, upper is 32768.0 because the previous f32 (i.e.
+/// `32768_f32.next_down()`) when truncated is 32767,
+/// which is not strictly larger than `i16::MAX`
+///
+/// Note that all upper bound values are 2^(w-1) which can be precisely
+/// represented in f32 (verified using
+/// https://www.h-schmidt.net/FloatConverter/IEEE754.html)
+/// However, for lower bound values, which should be -2^(w-1)-1 (i.e.
+/// i<N>::MIN-1), not all of them can be represented in f32.
+/// For instance, for w = 32, -2^(31)-1 = -2,147,483,649, but this number does
+/// **not** have an f32 representation, and the next **smaller** number is
+/// -2,147,483,904. Note that CBMC for example uses the formula above which
+/// leads to bugs, e.g.: https://github.com/diffblue/cbmc/issues/8488
+///
+/// For all unsigned types, lower is -1.0 because the next higher number, when
+/// truncated is -0.0 (or 0.0) which is not strictly smaller than `u<N>::MIN`
+fn get_bounds_f32(integral_ty: RigidTy, mm: &MachineModel) -> (f32, f32) {
+    match integral_ty {
+        RigidTy::Int(int_ty) => get_bounds_f32_int(int_ty, mm),
+        RigidTy::Uint(uint_ty) => get_bounds_f32_uint(uint_ty, mm),
+        _ => unreachable!(),
+    }
+}
+
+fn get_bounds_f64(integral_ty: RigidTy, mm: &MachineModel) -> (f64, f64) {
+    match integral_ty {
+        RigidTy::Int(int_ty) => get_bounds_f64_int(int_ty, mm),
+        RigidTy::Uint(uint_ty) => get_bounds_f64_uint(uint_ty, mm),
+        _ => unreachable!(),
+    }
+}
+
+fn get_bounds_f32_uint(uint_ty: UintTy, mm: &MachineModel) -> (f32, f32) {
+    let lower: f32 = f32::from_le_bytes(F32_U_LOWER);
+    let upper: f32 = match uint_ty {
+        UintTy::U8 => f32::from_le_bytes(F32_U8_UPPER),
+        UintTy::U16 => f32::from_le_bytes(F32_U16_UPPER),
+        UintTy::U32 => f32::from_le_bytes(F32_U32_UPPER),
+        UintTy::U64 => f32::from_le_bytes(F32_U64_UPPER),
+        UintTy::U128 => f32::from_le_bytes(F32_U128_UPPER),
+        UintTy::Usize => match mm.pointer_width {
+            32 => f32::from_le_bytes(F32_U32_UPPER),
+            64 => f32::from_le_bytes(F32_U64_UPPER),
+            _ => unreachable!(),
+        },
+    };
+    (lower, upper)
+}
+
+fn get_bounds_f64_uint(uint_ty: UintTy, mm: &MachineModel) -> (f64, f64) {
+    let lower = f64::from_le_bytes(F64_U_LOWER);
+    let upper = match uint_ty {
+        UintTy::U8 => f64::from_le_bytes(F64_U8_UPPER),
+        UintTy::U16 => f64::from_le_bytes(F64_U16_UPPER),
+        UintTy::U32 => f64::from_le_bytes(F64_U32_UPPER),
+        UintTy::U64 => f64::from_le_bytes(F64_U64_UPPER),
+        UintTy::U128 => f64::from_le_bytes(F64_U128_UPPER),
+        UintTy::Usize => match mm.pointer_width {
+            32 => f64::from_le_bytes(F64_U32_UPPER),
+            64 => f64::from_le_bytes(F64_U64_UPPER),
+            _ => unreachable!(),
+        },
+    };
+    (lower, upper)
+}
+
+fn get_bounds_f32_int(int_ty: IntTy, mm: &MachineModel) -> (f32, f32) {
+    let lower = match int_ty {
+        IntTy::I8 => f32::from_le_bytes(F32_I8_LOWER),
+        IntTy::I16 => f32::from_le_bytes(F32_I16_LOWER),
+        IntTy::I32 => f32::from_le_bytes(F32_I32_LOWER),
+        IntTy::I64 => f32::from_le_bytes(F32_I64_LOWER),
+        IntTy::I128 => f32::from_le_bytes(F32_I128_LOWER),
+        IntTy::Isize => match mm.pointer_width {
+            32 => f32::from_le_bytes(F32_I32_LOWER),
+            64 => f32::from_le_bytes(F32_I64_LOWER),
+            _ => unreachable!(),
+        },
+    };
+
+    let upper = match int_ty {
+        IntTy::I8 => f32::from_le_bytes(F32_I8_UPPER),
+        IntTy::I16 => f32::from_le_bytes(F32_I16_UPPER),
+        IntTy::I32 => f32::from_le_bytes(F32_I32_UPPER),
+        IntTy::I64 => f32::from_le_bytes(F32_I64_UPPER),
+        IntTy::I128 => f32::from_le_bytes(F32_I128_UPPER),
+        IntTy::Isize => match mm.pointer_width {
+            32 => f32::from_le_bytes(F32_I32_UPPER),
+            64 => f32::from_le_bytes(F32_I64_UPPER),
+            _ => unreachable!(),
+        },
+    };
+    (lower, upper)
+}
+
+fn get_bounds_f64_int(int_ty: IntTy, mm: &MachineModel) -> (f64, f64) {
+    let lower = match int_ty {
+        IntTy::I8 => f64::from_le_bytes(F64_I8_LOWER),
+        IntTy::I16 => f64::from_le_bytes(F64_I16_LOWER),
+        IntTy::I32 => f64::from_le_bytes(F64_I32_LOWER),
+        IntTy::I64 => f64::from_le_bytes(F64_I64_LOWER),
+        IntTy::I128 => f64::from_le_bytes(F64_I128_LOWER),
+        IntTy::Isize => match mm.pointer_width {
+            32 => f64::from_le_bytes(F64_I32_LOWER),
+            64 => f64::from_le_bytes(F64_I64_LOWER),
+            _ => unreachable!(),
+        },
+    };
+    let upper = match int_ty {
+        IntTy::I8 => f64::from_le_bytes(F64_I8_UPPER),
+        IntTy::I16 => f64::from_le_bytes(F64_I16_UPPER),
+        IntTy::I32 => f64::from_le_bytes(F64_I32_UPPER),
+        IntTy::I64 => f64::from_le_bytes(F64_I64_UPPER),
+        IntTy::I128 => f64::from_le_bytes(F64_I128_UPPER),
+        IntTy::Isize => match mm.pointer_width {
+            32 => f64::from_le_bytes(F64_I32_UPPER),
+            64 => f64::from_le_bytes(F64_I64_UPPER),
+            _ => unreachable!(),
+        },
+    };
+    (lower, upper)
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use num::BigInt;
+    use num::FromPrimitive;
+
+    macro_rules! check_lower_f32 {
+        ($val:ident, $min:expr) => {
+            let f = f32::from_le_bytes($val);
+            assert!(BigInt::from_f32(f.trunc()).unwrap() < BigInt::from($min));
+            assert!(BigInt::from_f32(f.next_up().trunc()).unwrap() >= BigInt::from($min));
+        };
+    }
+
+    macro_rules! check_upper_f32 {
+        ($val:ident, $max:expr) => {
+            let f = f32::from_le_bytes($val);
+            assert!(BigInt::from_f32(f.trunc()).unwrap() > BigInt::from($max));
+            assert!(BigInt::from_f32(f.next_down().trunc()).unwrap() <= BigInt::from($max));
+        };
+    }
+
+    #[test]
+    fn check_f32_bounds() {
+        // check that the bounds are correct, i.e. that for lower (upper) bounds:
+        //   1. the value when truncated is strictly smaller (larger) than i<N>::MIN or u<N>::MIN (i<N>::MAX or u<N>::MAX)
+        //   2. the next higher (lower) value when truncated is greater (smaller) than or equal to i<N>::MIN or u<N>::MIN (i<N>::MAX or u<N>::MAX)
+
+        check_lower_f32!(F32_U_LOWER, u8::MIN);
+
+        check_upper_f32!(F32_U8_UPPER, u8::MAX);
+        check_upper_f32!(F32_U16_UPPER, u16::MAX);
+        check_upper_f32!(F32_U32_UPPER, u32::MAX);
+        check_upper_f32!(F32_U64_UPPER, u64::MAX);
+        // 128 is not needed because the upper bounds is infinity
+        // Instead, check that `u128::MAX` is larger than the largest f32 value
+        assert!(f32::MAX < u128::MAX as f32);
+
+        check_lower_f32!(F32_I8_LOWER, i8::MIN);
+        check_lower_f32!(F32_I16_LOWER, i16::MIN);
+        check_lower_f32!(F32_I32_LOWER, i32::MIN);
+        check_lower_f32!(F32_I64_LOWER, i64::MIN);
+        check_lower_f32!(F32_I128_LOWER, i128::MIN);
+
+        check_upper_f32!(F32_I8_UPPER, i8::MAX);
+        check_upper_f32!(F32_I16_UPPER, i16::MAX);
+        check_upper_f32!(F32_I32_UPPER, i32::MAX);
+        check_upper_f32!(F32_I64_UPPER, i64::MAX);
+        check_upper_f32!(F32_I128_UPPER, i128::MAX);
+    }
+
+    macro_rules! check_lower_f64 {
+        ($val:ident, $min:expr) => {
+            let f = f64::from_le_bytes($val);
+            assert!(BigInt::from_f64(f.trunc()).unwrap() < BigInt::from($min));
+            assert!(BigInt::from_f64(f.next_up().trunc()).unwrap() >= BigInt::from($min));
+        };
+    }
+
+    macro_rules! check_upper_f64 {
+        ($val:ident, $max:expr) => {
+            let f = f64::from_le_bytes($val);
+            assert!(BigInt::from_f64(f.trunc()).unwrap() > BigInt::from($max));
+            assert!(BigInt::from_f64(f.next_down().trunc()).unwrap() <= BigInt::from($max));
+        };
+    }
+
+    #[test]
+    fn check_f64_bounds() {
+        // check that the bounds are correct, i.e. that for lower (upper) bounds:
+        //   1. the value when truncated is strictly smaller (larger) than {i, u}<N>::MIN ({i, u}<N>::MAX)
+        //   2. the next higher (lower) value when truncated is greater (smaller) than or equal to {i, u}<N>::MIN ({i, u}<N>::MAX)
+
+        check_lower_f64!(F64_U_LOWER, u8::MIN);
+
+        check_upper_f64!(F64_U8_UPPER, u8::MAX);
+        check_upper_f64!(F64_U16_UPPER, u16::MAX);
+        check_upper_f64!(F64_U32_UPPER, u32::MAX);
+        check_upper_f64!(F64_U64_UPPER, u64::MAX);
+        check_upper_f64!(F64_U128_UPPER, u128::MAX);
+
+        check_lower_f64!(F64_I8_LOWER, i8::MIN);
+        check_lower_f64!(F64_I16_LOWER, i16::MIN);
+        check_lower_f64!(F64_I32_LOWER, i32::MIN);
+        check_lower_f64!(F64_I64_LOWER, i64::MIN);
+        check_lower_f64!(F64_I128_LOWER, i128::MIN);
+
+        check_upper_f64!(F64_I8_UPPER, i8::MAX);
+        check_upper_f64!(F64_I16_UPPER, i16::MAX);
+        check_upper_f64!(F64_I32_UPPER, i32::MAX);
+        check_upper_f64!(F64_I64_UPPER, i64::MAX);
+        check_upper_f64!(F64_I128_UPPER, i128::MAX);
+    }
+
+    macro_rules! find_upper_fn {
+        ($fn_name:ident, $float_ty:ty) => {
+            fn $fn_name(start: u128) -> $float_ty {
+                let mut current = start + 1;
+                let mut f = current as $float_ty;
+
+                while f.trunc() as u128 <= start {
+                    let f1 = (current + 1) as $float_ty;
+                    let f2 = f.next_up();
+                    f = if f1 > f2 { f1 } else { f2 };
+                    current = f as u128;
+                }
+                f
+            }
+        };
+    }
+
+    macro_rules! find_lower_fn {
+        ($fn_name:ident, $float_ty:ty) => {
+            fn $fn_name(start: i128) -> $float_ty {
+                let mut current = start - 1;
+                let mut f = current as $float_ty;
+
+                while f.trunc() >= start as $float_ty {
+                    let f1 = (current - 1) as $float_ty;
+                    let f2 = f.next_down();
+                    f = if f1 < f2 { f1 } else { f2 };
+                    current = f as i128;
+                }
+                f
+            }
+        };
+    }
+
+    find_lower_fn!(find_lower_f32, f32);
+    find_upper_fn!(find_upper_f32, f32);
+    find_lower_fn!(find_lower_f64, f64);
+    find_upper_fn!(find_upper_f64, f64);
+
+    macro_rules! find_and_print {
+        (f32, $var_name:expr, $fn_name:ident, $start:expr) => {
+            let f = $fn_name($start);
+            let bytes = f.to_le_bytes();
+            println!("const {}: [u8; 4] = [0x{:02X}, 0x{:02X}, 0x{:02X}, 0x{:02X}]; // {f:.1}", $var_name, bytes[0], bytes[1], bytes[2], bytes[3]);
+        };
+        (f64, $var_name:expr, $fn_name:ident, $start:expr) => {
+            let f = $fn_name($start);
+            let bytes = f.to_le_bytes();
+            println!("const {}: [u8; 8] = [0x{:02X}, 0x{:02X}, 0x{:02X}, 0x{:02X}, 0x{:02X}, 0x{:02X}, 0x{:02X}, 0x{:02X}]; // {f:.1}", $var_name, bytes[0], bytes[1], bytes[2], bytes[3], bytes[4], bytes[5], bytes[6], bytes[7]);
+        };
+    }
+
+    #[test]
+    /// This test generates most of the bounds. To run it do:
+    /// `cargo test -p kani-compiler generate_bounds -- --nocapture`
+    fn generate_bounds() {
+        find_and_print!(f32, "F32_I8_LOWER", find_lower_f32, i8::MIN as i128);
+        find_and_print!(f32, "F32_I8_UPPER", find_upper_f32, i8::MAX as u128);
+        find_and_print!(f32, "F32_I16_LOWER", find_lower_f32, i16::MIN as i128);
+        find_and_print!(f32, "F32_I16_UPPER", find_upper_f32, i16::MAX as u128);
+        find_and_print!(f32, "F32_I32_LOWER", find_lower_f32, i32::MIN as i128);
+        find_and_print!(f32, "F32_I32_UPPER", find_upper_f32, i32::MAX as u128);
+        find_and_print!(f32, "F32_I64_LOWER", find_lower_f32, i64::MIN as i128);
+        find_and_print!(f32, "F32_I64_UPPER", find_upper_f32, i64::MAX as u128);
+        // cannot use because of overflow
+        //find_and_print!(f32, "F32_I128_LOWER", find_lower_f32, i128::MIN as i128);
+        find_and_print!(f32, "F32_I128_UPPER", find_upper_f32, i128::MAX as u128);
+        println!();
+        find_and_print!(f64, "F64_I8_LOWER", find_lower_f64, i8::MIN as i128);
+        find_and_print!(f64, "F64_I8_UPPER", find_upper_f64, i8::MAX as u128);
+        find_and_print!(f64, "F64_I16_LOWER", find_lower_f64, i16::MIN as i128);
+        find_and_print!(f64, "F64_I16_UPPER", find_upper_f64, i16::MAX as u128);
+        find_and_print!(f64, "F64_I32_LOWER", find_lower_f64, i32::MIN as i128);
+        find_and_print!(f64, "F64_I32_UPPER", find_upper_f64, i32::MAX as u128);
+        find_and_print!(f64, "F64_I64_LOWER", find_lower_f64, i64::MIN as i128);
+        find_and_print!(f64, "F64_I64_UPPER", find_upper_f64, i64::MAX as u128);
+        // cannot use because of overflow
+        //find_and_print!(f64, "F64_I128_LOWER", find_lower_f64, i128::MIN as i128);
+        find_and_print!(f64, "F64_I128_UPPER", find_upper_f64, i128::MAX as u128);
+        println!();
+        find_and_print!(f32, "F32_U_LOWER", find_lower_f32, u8::MIN as i128);
+        find_and_print!(f32, "F32_U8_UPPER", find_upper_f32, u8::MAX as u128);
+        find_and_print!(f32, "F32_U16_UPPER", find_upper_f32, u16::MAX as u128);
+        find_and_print!(f32, "F32_U32_UPPER", find_upper_f32, u32::MAX as u128);
+        find_and_print!(f32, "F32_U64_UPPER", find_upper_f32, u64::MAX as u128);
+        // cannot use because of overflow
+        //find_and_print!(f32, "F32_U128_UPPER", find_upper_f32, u128::MAX as u128);
+        println!();
+        find_and_print!(f64, "F64_U_LOWER", find_lower_f64, u8::MIN as i128);
+        find_and_print!(f64, "F64_U8_UPPER", find_upper_f64, u8::MAX as u128);
+        find_and_print!(f64, "F64_U16_UPPER", find_upper_f64, u16::MAX as u128);
+        find_and_print!(f64, "F64_U32_UPPER", find_upper_f64, u32::MAX as u128);
+        find_and_print!(f64, "F64_U64_UPPER", find_upper_f64, u64::MAX as u128);
+        // cannot use because of overflow
+        //find_and_print!(f64, "F64_U128_UPPER", find_upper_f64, u128::MAX as u128);
+    }
+}
diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/mod.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/mod.rs
index 9d832146e3e8..8f176510d348 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/utils/mod.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/mod.rs
@@ -4,12 +4,14 @@
 //! This module provides utils used across Kani
 
 mod debug;
+mod float_utils;
 mod names;
 #[allow(clippy::module_inception)]
 mod utils;
 
 // TODO clean this up
 
+pub use float_utils::*;
 pub use names::*;
 pub use utils::*;
 
diff --git a/kani-compiler/src/intrinsics.rs b/kani-compiler/src/intrinsics.rs
index 13a12751bd07..0121975b11a2 100644
--- a/kani-compiler/src/intrinsics.rs
+++ b/kani-compiler/src/intrinsics.rs
@@ -63,6 +63,7 @@ pub enum Intrinsic {
     FabsF64,
     FaddFast,
     FdivFast,
+    FloatToIntUnchecked,
     FloorF32,
     FloorF64,
     FmafF32,
@@ -283,6 +284,14 @@ impl Intrinsic {
                 assert_sig_matches!(sig, _, _ => _);
                 Self::FdivFast
             }
+            "float_to_int_unchecked" => {
+                assert_sig_matches!(sig, RigidTy::Float(_) => _);
+                assert!(matches!(
+                    sig.output().kind(),
+                    TyKind::RigidTy(RigidTy::Int(_)) | TyKind::RigidTy(RigidTy::Uint(_))
+                ));
+                Self::FloatToIntUnchecked
+            }
             "fmul_fast" => {
                 assert_sig_matches!(sig, _, _ => _);
                 Self::FmulFast
diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs
index a6b6cf3a03af..d0f41ca0e2dc 100644
--- a/kani-compiler/src/kani_compiler.rs
+++ b/kani-compiler/src/kani_compiler.rs
@@ -16,7 +16,7 @@
 //! `-C llvm-args`.
 
 use crate::args::{Arguments, BackendOption};
-#[cfg(feature = "aeneas")]
+#[cfg(feature = "llbc")]
 use crate::codegen_aeneas_llbc::LlbcCodegenBackend;
 #[cfg(feature = "cprover")]
 use crate::codegen_cprover_gotoc::GotocCodegenBackend;
@@ -44,11 +44,11 @@ pub fn run(args: Vec<String>) -> ExitCode {
     }
 }
 
-/// Configure the Aeneas backend that generates LLBC.
-fn aeneas_backend(_queries: Arc<Mutex<QueryDb>>) -> Box<dyn CodegenBackend> {
-    #[cfg(feature = "aeneas")]
+/// Configure the LLBC backend (Aeneas's IR).
+fn llbc_backend(_queries: Arc<Mutex<QueryDb>>) -> Box<dyn CodegenBackend> {
+    #[cfg(feature = "llbc")]
     return Box::new(LlbcCodegenBackend::new(_queries));
-    #[cfg(not(feature = "aeneas"))]
+    #[cfg(not(feature = "llbc"))]
     unreachable!()
 }
 
@@ -60,21 +60,21 @@ fn cprover_backend(_queries: Arc<Mutex<QueryDb>>) -> Box<dyn CodegenBackend> {
     unreachable!()
 }
 
-#[cfg(any(feature = "aeneas", feature = "cprover"))]
+#[cfg(any(feature = "cprover", feature = "llbc"))]
 fn backend(queries: Arc<Mutex<QueryDb>>) -> Box<dyn CodegenBackend> {
     let backend = queries.lock().unwrap().args().backend;
     match backend {
-        #[cfg(feature = "aeneas")]
-        BackendOption::Aeneas => aeneas_backend(queries),
         #[cfg(feature = "cprover")]
         BackendOption::CProver => cprover_backend(queries),
+        #[cfg(feature = "llbc")]
+        BackendOption::Llbc => llbc_backend(queries),
     }
 }
 
 /// Fallback backend. It will trigger an error if no backend has been enabled.
-#[cfg(not(any(feature = "aeneas", feature = "cprover")))]
+#[cfg(not(any(feature = "cprover", feature = "llbc")))]
 fn backend(queries: Arc<Mutex<QueryDb>>) -> Box<CodegenBackend> {
-    compile_error!("No backend is available. Use `aeneas` or `cprover`.");
+    compile_error!("No backend is available. Use `cprover` or `llbc`.");
 }
 
 /// This object controls the compiler behavior.
diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index a8a51747193d..19db20e04a3c 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/kani-compiler/src/kani_middle/attributes.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! This module contains code for processing Rust attributes (like `kani::proof`).
 
-use std::collections::BTreeMap;
+use std::collections::{BTreeMap, HashSet};
 
 use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub};
 use quote::ToTokens;
@@ -475,6 +475,20 @@ impl<'tcx> KaniAttributes<'tcx> {
             || self.map.contains_key(&KaniAttributeKind::ProofForContract)
     }
 
+    /// Check that the function specified in the `proof_for_contract` attribute
+    /// is reachable and emit an error if it isn't
+    pub fn check_proof_for_contract(&self, reachable_functions: &HashSet<DefId>) {
+        if let Some((symbol, function, span)) = self.interpret_for_contract_attribute() {
+            if !reachable_functions.contains(&function) {
+                let err_msg = format!(
+                    "The function specified in the `proof_for_contract` attribute, `{symbol}`, was not found.\
+                    \nMake sure the function is reachable from the harness."
+                );
+                self.tcx.dcx().span_err(span, err_msg);
+            }
+        }
+    }
+
     /// Extract harness attributes for a given `def_id`.
     ///
     /// We only extract attributes for harnesses that are local to the current crate.
diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs
index ebb12f7656b6..072528f9a765 100644
--- a/kani-compiler/src/kani_middle/codegen_units.rs
+++ b/kani-compiler/src/kani_middle/codegen_units.rs
@@ -91,6 +91,13 @@ impl CodegenUnits {
         }
     }
 
+    /// We flag that the harness contains usage of loop contracts.
+    pub fn store_loop_contracts(&mut self, harnesses: &[Harness]) {
+        for harness in harnesses {
+            self.harness_info.get_mut(harness).unwrap().has_loop_contracts = true;
+        }
+    }
+
     /// Write compilation metadata into a file.
     pub fn write_metadata(&self, queries: &QueryDb, tcx: TyCtxt) {
         let metadata = self.generate_metadata(tcx);
diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs
index c92b20cf49d6..67d32b0079c4 100644
--- a/kani-compiler/src/kani_middle/metadata.rs
+++ b/kani-compiler/src/kani_middle/metadata.rs
@@ -38,6 +38,7 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) ->
         // TODO: This no longer needs to be an Option.
         goto_file: Some(model_file),
         contract: Default::default(),
+        has_loop_contracts: false,
     }
 }
 
@@ -108,5 +109,6 @@ pub fn gen_test_metadata(
         // TODO: This no longer needs to be an Option.
         goto_file: Some(model_file),
         contract: Default::default(),
+        has_loop_contracts: false,
     }
 }
diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs
index 3f4ba4099fad..b825175b2e0b 100644
--- a/kani-compiler/src/kani_middle/mod.rs
+++ b/kani-compiler/src/kani_middle/mod.rs
@@ -103,6 +103,13 @@ impl TyVisitor for FindUnsafeCell<'_> {
 pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) {
     // Avoid printing the same error multiple times for different instantiations of the same item.
     let mut def_ids = HashSet::new();
+    let reachable_functions: HashSet<InternalDefId> = items
+        .iter()
+        .filter_map(|i| match i {
+            MonoItem::Fn(instance) => Some(rustc_internal::internal(tcx, instance.def.def_id())),
+            _ => None,
+        })
+        .collect();
     for item in items.iter().filter(|i| matches!(i, MonoItem::Fn(..) | MonoItem::Static(..))) {
         let def_id = match item {
             MonoItem::Fn(instance) => instance.def.def_id(),
@@ -112,20 +119,17 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem])
             }
         };
         if !def_ids.contains(&def_id) {
+            let attributes = KaniAttributes::for_def_id(tcx, def_id);
             // Check if any unstable attribute was reached.
-            KaniAttributes::for_def_id(tcx, def_id)
-                .check_unstable_features(&queries.args().unstable_features);
+            attributes.check_unstable_features(&queries.args().unstable_features);
+            // Check whether all `proof_for_contract` functions are reachable
+            attributes.check_proof_for_contract(&reachable_functions);
             def_ids.insert(def_id);
         }
     }
     tcx.dcx().abort_if_errors();
 }
 
-/// Check that Kani library is configured correctly.
-///
-/// We cache the results for function definitions since it scans all functions defined in the
-/// `kani` or `core` library.
-
 /// Structure that represents the source location of a definition.
 /// TODO: Use `InternedString` once we move it out of the cprover_bindings.
 /// <https://github.com/model-checking/kani/issues/2435>
diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs
index 75ba43ab388d..8d9f14b3f969 100644
--- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs
+++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs
@@ -96,7 +96,7 @@ impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> {
         // and solves the dataflow problem, producing the cursor, which contains dataflow state for
         // each instruction in the body.
         let mut cursor =
-            analysis.into_engine(tcx, body).iterate_to_fixpoint().into_results_cursor(body);
+            analysis.iterate_to_fixpoint(tcx, body, Some(Self::NAME)).into_results_cursor(body);
         // We collect dataflow state at each `Return` terminator to determine the full aliasing
         // graph for the function. This is sound since those are the only places where the function
         // finishes, so the dataflow state at those places will be a union of dataflow states
diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs
index a348d285a28a..90bb0173ac55 100644
--- a/kani-compiler/src/kani_middle/stubbing/mod.rs
+++ b/kani-compiler/src/kani_middle/stubbing/mod.rs
@@ -37,24 +37,6 @@ pub fn harness_stub_map(
     stub_pairs
 }
 
-/// Retrieve the index of the host parameter if old definition has one, but not the new definition.
-///
-/// This is to allow constant functions to be stubbed by non-constant functions when the
-/// `effect` feature is on.
-///
-/// Note that the opposite is not supported today, but users should be able to change their stubs.
-///
-/// Note that this has no effect at runtime.
-pub fn contract_host_param(tcx: TyCtxt, old_def: FnDef, new_def: FnDef) -> Option<usize> {
-    let old_generics = tcx.generics_of(rustc_internal::internal(tcx, old_def.def_id()));
-    let new_generics = tcx.generics_of(rustc_internal::internal(tcx, new_def.def_id()));
-    if old_generics.host_effect_index.is_some() && new_generics.host_effect_index.is_none() {
-        old_generics.host_effect_index
-    } else {
-        None
-    }
-}
-
 /// Checks whether the stub is compatible with the original function/method: do
 /// the arities and types (of the parameters and return values) match up? This
 /// does **NOT** check whether the type variables are constrained to implement
@@ -81,15 +63,12 @@ pub fn check_compatibility(tcx: TyCtxt, old_def: FnDef, new_def: FnDef) -> Resul
     let new_def_id = rustc_internal::internal(tcx, new_def.def_id());
     let old_ty = rustc_internal::stable(tcx.type_of(old_def_id)).value;
     let new_ty = rustc_internal::stable(tcx.type_of(new_def_id)).value;
-    let TyKind::RigidTy(RigidTy::FnDef(_, mut old_args)) = old_ty.kind() else {
+    let TyKind::RigidTy(RigidTy::FnDef(_, old_args)) = old_ty.kind() else {
         unreachable!("Expected function, but found {old_ty}")
     };
     let TyKind::RigidTy(RigidTy::FnDef(_, new_args)) = new_ty.kind() else {
         unreachable!("Expected function, but found {new_ty}")
     };
-    if let Some(idx) = contract_host_param(tcx, old_def, new_def) {
-        old_args.0.remove(idx);
-    }
 
     // TODO: We should check for the parameter type too or replacement will fail.
     if old_args.0.len() != new_args.0.len() {
diff --git a/kani-compiler/src/kani_middle/transform/loop_contracts.rs b/kani-compiler/src/kani_middle/transform/loop_contracts.rs
index 8038ef784970..887c07ed4792 100644
--- a/kani-compiler/src/kani_middle/transform/loop_contracts.rs
+++ b/kani-compiler/src/kani_middle/transform/loop_contracts.rs
@@ -114,7 +114,7 @@ impl TransformPass for LoopContractPass {
                     let mut loop_queue: VecDeque<BasicBlockIdx> = VecDeque::new();
                     queue.push_back(0);
 
-                    while let Some(bb_idx) = queue.pop_front().or(loop_queue.pop_front()) {
+                    while let Some(bb_idx) = queue.pop_front().or_else(|| loop_queue.pop_front()) {
                         visited.insert(bb_idx);
 
                         let terminator = new_body.blocks()[bb_idx].terminator.clone();
@@ -126,9 +126,11 @@ impl TransformPass for LoopContractPass {
                         // the visiting queue.
                         for to_visit in terminator.successors() {
                             if !visited.contains(&to_visit) {
-                                let target_queue =
-                                    if is_loop_head { &mut loop_queue } else { &mut queue };
-                                target_queue.push_back(to_visit);
+                                if is_loop_head {
+                                    loop_queue.push_back(to_visit);
+                                } else {
+                                    queue.push_back(to_visit)
+                                };
                             }
                         }
                     }
diff --git a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs
index 4b304dca0463..53832948bf6b 100644
--- a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs
+++ b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs
@@ -77,7 +77,7 @@ impl<'a> ReplaceIntrinsicVisitor<'a> {
     }
 }
 
-impl<'a> MutMirVisitor for ReplaceIntrinsicVisitor<'a> {
+impl MutMirVisitor for ReplaceIntrinsicVisitor<'_> {
     /// Replace the terminator for some intrinsics.
     ///
     /// Note that intrinsics must always be called directly.
diff --git a/kani-compiler/src/kani_middle/transform/stubs.rs b/kani-compiler/src/kani_middle/transform/stubs.rs
index ae9f77ba239d..3d72cff0d56d 100644
--- a/kani-compiler/src/kani_middle/transform/stubs.rs
+++ b/kani-compiler/src/kani_middle/transform/stubs.rs
@@ -3,7 +3,7 @@
 //! This module contains code related to the MIR-to-MIR pass that performs the
 //! stubbing of functions and methods.
 use crate::kani_middle::codegen_units::Stubs;
-use crate::kani_middle::stubbing::{contract_host_param, validate_stub_const};
+use crate::kani_middle::stubbing::validate_stub_const;
 use crate::kani_middle::transform::body::{MutMirVisitor, MutableBody};
 use crate::kani_middle::transform::{TransformPass, TransformationType};
 use crate::kani_queries::QueryDb;
@@ -46,12 +46,8 @@ impl TransformPass for FnStubPass {
     fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
         trace!(function=?instance.name(), "transform");
         let ty = instance.ty();
-        if let TyKind::RigidTy(RigidTy::FnDef(fn_def, mut args)) = ty.kind() {
+        if let TyKind::RigidTy(RigidTy::FnDef(fn_def, args)) = ty.kind() {
             if let Some(replace) = self.stubs.get(&fn_def) {
-                if let Some(idx) = contract_host_param(tcx, fn_def, *replace) {
-                    debug!(?idx, "FnStubPass::transform remove_host_param");
-                    args.0.remove(idx);
-                }
                 let new_instance = Instance::resolve(*replace, &args).unwrap();
                 debug!(from=?instance.name(), to=?new_instance.name(), "FnStubPass::transform");
                 if let Some(body) = FnStubValidator::validate(tcx, (fn_def, *replace), new_instance)
diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs
index 1ba05d990955..9558b4159224 100644
--- a/kani-compiler/src/main.rs
+++ b/kani-compiler/src/main.rs
@@ -16,6 +16,7 @@
 #![feature(f128)]
 #![feature(f16)]
 #![feature(non_exhaustive_omitted_patterns_lint)]
+#![feature(float_next_up_down)]
 extern crate rustc_abi;
 extern crate rustc_ast;
 extern crate rustc_ast_pretty;
@@ -38,7 +39,7 @@ extern crate stable_mir;
 extern crate tempfile;
 
 mod args;
-#[cfg(feature = "aeneas")]
+#[cfg(feature = "llbc")]
 mod codegen_aeneas_llbc;
 #[cfg(feature = "cprover")]
 mod codegen_cprover_gotoc;
diff --git a/kani-dependencies b/kani-dependencies
index 6f844839086c..1f4428827e4e 100644
--- a/kani-dependencies
+++ b/kani-dependencies
@@ -1,10 +1,5 @@
 CBMC_MAJOR="6"
-CBMC_MINOR="3"
-CBMC_VERSION="6.3.1"
-
-# If you update this version number, remember to bump it in `src/setup.rs` too
-CBMC_VIEWER_MAJOR="3"
-CBMC_VIEWER_MINOR="9"
-CBMC_VIEWER_VERSION="3.9"
+CBMC_MINOR="4"
+CBMC_VERSION="6.4.0"
 
 KISSAT_VERSION="3.1.1"
diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml
index 67214738fa7c..844b844b8ef4 100644
--- a/kani-driver/Cargo.toml
+++ b/kani-driver/Cargo.toml
@@ -36,6 +36,8 @@ tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"
 rand = "0.8"
 which = "6"
 time = {version = "0.3.36", features = ["formatting"]}
+tokio = { version = "1.40.0", features = ["io-util", "process", "rt", "time"] }
+
 
 # A good set of suggested dependencies can be found in rustup:
 # https://github.com/rust-lang/rustup/blob/master/Cargo.toml
diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs
index 8aa758219524..2be3ff58f2fc 100644
--- a/kani-driver/src/args/mod.rs
+++ b/kani-driver/src/args/mod.rs
@@ -21,6 +21,7 @@ use kani_metadata::CbmcSolver;
 use std::ffi::OsString;
 use std::path::PathBuf;
 use std::str::FromStr;
+use std::time::Duration;
 use strum::VariantNames;
 
 /// Trait used to perform extra validation after parsing.
@@ -62,6 +63,53 @@ pub fn print_deprecated(verbosity: &CommonArgs, option: &str, alternative: &str)
 // By default we configure CBMC to use 16 bits to represent the object bits in pointers.
 const DEFAULT_OBJECT_BITS: u32 = 16;
 
+#[derive(Clone, Copy, Debug, PartialEq, Eq, strum_macros::EnumString)]
+enum TimeUnit {
+    #[strum(serialize = "s")]
+    Seconds,
+    #[strum(serialize = "m")]
+    Minutes,
+    #[strum(serialize = "h")]
+    Hours,
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub struct Timeout {
+    value: u32,
+    unit: TimeUnit,
+}
+
+impl FromStr for Timeout {
+    type Err = String;
+
+    fn from_str(s: &str) -> Result<Self, Self::Err> {
+        let last_char = s.chars().last().unwrap();
+        let (value_str, unit_str) = if last_char.is_ascii_digit() {
+            // no suffix
+            (s, "s")
+        } else {
+            s.split_at(s.len() - 1)
+        };
+        let value = value_str.parse::<u32>().map_err(|_| "Invalid timeout value")?;
+
+        let unit = TimeUnit::from_str(unit_str).map_err(
+            |_| "Invalid time unit. Use 's' for seconds, 'm' for minutes, or 'h' for hours",
+        )?;
+
+        Ok(Timeout { value, unit })
+    }
+}
+
+impl From<Timeout> for Duration {
+    fn from(timeout: Timeout) -> Self {
+        match timeout.unit {
+            TimeUnit::Seconds => Duration::from_secs(timeout.value as u64),
+            TimeUnit::Minutes => Duration::from_secs(timeout.value as u64 * 60),
+            TimeUnit::Hours => Duration::from_secs(timeout.value as u64 * 3600),
+        }
+    }
+}
+
 #[derive(Debug, clap::Parser)]
 #[command(
     version,
@@ -136,19 +184,11 @@ pub struct VerificationArgs {
     #[arg(long, hide = true, requires("enable_unstable"))]
     pub assess: bool,
 
-    /// Generate visualizer report to `<target-dir>/report/html/index.html`
-    #[arg(long)]
-    pub visualize: bool,
     /// Generate concrete playback unit test.
     /// If value supplied is 'print', Kani prints the unit test to stdout.
     /// If value supplied is 'inplace', Kani automatically adds the unit test to your source code.
     /// This option does not work with `--output-format old`.
-    #[arg(
-        long,
-        conflicts_with_all(&["visualize"]),
-        ignore_case = true,
-        value_enum
-    )]
+    #[arg(long, ignore_case = true, value_enum)]
     pub concrete_playback: Option<ConcretePlaybackMode>,
     /// Keep temporary files generated throughout Kani process. This is already the default
     /// behavior for `cargo-kani`.
@@ -266,6 +306,10 @@ pub struct VerificationArgs {
     )]
     pub synthesize_loop_contracts: bool,
 
+    //Harness Output into individual files
+    #[arg(long, hide_short_help = true)]
+    pub output_into_files: bool,
+
     /// Randomize the layout of structures. This option can help catching code that relies on
     /// a specific layout chosen by the compiler that is not guaranteed to be stable in the future.
     /// If a value is given, it will be used as the seed for randomization
@@ -277,10 +321,14 @@ pub struct VerificationArgs {
     #[arg(long, hide_short_help = true)]
     pub coverage: bool,
 
-    /// Print final LLBC for Aeneas backend. This requires the `-Z aeneas` option.
+    /// Print final LLBC for Lean backend. This requires the `-Z lean` option.
     #[arg(long, hide = true)]
     pub print_llbc: bool,
 
+    /// Timeout for each harness with optional suffix ('s': seconds, 'm': minutes, 'h': hours). Default is seconds. This option is experimental and requires `-Z unstable-options` to be used.
+    #[arg(long)]
+    pub harness_timeout: Option<Timeout>,
+
     /// Arguments to pass down to Cargo
     #[command(flatten)]
     pub cargo: CargoCommonArgs,
@@ -299,9 +347,9 @@ impl VerificationArgs {
         // if we flip the default, this will become: !self.no_restrict_vtable
     }
 
-    /// Assertion reachability checks should be disabled when running with --visualize
+    /// Assertion reachability checks should be disabled
     pub fn assertion_reach_checks(&self) -> bool {
-        !self.no_assertion_reach_checks && !self.visualize
+        !self.no_assertion_reach_checks
     }
 
     /// Suppress our default value, if the user has supplied it explicitly in --cbmc-args
@@ -517,16 +565,8 @@ impl ValidateArgs for VerificationArgs {
             );
         }
 
-        if self.visualize {
-            if !self.common_args.enable_unstable {
-                return Err(Error::raw(
-                    ErrorKind::MissingRequiredArgument,
-                    "Missing argument: --visualize now requires --enable-unstable
-                    due to open issues involving incorrect results.",
-                ));
-            } else {
-                print_deprecated(&self.common_args, "--visualize", "--concrete-playback");
-            }
+        if self.write_json_symtab {
+            print_obsolete(&self.common_args, "--write-json-symtab");
         }
 
         // TODO: these conflicting flags reflect what's necessary to pass current tests unmodified.
@@ -621,21 +661,42 @@ impl ValidateArgs for VerificationArgs {
             ));
         }
 
-        if self.print_llbc && !self.common_args.unstable_features.contains(UnstableFeature::Aeneas)
+        if self.output_into_files
+            && !self.common_args.unstable_features.contains(UnstableFeature::UnstableOptions)
         {
             return Err(Error::raw(
                 ErrorKind::MissingRequiredArgument,
-                "The `--print-llbc` argument is unstable and requires `-Z aeneas` to be used.",
+                "The `--output-into-files` argument is unstable and requires `-Z unstable-options` to enable \
+            unstable options support.",
+            ));
+        }
+
+        if self.print_llbc && !self.common_args.unstable_features.contains(UnstableFeature::Lean) {
+            return Err(Error::raw(
+                ErrorKind::MissingRequiredArgument,
+                "The `--print-llbc` argument is unstable and requires `-Z lean` to be used.",
             ));
         }
 
         // TODO: error out for other CBMC-backend-specific arguments
-        if self.common_args.unstable_features.contains(UnstableFeature::Aeneas)
+        if self.common_args.unstable_features.contains(UnstableFeature::Lean)
             && !self.cbmc_args.is_empty()
         {
             return Err(Error::raw(
                 ErrorKind::ArgumentConflict,
-                "The `--cbmc-args` argument cannot be used with -Z aeneas.",
+                "The `--cbmc-args` argument cannot be used with -Z lean.",
+            ));
+        }
+
+        if self.harness_timeout.is_some()
+            && !self.common_args.unstable_features.contains(UnstableFeature::UnstableOptions)
+        {
+            return Err(Error::raw(
+                ErrorKind::MissingRequiredArgument,
+                format!(
+                    "The `--harness-timeout` argument is unstable and requires `-Z {}` to be used.",
+                    UnstableFeature::UnstableOptions
+                ),
             ));
         }
         Ok(())
@@ -930,8 +991,8 @@ mod tests {
     }
 
     #[test]
-    fn check_cbmc_args_aeneas_backend() {
-        let args = "kani input.rs -Z aeneas --enable-unstable --cbmc-args --object-bits 10"
+    fn check_cbmc_args_lean_backend() {
+        let args = "kani input.rs -Z lean --enable-unstable --cbmc-args --object-bits 10"
             .split_whitespace();
         let err = StandaloneArgs::try_parse_from(args).unwrap().validate().unwrap_err();
         assert_eq!(err.kind(), ErrorKind::ArgumentConflict);
diff --git a/kani-driver/src/assess/table_failure_reasons.rs b/kani-driver/src/assess/table_failure_reasons.rs
index 9836aaa871cd..0566532dd9df 100644
--- a/kani-driver/src/assess/table_failure_reasons.rs
+++ b/kani-driver/src/assess/table_failure_reasons.rs
@@ -6,7 +6,7 @@ use std::collections::HashSet;
 
 use serde::{Deserialize, Serialize};
 
-use crate::harness_runner::HarnessResult;
+use crate::{call_cbmc::ExitStatus, harness_runner::HarnessResult};
 
 use super::table_builder::{ColumnType, RenderableTableRow, TableBuilder, TableRow};
 
@@ -35,8 +35,12 @@ pub(crate) fn build(results: &[HarnessResult]) -> TableBuilder<FailureReasonsTab
     let mut builder = TableBuilder::new();
 
     for r in results {
-        let classification = if let Err(exit_code) = r.result.results {
-            format!("CBMC failed with status {exit_code}")
+        let classification = if let Err(exit_status) = r.result.results {
+            match exit_status {
+                ExitStatus::Timeout => String::from("CBMC timed out"),
+                ExitStatus::OutOfMemory => String::from("CBMC ran out of memory"),
+                ExitStatus::Other(exit_code) => format!("CBMC failed with status {exit_code}"),
+            }
         } else {
             let failures = r.result.failed_properties();
             if failures.is_empty() {
diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
index fbd3f4c84826..cec8226e5f8e 100644
--- a/kani-driver/src/call_cargo.rs
+++ b/kani-driver/src/call_cargo.rs
@@ -277,62 +277,59 @@ crate-type = ["lib"]
     fn run_build(&self, cargo_cmd: Command) -> Result<Vec<RustcArtifact>> {
         let support_color = std::io::stdout().is_terminal();
         let mut artifacts = vec![];
-        if let Some(mut cargo_process) = self.run_piped(cargo_cmd)? {
-            let reader = BufReader::new(cargo_process.stdout.take().unwrap());
-            let mut error_count = 0;
-            for message in Message::parse_stream(reader) {
-                let message = message.unwrap();
-                match message {
-                    Message::CompilerMessage(msg) => match msg.message.level {
-                        DiagnosticLevel::FailureNote => {
-                            print_msg(&msg.message, support_color)?;
-                        }
-                        DiagnosticLevel::Error => {
-                            error_count += 1;
-                            print_msg(&msg.message, support_color)?;
-                        }
-                        DiagnosticLevel::Ice => {
-                            print_msg(&msg.message, support_color)?;
-                            let _ = cargo_process.wait();
-                            return Err(anyhow::Error::msg(msg.message).context(format!(
-                                "Failed to compile `{}` due to an internal compiler error.",
-                                msg.target.name
-                            )));
-                        }
-                        _ => {
-                            if !self.args.common_args.quiet {
-                                print_msg(&msg.message, support_color)?;
-                            }
-                        }
-                    },
-                    Message::CompilerArtifact(rustc_artifact) => {
-                        // Compares two targets, and falls back to a weaker
-                        // comparison where we avoid dashes in their names.
-                        artifacts.push(rustc_artifact)
+        let mut cargo_process = self.run_piped(cargo_cmd)?;
+        let reader = BufReader::new(cargo_process.stdout.take().unwrap());
+        let mut error_count = 0;
+        for message in Message::parse_stream(reader) {
+            let message = message.unwrap();
+            match message {
+                Message::CompilerMessage(msg) => match msg.message.level {
+                    DiagnosticLevel::FailureNote => {
+                        print_msg(&msg.message, support_color)?;
                     }
-                    Message::BuildScriptExecuted(_) | Message::BuildFinished(_) => {
-                        // do nothing
+                    DiagnosticLevel::Error => {
+                        error_count += 1;
+                        print_msg(&msg.message, support_color)?;
                     }
-                    Message::TextLine(msg) => {
-                        if !self.args.common_args.quiet {
-                            println!("{msg}");
-                        }
+                    DiagnosticLevel::Ice => {
+                        print_msg(&msg.message, support_color)?;
+                        let _ = cargo_process.wait();
+                        return Err(anyhow::Error::msg(msg.message).context(format!(
+                            "Failed to compile `{}` due to an internal compiler error.",
+                            msg.target.name
+                        )));
                     }
-
-                    // Non-exhaustive enum.
                     _ => {
                         if !self.args.common_args.quiet {
-                            println!("{message:?}");
+                            print_msg(&msg.message, support_color)?;
                         }
                     }
+                },
+                Message::CompilerArtifact(rustc_artifact) => {
+                    // Compares two targets, and falls back to a weaker
+                    // comparison where we avoid dashes in their names.
+                    artifacts.push(rustc_artifact)
+                }
+                Message::BuildScriptExecuted(_) | Message::BuildFinished(_) => {
+                    // do nothing
+                }
+                Message::TextLine(msg) => {
+                    if !self.args.common_args.quiet {
+                        println!("{msg}");
+                    }
+                }
+
+                // Non-exhaustive enum.
+                _ => {
+                    if !self.args.common_args.quiet {
+                        println!("{message:?}");
+                    }
                 }
             }
-            let status = cargo_process.wait()?;
-            if !status.success() {
-                bail!(
-                    "Failed to execute cargo ({status}). Found {error_count} compilation errors."
-                );
-            }
+        }
+        let status = cargo_process.wait()?;
+        if !status.success() {
+            bail!("Failed to execute cargo ({status}). Found {error_count} compilation errors.");
         }
         Ok(artifacts)
     }
@@ -383,7 +380,7 @@ crate-type = ["lib"]
                 cmd.arg(pkg);
                 // For some reason clippy cannot see that we are invoking wait() in the next line.
                 #[allow(clippy::zombie_processes)]
-                let mut process = self.run_piped(cmd)?.unwrap();
+                let mut process = self.run_piped(cmd)?;
                 let result = process.wait()?;
                 if !result.success() {
                     bail!("Failed to retrieve information for `{pkg}`");
diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index 17e99bf17d0f..4e10cb98c650 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -10,10 +10,11 @@ use std::collections::btree_map::Entry;
 use std::ffi::OsString;
 use std::fmt::Write;
 use std::path::Path;
-use std::process::Command;
 use std::sync::OnceLock;
 use std::time::{Duration, Instant};
+use tokio::process::Command as TokioCommand;
 
+use crate::args::common::Verbosity;
 use crate::args::{OutputFormat, VerificationArgs};
 use crate::cbmc_output_parser::{
     CheckStatus, Property, VerificationOutput, extract_results, process_cbmc_output,
@@ -22,6 +23,7 @@ use crate::cbmc_property_renderer::{format_coverage, format_result, kani_cbmc_ou
 use crate::coverage::cov_results::{CoverageCheck, CoverageResults};
 use crate::coverage::cov_results::{CoverageRegion, CoverageTerm};
 use crate::session::KaniSession;
+use crate::util::render_command;
 
 /// We will use Cadical by default since it performed better than MiniSAT in our analysis.
 /// Note: Kissat was marginally better, but it is an external solver which could be more unstable.
@@ -45,6 +47,15 @@ pub enum FailedProperties {
     Other,
 }
 
+/// The possible CBMC exit statuses
+#[derive(Clone, Copy, Debug)]
+pub enum ExitStatus {
+    Timeout,
+    OutOfMemory,
+    /// the integer is the process exit status
+    Other(i32),
+}
+
 /// Our (kani-driver) notions of CBMC results.
 #[derive(Debug)]
 pub struct VerificationResult {
@@ -56,7 +67,7 @@ pub struct VerificationResult {
     /// Note: CBMC process exit status is only potentially useful if `status` is `Failure`.
     /// Kani will see CBMC report "failure" that's actually success (interpreting "failed"
     /// checks like coverage as expected and desirable.)
-    pub results: Result<Vec<Property>, i32>,
+    pub results: Result<Vec<Property>, ExitStatus>,
     /// The runtime duration of this CBMC invocation.
     pub runtime: Duration,
     /// Whether concrete playback generated a test
@@ -71,55 +82,89 @@ impl KaniSession {
         let args: Vec<OsString> = self.cbmc_flags(file, harness)?;
 
         // TODO get cbmc path from self
-        let mut cmd = Command::new("cbmc");
+        let mut cmd = TokioCommand::new("cbmc");
         cmd.args(args);
 
-        let start_time = Instant::now();
-
         let verification_results = if self.args.output_format == crate::args::OutputFormat::Old {
-            if self.run_terminal(cmd).is_err() {
+            if self.run_terminal_timeout(cmd).is_err() {
                 VerificationResult::mock_failure()
             } else {
                 VerificationResult::mock_success()
             }
         } else {
             // Add extra argument to receive the output in JSON format.
-            // Done here because `--visualize` uses the XML format instead.
+            // Done here because now removed `--visualize` used the XML format instead.
+            // TODO: move this now that we don't use --visualize
             cmd.arg("--json-ui");
 
-            // Spawn the CBMC process and process its output below
-            let cbmc_process_opt = self.run_piped(cmd)?;
-            let cbmc_process = cbmc_process_opt.ok_or(anyhow::Error::msg("Failed to run cbmc"))?;
-            let output = process_cbmc_output(cbmc_process, |i| {
+            self.runtime.block_on(self.run_cbmc_piped(cmd, harness))?
+        };
+
+        Ok(verification_results)
+    }
+
+    async fn run_cbmc_piped(
+        &self,
+        mut cmd: TokioCommand,
+        harness: &HarnessMetadata,
+    ) -> Result<VerificationResult> {
+        if self.args.common_args.verbose() {
+            println!("[Kani] Running: `{}`", render_command(cmd.as_std()).to_string_lossy());
+        }
+        // Spawn the CBMC process and process its output below
+        let mut cbmc_process = cmd
+            .stdout(std::process::Stdio::piped())
+            .spawn()
+            .map_err(|_| anyhow::Error::msg("Failed to run cbmc"))?;
+
+        let start_time = Instant::now();
+
+        let res = if let Some(timeout) = self.args.harness_timeout {
+            tokio::time::timeout(
+                timeout.into(),
+                process_cbmc_output(&mut cbmc_process, |i| {
+                    kani_cbmc_output_filter(
+                        i,
+                        self.args.extra_pointer_checks,
+                        self.args.common_args.quiet,
+                        &self.args.output_format,
+                    )
+                }),
+            )
+            .await
+        } else {
+            Ok(process_cbmc_output(&mut cbmc_process, |i| {
                 kani_cbmc_output_filter(
                     i,
                     self.args.extra_pointer_checks,
                     self.args.common_args.quiet,
                     &self.args.output_format,
                 )
-            })?;
-
-            VerificationResult::from(output, harness.attributes.should_panic, start_time)
+            })
+            .await)
         };
 
-        Ok(verification_results)
-    }
-
-    /// used by call_cbmc_viewer, invokes different variants of CBMC.
-    // TODO: this could use some cleanup and refactoring.
-    pub fn call_cbmc(&self, args: Vec<OsString>, output: &Path) -> Result<()> {
-        // TODO get cbmc path from self
-        let mut cmd = Command::new("cbmc");
-        cmd.args(args);
+        let verification_results = if res.is_err() {
+            // An error occurs if the timeout was reached
 
-        let result = self.run_redirect(cmd, output)?;
+            // Kill the process
+            cbmc_process.kill().await?;
 
-        if !result.success() {
-            bail!("cbmc exited with status {}", result);
-        }
-        // TODO: We 'bail' above, but then ignore it in 'call_cbmc_viewer' ...
+            VerificationResult {
+                status: VerificationStatus::Failure,
+                failed_properties: FailedProperties::None,
+                results: Err(ExitStatus::Timeout),
+                runtime: start_time.elapsed(),
+                generated_concrete_test: false,
+                coverage_results: None,
+            }
+        } else {
+            // The timeout wasn't reached
+            let output = res.unwrap()?;
+            VerificationResult::from(output, harness.attributes.should_panic, start_time)
+        };
 
-        Ok(())
+        Ok(verification_results)
     }
 
     /// "Internal," but also used by call_cbmc_viewer
@@ -147,10 +192,7 @@ impl KaniSession {
             args.push("--validate-ssa-equation".into());
         }
 
-        if !self.args.visualize
-            && self.args.concrete_playback.is_none()
-            && !self.args.no_slice_formula
-        {
+        if self.args.concrete_playback.is_none() && !self.args.no_slice_formula {
             args.push("--slice-formula".into());
         }
 
@@ -293,10 +335,15 @@ impl VerificationResult {
             }
         } else {
             // We never got results from CBMC - something went wrong (e.g. crash) so it's failure
+            let exit_status = if output.process_status == 137 {
+                ExitStatus::OutOfMemory
+            } else {
+                ExitStatus::Other(output.process_status)
+            };
             VerificationResult {
                 status: VerificationStatus::Failure,
                 failed_properties: FailedProperties::Other,
-                results: Err(output.process_status),
+                results: Err(exit_status),
                 runtime,
                 generated_concrete_test: false,
                 coverage_results: None,
@@ -322,7 +369,7 @@ impl VerificationResult {
             // on failure, exit codes in theory might be used,
             // but `mock_failure` should never be used in a context where they will,
             // so again use something weird:
-            results: Err(42),
+            results: Err(ExitStatus::Other(42)),
             runtime: Duration::from_secs(0),
             generated_concrete_test: false,
             coverage_results: None,
@@ -353,15 +400,24 @@ impl VerificationResult {
             }
             Err(exit_status) => {
                 let verification_result = console::style("FAILED").red();
-                let explanation = if *exit_status == 137 {
-                    "CBMC appears to have run out of memory. You may want to rerun your proof in \
+                let (header, explanation) = match exit_status {
+                    ExitStatus::OutOfMemory => (
+                        String::from("CBMC failed"),
+                        "CBMC appears to have run out of memory. You may want to rerun your proof in \
                     an environment with additional memory or use stubbing to reduce the size of the \
-                    code the verifier reasons about.\n"
-                } else {
-                    ""
+                    code the verifier reasons about.\n",
+                    ),
+                    ExitStatus::Timeout => (
+                        String::from("CBMC failed"),
+                        "CBMC timed out. You may want to rerun your proof with a larger timeout \
+                    or use stubbing to reduce the size of the code the verifier reasons about.\n",
+                    ),
+                    ExitStatus::Other(exit_status) => {
+                        (format!("CBMC failed with status {exit_status}"), "")
+                    }
                 };
                 format!(
-                    "\nCBMC failed with status {exit_status}\n\
+                    "\n{header}\n\
                     VERIFICATION:- {verification_result}\n\
                     {explanation}",
                 )
diff --git a/kani-driver/src/call_cbmc_viewer.rs b/kani-driver/src/call_cbmc_viewer.rs
deleted file mode 100644
index 41c6247ee121..000000000000
--- a/kani-driver/src/call_cbmc_viewer.rs
+++ /dev/null
@@ -1,97 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-
-use anyhow::Result;
-use kani_metadata::HarnessMetadata;
-use std::ffi::OsString;
-use std::path::Path;
-use std::process::Command;
-
-use crate::session::KaniSession;
-use crate::util::{alter_extension, warning};
-
-impl KaniSession {
-    /// Run CBMC appropriately to produce 3 output XML files, then run cbmc-viewer on them to produce a report.
-    /// Viewer doesn't give different error codes depending on verification failure, so as long as it works, we report success.
-    pub fn run_visualize(
-        &self,
-        file: &Path,
-        report_dir: &Path,
-        harness_metadata: &HarnessMetadata,
-    ) -> Result<()> {
-        let results_filename = alter_extension(file, "results.xml");
-        let property_filename = alter_extension(file, "property.xml");
-
-        self.record_temporary_file(&results_filename);
-        self.record_temporary_file(&property_filename);
-
-        self.cbmc_variant(file, &["--xml-ui", "--trace"], &results_filename, harness_metadata)?;
-        self.cbmc_variant(
-            file,
-            &["--xml-ui", "--show-properties"],
-            &property_filename,
-            harness_metadata,
-        )?;
-
-        let args: Vec<OsString> = vec![
-            "--result".into(),
-            results_filename.into(),
-            "--property".into(),
-            property_filename.into(),
-            "--srcdir".into(),
-            ".".into(), // os.path.realpath(srcdir),
-            "--wkdir".into(),
-            ".".into(), // os.path.realpath(wkdir),
-            "--goto".into(),
-            file.into(),
-            "--reportdir".into(),
-            report_dir.into(),
-        ];
-
-        // TODO get cbmc-viewer path from self
-        let mut cmd = Command::new("cbmc-viewer");
-        cmd.args(args);
-
-        self.run_suppress(cmd)?;
-
-        // Let the user know
-        if !self.args.common_args.quiet {
-            println!("Report written to: {}/html/index.html", report_dir.to_string_lossy());
-            warning("coverage information has been disabled for `--visualize` reports");
-            // If using VS Code with Remote-SSH, suggest an option for remote viewing:
-            if std::env::var("VSCODE_IPC_HOOK_CLI").is_ok()
-                && std::env::var("SSH_CONNECTION").is_ok()
-            {
-                println!(
-                    "VS Code automatically forwards ports for locally hosted servers. To view the report remotely,\nTry:  python3 -m http.server --directory {}/html",
-                    report_dir.to_string_lossy()
-                );
-            }
-        }
-
-        Ok(())
-    }
-
-    fn cbmc_variant(
-        &self,
-        file: &Path,
-        extra_args: &[&str],
-        output: &Path,
-        harness: &HarnessMetadata,
-    ) -> Result<()> {
-        let mut args = self.cbmc_flags(file, harness)?;
-        args.extend(extra_args.iter().map(|x| x.into()));
-
-        // TODO fix this hack, abstractions are wrong
-        if extra_args.contains(&"--cover") {
-            if let Some(i) = args.iter().position(|x| x == "--unwinding-assertions") {
-                args.remove(i);
-            }
-        }
-
-        // Expect and allow failures... maybe we should do better here somehow
-        let _result = self.call_cbmc(args, output);
-
-        Ok(())
-    }
-}
diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs
index a77e3c675aec..09b8cbb18fc8 100644
--- a/kani-driver/src/call_goto_instrument.rs
+++ b/kani-driver/src/call_goto_instrument.rs
@@ -37,16 +37,13 @@ impl KaniSession {
             self.goto_sanity_check(output)?;
         }
 
-        self.instrument_contracts(harness, output)?;
-
-        if self
+        let is_loop_contracts_enabled = self
             .args
             .common_args
             .unstable_features
             .contains(kani_metadata::UnstableFeature::LoopContracts)
-        {
-            self.instrument_loop_contracts(harness, output)?;
-        }
+            && harness.has_loop_contracts;
+        self.instrument_contracts(harness, is_loop_contracts_enabled, output)?;
 
         if self.args.checks.undefined_function_on() {
             self.add_library(output)?;
@@ -172,42 +169,46 @@ impl KaniSession {
         self.call_goto_instrument(args)
     }
 
-    /// Make CBMC enforce a function contract.
-    pub fn instrument_contracts(&self, harness: &HarnessMetadata, file: &Path) -> Result<()> {
-        let Some(assigns) = harness.contract.as_ref() else { return Ok(()) };
+    /// Apply annotated function contracts and loop contracts with goto-instrument.
+    pub fn instrument_contracts(
+        &self,
+        harness: &HarnessMetadata,
+        is_loop_contracts_enabled: bool,
+        file: &Path,
+    ) -> Result<()> {
+        // Do nothing if neither loop contracts nor function contracts is enabled.
+        if !is_loop_contracts_enabled && harness.contract.is_none() {
+            return Ok(());
+        }
 
-        let mut args: Vec<OsString> = vec![
-            "--dfcc".into(),
-            (&harness.mangled_name).into(),
-            "--enforce-contract".into(),
-            assigns.contracted_function_name.as_str().into(),
-            "--no-malloc-may-fail".into(),
-            file.into(),
-            file.into(),
-        ];
-        if let Some(tracker) = &assigns.recursion_tracker {
-            args.push("--nondet-static-exclude".into());
-            args.push(tracker.as_str().into());
+        let mut args: Vec<OsString> =
+            vec!["--dfcc".into(), (&harness.mangled_name).into(), "--no-malloc-may-fail".into()];
+
+        if is_loop_contracts_enabled {
+            args.append(&mut vec![
+                "--apply-loop-contracts".into(),
+                "--loop-contracts-no-unwind".into(),
+                // Because loop contracts now are wrapped in a closure which will be a side-effect expression in CBMC even they
+                // may not contain side-effect. So we disable the side-effect check for now and will implement a better check
+                // instead of simply rejecting function calls and statement expressions.
+                // See issue: diffblue/cbmc#8393
+                "--disable-loop-contracts-side-effect-check".into(),
+            ]);
         }
-        self.call_goto_instrument(&args)
-    }
 
-    /// Apply annotated loop contracts.
-    pub fn instrument_loop_contracts(&self, harness: &HarnessMetadata, file: &Path) -> Result<()> {
-        let args: Vec<OsString> = vec![
-            "--dfcc".into(),
-            (&harness.mangled_name).into(),
-            "--apply-loop-contracts".into(),
-            "--loop-contracts-no-unwind".into(),
-            "--no-malloc-may-fail".into(),
-            // Because loop contracts now are wrapped in a closure which will be a side-effect expression in CBMC even they
-            // may not contain side-effect. So we disable the side-effect check for now and will implement a better check
-            // instead of simply rejecting function calls and statement expressions.
-            // See issue: diffblue/cbmc#8393
-            "--disable-loop-contracts-side-effect-check".into(),
-            file.into(),
-            file.into(),
-        ];
+        if let Some(assigns) = harness.contract.as_ref() {
+            args.push("--enforce-contract".into());
+            args.push(assigns.contracted_function_name.as_str().into());
+
+            if let Some(tracker) = &assigns.recursion_tracker {
+                args.push("--nondet-static-exclude".into());
+                args.push(tracker.as_str().into());
+            }
+        }
+
+        args.push(file.into());
+        args.push(file.into());
+
         self.call_goto_instrument(&args)
     }
 
diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs
index e33fbe874946..edc200277113 100644
--- a/kani-driver/src/call_single_file.rs
+++ b/kani-driver/src/call_single_file.rs
@@ -53,8 +53,8 @@ impl KaniSession {
     ) -> Result<()> {
         let mut kani_args = self.kani_compiler_flags();
         kani_args.push(format!("--reachability={}", self.reachability_mode()));
-        if self.args.common_args.unstable_features.contains(UnstableFeature::Aeneas) {
-            kani_args.push("--backend=aeneas".into());
+        if self.args.common_args.unstable_features.contains(UnstableFeature::Lean) {
+            kani_args.push("--backend=llbc".into());
         }
 
         let lib_path = lib_folder().unwrap();
@@ -99,8 +99,8 @@ impl KaniSession {
     }
 
     pub fn backend_arg(&self) -> Option<String> {
-        if self.args.common_args.unstable_features.contains(UnstableFeature::Aeneas) {
-            Some(to_rustc_arg(vec!["--backend=aeneas".into()]))
+        if self.args.common_args.unstable_features.contains(UnstableFeature::Lean) {
+            Some(to_rustc_arg(vec!["--backend=llbc".into()]))
         } else {
             None
         }
@@ -129,11 +129,6 @@ impl KaniSession {
             flags.push("--ignore-global-asm".into());
         }
 
-        // Users activate it via the command line switch
-        if self.args.write_json_symtab {
-            flags.push("--write-json-symtab".into());
-        }
-
         if self.args.is_stubbing_enabled() {
             flags.push("--enable-stubbing".into());
         }
diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs
index 58a93df3a2f6..bf86ef08c217 100644
--- a/kani-driver/src/cbmc_output_parser.rs
+++ b/kani-driver/src/cbmc_output_parser.rs
@@ -30,10 +30,10 @@ use rustc_demangle::demangle;
 use serde::{Deserialize, Deserializer, Serialize};
 
 use std::env;
-use std::io::{BufRead, BufReader};
 use std::os::unix::process::ExitStatusExt;
 use std::path::PathBuf;
-use std::process::{Child, ChildStdout};
+use tokio::io::{AsyncBufReadExt, BufReader};
+use tokio::process::{Child, ChildStdout};
 
 const RESULT_ITEM_PREFIX: &str = "  {\n    \"result\":";
 
@@ -360,9 +360,8 @@ enum Action {
     ProcessItem,
 }
 
-/// A parser for CBMC output, whose state is determined by:
-///  1. The input accumulator, required to process items on the fly.
-///  2. The buffer, which is accessed to retrieve more lines.
+/// A parser for CBMC output, whose state is determined by
+/// the input accumulator, required to process items on the fly.
 ///
 /// CBMC's JSON output is defined as a JSON array which contains:
 ///  1. One program at the beginning (i.e., a message with CBMC's version).
@@ -377,14 +376,13 @@ enum Action {
 /// There is a feature request for serde_json which would obsolete this if
 /// it ever lands: <https://github.com/serde-rs/json/issues/404>
 /// (Would provide a streaming iterator over a json array.)
-struct Parser<'a, 'b> {
+struct Parser {
     pub input_so_far: String,
-    pub buffer: &'a mut BufReader<&'b mut ChildStdout>,
 }
 
-impl<'a, 'b> Parser<'a, 'b> {
-    fn new(buffer: &'a mut BufReader<&'b mut ChildStdout>) -> Self {
-        Parser { input_so_far: String::new(), buffer }
+impl Parser {
+    fn new() -> Self {
+        Parser { input_so_far: String::new() }
     }
 
     /// Triggers an action based on the input:
@@ -479,16 +477,16 @@ impl<'a, 'b> Parser<'a, 'b> {
         }
         None
     }
-}
 
-/// The iterator implementation for `Parser` reads the buffer line by line,
-/// and determines if it must return an item based on processing each line.
-impl Iterator for Parser<'_, '_> {
-    type Item = ParserItem;
-    fn next(&mut self) -> Option<Self::Item> {
+    /// Read the process output and return when an item is found in the output
+    /// or the EOF is reached
+    async fn read_output(
+        &mut self,
+        buffer: &mut BufReader<&mut ChildStdout>,
+    ) -> Option<ParserItem> {
         loop {
             let mut input = String::new();
-            match self.buffer.read_line(&mut input) {
+            match buffer.read_line(&mut input).await {
                 Ok(len) => {
                     if len == 0 {
                         return None;
@@ -522,17 +520,24 @@ pub struct VerificationOutput {
 /// then formatted (according to the output format) and print.
 ///
 /// The cbmc process status is returned, along with the (post-filter) items.
-pub fn process_cbmc_output(
-    mut process: Child,
-    eager_filter: impl FnMut(ParserItem) -> Option<ParserItem>,
+pub async fn process_cbmc_output(
+    process: &mut Child,
+    mut eager_filter: impl FnMut(ParserItem) -> Option<ParserItem>,
 ) -> Result<VerificationOutput> {
     let stdout = process.stdout.as_mut().unwrap();
     let mut stdout_reader = BufReader::new(stdout);
-    let parser = Parser::new(&mut stdout_reader);
-    // This should run until stdout is closed (which should mean the process exited)
-    let processed_items: Vec<_> = parser.filter_map(eager_filter).collect();
+    let mut parser = Parser::new();
+    // This should run until stdout is closed (which should mean the process
+    // exited) or the specified timeout is reached
+    let mut processed_items = Vec::new();
+    while let Some(item) = parser.read_output(&mut stdout_reader).await {
+        if let Some(item) = eager_filter(item) {
+            processed_items.push(item);
+        }
+    }
+
     // This will get us the process's exit code
-    let status = process.wait()?;
+    let status = process.wait().await?;
 
     let process_status = match (status.code(), status.signal()) {
         // normal unix exit codes (cbmc uses currently 0-10)
diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs
index 99991798beb8..5c10d08badb6 100644
--- a/kani-driver/src/cbmc_property_renderer.rs
+++ b/kani-driver/src/cbmc_property_renderer.rs
@@ -749,9 +749,9 @@ fn annotate_properties_with_reach_results(
         reach_map.entry(check_id_str).or_default().push(status);
     }
 
+    let check_marker_pat = Regex::new(r"\[KANI_CHECK_ID_([^\]]*)\]").unwrap();
     for prop in properties.iter_mut() {
         let description = &prop.description;
-        let check_marker_pat = Regex::new(r"\[KANI_CHECK_ID_([^\]]*)\]").unwrap();
         if check_marker_pat.is_match(description) {
             // Capture the ID in the property
             let prop_match_id =
diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs
index 32f184b3ce6a..ee14992cba78 100644
--- a/kani-driver/src/harness_runner.rs
+++ b/kani-driver/src/harness_runner.rs
@@ -4,6 +4,8 @@
 use anyhow::{Result, bail};
 use kani_metadata::{ArtifactType, HarnessMetadata};
 use rayon::prelude::*;
+use std::fs::File;
+use std::io::Write;
 use std::path::Path;
 
 use crate::args::OutputFormat;
@@ -11,6 +13,9 @@ use crate::call_cbmc::{VerificationResult, VerificationStatus};
 use crate::project::Project;
 use crate::session::KaniSession;
 
+use std::env::current_dir;
+use std::path::PathBuf;
+
 /// A HarnessRunner is responsible for checking all proof harnesses. The data in this structure represents
 /// "background information" that the controlling driver (e.g. cargo-kani or kani) computed.
 ///
@@ -39,7 +44,6 @@ impl<'pr> HarnessRunner<'_, 'pr> {
         self.check_stubbing(harnesses)?;
 
         let sorted_harnesses = crate::metadata::sort_harnesses_by_loc(harnesses);
-
         let pool = {
             let mut builder = rayon::ThreadPoolBuilder::new();
             if let Some(x) = self.sess.args.jobs() {
@@ -52,8 +56,6 @@ impl<'pr> HarnessRunner<'_, 'pr> {
             sorted_harnesses
                 .par_iter()
                 .map(|harness| -> Result<HarnessResult<'pr>> {
-                    let harness_filename = harness.pretty_name.replace("::", "-");
-                    let report_dir = self.project.outdir.join(format!("report-{harness_filename}"));
                     let goto_file =
                         self.project.get_harness_artifact(&harness, ArtifactType::Goto).unwrap();
 
@@ -63,7 +65,7 @@ impl<'pr> HarnessRunner<'_, 'pr> {
                         self.sess.synthesize_loop_contracts(goto_file, &goto_file, &harness)?;
                     }
 
-                    let result = self.sess.check_harness(goto_file, &report_dir, harness)?;
+                    let result = self.sess.check_harness(goto_file, harness)?;
                     Ok(HarnessResult { harness, result })
                 })
                 .collect::<Result<Vec<_>>>()
@@ -101,35 +103,60 @@ impl<'pr> HarnessRunner<'_, 'pr> {
 }
 
 impl KaniSession {
+    fn process_output(&self, result: &VerificationResult, harness: &HarnessMetadata) {
+        if self.should_print_output() {
+            if self.args.output_into_files {
+                self.write_output_to_file(result, harness);
+            }
+
+            let output = result.render(&self.args.output_format, harness.attributes.should_panic);
+            println!("{}", output);
+        }
+    }
+
+    fn should_print_output(&self) -> bool {
+        !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old
+    }
+
+    fn write_output_to_file(&self, result: &VerificationResult, harness: &HarnessMetadata) {
+        let target_dir = self.result_output_dir().unwrap();
+        let file_name = target_dir.join(harness.pretty_name.clone());
+        let path = Path::new(&file_name);
+        let prefix = path.parent().unwrap();
+
+        std::fs::create_dir_all(prefix).unwrap();
+        let mut file = File::create(&file_name).unwrap();
+        let file_output = result.render(&OutputFormat::Regular, harness.attributes.should_panic);
+
+        if let Err(e) = writeln!(file, "{}", file_output) {
+            eprintln!(
+                "Failed to write to file {}: {}",
+                file_name.into_os_string().into_string().unwrap(),
+                e
+            );
+        }
+    }
+
+    fn result_output_dir(&self) -> Result<PathBuf> {
+        let target_dir = self.args.target_dir.clone().map_or_else(current_dir, Ok)?;
+        Ok(target_dir.join("result_output_dir")) //Hardcode output to result_output_dir, may want to make it adjustable?
+    }
+
     /// Run the verification process for a single harness
     pub(crate) fn check_harness(
         &self,
         binary: &Path,
-        report_dir: &Path,
         harness: &HarnessMetadata,
     ) -> Result<VerificationResult> {
         if !self.args.common_args.quiet {
             println!("Checking harness {}...", harness.pretty_name);
         }
 
-        if self.args.visualize {
-            self.run_visualize(binary, report_dir, harness)?;
-            // Strictly speaking, we're faking success here. This is more "no error"
-            Ok(VerificationResult::mock_success())
-        } else {
-            let mut result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?;
+        let mut result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?;
 
-            // When quiet, we don't want to print anything at all.
-            // When output is old, we also don't have real results to print.
-            if !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old {
-                println!(
-                    "{}",
-                    result.render(&self.args.output_format, harness.attributes.should_panic)
-                );
-            }
-            self.gen_and_add_concrete_playback(harness, &mut result)?;
-            Ok(result)
-        }
+        self.process_output(&result, harness);
+        self.gen_and_add_concrete_playback(harness, &mut result)?;
+        Ok(result)
     }
 
     /// Concludes a session by printing a summary report and exiting the process with an
@@ -155,7 +182,7 @@ impl KaniSession {
         }
 
         // We currently omit a summary if there was just 1 harness
-        if !self.args.common_args.quiet && !self.args.visualize {
+        if !self.args.common_args.quiet {
             if failing > 0 {
                 println!("Summary:");
             }
diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs
index 88f92b3a70f6..b0fa22334da0 100644
--- a/kani-driver/src/main.rs
+++ b/kani-driver/src/main.rs
@@ -24,7 +24,6 @@ mod args_toml;
 mod assess;
 mod call_cargo;
 mod call_cbmc;
-mod call_cbmc_viewer;
 mod call_goto_cc;
 mod call_goto_instrument;
 mod call_goto_synthesizer;
diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs
index 174ce55187a6..94a5393408d3 100644
--- a/kani-driver/src/metadata.rs
+++ b/kani-driver/src/metadata.rs
@@ -223,6 +223,7 @@ pub mod tests {
             attributes,
             goto_file: model_file,
             contract: Default::default(),
+            has_loop_contracts: false,
         }
     }
 
diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs
index 363050958d61..0af517ca84bc 100644
--- a/kani-driver/src/project.rs
+++ b/kani-driver/src/project.rs
@@ -32,6 +32,8 @@ pub struct Project {
     pub metadata: Vec<KaniMetadata>,
     /// The directory where all outputs should be directed to. This path represents the canonical
     /// version of outdir.
+    /// NOTE: This needs to be marked as dead_code even when it's clearly not
+    #[allow(dead_code)]
     pub outdir: PathBuf,
     /// The path to the input file the project was built from.
     /// Note that it will only be `Some(...)` if this was built from a standalone project.
diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs
index 2df431eb4587..187a17ae6981 100644
--- a/kani-driver/src/session.rs
+++ b/kani-driver/src/session.rs
@@ -1,6 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+use crate::args::Timeout;
 use crate::args::VerificationArgs;
 use crate::args::common::Verbosity;
 use crate::util::render_command;
@@ -8,10 +9,11 @@ use anyhow::{Context, Result, bail};
 use std::io::IsTerminal;
 use std::io::Write;
 use std::path::{Path, PathBuf};
-use std::process::{Child, Command, ExitStatus, Stdio};
+use std::process::{Child, Command, Stdio};
 use std::sync::Mutex;
 use std::time::Instant;
 use strum_macros::Display;
+use tokio::process::Command as TokioCommand;
 use tracing::level_filters::LevelFilter;
 use tracing_subscriber::{EnvFilter, Registry, layer::SubscriberExt};
 
@@ -38,6 +40,9 @@ pub struct KaniSession {
 
     /// The temporary files we littered that need to be cleaned up at the end of execution
     pub temporaries: Mutex<Vec<PathBuf>>,
+
+    /// The tokio runtime
+    pub runtime: tokio::runtime::Runtime,
 }
 
 /// Represents where we detected Kani, with helper methods for using that information to find critical paths
@@ -61,6 +66,7 @@ impl KaniSession {
             kani_compiler: install.kani_compiler()?,
             kani_lib_c: install.kani_lib_c()?,
             temporaries: Mutex::new(vec![]),
+            runtime: tokio::runtime::Builder::new_current_thread().enable_all().build().unwrap(),
         })
     }
 
@@ -113,18 +119,23 @@ impl KaniSession {
         run_terminal(&self.args.common_args, cmd)
     }
 
+    /// Call [run_terminal_timeout] with the verbosity configured by the user.
+    /// The `bool` value indicates whether the command timed out
+    pub fn run_terminal_timeout(&self, cmd: TokioCommand) -> Result<bool> {
+        self.runtime.block_on(run_terminal_timeout(
+            &self.args.common_args,
+            cmd,
+            self.args.harness_timeout,
+        ))
+    }
+
     /// Call [run_suppress] with the verbosity configured by the user.
     pub fn run_suppress(&self, cmd: Command) -> Result<()> {
         run_suppress(&self.args.common_args, cmd)
     }
 
-    /// Call [run_redirect] with the verbosity configured by the user.
-    pub fn run_redirect(&self, cmd: Command, stdout: &Path) -> Result<ExitStatus> {
-        run_redirect(&self.args.common_args, cmd, stdout)
-    }
-
     /// Call [run_piped] with the verbosity configured by the user.
-    pub fn run_piped(&self, cmd: Command) -> Result<Option<Child>> {
+    pub fn run_piped(&self, cmd: Command) -> Result<Child> {
         run_piped(&self.args.common_args, cmd)
     }
 
@@ -148,7 +159,6 @@ impl KaniSession {
 //               Default  Quiet  Verbose   Default  Quiet  Verbose
 // run_terminal  Y        N      Y         Y        N      Y         (inherits terminal)
 // run_suppress  N        N      Y         Y        N      Y         (buffered text only)
-// run_redirect  (not applicable, always to the file)                (only option where error is acceptable)
 
 /// Run a job, leave it outputting to terminal (unless --quiet), and fail if there's a problem.
 pub fn run_terminal(verbosity: &impl Verbosity, mut cmd: Command) -> Result<()> {
@@ -174,6 +184,49 @@ pub fn run_terminal(verbosity: &impl Verbosity, mut cmd: Command) -> Result<()>
     Ok(())
 }
 
+/// The `bool` value indicates whether the command timed out
+async fn run_terminal_timeout(
+    verbosity: &impl Verbosity,
+    mut cmd: TokioCommand,
+    timeout: Option<Timeout>,
+) -> Result<bool> {
+    if verbosity.quiet() {
+        cmd.stdout(std::process::Stdio::null());
+        cmd.stderr(std::process::Stdio::null());
+    }
+    if verbosity.verbose() {
+        println!("[Kani] Running: `{}`", render_command(&cmd.as_std()).to_string_lossy());
+    }
+    let program = cmd.as_std().get_program().to_string_lossy().to_string();
+    let result = with_timer(
+        verbosity,
+        || async {
+            if let Some(timeout) = timeout {
+                let mut child = cmd.spawn().unwrap();
+                let res = tokio::time::timeout(timeout.into(), child.wait()).await;
+                if res.is_err() {
+                    // Kill the process
+                    child.kill().await.unwrap();
+                }
+                res
+            } else {
+                Ok(cmd.status().await)
+            }
+        },
+        &program,
+    )
+    .await;
+    // outer result indicates whether the command timed out
+    if result.is_err() {
+        return Ok(true);
+    }
+    let result = result.unwrap().context(format!("Failed to invoke {program}"))?;
+    if !result.success() {
+        bail!("{} exited with status {}", cmd.as_std().get_program().to_string_lossy(), result);
+    }
+    Ok(false)
+}
+
 /// Run a job, but only output (unless --quiet) if it fails, and fail if there's a problem.
 pub fn run_suppress(verbosity: &impl Verbosity, mut cmd: Command) -> Result<()> {
     if verbosity.is_set() {
@@ -195,39 +248,12 @@ pub fn run_suppress(verbosity: &impl Verbosity, mut cmd: Command) -> Result<()>
     Ok(())
 }
 
-/// Run a job, redirect its output to a file, and allow the caller to decide what to do with failure.
-pub fn run_redirect(
-    verbosity: &impl Verbosity,
-    mut cmd: Command,
-    stdout: &Path,
-) -> Result<ExitStatus> {
-    if verbosity.verbose() {
-        println!(
-            "[Kani] Running: `{} > {}`",
-            render_command(&cmd).to_string_lossy(),
-            stdout.display()
-        );
-    }
-    let output_file = std::fs::File::create(stdout)?;
-    cmd.stdout(output_file);
-
-    let program = cmd.get_program().to_string_lossy().to_string();
-    with_timer(
-        verbosity,
-        || {
-            cmd.status()
-                .context(format!("Failed to invoke {}", cmd.get_program().to_string_lossy()))
-        },
-        &program,
-    )
-}
-
 /// Run a job and pipe its output to this process.
 /// Returns an error if the process could not be spawned.
 ///
 /// NOTE: Unlike other `run_` functions, this function does not attempt to indicate
 /// the process exit code, you need to remember to check this yourself.
-pub fn run_piped(verbosity: &impl Verbosity, mut cmd: Command) -> Result<Option<Child>> {
+pub fn run_piped(verbosity: &impl Verbosity, mut cmd: Command) -> Result<Child> {
     if verbosity.verbose() {
         println!("[Kani] Running: `{}`", render_command(&cmd).to_string_lossy());
     }
@@ -237,7 +263,7 @@ pub fn run_piped(verbosity: &impl Verbosity, mut cmd: Command) -> Result<Option<
         .spawn()
         .context(format!("Failed to invoke {}", cmd.get_program().to_string_lossy()))?;
 
-    Ok(Some(process))
+    Ok(process)
 }
 
 /// Execute the provided function and measure the clock time it took for its execution.
diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs
index 426cf8d9e960..6932b15dc1a7 100644
--- a/kani_metadata/src/harness.rs
+++ b/kani_metadata/src/harness.rs
@@ -36,6 +36,8 @@ pub struct HarnessMetadata {
     pub attributes: HarnessAttributes,
     /// A CBMC-level assigns contract that should be enforced when running this harness.
     pub contract: Option<AssignsContract>,
+    /// If the harness contains some usage of loop contracts.
+    pub has_loop_contracts: bool,
 }
 
 /// The attributes added by the user to control how a harness is executed.
diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs
index 705732b6700e..ff2ca5c4830a 100644
--- a/kani_metadata/src/unstable.rs
+++ b/kani_metadata/src/unstable.rs
@@ -90,8 +90,8 @@ pub enum UnstableFeature {
     /// Automatically check that no invalid value is produced which is considered UB in Rust.
     /// Note that this does not include checking uninitialized value.
     ValidValueChecks,
-    /// Aeneas/LLBC
-    Aeneas,
+    /// Enabled Lean backend (Aeneas/LLBC)
+    Lean,
     /// Ghost state and shadow memory APIs.
     GhostState,
     /// Automatically check that uninitialized memory is not used.
diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index 94c805a7758a..fc47f8fec423 100644
--- a/library/kani/src/lib.rs
+++ b/library/kani/src/lib.rs
@@ -20,8 +20,6 @@
 #![feature(ptr_metadata)]
 #![feature(f16)]
 #![feature(f128)]
-// Need to add this since we are deprecating `kani::check`. Remove this when we remove that API.
-#![allow(deprecated)]
 
 // Allow us to use `kani::` to access crate features.
 extern crate self as kani;
@@ -32,7 +30,6 @@ mod concrete_playback;
 pub mod futures;
 pub mod invariant;
 pub mod shadow;
-pub mod slice;
 pub mod vec;
 
 mod models;
diff --git a/library/kani/src/slice.rs b/library/kani/src/slice.rs
deleted file mode 100644
index c419a881fa55..000000000000
--- a/library/kani/src/slice.rs
+++ /dev/null
@@ -1,35 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-use crate::{any, assume};
-
-/// Given an array `arr` of length `LENGTH`, this function returns a **valid**
-/// slice of `arr` with non-deterministic start and end points.  This is useful
-/// in situations where one wants to verify that all possible slices of a given
-/// array satisfy some property.
-///
-/// # Example:
-///
-/// ```no_run
-/// # fn foo(_: &[i32]) {}
-/// let arr = [1, 2, 3];
-/// let slice = kani::slice::any_slice_of_array(&arr);
-/// foo(slice); // where foo is a function that takes a slice and verifies a property about it
-/// ```
-pub fn any_slice_of_array<T, const LENGTH: usize>(arr: &[T; LENGTH]) -> &[T] {
-    let (from, to) = any_range::<LENGTH>();
-    &arr[from..to]
-}
-
-/// A mutable version of the previous function
-pub fn any_slice_of_array_mut<T, const LENGTH: usize>(arr: &mut [T; LENGTH]) -> &mut [T] {
-    let (from, to) = any_range::<LENGTH>();
-    &mut arr[from..to]
-}
-
-fn any_range<const LENGTH: usize>() -> (usize, usize) {
-    let from: usize = any();
-    let to: usize = any();
-    assume(to <= LENGTH);
-    assume(from <= to);
-    (from, to)
-}
diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs
index 1dc30feca566..3ef474b65364 100644
--- a/library/kani_core/src/arbitrary.rs
+++ b/library/kani_core/src/arbitrary.rs
@@ -9,6 +9,7 @@
 //! TODO: Use this inside kani library so that we dont have to maintain two copies of the same proc macro for arbitrary.
 
 mod pointer;
+mod slice;
 
 #[macro_export]
 #[allow(clippy::crate_in_macro_def)]
@@ -188,6 +189,78 @@ macro_rules! generate_arbitrary {
         mod arbitrary_ptr {
             kani_core::ptr_generator!();
         }
+
+        pub mod slice {
+            kani_core::slice_generator!();
+        }
+
+        mod range_structures {
+            use super::{
+                Arbitrary,
+                core_path::{
+                    mem,
+                    ops::{Bound, Range, RangeFrom, RangeInclusive, RangeTo, RangeToInclusive},
+                },
+            };
+
+            impl<T> Arbitrary for Bound<T>
+            where
+                T: Arbitrary,
+            {
+                fn any() -> Self {
+                    match u8::any() {
+                        0 => Bound::Included(T::any()),
+                        1 => Bound::Excluded(T::any()),
+                        _ => Bound::Unbounded,
+                    }
+                }
+            }
+
+            impl<T> Arbitrary for Range<T>
+            where
+                T: Arbitrary,
+            {
+                fn any() -> Self {
+                    T::any()..T::any()
+                }
+            }
+
+            impl<T> Arbitrary for RangeFrom<T>
+            where
+                T: Arbitrary,
+            {
+                fn any() -> Self {
+                    T::any()..
+                }
+            }
+
+            impl<T> Arbitrary for RangeInclusive<T>
+            where
+                T: Arbitrary,
+            {
+                fn any() -> Self {
+                    T::any()..=T::any()
+                }
+            }
+
+            impl<T> Arbitrary for RangeTo<T>
+            where
+                T: Arbitrary,
+            {
+                fn any() -> Self {
+                    ..T::any()
+                }
+            }
+
+            impl<T> Arbitrary for RangeToInclusive<T>
+            where
+                T: Arbitrary,
+            {
+                fn any() -> Self {
+                    ..=T::any()
+                }
+            }
+        }
     };
 }
 
diff --git a/library/kani_core/src/arbitrary/slice.rs b/library/kani_core/src/arbitrary/slice.rs
new file mode 100644
index 000000000000..5d6841c2f0c7
--- /dev/null
+++ b/library/kani_core/src/arbitrary/slice.rs
@@ -0,0 +1,43 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This macro generates the logic required to generate slice with arbitrary contents and length.
+#[allow(clippy::crate_in_macro_def)]
+#[macro_export]
+macro_rules! slice_generator {
+    () => {
+        use crate::kani;
+
+        /// Given an array `arr` of length `LENGTH`, this function returns a **valid**
+        /// slice of `arr` with non-deterministic start and end points.  This is useful
+        /// in situations where one wants to verify that all possible slices of a given
+        /// array satisfy some property.
+        ///
+        /// # Example:
+        ///
+        /// ```no_run
+        /// # fn foo(_: &[i32]) {}
+        /// let arr = [1, 2, 3];
+        /// let slice = kani::slice::any_slice_of_array(&arr);
+        /// foo(slice); // where foo is a function that takes a slice and verifies a property about it
+        /// ```
+        pub fn any_slice_of_array<T, const LENGTH: usize>(arr: &[T; LENGTH]) -> &[T] {
+            let (from, to) = any_range::<LENGTH>();
+            &arr[from..to]
+        }
+
+        /// A mutable version of the previous function
+        pub fn any_slice_of_array_mut<T, const LENGTH: usize>(arr: &mut [T; LENGTH]) -> &mut [T] {
+            let (from, to) = any_range::<LENGTH>();
+            &mut arr[from..to]
+        }
+
+        fn any_range<const LENGTH: usize>() -> (usize, usize) {
+            let from: usize = kani::any();
+            let to: usize = kani::any();
+            kani::assume(to <= LENGTH);
+            kani::assume(from <= to);
+            (from, to)
+        }
+    };
+}
diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs
index e579542fe08d..3a4a021b9b61 100644
--- a/library/kani_core/src/lib.rs
+++ b/library/kani_core/src/lib.rs
@@ -44,7 +44,6 @@ macro_rules! kani_lib {
             kani_core::kani_intrinsics!(core);
             kani_core::generate_arbitrary!(core);
             kani_core::generate_models!();
-            kani_core::check_intrinsic!();
 
             pub mod mem {
                 kani_core::kani_mem!(core);
@@ -61,9 +60,6 @@ macro_rules! kani_lib {
         kani_core::kani_intrinsics!(std);
         kani_core::generate_arbitrary!(std);
         kani_core::generate_models!();
-        kani_core::check_intrinsic! {
-            msg="This API will be made private in future releases.", vis=pub
-        }
 
         pub mod mem {
             kani_core::kani_mem!(std);
@@ -515,51 +511,35 @@ macro_rules! kani_intrinsics {
 
             /// Stub the body with its contract.
             pub const REPLACE: Mode = 3;
-        }
-    };
-}
 
-#[macro_export]
-macro_rules! check_intrinsic {
-    ($(msg=$msg:literal, vis=$vis:vis)?) => {
-        /// Creates a non-fatal property with the specified condition and message.
-        ///
-        /// This check will not impact the program control flow even when it fails.
-        ///
-        /// # Example:
-        ///
-        /// ```no_run
-        /// let x: bool = kani::any();
-        /// let y = !x;
-        /// kani::check(x || y, "ORing a boolean variable with its negation must be true");
-        /// kani::check(x == y, "A boolean variable is always different than its negation");
-        /// kani::cover!(true, "This should still be reachable");
-        /// ```
-        ///
-        /// # Deprecated
-        ///
-        /// This function was meant to be internal only, and it was added to Kani's public interface
-        /// by mistake. Thus, it will be made private in future releases.
-        /// Instead, we recommend users to either use `assert` or `cover` to create properties they
-        /// would like to verify.
-        ///
-        /// See <https://github.com/model-checking/kani/issues/3561> for more details.
-        #[cfg(not(feature = "concrete_playback"))]
-        #[inline(never)]
-        #[rustc_diagnostic_item = "KaniCheck"]
-        // TODO: Remove the `#![allow(deprecated)]` inside kani's crate once this is made private.
-        $(#[deprecated(since="0.55.0", note=$msg)])?
-        $($vis)? const fn check(cond: bool, msg: &'static str) {
-            let _ = cond;
-            let _ = msg;
-        }
+            /// Creates a non-fatal property with the specified condition and message.
+            ///
+            /// This check will not impact the program control flow even when it fails.
+            ///
+            /// # Example:
+            ///
+            /// ```no_run
+            /// let x: bool = kani::any();
+            /// let y = !x;
+            /// kani::check(x || y, "ORing a boolean variable with its negation must be true");
+            /// kani::check(x == y, "A boolean variable is always different than its negation");
+            /// kani::cover!(true, "This should still be reachable");
+            /// ```
+            ///
+            #[cfg(not(feature = "concrete_playback"))]
+            #[inline(never)]
+            #[rustc_diagnostic_item = "KaniCheck"]
+            pub(crate) const fn check(cond: bool, msg: &'static str) {
+                let _ = cond;
+                let _ = msg;
+            }
 
-        #[cfg(feature = "concrete_playback")]
-        #[inline(never)]
-        #[rustc_diagnostic_item = "KaniCheck"]
-        $(#[deprecated(since="0.55.0", note=$msg)])?
-        $($vis)? const fn check(cond: bool, msg: &'static str) {
-            assert!(cond, "{}", msg);
+            #[cfg(feature = "concrete_playback")]
+            #[inline(never)]
+            #[rustc_diagnostic_item = "KaniCheck"]
+            pub(crate) const fn check(cond: bool, msg: &'static str) {
+                assert!(cond, "{}", msg);
+            }
         }
     };
 }
diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs
index 4b5b13fddcd9..e1fba0c683a1 100644
--- a/library/kani_core/src/mem.rs
+++ b/library/kani_core/src/mem.rs
@@ -148,7 +148,7 @@ macro_rules! kani_mem {
             reason = "experimental memory predicate API"
         )]
         #[allow(clippy::not_unsafe_ptr_arg_deref)]
-        pub fn same_allocation<T>(ptr1: *const T, ptr2: *const T) -> bool {
+        pub fn same_allocation<T: ?Sized>(ptr1: *const T, ptr2: *const T) -> bool {
             cbmc::same_allocation(ptr1, ptr2)
         }
 
@@ -257,7 +257,7 @@ macro_rules! kani_mem {
 
         /// A helper to assert `is_initialized` to use it as a part of other predicates.
         fn assert_is_initialized<T: ?Sized>(ptr: *const T) -> bool {
-            super::check(
+            super::internal::check(
                 is_initialized(ptr),
                 "Undefined Behavior: Reading from an uninitialized pointer",
             );
@@ -267,18 +267,16 @@ macro_rules! kani_mem {
         pub(super) mod cbmc {
             use super::*;
             /// CBMC specific implementation of [super::same_allocation].
-            pub fn same_allocation<T>(ptr1: *const T, ptr2: *const T) -> bool {
-                let obj1 = crate::kani::mem::pointer_object(ptr1);
-                (obj1 == crate::kani::mem::pointer_object(ptr2)) && {
+            pub fn same_allocation<T: ?Sized>(ptr1: *const T, ptr2: *const T) -> bool {
+                let addr1 = ptr1 as *const ();
+                let addr2 = ptr2 as *const ();
+                let obj1 = crate::kani::mem::pointer_object(addr1);
+                (obj1 == crate::kani::mem::pointer_object(addr2)) && {
                     crate::kani::assert(
-                        unsafe {
-                            is_allocated(ptr1 as *const (), 0) || is_allocated(ptr2 as *const (), 0)
-                        },
+                        unsafe { is_allocated(addr1, 0) || is_allocated(addr2, 0) },
                         "Kani does not support reasoning about pointer to unallocated memory",
                     );
-                    unsafe {
-                        is_allocated(ptr1 as *const (), 0) && is_allocated(ptr2 as *const (), 0)
-                    }
+                    unsafe { is_allocated(addr1, 0) && is_allocated(addr2, 0) }
                 }
             }
         }
diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs
index 258afc36af77..f8eaf8354280 100644
--- a/library/kani_macros/src/derive.rs
+++ b/library/kani_macros/src/derive.rs
@@ -364,6 +364,12 @@ fn fn_any_enum(ident: &Ident, data: &DataEnum) -> TokenStream {
         quote! {
             panic!(#msg)
         }
+    } else if data.variants.len() == 1 {
+        let variant = data.variants.first().unwrap();
+        let init = init_symbolic_item(&variant.ident, &variant.fields);
+        quote! {
+            #ident::#init
+        }
     } else {
         let arms = data.variants.iter().enumerate().map(|(idx, variant)| {
             let init = init_symbolic_item(&variant.ident, &variant.fields);
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 3ed311186f56..16b1d374e0b9 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-10-18"
+channel = "nightly-2024-11-09"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/scripts/check-cbmc-viewer-version.py b/scripts/check-cbmc-viewer-version.py
deleted file mode 100755
index 88c0f7ed31cb..000000000000
--- a/scripts/check-cbmc-viewer-version.py
+++ /dev/null
@@ -1,56 +0,0 @@
-#!/usr/bin/env python3
-# Copyright Kani Contributors
-# SPDX-License-Identifier: Apache-2.0 OR MIT
-
-import argparse
-import re
-import sys
-import subprocess
-from subprocess import PIPE
-
-
-EXIT_CODE_SUCCESS = 0
-EXIT_CODE_MISMATCH = 1
-EXIT_CODE_FAIL = 2
-
-
-def cbmc_viewer_version():
-    cmd = ["cbmc-viewer", "--version"]
-    try:
-        version = subprocess.run(cmd, stdout=PIPE, stderr=PIPE, check=True,
-                                 universal_newlines=True)
-    except (OSError, subprocess.SubprocessError) as error:
-        print(error)
-        print(f"Can't run command '{' '.join(cmd)}'")
-        sys.exit(EXIT_CODE_FAIL)
-
-    match = re.match("CBMC viewer ([0-9]+).([0-9]+)", version.stdout)
-    if not match:
-        print(f"Can't parse CBMC-viewer version string: '{version.stdout.strip()}'")
-        sys.exit(EXIT_CODE_FAIL)
-
-    return match.groups()
-
-def complete_version(*version):
-    numbers = [int(num) if num else 0 for num in version]
-    return (numbers + [0, 0])[:2]
-
-def main():
-    parser = argparse.ArgumentParser(
-        description='Check CBMC-viewer version matches major/minor')
-    parser.add_argument('--major', required=True)
-    parser.add_argument('--minor', required=True)
-    args = parser.parse_args()
-
-    current_version = complete_version(*cbmc_viewer_version())
-    desired_version = complete_version(args.major, args.minor)
-
-    if desired_version > current_version:
-        version_string = '.'.join([str(num) for num in current_version])
-        desired_version_string = '.'.join([str(num) for num in desired_version])
-        print(f'ERROR: CBMC-viewer version is {version_string}, expected at least {desired_version_string}')
-        sys.exit(EXIT_CODE_MISMATCH)
-
-
-if __name__ == "__main__":
-    main()
diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh
index 728129d784b6..88215bdf0317 100755
--- a/scripts/kani-regression.sh
+++ b/scripts/kani-regression.sh
@@ -23,11 +23,8 @@ source "${KANI_DIR}/kani-dependencies"
 # Sanity check dependencies values.
 [[ "${CBMC_MAJOR}.${CBMC_MINOR}" == "${CBMC_VERSION%.*}" ]] || \
     (echo "Conflicting CBMC versions"; exit 1)
-[[ "${CBMC_VIEWER_MAJOR}.${CBMC_VIEWER_MINOR}" == "${CBMC_VIEWER_VERSION}" ]] || \
-    (echo "Conflicting CBMC viewer versions"; exit 1)
 # Check if installed versions are correct.
 check-cbmc-version.py --major ${CBMC_MAJOR} --minor ${CBMC_MINOR}
-check-cbmc-viewer-version.py --major ${CBMC_VIEWER_MAJOR} --minor ${CBMC_VIEWER_MINOR}
 check_kissat_version.sh
 
 # Formatting check
diff --git a/scripts/setup/al2/install_deps.sh b/scripts/setup/al2/install_deps.sh
index ce901ab8afa5..648715e9b055 100755
--- a/scripts/setup/al2/install_deps.sh
+++ b/scripts/setup/al2/install_deps.sh
@@ -31,7 +31,6 @@ python3 -m pip install autopep8
 SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 
 ${SCRIPT_DIR}/install_cbmc.sh
-${SCRIPT_DIR}/install_viewer.sh
 # The Kissat installation script is platform-independent, so is placed one level up
 ${SCRIPT_DIR}/../install_kissat.sh
 ${SCRIPT_DIR}/../install_rustup.sh
diff --git a/scripts/setup/al2/install_viewer.sh b/scripts/setup/al2/install_viewer.sh
deleted file mode 100755
index c8ba7b7b838e..000000000000
--- a/scripts/setup/al2/install_viewer.sh
+++ /dev/null
@@ -1,19 +0,0 @@
-#!/bin/bash
-# Copyright Kani Contributors
-# SPDX-License-Identifier: Apache-2.0 OR MIT
-
-set -eu
-
-# Install cbmc-viewer
-
-# Source kani-dependencies to get CBMC_VIEWER_VERSION
-source kani-dependencies
-
-if [ -z "${CBMC_VIEWER_VERSION:-}" ]; then
-  echo "$0: Error: CBMC_VIEWER_VERSION is not specified"
-  exit 1
-fi
-
-set -x
-
-python3 -m pip install cbmc-viewer==$CBMC_VIEWER_VERSION
diff --git a/scripts/setup/macos/install_deps.sh b/scripts/setup/macos/install_deps.sh
index 179bf8c1237f..112e34680b11 100755
--- a/scripts/setup/macos/install_deps.sh
+++ b/scripts/setup/macos/install_deps.sh
@@ -21,6 +21,5 @@ brew install universal-ctags wget jq
 SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 
 ${SCRIPT_DIR}/install_cbmc.sh
-${SCRIPT_DIR}/install_viewer.sh
 # The Kissat installation script is platform-independent, so is placed one level up
 ${SCRIPT_DIR}/../install_kissat.sh
diff --git a/scripts/setup/macos/install_viewer.sh b/scripts/setup/macos/install_viewer.sh
deleted file mode 100755
index b55eca370d82..000000000000
--- a/scripts/setup/macos/install_viewer.sh
+++ /dev/null
@@ -1,25 +0,0 @@
-#!/bin/bash
-# Copyright Kani Contributors
-# SPDX-License-Identifier: Apache-2.0 OR MIT
-
-set -eu
-
-# Install cbmc-viewer
-
-# Source kani-dependencies to get CBMC_VIEWER_VERSION
-source kani-dependencies
-
-if [ -z "${CBMC_VIEWER_VERSION:-}" ]; then
-  echo "$0: Error: CBMC_VIEWER_VERSION is not specified"
-  exit 1
-fi
-
-set -x
-
-# brew doesn't recognize specific versions of viewer
-# Build from source, since there's only a macos-12 bottle which doesn't seem to work.
-# Install Python 3.12 first while ignoring errors: the system may provide this
-# version, which will hinder brew from installing symlinks
-brew install python@3.12 || true
-brew install -s aws/tap/cbmc-viewer
-echo "Installed: $(cbmc-viewer --version)"
diff --git a/scripts/setup/ubuntu/install_deps.sh b/scripts/setup/ubuntu/install_deps.sh
index b93602691222..2633607744c5 100755
--- a/scripts/setup/ubuntu/install_deps.sh
+++ b/scripts/setup/ubuntu/install_deps.sh
@@ -57,6 +57,5 @@ fi
 SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 
 ${SCRIPT_DIR}/install_cbmc.sh
-${SCRIPT_DIR}/install_viewer.sh
 # The Kissat installation script is platform-independent, so is placed one level up
 ${SCRIPT_DIR}/../install_kissat.sh
diff --git a/scripts/setup/ubuntu/install_viewer.sh b/scripts/setup/ubuntu/install_viewer.sh
deleted file mode 100755
index c8ba7b7b838e..000000000000
--- a/scripts/setup/ubuntu/install_viewer.sh
+++ /dev/null
@@ -1,19 +0,0 @@
-#!/bin/bash
-# Copyright Kani Contributors
-# SPDX-License-Identifier: Apache-2.0 OR MIT
-
-set -eu
-
-# Install cbmc-viewer
-
-# Source kani-dependencies to get CBMC_VIEWER_VERSION
-source kani-dependencies
-
-if [ -z "${CBMC_VIEWER_VERSION:-}" ]; then
-  echo "$0: Error: CBMC_VIEWER_VERSION is not specified"
-  exit 1
-fi
-
-set -x
-
-python3 -m pip install cbmc-viewer==$CBMC_VIEWER_VERSION
diff --git a/src/lib.rs b/src/lib.rs
index f24163d3213c..5b79ec504d4c 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -140,7 +140,7 @@ fn exec(bin: &str) -> Result<()> {
 
     // Allow python scripts to find dependencies under our pyroot
     let pythonpath = prepend_search_path(&[pyroot], env::var_os("PYTHONPATH"))?;
-    // Add: kani, cbmc, viewer (pyroot), and our rust toolchain directly to our PATH
+    // Add: kani, cbmc, and our rust toolchain directly to our PATH
     let path = prepend_search_path(&[bin_kani, bin_pyroot], env::var_os("PATH"))?;
 
     // Ensure our environment variables for linker search paths won't cause failures, before we execute:
diff --git a/src/setup.rs b/src/setup.rs
index eb1227269ccc..96daf82e4a27 100644
--- a/src/setup.rs
+++ b/src/setup.rs
@@ -86,8 +86,6 @@ pub fn setup(
 
     setup_rust_toolchain(&kani_dir, use_local_toolchain)?;
 
-    setup_python_deps(&kani_dir)?;
-
     os_hacks::setup_os_hacks(&kani_dir, &os)?;
 
     println!("[5/5] Successfully completed Kani first-time setup.");
@@ -183,23 +181,6 @@ fn setup_rust_toolchain(kani_dir: &Path, use_local_toolchain: Option<OsString>)
     Ok(toolchain_version)
 }
 
-/// Install into the pyroot the python dependencies we need
-fn setup_python_deps(kani_dir: &Path) -> Result<()> {
-    println!("[4/5] Installing Kani python dependencies...");
-    let pyroot = kani_dir.join("pyroot");
-
-    // TODO: this is a repetition of versions from kani/kani-dependencies
-    let pkg_versions = &["cbmc-viewer==3.9"];
-
-    Command::new("python3")
-        .args(["-m", "pip", "install", "--target"])
-        .arg(&pyroot)
-        .args(pkg_versions)
-        .run()?;
-
-    Ok(())
-}
-
 // This ends the setup steps above.
 //
 // Just putting a bit of space between that and the helper functions below.
diff --git a/tests/.gitignore b/tests/.gitignore
index 7f948a83337c..814a069a9424 100644
--- a/tests/.gitignore
+++ b/tests/.gitignore
@@ -6,7 +6,7 @@ target/
 
 # Binary artifacts
 *.goto
-*out
+*.out
 smoke
 check_tests
 function
diff --git a/tests/cargo-kani/rectangle-example/README.md b/tests/cargo-kani/rectangle-example/README.md
index b07c61a96c9c..b16c1d464881 100644
--- a/tests/cargo-kani/rectangle-example/README.md
+++ b/tests/cargo-kani/rectangle-example/README.md
@@ -31,17 +31,14 @@ $ cargo kani --harness stretched_rectangle_can_hold_original --output-format ter
 VERIFICATION:- FAILED
 ```
 
-In order to view a trace (a step-by-step execution of the program) use the `--visualize` flag:
+In order to view a counterexample use the `--concrete-playback` flag:
 
 ```bash
-$ cargo kani --harness stretched_rectangle_can_hold_original --output-format terse --visualize
+$ cargo kani --harness stretched_rectangle_can_hold_original --output-format terse -Zconcrete-playback --concrete-playback=print
 # --snip--
 VERIFICATION:- FAILED
-# and generates a html report in target/report/html/index.html
 ```
 
-And open the report in a browser.
-
 After fixing the problem we can re-run Kani (on the proof harness `stretched_rectangle_can_hold_original_fixed`). This time we expect verification success:
 
 ```bash
diff --git a/tests/cargo-kani/simple-visualize/Cargo.toml b/tests/cargo-kani/simple-visualize/Cargo.toml
deleted file mode 100644
index 24f2576ca69f..000000000000
--- a/tests/cargo-kani/simple-visualize/Cargo.toml
+++ /dev/null
@@ -1,13 +0,0 @@
-# Copyright Kani Contributors
-# SPDX-License-Identifier: Apache-2.0 OR MIT
-[package]
-name = "simple-visualize"
-version = "0.1.0"
-edition = "2018"
-
-[dependencies]
-
-[workspace]
-
-[package.metadata.kani]
-flags = {enable-unstable = true, visualize = true}
diff --git a/tests/cargo-kani/simple-visualize/main.expected b/tests/cargo-kani/simple-visualize/main.expected
deleted file mode 100644
index 1d0839175310..000000000000
--- a/tests/cargo-kani/simple-visualize/main.expected
+++ /dev/null
@@ -1,2 +0,0 @@
-warning: The `--visualize` option is deprecated. This option will be removed soon. Consider using `--concrete-playback` instead
-report-main/html/index.html
diff --git a/tests/cargo-kani/simple-visualize/src/main.rs b/tests/cargo-kani/simple-visualize/src/main.rs
deleted file mode 100644
index 390a15b9c89d..000000000000
--- a/tests/cargo-kani/simple-visualize/src/main.rs
+++ /dev/null
@@ -1,6 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-#[kani::proof]
-fn main() {
-    assert!(1 == 2);
-}
diff --git a/tests/expected/function-contract/const_fn_with_effect.rs b/tests/expected/function-contract/const_fn_with_effect.rs
index 070c44482a80..ab0725eee244 100644
--- a/tests/expected/function-contract/const_fn_with_effect.rs
+++ b/tests/expected/function-contract/const_fn_with_effect.rs
@@ -6,7 +6,6 @@
 //! Check that Kani contract can be applied to a constant function.
 //! <https://github.com/model-checking/kani/issues/3258>
 
-#![feature(effects)]
 #![allow(incomplete_features)]
 
 #[kani::requires(kani::mem::can_dereference(arg))]
diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs
index 1cce5e2364c3..518c8140ea37 100644
--- a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs
+++ b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs
@@ -1,6 +1,8 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// Temporarily reduce the number of object bits till
+// https://github.com/model-checking/kani/issues/3611 is fixed
+// kani-flags: -Zfunction-contracts --enable-unstable --cbmc-args --object-bits 12
 
 /// The objective of this test is to check the modification of a RefCell used as interior mutability in an immutable struct
 use std::cell::RefCell;
diff --git a/tests/expected/intrinsics/float-to-int/non_finite.expected b/tests/expected/intrinsics/float-to-int/non_finite.expected
new file mode 100644
index 000000000000..703853398bf2
--- /dev/null
+++ b/tests/expected/intrinsics/float-to-int/non_finite.expected
@@ -0,0 +1,5 @@
+Failed Checks: float_to_int_unchecked: attempt to convert a non-finite value to an integer
+Verification failed for - check_neg_inf
+Verification failed for - check_inf
+Verification failed for - check_nan
+Complete - 0 successfully verified harnesses, 3 failures, 3 total.
diff --git a/tests/expected/intrinsics/float-to-int/non_finite.rs b/tests/expected/intrinsics/float-to-int/non_finite.rs
new file mode 100644
index 000000000000..1aace2f7d403
--- /dev/null
+++ b/tests/expected/intrinsics/float-to-int/non_finite.rs
@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#![feature(core_intrinsics)]
+
+//! Check that Kani flags a conversion of a NaN or INFINITY to an int via
+//! `float_to_int_unchecked`
+
+#[kani::proof]
+fn check_nan() {
+    let f: f32 = f32::NAN;
+    let _i: u32 = unsafe { std::intrinsics::float_to_int_unchecked(f) };
+}
+
+#[kani::proof]
+fn check_inf() {
+    let f: f32 = f32::INFINITY;
+    let _i: u32 = unsafe { std::intrinsics::float_to_int_unchecked(f) };
+}
+
+#[kani::proof]
+fn check_neg_inf() {
+    let f: f32 = f32::NEG_INFINITY;
+    let _i: u32 = unsafe { std::intrinsics::float_to_int_unchecked(f) };
+}
diff --git a/tests/expected/intrinsics/float-to-int/oob.expected b/tests/expected/intrinsics/float-to-int/oob.expected
new file mode 100644
index 000000000000..f862df90f706
--- /dev/null
+++ b/tests/expected/intrinsics/float-to-int/oob.expected
@@ -0,0 +1,14 @@
+Failed Checks: float_to_int_unchecked: attempt to convert a value out of range of the target integer
+
+Verification failed for - check_u16_upper
+Verification failed for - check_u64_upper
+Verification failed for - check_usize_upper
+Verification failed for - check_u32_upper
+Verification failed for - check_u8_upper
+Verification failed for - check_u128_lower
+Verification failed for - check_u32_lower
+Verification failed for - check_u8_lower
+Verification failed for - check_u64_lower
+Verification failed for - check_usize_lower
+Verification failed for - check_u16_lower
+Complete - 1 successfully verified harnesses, 11 failures, 12 total.
diff --git a/tests/expected/intrinsics/float-to-int/oob.rs b/tests/expected/intrinsics/float-to-int/oob.rs
new file mode 100644
index 000000000000..a49cf89ca82c
--- /dev/null
+++ b/tests/expected/intrinsics/float-to-int/oob.rs
@@ -0,0 +1,41 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#![feature(core_intrinsics)]
+
+//! Check that Kani flags a conversion of an out-of-bounds float value to an int
+//! via `float_to_int_unchecked`
+
+macro_rules! check_unsigned_lower {
+    ($name:ident, $t:ty) => {
+        #[kani::proof]
+        fn $name() {
+            let x: f32 = kani::any_where(|v: &f32| v.is_finite() && *v <= -1.0);
+            let _u: $t = unsafe { std::intrinsics::float_to_int_unchecked(x) };
+        }
+    };
+}
+
+check_unsigned_lower!(check_u8_lower, u8);
+check_unsigned_lower!(check_u16_lower, u16);
+check_unsigned_lower!(check_u32_lower, u32);
+check_unsigned_lower!(check_u64_lower, u64);
+check_unsigned_lower!(check_u128_lower, u128);
+check_unsigned_lower!(check_usize_lower, usize);
+
+macro_rules! check_unsigned_upper {
+    ($name:ident, $t:ty, $v:expr) => {
+        #[kani::proof]
+        fn $name() {
+            let x: f32 = kani::any_where(|v: &f32| v.is_finite() && *v >= $v);
+            let _u: $t = unsafe { std::intrinsics::float_to_int_unchecked(x) };
+        }
+    };
+}
+
+check_unsigned_upper!(check_u8_upper, u8, (1u128 << 8) as f32);
+check_unsigned_upper!(check_u16_upper, u16, (1u128 << 16) as f32);
+check_unsigned_upper!(check_u32_upper, u32, (1u128 << 32) as f32);
+check_unsigned_upper!(check_u64_upper, u64, (1u128 << 64) as f32);
+// this harness should pass
+check_unsigned_upper!(check_u128_upper, u128, f32::INFINITY);
+check_unsigned_upper!(check_usize_upper, usize, (1u128 << 64) as f32);
diff --git a/tests/expected/llbc/basic0/expected b/tests/expected/llbc/basic0/expected
index 112a67a21548..45d073737f3b 100644
--- a/tests/expected/llbc/basic0/expected
+++ b/tests/expected/llbc/basic0/expected
@@ -1,8 +1,8 @@
 fn test::is_zero(@1: i32) -> bool\
 {\
     let @0: bool; // return\
-    let @1: i32; // arg #1\
+    let i@1: i32; // arg #1\
 
-    @0 := copy (@1) == const (0 : i32)\
+    @0 := copy (i@1) == const (0 : i32)\
     return\
 }
diff --git a/tests/expected/llbc/basic0/test.rs b/tests/expected/llbc/basic0/test.rs
index 5025994ab31c..410cf1848d44 100644
--- a/tests/expected/llbc/basic0/test.rs
+++ b/tests/expected/llbc/basic0/test.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zaeneas --print-llbc
+// kani-flags: -Zlean --print-llbc
 
 //! This test checks that Kani's LLBC backend handles basic expressions, in this
 //! case an equality between a variable and a constant
diff --git a/tests/expected/llbc/basic1/expected b/tests/expected/llbc/basic1/expected
index 9cb0bef6f7c6..233940af9752 100644
--- a/tests/expected/llbc/basic1/expected
+++ b/tests/expected/llbc/basic1/expected
@@ -1,15 +1,15 @@
 fn test::select(@1: bool, @2: i32, @3: i32) -> i32
 {
     let @0: i32; // return
-    let @1: bool; // arg #1
-    let @2: i32; // arg #2
-    let @3: i32; // arg #3
+    let s@1: bool; // arg #1
+    let x@2: i32; // arg #2
+    let y@3: i32; // arg #3
 
-    if copy (@1) {
-        @0 := copy (@2)
+    if copy (s@1) {
+        @0 := copy (x@2)
     }
     else {
-        @0 := copy (@3)
+        @0 := copy (y@3)
     }
     return
 }
diff --git a/tests/expected/llbc/basic1/test.rs b/tests/expected/llbc/basic1/test.rs
index 92818fb93bfb..80f39e91ea9e 100644
--- a/tests/expected/llbc/basic1/test.rs
+++ b/tests/expected/llbc/basic1/test.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zaeneas --print-llbc
+// kani-flags: -Zlean --print-llbc
 
 //! This test checks that Kani's LLBC backend handles basic expressions, in this
 //! case an if condition
diff --git a/tests/expected/loop-contract/count_zero.rs b/tests/expected/loop-contract/count_zero.rs
index 1b6cee925c97..e4d8d2a78cf3 100644
--- a/tests/expected/loop-contract/count_zero.rs
+++ b/tests/expected/loop-contract/count_zero.rs
@@ -27,9 +27,5 @@ const fn count_zero(slice: &[u8]) -> usize {
 
 #[kani::proof]
 pub fn check_counter() {
-    // Needed to avoid having `free` be removed as unused function. This is
-    // because DFCC contract enforcement assumes that a definition for `free`
-    // exists.
-    let _ = Box::new(10);
     assert_eq!(count_zero(&[1, 2, 3]), 0)
 }
diff --git a/tests/expected/loop-contract/memchar_naive.rs b/tests/expected/loop-contract/memchar_naive.rs
index 140d9f6342ed..9d4e208917b4 100644
--- a/tests/expected/loop-contract/memchar_naive.rs
+++ b/tests/expected/loop-contract/memchar_naive.rs
@@ -13,10 +13,6 @@
 
 #[kani::proof]
 fn memchar_naive_harness() {
-    // Needed to avoid having `free` be removed as unused function. This is
-    // because DFCC contract enforcement assumes that a definition for `free`
-    // exists.
-    let _ = Box::new(10);
     let text = [1, 2, 3, 4, 5];
     let x = 5;
     let mut i = 0;
diff --git a/tests/expected/loop-contract/multiple_loops.expected b/tests/expected/loop-contract/multiple_loops.expected
index 34c886c358cb..5d63471c6fa8 100644
--- a/tests/expected/loop-contract/multiple_loops.expected
+++ b/tests/expected/loop-contract/multiple_loops.expected
@@ -1 +1,2 @@
 VERIFICATION:- SUCCESSFUL
+Complete - 2 successfully verified harnesses, 0 failures, 2 total.
diff --git a/tests/expected/loop-contract/multiple_loops.rs b/tests/expected/loop-contract/multiple_loops.rs
index 5fa2d6b9889a..b99278d32b43 100644
--- a/tests/expected/loop-contract/multiple_loops.rs
+++ b/tests/expected/loop-contract/multiple_loops.rs
@@ -11,12 +11,14 @@
 fn multiple_loops() {
     let mut x: u8 = kani::any_where(|i| *i >= 10);
 
-    #[kani::loop_invariant(x >= 5)]
-    while x > 5 {
-        x = x - 1;
+    if x != 20 {
+        #[kani::loop_invariant(x >= 5)]
+        while x > 5 {
+            x = x - 1;
+        }
     }
 
-    assert!(x == 5);
+    assert!(x == 5 || x == 20);
 
     #[kani::loop_invariant(x >= 2)]
     while x > 2 {
@@ -42,12 +44,16 @@ fn simple_while_loops() {
     assert!(x == 2);
 }
 
+/// Check that `loop-contracts` works correctly for harness
+/// without loop contracts.
+#[kani::proof]
+fn no_loop_harness() {
+    let x = 2;
+    assert!(x == 2);
+}
+
 #[kani::proof]
 fn multiple_loops_harness() {
-    // Needed to avoid having `free` be removed as unused function. This is
-    // because DFCC contract enforcement assumes that a definition for `free`
-    // exists.
-    let _ = Box::new(10);
     multiple_loops();
     simple_while_loops();
 }
diff --git a/tests/expected/loop-contract/simple_while_loop.rs b/tests/expected/loop-contract/simple_while_loop.rs
index 6880d86d673a..e3b75ab4a8b7 100644
--- a/tests/expected/loop-contract/simple_while_loop.rs
+++ b/tests/expected/loop-contract/simple_while_loop.rs
@@ -9,12 +9,7 @@
 #![feature(proc_macro_hygiene)]
 
 #[kani::proof]
-#[kani::solver(kissat)]
 fn simple_while_loop_harness() {
-    // Needed to avoid having `free` be removed as unused function. This is
-    // because DFCC contract enforcement assumes that a definition for `free`
-    // exists.
-    let _ = Box::new(10);
     let mut x: u8 = kani::any_where(|i| *i >= 2);
 
     #[kani::loop_invariant(x >= 2)]
diff --git a/tests/expected/loop-contract/simple_while_loop_not_enabled.expected b/tests/expected/loop-contract/simple_while_loop_not_enabled.expected
new file mode 100644
index 000000000000..c0356572717d
--- /dev/null
+++ b/tests/expected/loop-contract/simple_while_loop_not_enabled.expected
@@ -0,0 +1,2 @@
+Unwinding loop
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/loop-contract/simple_while_loop_not_enabled.rs b/tests/expected/loop-contract/simple_while_loop_not_enabled.rs
new file mode 100644
index 000000000000..71851f7d875b
--- /dev/null
+++ b/tests/expected/loop-contract/simple_while_loop_not_enabled.rs
@@ -0,0 +1,21 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags:
+
+//! Check if the harness can be proved when loop contracts is not enabled.
+
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+
+#[kani::proof]
+fn simple_while_loop_harness() {
+    let mut x: u8 = 10;
+
+    #[kani::loop_invariant(x >= 2)]
+    while x > 2 {
+        x = x - 1;
+    }
+
+    assert!(x == 2);
+}
diff --git a/tests/expected/loop-contract/small_slice_eq.rs b/tests/expected/loop-contract/small_slice_eq.rs
index a59436122da5..4c97d8a18502 100644
--- a/tests/expected/loop-contract/small_slice_eq.rs
+++ b/tests/expected/loop-contract/small_slice_eq.rs
@@ -6,20 +6,25 @@
 // Modifications Copyright Kani Contributors
 // See GitHub history for details.
 
-// kani-flags: -Z loop-contracts --enable-unstable --cbmc-args --arrays-uf-always --no-standard-checks --object-bits 8
+// kani-flags: -Z loop-contracts -Z mem-predicates --enable-unstable --cbmc-args --object-bits 8
 
-//! Check if loop contracts are correctly applied. The flag --no-standard-checks should be
-//! removed once same_object predicate is supported in loop contracts.
+//! Check if loop contracts are correctly applied.
 
 #![feature(stmt_expr_attributes)]
 #![feature(proc_macro_hygiene)]
 #![feature(ptr_sub_ptr)]
+
+extern crate kani;
+
+use kani::mem::same_allocation;
+
 unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool {
     debug_assert_eq!(x.len(), y.len());
     unsafe {
         let (mut px, mut py) = (x.as_ptr(), y.as_ptr());
         let (pxend, pyend) = (px.add(x.len() - 4), py.add(y.len() - 4));
-        #[kani::loop_invariant( px as isize >= x.as_ptr() as isize
+        #[kani::loop_invariant( same_allocation(x.as_ptr(), px) && same_allocation(y.as_ptr(), py)
+        && px as isize >= x.as_ptr() as isize
         && py as isize >= y.as_ptr() as isize
         && px as isize - x.as_ptr() as isize == (py as isize - y.as_ptr() as isize))]
         while px < pxend {
@@ -39,13 +44,10 @@ unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool {
 
 #[kani::proof]
 fn small_slice_eq_harness() {
-    // Needed to avoid having `free` be removed as unused function. This is
-    // because DFCC contract enforcement assumes that a definition for `free`
-    // exists.
-    let _ = Box::new(10);
-    let mut a = [1; 2000];
-    let mut b = [1; 2000];
+    const ARR_SIZE: usize = 2000;
+    let x: [u8; ARR_SIZE] = kani::any();
+    let y: [u8; ARR_SIZE] = kani::any();
     unsafe {
-        small_slice_eq(&mut a, &mut b);
+        small_slice_eq(&x, &y);
     }
 }
diff --git a/tests/kani/Arbitrary/ops.rs b/tests/kani/Arbitrary/ops.rs
new file mode 100644
index 000000000000..6ae97b2335f4
--- /dev/null
+++ b/tests/kani/Arbitrary/ops.rs
@@ -0,0 +1,114 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Check that users can generate range structures
+
+extern crate kani;
+
+use std::ops::{Bound, Range, RangeFrom, RangeInclusive, RangeTo, RangeToInclusive};
+
+#[kani::proof]
+fn bound() {
+    let elem: Wrapper<Bound<u8>> = kani::any();
+    match elem.0 {
+        Bound::Included(elem) => {
+            assert!(elem < 100);
+        }
+        Bound::Excluded(elem) => {
+            assert!(elem < 100);
+        }
+        Bound::Unbounded => {}
+    }
+}
+
+#[kani::proof]
+fn range() {
+    let elem: Wrapper<Range<u8>> = kani::any();
+    assert!(elem.0.start < 100);
+    assert!(elem.0.end < 100);
+}
+
+#[kani::proof]
+fn range_from() {
+    let elem: Wrapper<RangeFrom<u8>> = kani::any();
+    assert!(elem.0.start < 100);
+}
+
+#[kani::proof]
+fn range_inclusive() {
+    let elem: Wrapper<RangeInclusive<u8>> = kani::any();
+    assert!(*elem.0.start() < 100);
+    assert!(*elem.0.end() < 100);
+}
+
+#[kani::proof]
+fn range_to() {
+    let elem: Wrapper<RangeTo<u8>> = kani::any();
+    assert!(elem.0.end < 100);
+}
+
+#[kani::proof]
+fn range_to_inclusive() {
+    let elem: Wrapper<RangeToInclusive<u8>> = kani::any();
+    assert!(elem.0.end < 100);
+}
+
+struct Wrapper<T>(T);
+
+impl kani::Arbitrary for Wrapper<Bound<u8>> {
+    fn any() -> Self {
+        let val = kani::any();
+        match val {
+            Bound::Included(elem) => {
+                kani::assume(elem < 100);
+            }
+            Bound::Excluded(elem) => {
+                kani::assume(elem < 100);
+            }
+            Bound::Unbounded => {}
+        }
+        Self(val)
+    }
+}
+
+impl kani::Arbitrary for Wrapper<Range<u8>> {
+    fn any() -> Self {
+        let val = kani::any()..kani::any();
+        kani::assume(val.start < 100);
+        kani::assume(val.end < 100);
+        Self(val)
+    }
+}
+
+impl kani::Arbitrary for Wrapper<RangeFrom<u8>> {
+    fn any() -> Self {
+        let val = kani::any()..;
+        kani::assume(val.start < 100);
+        Self(val)
+    }
+}
+
+impl kani::Arbitrary for Wrapper<RangeInclusive<u8>> {
+    fn any() -> Self {
+        let val = kani::any()..=kani::any();
+        kani::assume(*val.start() < 100);
+        kani::assume(*val.end() < 100);
+        Self(val)
+    }
+}
+
+impl kani::Arbitrary for Wrapper<RangeTo<u8>> {
+    fn any() -> Self {
+        let val = ..kani::any();
+        kani::assume(val.end < 100);
+        Self(val)
+    }
+}
+
+impl kani::Arbitrary for Wrapper<RangeToInclusive<u8>> {
+    fn any() -> Self {
+        let val = ..=kani::any();
+        kani::assume(val.end < 100);
+        Self(val)
+    }
+}
diff --git a/tests/kani/CodegenAggregateRawPtrTraitObject/main.rs b/tests/kani/CodegenAggregateRawPtrTraitObject/main.rs
new file mode 100644
index 000000000000..92ffb413ae70
--- /dev/null
+++ b/tests/kani/CodegenAggregateRawPtrTraitObject/main.rs
@@ -0,0 +1,46 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// Test that Kani can verify code that produces a aggregate raw pointer to trait objects
+// c.f. https://github.com/model-checking/kani/issues/3631
+
+#![feature(ptr_metadata)]
+
+use std::ptr::NonNull;
+
+trait SampleTrait {
+    fn get_value(&self) -> i32;
+}
+
+struct SampleStruct {
+    value: i32,
+}
+
+impl SampleTrait for SampleStruct {
+    fn get_value(&self) -> i32 {
+        self.value
+    }
+}
+
+#[cfg(kani)]
+#[kani::proof]
+fn check_nonnull_dyn_from_raw_parts() {
+    // Create a SampleTrait object from SampleStruct
+    let sample_struct = SampleStruct { value: kani::any() };
+    let trait_object: &dyn SampleTrait = &sample_struct;
+
+    // Get the raw data pointer and metadata for the trait object
+    let trait_ptr = NonNull::new(trait_object as *const dyn SampleTrait as *mut ()).unwrap();
+    let metadata = std::ptr::metadata(trait_object);
+
+    // Create NonNull<dyn SampleTrait> from the data pointer and metadata
+    let nonnull_trait_object: NonNull<dyn SampleTrait> =
+        NonNull::from_raw_parts(trait_ptr, metadata);
+
+    unsafe {
+        // Ensure trait method and member is preserved
+        kani::assert(
+            trait_object.get_value() == nonnull_trait_object.as_ref().get_value(),
+            "trait method and member must correctly preserve",
+        );
+    }
+}
diff --git a/tests/kani/FunctionContracts/fixme_receiver_contracts.rs b/tests/kani/FunctionContracts/fixme_receiver_contracts.rs
new file mode 100644
index 000000000000..3a894354b868
--- /dev/null
+++ b/tests/kani/FunctionContracts/fixme_receiver_contracts.rs
@@ -0,0 +1,147 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Checks that function contracts work with different types of receivers. I.e.:
+//! - &Self (i.e. &self)
+//! - &mut Self (i.e &mut self)
+//! - Box<Self>
+//! - Rc<Self>
+//! - Arc<Self>
+//! - Pin<P> where P is one of the types above
+//! Source: <https://doc.rust-lang.org/reference/items/traits.html?highlight=receiver#object-safety>
+// compile-flags: --edition 2021
+// kani-flags: -Zfunction-contracts
+
+#![feature(rustc_attrs)]
+
+extern crate kani;
+
+use std::boxed::Box;
+use std::pin::Pin;
+use std::rc::Rc;
+use std::sync::Arc;
+
+/// Type representing a valid ASCII value going from `0..128`.
+#[derive(Copy, Clone, PartialEq, Eq)]
+#[rustc_layout_scalar_valid_range_start(0)]
+#[rustc_layout_scalar_valid_range_end(128)]
+struct CharASCII(u8);
+
+impl kani::Arbitrary for CharASCII {
+    fn any() -> CharASCII {
+        let val = kani::any_where(|inner: &u8| *inner < 128);
+        unsafe { CharASCII(val) }
+    }
+}
+
+/// This type contains unsafe setter functions with the same contract but different type of
+/// receivers.
+impl CharASCII {
+    #[kani::modifies(&self.0)]
+    #[kani::requires(new_val < 128)]
+    #[kani::ensures(|_| self.0 == new_val)]
+    unsafe fn set_val(&mut self, new_val: u8) {
+        self.0 = new_val
+    }
+
+    #[kani::modifies(&self.0)]
+    #[kani::requires(new_val < 128)]
+    #[kani::ensures(|_| self.0 == new_val)]
+    unsafe fn set_mut_ref(self: &mut Self, new_val: u8) {
+        self.0 = new_val
+    }
+
+    #[kani::modifies(&self.as_ref().0)]
+    #[kani::requires(new_val < 128)]
+    #[kani::ensures(|_| self.as_ref().0 == new_val)]
+    unsafe fn set_box(mut self: Box<Self>, new_val: u8) {
+        self.as_mut().0 = new_val
+    }
+
+    #[kani::modifies(&self.as_ref().0)]
+    #[kani::requires(new_val < 128)]
+    #[kani::ensures(|_| self.as_ref().0 == new_val)]
+    unsafe fn set_rc(mut self: Rc<Self>, new_val: u8) {
+        Rc::<_>::get_mut(&mut self).unwrap().0 = new_val
+    }
+
+    #[kani::modifies(&self.as_ref().0)]
+    #[kani::requires(new_val < 128)]
+    #[kani::ensures(|_| self.as_ref().0 == new_val)]
+    unsafe fn set_arc(mut self: Arc<Self>, new_val: u8) {
+        Arc::<_>::get_mut(&mut self).unwrap().0 = new_val;
+    }
+
+    #[kani::modifies(&self.0)]
+    #[kani::requires(new_val < 128)]
+    #[kani::ensures(|_| self.0 == new_val)]
+    unsafe fn set_pin(mut self: Pin<&mut Self>, new_val: u8) {
+        self.0 = new_val
+    }
+
+    #[kani::modifies(&self.0)]
+    #[kani::requires(new_val < 128)]
+    #[kani::ensures(|_| self.0 == new_val)]
+    unsafe fn set_pin_box(mut self: Pin<Box<Self>>, new_val: u8) {
+        self.0 = new_val
+    }
+}
+
+mod verify {
+    use super::*;
+    use kani::Arbitrary;
+
+    #[kani::proof_for_contract(CharASCII::set_val)]
+    fn check_set_val() {
+        let mut obj = CharASCII::any();
+        let original = obj.0;
+        let new_val: u8 = kani::any();
+        unsafe { obj.set_val(new_val) };
+    }
+
+    #[kani::proof_for_contract(CharASCII::set_mut_ref)]
+    fn check_mut_ref() {
+        let mut obj = CharASCII::any();
+        let new_val: u8 = kani::any();
+        unsafe { obj.set_mut_ref(new_val) };
+    }
+
+    #[kani::proof_for_contract(CharASCII::set_box)]
+    fn check_box() {
+        let obj = CharASCII::any();
+        let original = obj.0;
+        let new_val: u8 = kani::any();
+        unsafe { Box::new(obj).set_box(new_val) };
+    }
+
+    #[kani::proof_for_contract(CharASCII::set_rc)]
+    fn check_rc() {
+        let obj = CharASCII::any();
+        let original = obj.0;
+        let new_val: u8 = kani::any();
+        unsafe { Rc::new(obj).set_rc(new_val) };
+    }
+
+    #[kani::proof_for_contract(CharASCII::set_arc)]
+    fn check_arc() {
+        let obj = CharASCII::any();
+        let original = obj.0;
+        let new_val: u8 = kani::any();
+        unsafe { Arc::new(obj).set_arc(new_val) };
+    }
+
+    #[kani::proof_for_contract(CharASCII::set_pin)]
+    fn check_pin() {
+        let mut obj = CharASCII::any();
+        let original = obj.0;
+        let new_val: u8 = kani::any();
+        unsafe { Pin::new(&mut obj).set_pin(new_val) };
+    }
+
+    #[kani::proof_for_contract(CharASCII::set_pin_box)]
+    fn check_pin_box() {
+        let obj = CharASCII::any();
+        let original = obj.0;
+        let new_val: u8 = kani::any();
+        unsafe { Pin::new(Box::new(obj)).set_pin_box(new_val) };
+    }
+}
diff --git a/tests/kani/FunctionContracts/fn_params.rs b/tests/kani/FunctionContracts/fn_params.rs
index b485ddf2b32b..42e2c52c193e 100644
--- a/tests/kani/FunctionContracts/fn_params.rs
+++ b/tests/kani/FunctionContracts/fn_params.rs
@@ -21,8 +21,6 @@ struct MyStruct {
 #[kani::requires(val.u == tup_u)]
 #[kani::requires(Ok(val.c) == char::try_from(first))]
 #[kani::requires(val.c == tup_c)]
-/// We need this extra clause due to <https://github.com/model-checking/kani/issues/3370>.
-#[kani::requires(char::try_from(first).is_ok())]
 pub fn odd_parameters_eq(
     [first, second]: [u32; 2],
     (tup_c, tup_u): (char, u32),
@@ -41,8 +39,6 @@ pub fn odd_parameters_eq(
 #[kani::requires(val.u == tup_u)]
 #[kani::requires(Ok(val.c) == char::try_from(first))]
 // MISSING: #[kani::requires(val.c == tup_c)]
-// We need this extra clause due to <https://github.com/model-checking/kani/issues/3370>.
-#[kani::requires(char::try_from(first).is_ok())]
 pub fn odd_parameters_eq_wrong(
     [first, second]: [u32; 2],
     (tup_c, tup_u): (char, u32),
diff --git a/tests/kani/FunctionContracts/modify_slice_elem.rs b/tests/kani/FunctionContracts/modify_slice_elem.rs
new file mode 100644
index 000000000000..50df13b45af3
--- /dev/null
+++ b/tests/kani/FunctionContracts/modify_slice_elem.rs
@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Check that Kani correctly verifies the contract that modifies slices.
+//!
+//! Note that this test used to crash while parsing the annotations.
+// kani-flags: -Zfunction-contracts
+extern crate kani;
+
+#[kani::requires(idx < slice.len())]
+#[kani::modifies(slice.as_ptr().wrapping_add(idx))]
+#[kani::ensures(|_| slice[idx] == new_val)]
+fn modify_slice(slice: &mut [u32], idx: usize, new_val: u32) {
+    *slice.get_mut(idx).unwrap() = new_val;
+}
+
+#[cfg(kani)]
+mod verify {
+    use super::modify_slice;
+
+    #[kani::proof_for_contract(modify_slice)]
+    fn check_modify_slice() {
+        let mut data = kani::vec::any_vec::<u32, 5>();
+        modify_slice(&mut data, kani::any(), kani::any())
+    }
+}
diff --git a/tests/kani/Intrinsics/FloatToInt/float_to_int.rs b/tests/kani/Intrinsics/FloatToInt/float_to_int.rs
new file mode 100644
index 000000000000..4797669b9b61
--- /dev/null
+++ b/tests/kani/Intrinsics/FloatToInt/float_to_int.rs
@@ -0,0 +1,49 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#![feature(core_intrinsics)]
+
+// Check that the `float_to_int_unchecked` intrinsic works as expected
+
+use std::intrinsics::float_to_int_unchecked;
+
+macro_rules! check_float_to_int_unchecked {
+    ($float_ty:ty, $int_ty:ty) => {
+        let f: $float_ty = kani::any_where(|f: &$float_ty| {
+            f.is_finite() && *f > <$int_ty>::MIN as $float_ty && *f < <$int_ty>::MAX as $float_ty
+        });
+        let u: $int_ty = unsafe { float_to_int_unchecked(f) };
+        assert_eq!(u as $float_ty, f.trunc());
+    };
+}
+
+#[kani::proof]
+fn check_f32_to_int_unchecked() {
+    check_float_to_int_unchecked!(f32, u8);
+    check_float_to_int_unchecked!(f32, u16);
+    check_float_to_int_unchecked!(f32, u32);
+    check_float_to_int_unchecked!(f32, u64);
+    check_float_to_int_unchecked!(f32, u128);
+    check_float_to_int_unchecked!(f32, usize);
+    check_float_to_int_unchecked!(f32, i8);
+    check_float_to_int_unchecked!(f32, i16);
+    check_float_to_int_unchecked!(f32, i32);
+    check_float_to_int_unchecked!(f32, i64);
+    check_float_to_int_unchecked!(f32, i128);
+    check_float_to_int_unchecked!(f32, isize);
+}
+
+#[kani::proof]
+fn check_f64_to_int_unchecked() {
+    check_float_to_int_unchecked!(f64, u8);
+    check_float_to_int_unchecked!(f64, u16);
+    check_float_to_int_unchecked!(f64, u32);
+    check_float_to_int_unchecked!(f64, u64);
+    check_float_to_int_unchecked!(f64, u128);
+    check_float_to_int_unchecked!(f64, usize);
+    check_float_to_int_unchecked!(f64, i8);
+    check_float_to_int_unchecked!(f64, i16);
+    check_float_to_int_unchecked!(f64, i32);
+    check_float_to_int_unchecked!(f64, i64);
+    check_float_to_int_unchecked!(f64, i128);
+    check_float_to_int_unchecked!(f64, isize);
+}
diff --git a/tests/kani/MemPredicates/same_allocation.rs b/tests/kani/MemPredicates/same_allocation.rs
index 63d59e857ba2..04825c413118 100644
--- a/tests/kani/MemPredicates/same_allocation.rs
+++ b/tests/kani/MemPredicates/same_allocation.rs
@@ -7,6 +7,7 @@ extern crate kani;
 
 use kani::mem::same_allocation;
 use kani::{AllocationStatus, ArbitraryPointer, PointerGenerator};
+use std::any::Any;
 
 #[kani::proof]
 fn check_inbounds() {
@@ -54,3 +55,45 @@ fn check_dyn_alloc() {
     let ArbitraryPointer { ptr: ptr2, .. } = generator2.any_in_bounds::<u8>();
     assert!(!same_allocation(ptr1a, ptr2));
 }
+
+#[kani::proof]
+fn check_same_alloc_dyn_ptr() {
+    let mut generator = PointerGenerator::<100>::new();
+    let ArbitraryPointer { ptr: ptr1, .. } = generator.any_in_bounds::<()>();
+    let ArbitraryPointer { ptr: ptr2, .. } = generator.any_in_bounds::<char>();
+    let dyn_1 = ptr1 as *const dyn Any;
+    let dyn_2 = ptr2 as *const dyn Any;
+    assert!(same_allocation(dyn_1, dyn_2));
+}
+
+#[kani::proof]
+fn check_not_same_alloc_dyn_ptr() {
+    let mut generator1 = PointerGenerator::<100>::new();
+    let mut generator2 = PointerGenerator::<100>::new();
+    let ArbitraryPointer { ptr: ptr1, .. } = generator1.any_in_bounds::<()>();
+    let ArbitraryPointer { ptr: ptr2, .. } = generator2.any_in_bounds::<char>();
+    let dyn_1 = ptr1 as *const dyn Any;
+    let dyn_2 = ptr2 as *const dyn Any;
+    assert!(!same_allocation(dyn_1, dyn_2));
+}
+
+#[kani::proof]
+fn check_same_alloc_slice() {
+    let mut generator = PointerGenerator::<100>::new();
+    let ArbitraryPointer { ptr: ptr1, .. } = generator.any_in_bounds::<[u16; 4]>();
+    let ArbitraryPointer { ptr: ptr2, .. } = generator.any_in_bounds::<[u16; 10]>();
+    let slice_1 = ptr1 as *const [_];
+    let slice_2 = ptr2 as *const [_];
+    assert!(same_allocation(slice_1, slice_2));
+}
+
+#[kani::proof]
+fn check_not_same_alloc_slice() {
+    let mut generator1 = PointerGenerator::<100>::new();
+    let mut generator2 = PointerGenerator::<100>::new();
+    let ArbitraryPointer { ptr: ptr1, .. } = generator1.any_in_bounds::<[u16; 4]>();
+    let ArbitraryPointer { ptr: ptr2, .. } = generator2.any_in_bounds::<[u16; 10]>();
+    let slice_1 = ptr1 as *const [_];
+    let slice_2 = ptr2 as *const [_];
+    assert!(!same_allocation(slice_1, slice_2));
+}
diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic
index 7752afba439f..cb41b35a9bc0 160000
--- a/tests/perf/s2n-quic
+++ b/tests/perf/s2n-quic
@@ -1 +1 @@
-Subproject commit 7752afba439f5692612dbfd96f65bb561da86858
+Subproject commit cb41b35a9bc0412435b70b5038df0681a881e414
diff --git a/tests/script-based-pre/individual_file_output/config.yml b/tests/script-based-pre/individual_file_output/config.yml
new file mode 100644
index 000000000000..932ebf466727
--- /dev/null
+++ b/tests/script-based-pre/individual_file_output/config.yml
@@ -0,0 +1,3 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: individual_file_output.sh
diff --git a/tests/script-based-pre/individual_file_output/individual_file_output.sh b/tests/script-based-pre/individual_file_output/individual_file_output.sh
new file mode 100755
index 000000000000..49d110983527
--- /dev/null
+++ b/tests/script-based-pre/individual_file_output/individual_file_output.sh
@@ -0,0 +1,46 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set +e
+
+OUT_DIR=tmp_sample_crate
+
+# Ensure output folder is clean
+rm -rf ${OUT_DIR}
+
+# Move the original source to the output folder since it will be modified
+cp -r sample_crate ${OUT_DIR}
+pushd $OUT_DIR
+
+echo "Run verification..."
+cargo kani -Z unstable-options --output-into-files
+
+OUTPUT_DIR="result_output_dir" 
+
+# Check if the output directory exists
+if [ ! -d "$OUTPUT_DIR" ]; then
+    echo "Output directory $OUT_DIR/$OUTPUT_DIR does not exist. Verification failed."
+    exit 1
+fi
+
+# Check if there are any files in the output directory
+output_files=("$OUTPUT_DIR"/*)
+
+if [ ${#output_files[@]} -eq 0 ]; then
+    echo "No files found in the output directory. Verification failed."
+    exit 1
+fi
+
+# Check if each file contains text
+for file in "${output_files[@]}"; do
+    if [ ! -s "$file" ]; then
+        echo "File $file is empty. Verification failed."
+        exit 1
+    else
+        echo "File $file is present and contains text."
+    fi
+done
+
+popd
+rm -rf ${OUT_DIR}
diff --git a/tests/script-based-pre/individual_file_output/sample_crate/Cargo.toml b/tests/script-based-pre/individual_file_output/sample_crate/Cargo.toml
new file mode 100644
index 000000000000..39cfab289878
--- /dev/null
+++ b/tests/script-based-pre/individual_file_output/sample_crate/Cargo.toml
@@ -0,0 +1,15 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "sample_crate"
+version = "0.1.0"
+edition = "2021"
+
+[package.metadata.kani.flags]
+concrete-playback = "inplace"
+
+[package.metadata.kani.unstable]
+concrete-playback = true
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }
diff --git a/tests/script-based-pre/individual_file_output/sample_crate/src/lib.rs b/tests/script-based-pre/individual_file_output/sample_crate/src/lib.rs
new file mode 100644
index 000000000000..3cf83c8e3597
--- /dev/null
+++ b/tests/script-based-pre/individual_file_output/sample_crate/src/lib.rs
@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks that we can correctly generate tests from a cover statement and run them.
+
+#[cfg(kani)]
+mod verify {
+    #[kani::proof]
+    fn any_is_ok() {
+        let result: Result<char, bool> = kani::any();
+        kani::cover!(result.is_ok());
+    }
+
+    #[kani::proof]
+    fn any_is_err() {
+        let result: Result<char, bool> = kani::any();
+        kani::cover!(result.is_err());
+    }
+}
diff --git a/tests/ui/check_deprecated/deprecated_warning.expected b/tests/ui/check_deprecated/deprecated_warning.expected
deleted file mode 100644
index 3a0760035f8b..000000000000
--- a/tests/ui/check_deprecated/deprecated_warning.expected
+++ /dev/null
@@ -1 +0,0 @@
-warning: use of deprecated function `kani::check`: This API will be made private in future releases.
diff --git a/tests/ui/check_deprecated/deprecated_warning.rs b/tests/ui/check_deprecated/deprecated_warning.rs
deleted file mode 100644
index f3d791256081..000000000000
--- a/tests/ui/check_deprecated/deprecated_warning.rs
+++ /dev/null
@@ -1,10 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-//
-// kani-flags: --only-codegen
-
-/// Ensure that Kani prints a deprecation warning if users invoke `kani::check`.
-#[kani::proof]
-fn internal_api() {
-    kani::check(kani::any(), "oops");
-}
diff --git a/tests/ui/derive-arbitrary/non_arbitrary_param/expected b/tests/ui/derive-arbitrary/non_arbitrary_param/expected
index 68e3710d6dcb..194d13aa07c4 100644
--- a/tests/ui/derive-arbitrary/non_arbitrary_param/expected
+++ b/tests/ui/derive-arbitrary/non_arbitrary_param/expected
@@ -1,4 +1,4 @@
 error[E0277]: the trait bound `Void: kani::Arbitrary` is not satisfied
 |\
 |     let _wrapper: Wrapper<Void> = kani::any();\
-|                                   ^^^^^^^^^^^ the trait `kani::Arbitrary` is not implemented for `Void`, which is required by `Wrapper<Void>: kani::Arbitrary`\
+|                                   ^^^^^^^^^^^ the trait `kani::Arbitrary` is not implemented for `Void`
diff --git a/tests/ui/derive-arbitrary/single_variant_enum/expected b/tests/ui/derive-arbitrary/single_variant_enum/expected
new file mode 100644
index 000000000000..35ea4d3a01ba
--- /dev/null
+++ b/tests/ui/derive-arbitrary/single_variant_enum/expected
@@ -0,0 +1,16 @@
+Checking harness check_with_discriminant...
+SUCCESS\
+"assertion failed: disc == 42"
+
+Checking harness check_with_named_args...
+SUCCESS\
+"assertion failed: flag as u8 == 0 || flag as u8 == 1"
+2 of 2 cover properties satisfied
+
+Checking harness check_with_args...
+SUCCESS\
+"assertion failed: c <= char::MAX"
+2 of 2 cover properties satisfied
+
+Checking harness check_simple...
+1 of 1 cover properties satisfied
diff --git a/tests/ui/derive-arbitrary/single_variant_enum/single_variant_enum.rs b/tests/ui/derive-arbitrary/single_variant_enum/single_variant_enum.rs
new file mode 100644
index 000000000000..7f4bb4dc1643
--- /dev/null
+++ b/tests/ui/derive-arbitrary/single_variant_enum/single_variant_enum.rs
@@ -0,0 +1,65 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Check that Kani can automatically derive Arbitrary enums.
+//! An arbitrary enum should always generate a valid arbitrary variant.
+
+extern crate kani;
+use kani::cover;
+
+#[derive(kani::Arbitrary)]
+enum Simple {
+    Empty,
+}
+
+#[kani::proof]
+fn check_simple() {
+    match kani::any::<Simple>() {
+        Simple::Empty => cover!(),
+    }
+}
+
+#[derive(kani::Arbitrary)]
+enum WithArgs {
+    Args(char),
+}
+
+#[kani::proof]
+fn check_with_args() {
+    match kani::any::<WithArgs>() {
+        WithArgs::Args(c) => {
+            assert!(c <= char::MAX);
+            cover!(c == 'a');
+            cover!(c == '1');
+        }
+    }
+}
+
+#[derive(kani::Arbitrary)]
+enum WithNamedArgs {
+    Args { flag: bool },
+}
+
+#[kani::proof]
+fn check_with_named_args() {
+    match kani::any::<WithNamedArgs>() {
+        WithNamedArgs::Args { flag } => {
+            cover!(flag as u8 == 0);
+            cover!(flag as u8 == 1);
+            assert!(flag as u8 == 0 || flag as u8 == 1);
+        }
+    }
+}
+
+#[derive(kani::Arbitrary)]
+enum WithDiscriminant {
+    Disc = 42,
+}
+
+#[kani::proof]
+fn check_with_discriminant() {
+    let v = kani::any::<WithDiscriminant>();
+    let disc = v as i8;
+    match v {
+        WithDiscriminant::Disc => assert!(disc == 42),
+    }
+}
diff --git a/tests/ui/harness-timeout/hours.expected b/tests/ui/harness-timeout/hours.expected
new file mode 100644
index 000000000000..34c886c358cb
--- /dev/null
+++ b/tests/ui/harness-timeout/hours.expected
@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/ui/harness-timeout/hours.rs b/tests/ui/harness-timeout/hours.rs
new file mode 100644
index 000000000000..d003679daae4
--- /dev/null
+++ b/tests/ui/harness-timeout/hours.rs
@@ -0,0 +1,10 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --harness-timeout 24h -Zunstable-options
+//
+// This test checks that Kani accepts a `--harness-timeout` specified in hours
+
+#[kani::proof]
+fn check_harness_timeout_hours() {
+    assert_ne!(42, 17);
+}
diff --git a/tests/ui/harness-timeout/invalid.expected b/tests/ui/harness-timeout/invalid.expected
new file mode 100644
index 000000000000..aa44e32a052d
--- /dev/null
+++ b/tests/ui/harness-timeout/invalid.expected
@@ -0,0 +1 @@
+error: invalid value '5k' for '--harness-timeout <HARNESS_TIMEOUT>': Invalid time unit. Use 's' for seconds, 'm' for minutes, or 'h' for hours
diff --git a/tests/ui/harness-timeout/invalid.rs b/tests/ui/harness-timeout/invalid.rs
new file mode 100644
index 000000000000..4859ff4bc262
--- /dev/null
+++ b/tests/ui/harness-timeout/invalid.rs
@@ -0,0 +1,10 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --harness-timeout 5k -Zunstable-options
+//
+// This test checks the error message when the argument to the `--harness-timeout` option is invalid
+
+#[kani::proof]
+fn check_invalid_harness_timeout() {
+    assert!(true);
+}
diff --git a/tests/ui/harness-timeout/minutes.expected b/tests/ui/harness-timeout/minutes.expected
new file mode 100644
index 000000000000..34c886c358cb
--- /dev/null
+++ b/tests/ui/harness-timeout/minutes.expected
@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/ui/harness-timeout/minutes.rs b/tests/ui/harness-timeout/minutes.rs
new file mode 100644
index 000000000000..4737a1f98a49
--- /dev/null
+++ b/tests/ui/harness-timeout/minutes.rs
@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --harness-timeout 1m -Zunstable-options
+//
+// This test checks that Kani accepts a `--harness-timeout` specified in minutes
+
+#[kani::proof]
+fn check_harness_timeout_minutes() {
+    let s = String::from("Hello, world!");
+    assert_eq!(s.len(), 13);
+}
diff --git a/tests/ui/harness-timeout/no_timeout.expected b/tests/ui/harness-timeout/no_timeout.expected
new file mode 100644
index 000000000000..34c886c358cb
--- /dev/null
+++ b/tests/ui/harness-timeout/no_timeout.expected
@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/ui/harness-timeout/no_timeout.rs b/tests/ui/harness-timeout/no_timeout.rs
new file mode 100644
index 000000000000..493030fe378c
--- /dev/null
+++ b/tests/ui/harness-timeout/no_timeout.rs
@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --harness-timeout 10 -Zunstable-options
+//
+// This test covers the case where a timeout is specified via `--harness-timeout`, but
+// CBMC completes before the timeout is reached
+
+#[kani::proof]
+fn check_harness_no_timeout() {
+    let x: u8 = kani::any();
+    let y: u8 = kani::any();
+    kani::assume(y == 0);
+    assert_eq!(x + y, x);
+}
diff --git a/tests/ui/harness-timeout/timeout.expected b/tests/ui/harness-timeout/timeout.expected
new file mode 100644
index 000000000000..aefd7a340753
--- /dev/null
+++ b/tests/ui/harness-timeout/timeout.expected
@@ -0,0 +1,4 @@
+VERIFICATION:- FAILED
+CBMC timed out. You may want to rerun your proof with a larger timeout or use stubbing to reduce the size of the code the verifier reasons about.
+
+Verification failed for - check_harness_timeout
diff --git a/tests/ui/harness-timeout/timeout.rs b/tests/ui/harness-timeout/timeout.rs
new file mode 100644
index 000000000000..4b63551a79ac
--- /dev/null
+++ b/tests/ui/harness-timeout/timeout.rs
@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --harness-timeout 5 -Zunstable-options
+//
+// Check that Kani respects the specified `--harness-timeout` option
+
+#[kani::proof]
+fn check_harness_timeout() {
+    // construct a problem that requires a long time to solve
+    let (a1, b1, c1): (u64, u64, u64) = kani::any();
+    let (a2, b2, c2): (u64, u64, u64) = kani::any();
+    let p1 = a1.saturating_mul(b1).saturating_mul(c1);
+    let p2 = a2.saturating_mul(b2).saturating_mul(c2);
+    // (a1 == a2 && b1 == b2 && c1 == c2) implies p1 == p2
+    assert!(a1 != a2 || b1 != b2 || c1 != c2 || p1 == p2)
+}
diff --git a/tests/ui/unknown-contract-harness/expected b/tests/ui/unknown-contract-harness/expected
new file mode 100644
index 000000000000..dec02f9b0a50
--- /dev/null
+++ b/tests/ui/unknown-contract-harness/expected
@@ -0,0 +1,6 @@
+error: The function specified in the `proof_for_contract` attribute, `foo`, was not found.\
+Make sure the function is reachable from the harness.
+test.rs:\
+|\
+| #[kani::proof_for_contract(foo)]\
+| ^^^^^^^^^^^^^^
diff --git a/tests/ui/unknown-contract-harness/test.rs b/tests/ui/unknown-contract-harness/test.rs
new file mode 100644
index 000000000000..70c323c144aa
--- /dev/null
+++ b/tests/ui/unknown-contract-harness/test.rs
@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+// This test checks Kani's error when function specified in `proof_for_contract`
+// harness is not found (e.g. because it's not reachable from the harness)
+
+#[kani::requires(true)]
+fn foo() {}
+
+#[kani::proof_for_contract(foo)]
+fn check_foo() {
+    assert!(true);
+}
diff --git a/tools/build-kani/license-notes.txt b/tools/build-kani/license-notes.txt
index 6e717c98012b..04070480ccd0 100644
--- a/tools/build-kani/license-notes.txt
+++ b/tools/build-kani/license-notes.txt
@@ -17,9 +17,6 @@ Acknowledgement:
      Computer Science Department, University of Oxford
      Computer Science Department, Carnegie Mellon University
 
-cbmc-viewer: https://github.com/model-checking/cbmc-viewer
-License: Apache-2.0
-
 ## Notable Python dependencies
 
 voluptuous: https://github.com/alecthomas/voluptuous
diff --git a/tools/build-kani/src/main.rs b/tools/build-kani/src/main.rs
index 7000ddb045a7..c45e9a72b189 100644
--- a/tools/build-kani/src/main.rs
+++ b/tools/build-kani/src/main.rs
@@ -10,7 +10,9 @@
 mod parser;
 mod sysroot;
 
-use crate::sysroot::{build_bin, build_lib, kani_no_core_lib, kani_playback_lib, kani_sysroot_lib};
+use crate::sysroot::{
+    build_bin, build_lib, build_tools, kani_no_core_lib, kani_playback_lib, kani_sysroot_lib,
+};
 use anyhow::{Result, bail};
 use clap::Parser;
 use std::{ffi::OsString, path::Path, process::Command};
@@ -41,7 +43,6 @@ fn main() -> Result<()> {
             bundle_kani(dir)?;
             bundle_cbmc(dir)?;
             bundle_kissat(dir)?;
-            // cbmc-viewer isn't bundled, it's pip install'd on first-time setup
 
             create_release_bundle(dir, &bundle_name)?;
 
@@ -72,6 +73,8 @@ fn prebundle(dir: &Path) -> Result<()> {
         bail!("Couldn't find the 'cbmc' binary to include in the release bundle.");
     }
 
+    build_tools(&["--release"])?;
+
     // Before we begin, ensure Kani is built successfully in release mode.
     // And that libraries have been built too.
     build_lib(&build_bin(&["--release"])?)
@@ -86,6 +89,7 @@ fn bundle_kani(dir: &Path) -> Result<()> {
     let release = Path::new("./target/release");
     cp(&release.join("kani-driver"), &bin)?;
     cp(&release.join("kani-compiler"), &bin)?;
+    cp(&release.join("kani-cov"), &bin)?;
 
     // 2. Kani scripts
     let scripts = dir.join("scripts");
@@ -135,7 +139,6 @@ fn bundle_cbmc(dir: &Path) -> Result<()> {
     cp(&which::which("goto-instrument")?, &bin)?;
     cp(&which::which("goto-cc")?, &bin)?;
     cp(&which::which("symtab2gb")?, &bin)?;
-    // cbmc-viewer invokes this
     cp(&which::which("goto-analyzer")?, &bin)?;
 
     Ok(())
diff --git a/tools/build-kani/src/sysroot.rs b/tools/build-kani/src/sysroot.rs
index edd2a0973a83..29d481e4b9dd 100644
--- a/tools/build-kani/src/sysroot.rs
+++ b/tools/build-kani/src/sysroot.rs
@@ -278,3 +278,17 @@ pub fn build_bin<T: AsRef<OsStr>>(extra_args: &[T]) -> Result<PathBuf> {
         .or(Err(format_err!("Failed to build binaries.")))?;
     Ok(out_dir)
 }
+
+/// Build tool binaries with the extra arguments provided.
+/// At present, the only tool we build for the bundle is `kani-cov`, but this
+/// could include other tools in the future.
+pub fn build_tools<T: AsRef<OsStr>>(extra_args: &[T]) -> Result<()> {
+    let args = ["-p", "kani-cov"];
+    Command::new("cargo")
+        .arg("build")
+        .args(extra_args)
+        .args(args)
+        .run()
+        .or(Err(format_err!("Failed to build tool binaries.")))?;
+    Ok(())
+}