diff --git a/Cargo.lock b/Cargo.lock
index 4dbff37574b..0e45e2914d7 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -49,7 +49,7 @@ dependencies = [
  "prusti-rustc-interface",
  "serde",
  "serde_json",
- "syn",
+ "syn 1.0.109",
  "tracing 0.1.0",
 ]
 
@@ -62,11 +62,51 @@ dependencies = [
  "libc",
 ]
 
+[[package]]
+name = "anstream"
+version = "0.2.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "342258dd14006105c2b75ab1bd7543a03bdf0cfc94383303ac212a04939dff6f"
+dependencies = [
+ "anstyle",
+ "anstyle-parse",
+ "anstyle-wincon",
+ "concolor-override",
+ "concolor-query 0.3.3",
+ "is-terminal",
+ "utf8parse",
+]
+
+[[package]]
+name = "anstyle"
+version = "0.3.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "23ea9e81bd02e310c216d080f6223c179012256e5151c41db88d12c88a1684d2"
+
+[[package]]
+name = "anstyle-parse"
+version = "0.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a7d1bb534e9efed14f3e5f44e7dd1a4f709384023a4165199a4241e18dff0116"
+dependencies = [
+ "utf8parse",
+]
+
+[[package]]
+name = "anstyle-wincon"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c3127af6145b149f3287bb9a0d10ad9c5692dba8c53ad48285e5bec4063834fa"
+dependencies = [
+ "anstyle",
+ "windows-sys 0.45.0",
+]
+
 [[package]]
 name = "anyhow"
-version = "1.0.69"
+version = "1.0.70"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "224afbd727c3d6e4b90103ece64b8d1b67fbb1973b1046c2281eed3f3803f800"
+checksum = "7de8ce5e0f9f8d88245311066a578d72b7af3e7088f32783804676302df237e4"
 
 [[package]]
 name = "async-attributes"
@@ -75,7 +115,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "a3203e79f4dd9bdda415ed03cf14dae5a2bf775c683a00f94e9cd1faf0f596e5"
 dependencies = [
  "quote",
- "syn",
+ "syn 1.0.109",
 ]
 
 [[package]]
@@ -91,9 +131,9 @@ dependencies = [
 
 [[package]]
 name = "async-executor"
-version = "1.5.0"
+version = "1.5.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "17adb73da160dfb475c183343c8cccd80721ea5a605d3eb57125f0a7b7a92d0b"
+checksum = "6fa3dc5f2a8564f07759c008b9109dc0d39de92a88d5588b8a5036d286383afb"
 dependencies = [
  "async-lock",
  "async-task",
@@ -120,22 +160,22 @@ dependencies = [
 
 [[package]]
 name = "async-io"
-version = "1.12.0"
+version = "1.13.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8c374dda1ed3e7d8f0d9ba58715f924862c63eae6849c92d3a18e7fbde9e2794"
+checksum = "0fc5b45d93ef0529756f812ca52e44c221b35341892d3dcc34132ac02f3dd2af"
 dependencies = [
  "async-lock",
  "autocfg",
+ "cfg-if",
  "concurrent-queue",
  "futures-lite",
- "libc",
  "log",
  "parking",
  "polling",
+ "rustix",
  "slab",
  "socket2",
  "waker-fn",
- "windows-sys 0.42.0",
 ]
 
 [[package]]
@@ -149,9 +189,9 @@ dependencies = [
 
 [[package]]
 name = "async-process"
-version = "1.6.0"
+version = "1.7.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6381ead98388605d0d9ff86371043b5aa922a3905824244de40dc263a14fcba4"
+checksum = "7a9d28b1d97e08915212e2e45310d47854eafa69600756fc735fb788f75199c9"
 dependencies = [
  "async-io",
  "async-lock",
@@ -160,9 +200,9 @@ dependencies = [
  "cfg-if",
  "event-listener",
  "futures-lite",
- "libc",
+ "rustix",
  "signal-hook",
- "windows-sys 0.42.0",
+ "windows-sys 0.48.0",
 ]
 
 [[package]]
@@ -195,26 +235,26 @@ dependencies = [
 
 [[package]]
 name = "async-task"
-version = "4.3.0"
+version = "4.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7a40729d2133846d9ed0ea60a8b9541bccddab49cd30f0715a1da672fe9a2524"
+checksum = "ecc7ab41815b3c653ccd2978ec3255c81349336702dfdf62ee6f7069b12a3aae"
 
 [[package]]
 name = "async-trait"
-version = "0.1.66"
+version = "0.1.68"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b84f9ebcc6c1f5b8cb160f6990096a5c127f423fcb6e1ccc46c370cbdfb75dfc"
+checksum = "b9ccdd8f2a161be9bd5c023df56f1b2a0bd1d83872ae53b71a84a12c9bf6e842"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.14",
 ]
 
 [[package]]
 name = "atomic-waker"
-version = "1.1.0"
+version = "1.1.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "debc29dde2e69f9e47506b525f639ed42300fc014a3e007832592448fa8e4599"
+checksum = "1181e1e0d1fce796a03db1ae795d67167da795f9cf4a39c37589e85ef57f26d3"
 
 [[package]]
 name = "attohttpc"
@@ -307,9 +347,9 @@ dependencies = [
 
 [[package]]
 name = "blocking"
-version = "1.3.0"
+version = "1.3.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3c67b173a56acffd6d2326fb7ab938ba0b00a71480e14902b2591c87bc5741e8"
+checksum = "77231a1c8f801696fc0123ec6150ce92cffb8e164a02afb9c8ddee0e9b65ad65"
 dependencies = [
  "async-channel",
  "async-lock",
@@ -317,16 +357,7 @@ dependencies = [
  "atomic-waker",
  "fastrand",
  "futures-lite",
-]
-
-[[package]]
-name = "buf_redux"
-version = "0.8.4"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b953a6887648bb07a535631f2bc00fbdb2a2216f135552cb3f534ed136b9c07f"
-dependencies = [
- "memchr",
- "safemem",
+ "log",
 ]
 
 [[package]]
@@ -431,40 +462,45 @@ dependencies = [
 
 [[package]]
 name = "clap"
-version = "4.1.8"
+version = "4.2.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c3d7ae14b20b94cb02149ed21a86c423859cbe18dc7ed69845cace50e52b40a5"
+checksum = "046ae530c528f252094e4a77886ee1374437744b2bff1497aa898bbddbbb29b3"
 dependencies = [
- "bitflags",
+ "clap_builder",
  "clap_derive",
- "clap_lex",
- "is-terminal",
  "once_cell",
+]
+
+[[package]]
+name = "clap_builder"
+version = "4.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "223163f58c9a40c3b0a43e1c4b50a9ce09f007ea2cb1ec258a687945b4b7929f"
+dependencies = [
+ "anstream",
+ "anstyle",
+ "bitflags",
+ "clap_lex",
  "strsim",
- "termcolor",
 ]
 
 [[package]]
 name = "clap_derive"
-version = "4.1.8"
+version = "4.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "44bec8e5c9d09e439c4335b1af0abaab56dcf3b94999a936e1bb47b9134288f0"
+checksum = "3f9644cd56d6b87dbe899ef8b053e331c0637664e9e21a33dfcdc36093f5c5c4"
 dependencies = [
  "heck",
- "proc-macro-error",
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.14",
 ]
 
 [[package]]
 name = "clap_lex"
-version = "0.3.2"
+version = "0.4.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "350b9cf31731f9957399229e9b2adc51eeabdfbe9d71d9a0552275fd12710d09"
-dependencies = [
- "os_str_bytes",
-]
+checksum = "8a2dd5a6fe8c6e3502f568a6353e5273bbb15193ad9a89e457b9970798efbea1"
 
 [[package]]
 name = "codespan-reporting"
@@ -545,20 +581,35 @@ checksum = "015267563b1df20adccdd00cb05257b1dfbea70a04928e9cf88ffb850c1a40af"
 dependencies = [
  "atty",
  "bitflags",
- "concolor-query",
+ "concolor-query 0.0.5",
 ]
 
+[[package]]
+name = "concolor-override"
+version = "1.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a855d4a1978dc52fb0536a04d384c2c0c1aa273597f08b77c8c4d3b2eec6037f"
+
 [[package]]
 name = "concolor-query"
 version = "0.0.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "d6417fe6fc03a8b533fd2177742eeb39a90c7233eedec7bac96d4d6b69a09449"
 
+[[package]]
+name = "concolor-query"
+version = "0.3.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "88d11d52c3d7ca2e6d0040212be9e4dbbcd78b6447f535b6b561f449427944cf"
+dependencies = [
+ "windows-sys 0.45.0",
+]
+
 [[package]]
 name = "concurrent-queue"
-version = "2.1.0"
+version = "2.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c278839b831783b70278b14df4d45e1beb1aad306c07bb796637de9a0e323e8e"
+checksum = "62ec6771ecfa0762d24683ee5a32ad78487a3d3afdc0fb8cae19d2c5deb50b7c"
 dependencies = [
  "crossbeam-utils",
 ]
@@ -609,15 +660,15 @@ dependencies = [
 
 [[package]]
 name = "core-foundation-sys"
-version = "0.8.3"
+version = "0.8.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5827cebf4670468b8772dd191856768aedcb1b0278a04f989f7766351917b9dc"
+checksum = "e496a50fda8aacccc86d7529e2c1e0892dbd0f898a6b5645b5561b89c3210efa"
 
 [[package]]
 name = "cpufeatures"
-version = "0.2.5"
+version = "0.2.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "28d997bd5e24a5928dd43e46dc529867e207907fe0b239c3477d924f7f2ca320"
+checksum = "280a9f2d8b3a38871a3c8a46fb80db65e5e5ed97da80c4d08bf27fb63e35e181"
 dependencies = [
  "libc",
 ]
@@ -633,9 +684,9 @@ dependencies = [
 
 [[package]]
 name = "crossbeam-channel"
-version = "0.5.7"
+version = "0.5.8"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "cf2b3e8478797446514c91ef04bafcb59faba183e621ad488df88983cc14128c"
+checksum = "a33c2bf77f2df06183c3aa30d1e96c0695a313d4f9c453cc3762a6db39f99200"
 dependencies = [
  "cfg-if",
  "crossbeam-utils",
@@ -724,7 +775,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "6d2301688392eb071b0bf1a37be05c469d3cc4dbbd95df672fe28ab021e6a096"
 dependencies = [
  "quote",
- "syn",
+ "syn 1.0.109",
 ]
 
 [[package]]
@@ -739,9 +790,9 @@ dependencies = [
 
 [[package]]
 name = "cxx"
-version = "1.0.92"
+version = "1.0.94"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9a140f260e6f3f79013b8bfc65e7ce630c9ab4388c6a89c71e07226f49487b72"
+checksum = "f61f1b6389c3fe1c316bf8a4dccc90a38208354b330925bce1f74a6c4756eb93"
 dependencies = [
  "cc",
  "cxxbridge-flags",
@@ -751,9 +802,9 @@ dependencies = [
 
 [[package]]
 name = "cxx-build"
-version = "1.0.92"
+version = "1.0.94"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "da6383f459341ea689374bf0a42979739dc421874f112ff26f829b8040b8e613"
+checksum = "12cee708e8962df2aeb38f594aae5d827c022b6460ac71a7a3e2c3c2aae5a07b"
 dependencies = [
  "cc",
  "codespan-reporting",
@@ -761,24 +812,24 @@ dependencies = [
  "proc-macro2",
  "quote",
  "scratch",
- "syn",
+ "syn 2.0.14",
 ]
 
 [[package]]
 name = "cxxbridge-flags"
-version = "1.0.92"
+version = "1.0.94"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "90201c1a650e95ccff1c8c0bb5a343213bdd317c6e600a93075bca2eff54ec97"
+checksum = "7944172ae7e4068c533afbb984114a56c46e9ccddda550499caa222902c7f7bb"
 
 [[package]]
 name = "cxxbridge-macro"
-version = "1.0.92"
+version = "1.0.94"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0b75aed41bb2e6367cae39e6326ef817a851db13c13e4f3263714ca3cfb8de56"
+checksum = "2345488264226bf682893e25de0769f3360aac9957980ec49361b083ddaa5bc5"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.14",
 ]
 
 [[package]]
@@ -795,7 +846,7 @@ checksum = "fcc3dd5e9e9c0b295d6e1e4d811fb6f157d5ffd784b8d202fc62eac8035a770b"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 1.0.109",
 ]
 
 [[package]]
@@ -808,7 +859,7 @@ dependencies = [
  "proc-macro2",
  "quote",
  "rustc_version",
- "syn",
+ "syn 1.0.109",
 ]
 
 [[package]]
@@ -899,13 +950,13 @@ dependencies = [
 
 [[package]]
 name = "errno"
-version = "0.2.8"
+version = "0.3.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f639046355ee4f37944e44f60642c6f3a7efa3cf6b78c78a0d989a8ce6c396a1"
+checksum = "4bcfec3a70f97c962c307b2d2c56e358cf1d00b558d74262b5f929ee8cc7e73a"
 dependencies = [
  "errno-dragonfly",
  "libc",
- "winapi",
+ "windows-sys 0.48.0",
 ]
 
 [[package]]
@@ -952,7 +1003,7 @@ checksum = "aa4da3c766cd7a0db8242e326e9e4e081edd567072893ed320008189715366a4"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 1.0.109",
  "synstructure",
 ]
 
@@ -967,14 +1018,14 @@ dependencies = [
 
 [[package]]
 name = "filetime"
-version = "0.2.20"
+version = "0.2.21"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8a3de6e8d11b22ff9edc6d916f890800597d60f8b2da1caf2955c274638d6412"
+checksum = "5cbc844cecaee9d4443931972e1289c8ff485cb4cc2767cb03ca139ed6885153"
 dependencies = [
  "cfg-if",
  "libc",
- "redox_syscall",
- "windows-sys 0.45.0",
+ "redox_syscall 0.2.16",
+ "windows-sys 0.48.0",
 ]
 
 [[package]]
@@ -1030,9 +1081,9 @@ dependencies = [
 
 [[package]]
 name = "futures"
-version = "0.3.27"
+version = "0.3.28"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "531ac96c6ff5fd7c62263c5e3c67a603af4fcaee2e1a0ae5565ba3a11e69e549"
+checksum = "23342abe12aba583913b2e62f22225ff9c950774065e4bfb61a19cd9770fec40"
 dependencies = [
  "futures-channel",
  "futures-core",
@@ -1045,9 +1096,9 @@ dependencies = [
 
 [[package]]
 name = "futures-channel"
-version = "0.3.27"
+version = "0.3.28"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "164713a5a0dcc3e7b4b1ed7d3b433cabc18025386f9339346e8daf15963cf7ac"
+checksum = "955518d47e09b25bbebc7a18df10b81f0c766eaf4c4f1cccef2fca5f2a4fb5f2"
 dependencies = [
  "futures-core",
  "futures-sink",
@@ -1055,15 +1106,15 @@ dependencies = [
 
 [[package]]
 name = "futures-core"
-version = "0.3.27"
+version = "0.3.28"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "86d7a0c1aa76363dac491de0ee99faf6941128376f1cf96f07db7603b7de69dd"
+checksum = "4bca583b7e26f571124fe5b7561d49cb2868d79116cfa0eefce955557c6fee8c"
 
 [[package]]
 name = "futures-executor"
-version = "0.3.27"
+version = "0.3.28"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1997dd9df74cdac935c76252744c1ed5794fac083242ea4fe77ef3ed60ba0f83"
+checksum = "ccecee823288125bd88b4d7f565c9e58e41858e47ab72e8ea2d64e93624386e0"
 dependencies = [
  "futures-core",
  "futures-task",
@@ -1072,15 +1123,15 @@ dependencies = [
 
 [[package]]
 name = "futures-io"
-version = "0.3.27"
+version = "0.3.28"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "89d422fa3cbe3b40dca574ab087abb5bc98258ea57eea3fd6f1fa7162c778b91"
+checksum = "4fff74096e71ed47f8e023204cfd0aa1289cd54ae5430a9523be060cdb849964"
 
 [[package]]
 name = "futures-lite"
-version = "1.12.0"
+version = "1.13.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7694489acd39452c77daa48516b894c153f192c3578d5a839b62c58099fcbf48"
+checksum = "49a9d51ce47660b1e808d3c990b4709f2f415d928835a17dfd16991515c46bce"
 dependencies = [
  "fastrand",
  "futures-core",
@@ -1093,32 +1144,32 @@ dependencies = [
 
 [[package]]
 name = "futures-macro"
-version = "0.3.27"
+version = "0.3.28"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3eb14ed937631bd8b8b8977f2c198443447a8355b6e3ca599f38c975e5a963b6"
+checksum = "89ca545a94061b6365f2c7355b4b32bd20df3ff95f02da9329b34ccc3bd6ee72"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.14",
 ]
 
 [[package]]
 name = "futures-sink"
-version = "0.3.27"
+version = "0.3.28"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ec93083a4aecafb2a80a885c9de1f0ccae9dbd32c2bb54b0c3a65690e0b8d2f2"
+checksum = "f43be4fe21a13b9781a69afa4985b0f6ee0e1afab2c6f454a8cf30e2b2237b6e"
 
 [[package]]
 name = "futures-task"
-version = "0.3.27"
+version = "0.3.28"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "fd65540d33b37b16542a0438c12e6aeead10d4ac5d05bd3f805b8f35ab592879"
+checksum = "76d3d132be6c0e6aa1534069c705a74a5997a356c0dc2f86a47765e5617c5b65"
 
 [[package]]
 name = "futures-util"
-version = "0.3.27"
+version = "0.3.28"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3ef6b17e481503ec85211fed8f39d1970f128935ca1f814cd32ac4a6842e84ab"
+checksum = "26b01e40b772d54cf6c6d721c1d1abd0647a0106a12ecaa1c186273392a69533"
 dependencies = [
  "futures-channel",
  "futures-core",
@@ -1134,9 +1185,9 @@ dependencies = [
 
 [[package]]
 name = "generic-array"
-version = "0.14.6"
+version = "0.14.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "bff49e947297f3312447abdca79f45f4738097cc82b06e72054d2223f601f1b9"
+checksum = "85649ca51fd72272d7821adaf274ad91c288277713d9c18820d8499a7ff69e9a"
 dependencies = [
  "typenum",
  "version_check",
@@ -1153,9 +1204,9 @@ dependencies = [
 
 [[package]]
 name = "getrandom"
-version = "0.2.8"
+version = "0.2.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c05aeb6a22b8f62540c194aac980f2115af067bfe15a0734d7277a768d396b31"
+checksum = "c85e1d9ab2eadba7e5040d4e09cbd6d072b76a557ad64e797c2cb9d4da21d7e4"
 dependencies = [
  "cfg-if",
  "libc",
@@ -1375,16 +1426,16 @@ dependencies = [
 
 [[package]]
 name = "iana-time-zone"
-version = "0.1.53"
+version = "0.1.56"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "64c122667b287044802d6ce17ee2ddf13207ed924c712de9a66a5814d5b64765"
+checksum = "0722cd7114b7de04316e7ea5456a0bbb20e4adb46fd27a3697adb812cff0f37c"
 dependencies = [
  "android_system_properties",
  "core-foundation-sys",
  "iana-time-zone-haiku",
  "js-sys",
  "wasm-bindgen",
- "winapi",
+ "windows",
 ]
 
 [[package]]
@@ -1418,9 +1469,9 @@ dependencies = [
 
 [[package]]
 name = "indexmap"
-version = "1.9.2"
+version = "1.9.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1885e79c1fc4b10f0e172c475f458b7f7b93061064d98c3293e98c5ba0c8b399"
+checksum = "bd070e393353796e801d209ad339e89596eb4c8d430d18ede6a1cced8fafbd99"
 dependencies = [
  "autocfg",
  "hashbrown",
@@ -1437,30 +1488,31 @@ dependencies = [
 
 [[package]]
 name = "io-lifetimes"
-version = "1.0.6"
+version = "1.0.10"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "cfa919a82ea574332e2de6e74b4c36e74d41982b335080fa59d4ef31be20fdf3"
+checksum = "9c66c74d2ae7e79a5a8f7ac924adbe38ee42a859c6539ad869eb51f0b52dc220"
 dependencies = [
+ "hermit-abi 0.3.1",
  "libc",
- "windows-sys 0.45.0",
+ "windows-sys 0.48.0",
 ]
 
 [[package]]
 name = "ipnet"
-version = "2.7.1"
+version = "2.7.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "30e22bd8629359895450b59ea7a776c850561b96a3b1d31321c1949d9e6c9146"
+checksum = "12b6ee2129af8d4fb011108c73d99a1b83a85977f23b82460c0ae2e25bb4b57f"
 
 [[package]]
 name = "is-terminal"
-version = "0.4.4"
+version = "0.4.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "21b6b32576413a8e69b90e952e4a026476040d81017b80445deda5f2d3921857"
+checksum = "adcf93614601c8129ddf72e2d5633df827ba6551541c6d8c59520a371475be1f"
 dependencies = [
  "hermit-abi 0.3.1",
  "io-lifetimes",
  "rustix",
- "windows-sys 0.45.0",
+ "windows-sys 0.48.0",
 ]
 
 [[package]]
@@ -1565,9 +1617,9 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646"
 
 [[package]]
 name = "libc"
-version = "0.2.140"
+version = "0.2.141"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "99227334921fae1a979cf0bfdfcc6b3e5ce376ef57e16fb6fb3ea2ed6095f80c"
+checksum = "3304a64d199bb964be99741b7a14d26972741915b3649639149b2479bb46f4b5"
 
 [[package]]
 name = "libgit2-sys"
@@ -1626,9 +1678,9 @@ checksum = "0717cef1bc8b636c6e1c1bbdefc09e6322da8a9321966e8928ef80d20f7f770f"
 
 [[package]]
 name = "linux-raw-sys"
-version = "0.1.4"
+version = "0.3.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f051f77a7c8e6957c0696eac88f26b0117e54f52d3fc682ab19397a8812846a4"
+checksum = "d59d8c75012853d2e872fb56bc8a2e53718e2cafe1a4c823143141c6d90c322f"
 
 [[package]]
 name = "log"
@@ -1684,9 +1736,9 @@ dependencies = [
 
 [[package]]
 name = "mime"
-version = "0.3.16"
+version = "0.3.17"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2a60c7ce501c71e03a9c9c0d35b861413ae925bd979cc7a4e30d060069aaac8d"
+checksum = "6877bb514081ee2a7ff5ef9de3281f14a4dd4bceac4c09388074a6b5df8a139a"
 
 [[package]]
 name = "mime_guess"
@@ -1735,21 +1787,17 @@ dependencies = [
 ]
 
 [[package]]
-name = "multipart"
-version = "0.18.0"
+name = "multiparty"
+version = "0.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "00dec633863867f29cb39df64a397cdf4a6354708ddd7759f70c7fb51c5f9182"
+checksum = "ed1ec6589a6d4a1e0b33b4c0a3f6ee96dfba88ebdb3da51403fd7cf0a24a4b04"
 dependencies = [
- "buf_redux",
+ "bytes",
+ "futures-core",
  "httparse",
- "log",
- "mime",
- "mime_guess",
- "quick-error",
- "rand",
- "safemem",
- "tempfile",
- "twoway",
+ "memchr",
+ "pin-project-lite",
+ "try-lock",
 ]
 
 [[package]]
@@ -1870,9 +1918,9 @@ checksum = "b7e5500299e16ebb147ae15a00a942af264cf3688f47923b8fc2cd5858f23ad3"
 
 [[package]]
 name = "openssl"
-version = "0.10.45"
+version = "0.10.50"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b102428fd03bc5edf97f62620f7298614c45cedf287c271e7ed450bbaf83f2e1"
+checksum = "7e30d8bc91859781f0a943411186324d580f2bbeb71b452fe91ae344806af3f1"
 dependencies = [
  "bitflags",
  "cfg-if",
@@ -1885,13 +1933,13 @@ dependencies = [
 
 [[package]]
 name = "openssl-macros"
-version = "0.1.0"
+version = "0.1.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b501e44f11665960c7e7fcf062c7d96a14ade4aa98116c004b2e37b5be7d736c"
+checksum = "a948666b637a0f465e8564c73e89d4dde00d72d4d473cc972f390fc3dcee7d9c"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.14",
 ]
 
 [[package]]
@@ -1902,11 +1950,10 @@ checksum = "ff011a302c396a5197692431fc1948019154afc178baf7d8e37367442a4601cf"
 
 [[package]]
 name = "openssl-sys"
-version = "0.9.80"
+version = "0.9.85"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "23bbbf7854cd45b83958ebe919f0e8e516793727652e27fda10a8384cfc790b7"
+checksum = "0d3d193fb1488ad46ffe3aaabc912cc931d02ee8518fe2959aea8ef52718b0c0"
 dependencies = [
- "autocfg",
  "cc",
  "libc",
  "pkg-config",
@@ -1923,12 +1970,6 @@ dependencies = [
  "hashbrown",
 ]
 
-[[package]]
-name = "os_str_bytes"
-version = "6.4.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9b7820b9daea5457c9f21c69448905d723fbd21136ccf521748f23fd49e723ee"
-
 [[package]]
 name = "overload"
 version = "0.1.1"
@@ -1937,9 +1978,9 @@ checksum = "b15813163c1d831bf4a13c3610c05c0d03b39feb07f7e09fa234dac9b15aaf39"
 
 [[package]]
 name = "parking"
-version = "2.0.0"
+version = "2.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "427c3892f9e783d91cc128285287e70a59e206ca452770ece88a76f7a3eddd72"
+checksum = "14f2252c834a40ed9bb5422029649578e63aa341ac401f74e719dd1afda8394e"
 
 [[package]]
 name = "pathdiff"
@@ -1955,9 +1996,9 @@ checksum = "478c572c3d73181ff3c2539045f6eb99e5491218eae919370993b890cdbdd98e"
 
 [[package]]
 name = "pest"
-version = "2.5.6"
+version = "2.5.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8cbd939b234e95d72bc393d51788aec68aeeb5d51e748ca08ff3aad58cb722f7"
+checksum = "7b1403e8401ad5dedea73c626b99758535b342502f8d1e361f4a2dd952749122"
 dependencies = [
  "thiserror",
  "ucd-trie",
@@ -1965,9 +2006,9 @@ dependencies = [
 
 [[package]]
 name = "pest_derive"
-version = "2.5.6"
+version = "2.5.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a81186863f3d0a27340815be8f2078dd8050b14cd71913db9fbda795e5f707d7"
+checksum = "be99c4c1d2fc2769b1d00239431d711d08f6efedcecb8b6e30707160aee99c15"
 dependencies = [
  "pest",
  "pest_generator",
@@ -1975,22 +2016,22 @@ dependencies = [
 
 [[package]]
 name = "pest_generator"
-version = "2.5.6"
+version = "2.5.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "75a1ef20bf3193c15ac345acb32e26b3dc3223aff4d77ae4fc5359567683796b"
+checksum = "e56094789873daa36164de2e822b3888c6ae4b4f9da555a1103587658c805b1e"
 dependencies = [
  "pest",
  "pest_meta",
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.14",
 ]
 
 [[package]]
 name = "pest_meta"
-version = "2.5.6"
+version = "2.5.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5e3b284b1f13a20dc5ebc90aff59a51b8d7137c221131b52a7260c08cbc1cc80"
+checksum = "6733073c7cff3d8459fda0e42f13a047870242aed8b509fe98000928975f359e"
 dependencies = [
  "once_cell",
  "pest",
@@ -2014,7 +2055,7 @@ checksum = "069bdb1e05adc7a8990dce9cc75370895fbe4e3d58b9b73bf1aee56359344a55"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 1.0.109",
 ]
 
 [[package]]
@@ -2037,9 +2078,9 @@ checksum = "6ac9a59f73473f1b8d852421e59e64809f025994837ef743615c6d0c5b305160"
 
 [[package]]
 name = "polling"
-version = "2.6.0"
+version = "2.7.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7e1f879b2998099c2d69ab9605d145d5b661195627eccc680002c4918a7fb6fa"
+checksum = "4be1c66a6add46bff50935c313dae30a5030cf8385c5206e8a95e9e9def974aa"
 dependencies = [
  "autocfg",
  "bitflags",
@@ -2048,7 +2089,7 @@ dependencies = [
  "libc",
  "log",
  "pin-project-lite",
- "windows-sys 0.45.0",
+ "windows-sys 0.48.0",
 ]
 
 [[package]]
@@ -2057,44 +2098,20 @@ version = "0.2.17"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "5b40af805b3121feab8a3c29f04d8ad262fa8e0561883e7653e024ae4479e6de"
 
-[[package]]
-name = "proc-macro-error"
-version = "1.0.4"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c"
-dependencies = [
- "proc-macro-error-attr",
- "proc-macro2",
- "quote",
- "syn",
- "version_check",
-]
-
-[[package]]
-name = "proc-macro-error-attr"
-version = "1.0.4"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869"
-dependencies = [
- "proc-macro2",
- "quote",
- "version_check",
-]
-
 [[package]]
 name = "proc-macro-tracing"
 version = "0.1.0"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 1.0.109",
 ]
 
 [[package]]
 name = "proc-macro2"
-version = "1.0.52"
+version = "1.0.56"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1d0e1ae9e836cc3beddd63db0df682593d7e2d3d891ae8c9083d2113e1744224"
+checksum = "2b63bdb0cd06f1f4dedf69b254734f9b45af66e4a031e42a7480257d9898b435"
 dependencies = [
  "unicode-ident",
 ]
@@ -2214,7 +2231,7 @@ dependencies = [
  "proc-macro2",
  "quote",
  "rustc-hash",
- "syn",
+ "syn 1.0.109",
  "uuid",
 ]
 
@@ -2244,7 +2261,7 @@ dependencies = [
  "nix 0.26.2",
  "rustc-hash",
  "serde",
- "toml 0.7.2",
+ "toml 0.7.3",
  "uuid",
  "walkdir",
  "winapi",
@@ -2275,17 +2292,11 @@ dependencies = [
  "vir",
 ]
 
-[[package]]
-name = "quick-error"
-version = "1.2.3"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a1d01941d82fa2ab50be1e79e6714289dd7cde78eba4c074bc5a4374f650dfe0"
-
 [[package]]
 name = "quote"
-version = "1.0.24"
+version = "1.0.26"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "50686e0021c4136d1d453b2dfe059902278681512a34d4248435dc34b6b5c8ec"
+checksum = "4424af4bf778aae2051a77b60283332f386554255d722233d09fbfc7e30da2fc"
 dependencies = [
  "proc-macro2",
 ]
@@ -2351,6 +2362,15 @@ dependencies = [
  "bitflags",
 ]
 
+[[package]]
+name = "redox_syscall"
+version = "0.3.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "567664f262709473930a4bf9e51bf2ebf3348f2e748ccc50dea20646858f8f29"
+dependencies = [
+ "bitflags",
+]
+
 [[package]]
 name = "redox_users"
 version = "0.4.3"
@@ -2358,15 +2378,15 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "b033d837a7cf162d7993aded9304e30a83213c648b6e389db233191f891e5c2b"
 dependencies = [
  "getrandom",
- "redox_syscall",
+ "redox_syscall 0.2.16",
  "thiserror",
 ]
 
 [[package]]
 name = "regex"
-version = "1.7.1"
+version = "1.7.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "48aaa5748ba571fb95cd2c85c09f629215d3a6ece942baa100950af03a34f733"
+checksum = "8b1f693b24f6ac912f4893ef08244d70b6067480d2f1a46e950c9691e6749d1d"
 dependencies = [
  "aho-corasick",
  "memchr",
@@ -2384,9 +2404,9 @@ dependencies = [
 
 [[package]]
 name = "regex-syntax"
-version = "0.6.28"
+version = "0.6.29"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "456c603be3e8d448b072f410900c09faf164fbce2d480456f50eea6e25f9c848"
+checksum = "f162c6dd7b008981e4d40210aca20b4bd0f9b60ca9271061b07f78537722f2e1"
 
 [[package]]
 name = "remove_dir_all"
@@ -2412,9 +2432,9 @@ dependencies = [
 
 [[package]]
 name = "reqwest"
-version = "0.11.14"
+version = "0.11.16"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "21eed90ec8570952d53b772ecf8f206aa1ec9a3d76b2521c56c42973f2d91ee9"
+checksum = "27b71749df584b7f4cac2c426c127a7c785a5106cc98f7a8feb044115f0fa254"
 dependencies = [
  "base64 0.21.0",
  "bytes",
@@ -2434,7 +2454,7 @@ dependencies = [
  "percent-encoding",
  "pin-project-lite",
  "rustls",
- "rustls-pemfile 1.0.2",
+ "rustls-pemfile",
  "serde",
  "serde_json",
  "serde_urlencoded",
@@ -2487,9 +2507,9 @@ dependencies = [
 
 [[package]]
 name = "rustc-demangle"
-version = "0.1.21"
+version = "0.1.22"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7ef03e0a2b150c7a90d01faf6254c9c48a41e95fb2a8c2ac1c6f0d2b9aefc342"
+checksum = "d4a36c42d1873f9a77c53bde094f9664d9891bc604a45b4798fd2c389ed12e5b"
 
 [[package]]
 name = "rustc-hash"
@@ -2520,16 +2540,16 @@ dependencies = [
 
 [[package]]
 name = "rustix"
-version = "0.36.9"
+version = "0.37.11"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "fd5c6ff11fecd55b40746d1995a02f2eb375bf8c00d192d521ee09f42bef37bc"
+checksum = "85597d61f83914ddeba6a47b3b8ffe7365107221c2e557ed94426489fefb5f77"
 dependencies = [
  "bitflags",
  "errno",
  "io-lifetimes",
  "libc",
  "linux-raw-sys",
- "windows-sys 0.45.0",
+ "windows-sys 0.48.0",
 ]
 
 [[package]]
@@ -2544,15 +2564,6 @@ dependencies = [
  "webpki",
 ]
 
-[[package]]
-name = "rustls-pemfile"
-version = "0.2.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5eebeaeb360c87bfb72e84abdb3447159c0eaececf1bef2aecd65a8be949d1c9"
-dependencies = [
- "base64 0.13.1",
-]
-
 [[package]]
 name = "rustls-pemfile"
 version = "1.0.2"
@@ -2607,12 +2618,6 @@ version = "1.0.13"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "f91339c0467de62360649f8d3e185ca8de4224ff281f66000de5eb2a77a79041"
 
-[[package]]
-name = "safemem"
-version = "0.3.3"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ef703b7cb59335eae2eb93ceb664c0eb7ea6bf567079d843e09420219668e072"
-
 [[package]]
 name = "same-file"
 version = "1.0.6"
@@ -2690,29 +2695,29 @@ checksum = "bebd363326d05ec3e2f532ab7660680f3b02130d780c299bca73469d521bc0ed"
 
 [[package]]
 name = "serde"
-version = "1.0.155"
+version = "1.0.160"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "71f2b4817415c6d4210bfe1c7bfcf4801b2d904cb4d0e1a8fdb651013c9e86b8"
+checksum = "bb2f3770c8bce3bcda7e149193a069a0f4365bda1fa5cd88e03bca26afc1216c"
 dependencies = [
  "serde_derive",
 ]
 
 [[package]]
 name = "serde_derive"
-version = "1.0.155"
+version = "1.0.160"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d071a94a3fac4aff69d023a7f411e33f40f3483f8c5190b1953822b6b76d7630"
+checksum = "291a097c63d8497e00160b166a967a4a79c64f3facdd01cbd7502231688d77df"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.14",
 ]
 
 [[package]]
 name = "serde_json"
-version = "1.0.94"
+version = "1.0.95"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1c533a59c9d8a93a09c6ab31f0fd5e5f4dd1b8fc9434804029839884765d04ea"
+checksum = "d721eca97ac802aa7777b701877c8004d950fc142651367300d21c1cc0194744"
 dependencies = [
  "itoa",
  "ryu",
@@ -2740,17 +2745,6 @@ dependencies = [
  "serde",
 ]
 
-[[package]]
-name = "sha-1"
-version = "0.10.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f5058ada175748e33390e40e872bd0fe59a19f265d0158daa551c5a88a76009c"
-dependencies = [
- "cfg-if",
- "cpufeatures",
- "digest",
-]
-
 [[package]]
 name = "sha1"
 version = "0.10.5"
@@ -2899,6 +2893,17 @@ dependencies = [
  "unicode-ident",
 ]
 
+[[package]]
+name = "syn"
+version = "2.0.14"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "fcf316d5356ed6847742d036f8a39c3b8435cac10bd528a4bd461928a6ab34d5"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
 [[package]]
 name = "synstructure"
 version = "0.12.6"
@@ -2907,7 +2912,7 @@ checksum = "f36bdaa60a83aca3921b5259d5400cbf5e90fc51931376a9bd4a0eb79aa7210f"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 1.0.109",
  "unicode-xid",
 ]
 
@@ -2937,15 +2942,15 @@ dependencies = [
 
 [[package]]
 name = "tempfile"
-version = "3.4.0"
+version = "3.5.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "af18f7ae1acd354b992402e9ec5864359d693cd8a79dcbef59f76891701c1e95"
+checksum = "b9fbec84f381d5795b08656e4912bec604d162bff9291d6189a78f4c8ab87998"
 dependencies = [
  "cfg-if",
  "fastrand",
- "redox_syscall",
+ "redox_syscall 0.3.5",
  "rustix",
- "windows-sys 0.42.0",
+ "windows-sys 0.45.0",
 ]
 
 [[package]]
@@ -2983,7 +2988,7 @@ dependencies = [
  "prusti-launch",
  "rustwide",
  "serde",
- "toml 0.7.2",
+ "toml 0.7.3",
 ]
 
 [[package]]
@@ -3001,22 +3006,22 @@ dependencies = [
 
 [[package]]
 name = "thiserror"
-version = "1.0.39"
+version = "1.0.40"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a5ab016db510546d856297882807df8da66a16fb8c4101cb8b30054b0d5b2d9c"
+checksum = "978c9a314bd8dc99be594bc3c175faaa9794be04a5a5e153caba6915336cebac"
 dependencies = [
  "thiserror-impl",
 ]
 
 [[package]]
 name = "thiserror-impl"
-version = "1.0.39"
+version = "1.0.40"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5420d42e90af0c38c3290abcca25b9b3bdf379fc9f55c528f53a269d9c9a267e"
+checksum = "f9456a42c5b0d803c8cd86e73dd7cc9edd429499f37a3550d286d5e86720569f"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.14",
 ]
 
 [[package]]
@@ -3046,14 +3051,13 @@ checksum = "1f3ccbac311fea05f86f61904b462b55fb3df8837a366dfc601a0161d0532f20"
 
 [[package]]
 name = "tokio"
-version = "1.26.0"
+version = "1.27.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "03201d01c3c27a29c8a5cee5b55a93ddae1ccf6f08f65365c2c918f8c1b76f64"
+checksum = "d0de47a4eecbe11f498978a9b29d792f0d2692d1dd003650c24c76510e3bc001"
 dependencies = [
  "autocfg",
  "bytes",
  "libc",
- "memchr",
  "mio",
  "num_cpus",
  "pin-project-lite",
@@ -3086,9 +3090,9 @@ dependencies = [
 
 [[package]]
 name = "tokio-tungstenite"
-version = "0.17.2"
+version = "0.18.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f714dd15bead90401d77e04243611caec13726c2408afd5b31901dfcdcb3b181"
+checksum = "54319c93411147bced34cb5609a80e0a8e44c5999c93903a81cd866630ec0bfd"
 dependencies = [
  "futures-util",
  "log",
@@ -3121,14 +3125,14 @@ dependencies = [
 
 [[package]]
 name = "toml"
-version = "0.7.2"
+version = "0.7.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f7afcae9e3f0fe2c370fd4657108972cbb2fa9db1b9f84849cefd80741b01cb6"
+checksum = "b403acf6f2bb0859c93c7f0d967cb4a75a7ac552100f9322faf64dc047669b21"
 dependencies = [
  "serde",
  "serde_spanned",
  "toml_datetime",
- "toml_edit 0.19.5",
+ "toml_edit 0.19.8",
 ]
 
 [[package]]
@@ -3155,9 +3159,9 @@ dependencies = [
 
 [[package]]
 name = "toml_edit"
-version = "0.19.5"
+version = "0.19.8"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7082a95d48029677a28f181e5f6422d0c8339ad8396a39d3f33d62a90c1f6c30"
+checksum = "239410c8609e8125456927e6707163a3b1fdb40561e4b803bc041f466ccfdc13"
 dependencies = [
  "indexmap",
  "serde",
@@ -3201,7 +3205,7 @@ checksum = "4017f8f45139870ca7e672686113917c71c7a6e02d4924eda67186083c03081a"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 1.0.109",
 ]
 
 [[package]]
@@ -3262,9 +3266,9 @@ checksum = "3528ecfd12c466c6f163363caf2d02a71161dd5e1cc6ae7b34207ea2d42d81ed"
 
 [[package]]
 name = "tungstenite"
-version = "0.17.3"
+version = "0.18.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e27992fd6a8c29ee7eef28fc78349aa244134e10ad447ce3b9f0ac0ed0fa4ce0"
+checksum = "30ee6ab729cd4cf0fd55218530c4522ed30b7b6081752839b68fcec8d0960788"
 dependencies = [
  "base64 0.13.1",
  "byteorder",
@@ -3273,21 +3277,12 @@ dependencies = [
  "httparse",
  "log",
  "rand",
- "sha-1",
+ "sha1",
  "thiserror",
  "url",
  "utf-8",
 ]
 
-[[package]]
-name = "twoway"
-version = "0.1.8"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "59b11b2b5241ba34be09c3cc85a36e56e48f9888862e19cedf23336d35316ed1"
-dependencies = [
- "memchr",
-]
-
 [[package]]
 name = "typenum"
 version = "1.16.0"
@@ -3311,9 +3306,9 @@ dependencies = [
 
 [[package]]
 name = "unicode-bidi"
-version = "0.3.11"
+version = "0.3.13"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "524b68aca1d05e03fdf03fcdce2c6c94b6daf6d16861ddaa7e4f2b6638a9052c"
+checksum = "92888ba5573ff080736b3648696b70cafad7d250551175acbaa4e0385b3e1460"
 
 [[package]]
 name = "unicode-ident"
@@ -3381,11 +3376,17 @@ version = "0.7.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "09cc8ee72d2a9becf2f2febe0205bbed8fc6615b7cb429ad062dc7b7ddd036a9"
 
+[[package]]
+name = "utf8parse"
+version = "0.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "711b9620af191e0cdc7468a8d14e709c3dcdb115b36f838e601583af800a370a"
+
 [[package]]
 name = "uuid"
-version = "1.3.0"
+version = "1.3.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1674845326ee10d37ca60470760d4288a6f80f304007d92e5c53bab78c9cfd79"
+checksum = "5b55a3fef2a1e3b3a00ce878640918820d3c51081576ac657d23af9fc7928fdb"
 dependencies = [
  "getrandom",
 ]
@@ -3474,7 +3475,7 @@ dependencies = [
  "regex",
  "rustc-hash",
  "serde",
- "syn",
+ "syn 1.0.109",
  "thiserror",
  "tracing 0.1.0",
  "uuid",
@@ -3489,7 +3490,7 @@ dependencies = [
  "proc-macro2",
  "quote",
  "rustc-hash",
- "syn",
+ "syn 1.0.109",
  "tempfile",
 ]
 
@@ -3501,12 +3502,11 @@ checksum = "9d5b2c62b4012a3e1eca5a7e077d13b3bf498c4073e33ccd58626607748ceeca"
 
 [[package]]
 name = "walkdir"
-version = "2.3.2"
+version = "2.3.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "808cf2735cd4b6866113f648b791c6adc5714537bc222d9347bb203386ffda56"
+checksum = "36df944cda56c7d8d8b7496af378e6b16de9284591917d307c9b4d313c44e698"
 dependencies = [
  "same-file",
- "winapi",
  "winapi-util",
 ]
 
@@ -3522,9 +3522,9 @@ dependencies = [
 
 [[package]]
 name = "warp"
-version = "0.3.3"
+version = "0.3.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ed7b8be92646fc3d18b06147664ebc5f48d222686cb11a8755e561a735aacc6d"
+checksum = "27e1a710288f0f91a98dd8a74f05b76a10768db245ce183edf64dc1afdc3016c"
 dependencies = [
  "bytes",
  "futures-channel",
@@ -3535,10 +3535,10 @@ dependencies = [
  "log",
  "mime",
  "mime_guess",
- "multipart",
+ "multiparty",
  "percent-encoding",
  "pin-project",
- "rustls-pemfile 0.2.1",
+ "rustls-pemfile",
  "scoped-tls",
  "serde",
  "serde_json",
@@ -3578,7 +3578,7 @@ dependencies = [
  "once_cell",
  "proc-macro2",
  "quote",
- "syn",
+ "syn 1.0.109",
  "wasm-bindgen-shared",
 ]
 
@@ -3612,7 +3612,7 @@ checksum = "2aff81306fcac3c7515ad4e177f521b5c9a15f2b08f4e32d823066102f35a5f6"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 1.0.109",
  "wasm-bindgen-backend",
  "wasm-bindgen-shared",
 ]
@@ -3689,6 +3689,15 @@ version = "0.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f"
 
+[[package]]
+name = "windows"
+version = "0.48.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e686886bc078bc1b0b600cac0147aadb815089b6e4da64016cbd754b6342700f"
+dependencies = [
+ "windows-targets 0.48.0",
+]
+
 [[package]]
 name = "windows-sys"
 version = "0.36.1"
@@ -3708,13 +3717,13 @@ version = "0.42.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "5a3e1820f08b8513f676f7ab6c1f99ff312fb97b553d30ff4dd86f9f15728aa7"
 dependencies = [
- "windows_aarch64_gnullvm",
- "windows_aarch64_msvc 0.42.1",
- "windows_i686_gnu 0.42.1",
- "windows_i686_msvc 0.42.1",
- "windows_x86_64_gnu 0.42.1",
- "windows_x86_64_gnullvm",
- "windows_x86_64_msvc 0.42.1",
+ "windows_aarch64_gnullvm 0.42.2",
+ "windows_aarch64_msvc 0.42.2",
+ "windows_i686_gnu 0.42.2",
+ "windows_i686_msvc 0.42.2",
+ "windows_x86_64_gnu 0.42.2",
+ "windows_x86_64_gnullvm 0.42.2",
+ "windows_x86_64_msvc 0.42.2",
 ]
 
 [[package]]
@@ -3723,29 +3732,59 @@ version = "0.45.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "75283be5efb2831d37ea142365f009c02ec203cd29a3ebecbc093d52315b66d0"
 dependencies = [
- "windows-targets",
+ "windows-targets 0.42.2",
+]
+
+[[package]]
+name = "windows-sys"
+version = "0.48.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9"
+dependencies = [
+ "windows-targets 0.48.0",
+]
+
+[[package]]
+name = "windows-targets"
+version = "0.42.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8e5180c00cd44c9b1c88adb3693291f1cd93605ded80c250a75d472756b4d071"
+dependencies = [
+ "windows_aarch64_gnullvm 0.42.2",
+ "windows_aarch64_msvc 0.42.2",
+ "windows_i686_gnu 0.42.2",
+ "windows_i686_msvc 0.42.2",
+ "windows_x86_64_gnu 0.42.2",
+ "windows_x86_64_gnullvm 0.42.2",
+ "windows_x86_64_msvc 0.42.2",
 ]
 
 [[package]]
 name = "windows-targets"
-version = "0.42.1"
+version = "0.48.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8e2522491fbfcd58cc84d47aeb2958948c4b8982e9a2d8a2a35bbaed431390e7"
+checksum = "7b1eb6f0cd7c80c79759c929114ef071b87354ce476d9d94271031c0497adfd5"
 dependencies = [
- "windows_aarch64_gnullvm",
- "windows_aarch64_msvc 0.42.1",
- "windows_i686_gnu 0.42.1",
- "windows_i686_msvc 0.42.1",
- "windows_x86_64_gnu 0.42.1",
- "windows_x86_64_gnullvm",
- "windows_x86_64_msvc 0.42.1",
+ "windows_aarch64_gnullvm 0.48.0",
+ "windows_aarch64_msvc 0.48.0",
+ "windows_i686_gnu 0.48.0",
+ "windows_i686_msvc 0.48.0",
+ "windows_x86_64_gnu 0.48.0",
+ "windows_x86_64_gnullvm 0.48.0",
+ "windows_x86_64_msvc 0.48.0",
 ]
 
 [[package]]
 name = "windows_aarch64_gnullvm"
-version = "0.42.1"
+version = "0.42.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8c9864e83243fdec7fc9c5444389dcbbfd258f745e7853198f365e3c4968a608"
+checksum = "597a5118570b68bc08d8d59125332c54f1ba9d9adeedeef5b99b02ba2b0698f8"
+
+[[package]]
+name = "windows_aarch64_gnullvm"
+version = "0.48.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "91ae572e1b79dba883e0d315474df7305d12f569b400fcf90581b06062f7e1bc"
 
 [[package]]
 name = "windows_aarch64_msvc"
@@ -3755,9 +3794,15 @@ checksum = "9bb8c3fd39ade2d67e9874ac4f3db21f0d710bee00fe7cab16949ec184eeaa47"
 
 [[package]]
 name = "windows_aarch64_msvc"
-version = "0.42.1"
+version = "0.42.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e08e8864a60f06ef0d0ff4ba04124db8b0fb3be5776a5cd47641e942e58c4d43"
+
+[[package]]
+name = "windows_aarch64_msvc"
+version = "0.48.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4c8b1b673ffc16c47a9ff48570a9d85e25d265735c503681332589af6253c6c7"
+checksum = "b2ef27e0d7bdfcfc7b868b317c1d32c641a6fe4629c171b8928c7b08d98d7cf3"
 
 [[package]]
 name = "windows_i686_gnu"
@@ -3767,9 +3812,15 @@ checksum = "180e6ccf01daf4c426b846dfc66db1fc518f074baa793aa7d9b9aaeffad6a3b6"
 
 [[package]]
 name = "windows_i686_gnu"
-version = "0.42.1"
+version = "0.42.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "de3887528ad530ba7bdbb1faa8275ec7a1155a45ffa57c37993960277145d640"
+checksum = "c61d927d8da41da96a81f029489353e68739737d3beca43145c8afec9a31a84f"
+
+[[package]]
+name = "windows_i686_gnu"
+version = "0.48.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "622a1962a7db830d6fd0a69683c80a18fda201879f0f447f065a3b7467daa241"
 
 [[package]]
 name = "windows_i686_msvc"
@@ -3779,9 +3830,15 @@ checksum = "e2e7917148b2812d1eeafaeb22a97e4813dfa60a3f8f78ebe204bcc88f12f024"
 
 [[package]]
 name = "windows_i686_msvc"
-version = "0.42.1"
+version = "0.42.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "44d840b6ec649f480a41c8d80f9c65108b92d89345dd94027bfe06ac444d1060"
+
+[[package]]
+name = "windows_i686_msvc"
+version = "0.48.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "bf4d1122317eddd6ff351aa852118a2418ad4214e6613a50e0191f7004372605"
+checksum = "4542c6e364ce21bf45d69fdd2a8e455fa38d316158cfd43b3ac1c5b1b19f8e00"
 
 [[package]]
 name = "windows_x86_64_gnu"
@@ -3791,15 +3848,27 @@ checksum = "4dcd171b8776c41b97521e5da127a2d86ad280114807d0b2ab1e462bc764d9e1"
 
 [[package]]
 name = "windows_x86_64_gnu"
-version = "0.42.1"
+version = "0.42.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8de912b8b8feb55c064867cf047dda097f92d51efad5b491dfb98f6bbb70cb36"
+
+[[package]]
+name = "windows_x86_64_gnu"
+version = "0.48.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c1040f221285e17ebccbc2591ffdc2d44ee1f9186324dd3e84e99ac68d699c45"
+checksum = "ca2b8a661f7628cbd23440e50b05d705db3686f894fc9580820623656af974b1"
 
 [[package]]
 name = "windows_x86_64_gnullvm"
-version = "0.42.1"
+version = "0.42.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "628bfdf232daa22b0d64fdb62b09fcc36bb01f05a3939e20ab73aaf9470d0463"
+checksum = "26d41b46a36d453748aedef1486d5c7a85db22e56aff34643984ea85514e94a3"
+
+[[package]]
+name = "windows_x86_64_gnullvm"
+version = "0.48.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7896dbc1f41e08872e9d5e8f8baa8fdd2677f29468c4e156210174edc7f7b953"
 
 [[package]]
 name = "windows_x86_64_msvc"
@@ -3809,15 +3878,21 @@ checksum = "c811ca4a8c853ef420abd8592ba53ddbbac90410fab6903b3e79972a631f7680"
 
 [[package]]
 name = "windows_x86_64_msvc"
-version = "0.42.1"
+version = "0.42.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "447660ad36a13288b1db4d4248e857b510e8c3a225c822ba4fb748c0aafecffd"
+checksum = "9aec5da331524158c6d1a4ac0ab1541149c0b9505fde06423b02f5ef0106b9f0"
+
+[[package]]
+name = "windows_x86_64_msvc"
+version = "0.48.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1a515f5799fe4961cb532f983ce2b23082366b898e52ffbce459c86f67c8378a"
 
 [[package]]
 name = "winnow"
-version = "0.3.5"
+version = "0.4.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ee7b2c67f962bf5042bfd8b6a916178df33a26eec343ae064cb8e069f638fa6f"
+checksum = "ae8970b36c66498d8ff1d66685dc86b91b29db0c7739899012f63a63814b4b28"
 dependencies = [
  "memchr",
 ]
diff --git a/analysis/src/domains/definitely_accessible/state.rs b/analysis/src/domains/definitely_accessible/state.rs
index a21f2693cef..f27680c876b 100644
--- a/analysis/src/domains/definitely_accessible/state.rs
+++ b/analysis/src/domains/definitely_accessible/state.rs
@@ -10,6 +10,7 @@ use crate::{
 };
 use log::info;
 use prusti_rustc_interface::{
+    abi::FieldIdx,
     data_structures::fx::{FxHashMap, FxHashSet},
     middle::{mir, ty, ty::TyCtxt},
     span::source_map::SourceMap,
@@ -237,7 +238,7 @@ fn pretty_print_place<'tcx>(
 fn describe_field_from_ty(
     tcx: TyCtxt<'_>,
     ty: ty::Ty<'_>,
-    field: mir::Field,
+    field: FieldIdx,
     variant_index: Option<VariantIdx>,
 ) -> Option<String> {
     if ty.is_box() {
@@ -252,7 +253,7 @@ fn describe_field_from_ty(
                 } else {
                     def.non_enum_variant()
                 };
-                Some(variant.fields[field.index()].ident(tcx).to_string())
+                Some(variant.fields[field].ident(tcx).to_string())
             }
             ty::TyKind::Tuple(_) => Some(field.index().to_string()),
             ty::TyKind::Ref(_, ty, _) | ty::TyKind::RawPtr(ty::TypeAndMut { ty, .. }) => {
diff --git a/analysis/src/domains/definitely_initialized/state.rs b/analysis/src/domains/definitely_initialized/state.rs
index 22b4c5b717d..4a1e213c2ef 100644
--- a/analysis/src/domains/definitely_initialized/state.rs
+++ b/analysis/src/domains/definitely_initialized/state.rs
@@ -270,22 +270,6 @@ impl<'mir, 'tcx: 'mir> DefinitelyInitializedState<'mir, 'tcx> {
                     res_vec.push((bb, Self::new_top(self.def_id, self.mir, self.tcx)));
                 }
             }
-            mir::TerminatorKind::DropAndReplace {
-                place,
-                ref value,
-                target,
-                unwind,
-            } => {
-                new_state.set_place_uninitialised(place);
-                new_state.apply_operand_effect(value, move_out_copy_types);
-                new_state.set_place_initialised(place);
-                res_vec.push((target, new_state));
-
-                if let Some(bb) = unwind {
-                    // imprecision for error states
-                    res_vec.push((bb, Self::new_top(self.def_id, self.mir, self.tcx)));
-                }
-            }
             mir::TerminatorKind::Call {
                 ref func,
                 ref args,
diff --git a/analysis/src/mir_utils.rs b/analysis/src/mir_utils.rs
index 119777805fc..f09a891604f 100644
--- a/analysis/src/mir_utils.rs
+++ b/analysis/src/mir_utils.rs
@@ -8,6 +8,7 @@
 //! copied from prusti-interface/utils
 
 use prusti_rustc_interface::{
+    abi::FieldIdx,
     data_structures::fx::FxHashSet,
     infer::infer::TyCtxtInferExt,
     middle::{
@@ -139,7 +140,7 @@ pub fn expand_struct_place<'tcx, P: PlaceImpl<'tcx> + std::marker::Copy>(
                 .unwrap_or_else(|| def.non_enum_variant());
             for (index, field_def) in variant.fields.iter().enumerate() {
                 if Some(index) != without_field {
-                    let field = mir::Field::from_usize(index);
+                    let field = FieldIdx::from_usize(index);
                     let field_place =
                         tcx.mk_place_field(place.to_mir_place(), field, field_def.ty(tcx, substs));
                     places.push(P::from_mir_place(field_place));
@@ -149,7 +150,7 @@ pub fn expand_struct_place<'tcx, P: PlaceImpl<'tcx> + std::marker::Copy>(
         ty::Tuple(slice) => {
             for (index, arg) in slice.iter().enumerate() {
                 if Some(index) != without_field {
-                    let field = mir::Field::from_usize(index);
+                    let field = FieldIdx::from_usize(index);
                     let field_place = tcx.mk_place_field(place.to_mir_place(), field, arg);
                     places.push(P::from_mir_place(field_place));
                 }
@@ -158,7 +159,7 @@ pub fn expand_struct_place<'tcx, P: PlaceImpl<'tcx> + std::marker::Copy>(
         ty::Closure(_, substs) => {
             for (index, subst_ty) in substs.as_closure().upvar_tys().enumerate() {
                 if Some(index) != without_field {
-                    let field = mir::Field::from_usize(index);
+                    let field = FieldIdx::from_usize(index);
                     let field_place = tcx.mk_place_field(place.to_mir_place(), field, subst_ty);
                     places.push(P::from_mir_place(field_place));
                 }
@@ -167,7 +168,7 @@ pub fn expand_struct_place<'tcx, P: PlaceImpl<'tcx> + std::marker::Copy>(
         ty::Generator(_, substs, _) => {
             for (index, subst_ty) in substs.as_generator().upvar_tys().enumerate() {
                 if Some(index) != without_field {
-                    let field = mir::Field::from_usize(index);
+                    let field = FieldIdx::from_usize(index);
                     let field_place = tcx.mk_place_field(place.to_mir_place(), field, subst_ty);
                     places.push(P::from_mir_place(field_place));
                 }
diff --git a/analysis/tests/test_cases/gen_accessibility/create-box.rs b/analysis/tests/test_cases/gen_accessibility/create-box.rs
index d66e6a40b93..3e7e389eabb 100644
--- a/analysis/tests/test_cases/gen_accessibility/create-box.rs
+++ b/analysis/tests/test_cases/gen_accessibility/create-box.rs
@@ -1,5 +1,4 @@
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 fn use_box(v: i32) -> Box<i32> {
     let x = Box::new(v);
@@ -7,6 +6,6 @@ fn use_box(v: i32) -> Box<i32> {
     assert!(v == y);
     let z = Box::new(y);
     assert!(v == *z);
-    let result = box *z;
+    let result = Box::new(*z);
     result
 }
diff --git a/analysis/tests/test_cases/gen_accessibility/deref.rs b/analysis/tests/test_cases/gen_accessibility/deref.rs
index 2753cce0b01..18c03c3af8f 100644
--- a/analysis/tests/test_cases/gen_accessibility/deref.rs
+++ b/analysis/tests/test_cases/gen_accessibility/deref.rs
@@ -1,5 +1,4 @@
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 struct InfiniteList1 {
     next: Box<InfiniteList1>
diff --git a/analysis/tests/test_cases/gen_accessibility/loops/tmp-in-guard.rs b/analysis/tests/test_cases/gen_accessibility/loops/tmp-in-guard.rs
index c1f0cd8523b..f46d252a359 100644
--- a/analysis/tests/test_cases/gen_accessibility/loops/tmp-in-guard.rs
+++ b/analysis/tests/test_cases/gen_accessibility/loops/tmp-in-guard.rs
@@ -1,53 +1,51 @@
-#![feature(box_syntax)]
-
 fn random() -> u32 {
     unimplemented!()
 }
 
 fn test1() {
-    let mut tmp = box box random();
+    let mut tmp = Box::new(Box::new(random()));
     let tmp_ref = &tmp;
     let tmp_ref_mut = &mut tmp;
 
     while {
         let guard = random() < 55;
 
-        let mut tmp = box box random();
+        let mut tmp = Box::new(Box::new(random()));
         let tmp_ref = &tmp;
         let tmp_ref_mut = &mut tmp;
 
         guard
     } {
-        let mut tmp = box box random();
+        let mut tmp = Box::new(Box::new(random()));
         let tmp_ref = &tmp;
         let tmp_ref_mut = &mut tmp;
     }
 
-    let mut tmp = box box random();
+    let mut tmp = Box::new(Box::new(random()));
     let tmp_ref = &tmp;
     let tmp_ref_mut = &mut tmp;
 }
 
 fn test2() {
-    let mut tmp = box box random();
+    let mut tmp = Box::new(Box::new(random()));
     let tmp_ref = &tmp;
     let tmp_ref_mut = &mut tmp;
 
     while {
         let guard = random() < 55;
 
-        let mut tmp = box box random();
+        let mut tmp = Box::new(Box::new(random()));
         let tmp_ref = &tmp;
         let tmp_ref_mut = &mut tmp;
 
         guard
     } {
-        let mut tmp = box box random();
+        let mut tmp = Box::new(Box::new(random()));
         let tmp_ref = &tmp;
         let tmp_ref_mut = &mut tmp;
     }
 
-    let mut tmp = box box random();
+    let mut tmp = Box::new(Box::new(random()));
     let tmp_ref = &tmp;
     let tmp_ref_mut = &mut tmp;
 }
diff --git a/analysis/tests/test_cases/gen_accessibility/predicate-old-expr.rs b/analysis/tests/test_cases/gen_accessibility/predicate-old-expr.rs
index 5ea3476744f..673a5feda48 100644
--- a/analysis/tests/test_cases/gen_accessibility/predicate-old-expr.rs
+++ b/analysis/tests/test_cases/gen_accessibility/predicate-old-expr.rs
@@ -1,5 +1,4 @@
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 use std::borrow::BorrowMut;
 
diff --git a/analysis/tests/test_cases/gen_accessibility/reassignment.rs b/analysis/tests/test_cases/gen_accessibility/reassignment.rs
index 3bf58abb928..c775e177611 100644
--- a/analysis/tests/test_cases/gen_accessibility/reassignment.rs
+++ b/analysis/tests/test_cases/gen_accessibility/reassignment.rs
@@ -1,7 +1,6 @@
 //! Example of reassignment
 
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 struct InfiniteList {
     val: i32,
diff --git a/prusti-common/src/lib.rs b/prusti-common/src/lib.rs
index c97deb01c18..73f8f4dd751 100644
--- a/prusti-common/src/lib.rs
+++ b/prusti-common/src/lib.rs
@@ -5,7 +5,6 @@
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 #![deny(unused_must_use)]
 #![warn(clippy::disallowed_types)]
 
diff --git a/prusti-common/src/vir/optimizations/folding/expressions.rs b/prusti-common/src/vir/optimizations/folding/expressions.rs
index 169a6c01773..40dd44d3cfd 100644
--- a/prusti-common/src/vir/optimizations/folding/expressions.rs
+++ b/prusti-common/src/vir/optimizations/folding/expressions.rs
@@ -111,7 +111,7 @@ impl ExprOptimizer {
 }
 
 fn restore_unfoldings_boxed(unfolding_map: UnfoldingMap, expr: Box<ast::Expr>) -> Box<ast::Expr> {
-    box restore_unfoldings(unfolding_map, *expr)
+    Box::new(restore_unfoldings(unfolding_map, *expr))
 }
 
 /// Restore unfoldings on a given expression.
diff --git a/prusti-common/src/vir/optimizations/functions/simplifier.rs b/prusti-common/src/vir/optimizations/functions/simplifier.rs
index e2406e87059..1edf2e479cb 100644
--- a/prusti-common/src/vir/optimizations/functions/simplifier.rs
+++ b/prusti-common/src/vir/optimizations/functions/simplifier.rs
@@ -63,8 +63,8 @@ impl ExprSimplifier {
                 position: pos,
             }) => ast::Expr::BinOp(ast::BinOp {
                 op_kind: ast::BinaryOpKind::NeCmp,
-                left: box left,
-                right: box right,
+                left: Box::new(left),
+                right: Box::new(right),
                 position: pos,
             }),
             ast::Expr::BinOp(ast::BinOp {
@@ -179,8 +179,8 @@ impl ExprSimplifier {
                 position: pos,
             }) => ast::Expr::BinOp(ast::BinOp {
                 op_kind: ast::BinaryOpKind::And,
-                left: box Self::apply_rules(op1),
-                right: box Self::apply_rules(op2),
+                left: Box::new(Self::apply_rules(op1)),
+                right: Box::new(Self::apply_rules(op2)),
                 position: pos,
             }),
             r => r,
@@ -208,22 +208,22 @@ impl ExprFolder for ExprSimplifier {
         let result = if simplified_then.is_bool() || simplified_else.is_bool() {
             ast::Expr::BinOp(ast::BinOp {
                 op_kind: ast::BinaryOpKind::And,
-                left: box ast::Expr::BinOp(ast::BinOp {
+                left: Box::new(ast::Expr::BinOp(ast::BinOp {
                     op_kind: ast::BinaryOpKind::Implies,
                     left: simplified_guard.clone(),
                     right: simplified_then,
                     position,
-                }),
-                right: box ast::Expr::BinOp(ast::BinOp {
+                })),
+                right: Box::new(ast::Expr::BinOp(ast::BinOp {
                     op_kind: ast::BinaryOpKind::Implies,
-                    left: box ast::Expr::UnaryOp(ast::UnaryOp {
+                    left: Box::new(ast::Expr::UnaryOp(ast::UnaryOp {
                         op_kind: ast::UnaryOpKind::Not,
                         argument: simplified_guard,
                         position,
-                    }),
+                    })),
                     right: simplified_else,
                     position,
-                }),
+                })),
                 position,
             })
         } else {
diff --git a/prusti-common/src/vir/optimizations/methods/quantifier_fixer.rs b/prusti-common/src/vir/optimizations/methods/quantifier_fixer.rs
index 94de255742e..f51630041f2 100644
--- a/prusti-common/src/vir/optimizations/methods/quantifier_fixer.rs
+++ b/prusti-common/src/vir/optimizations/methods/quantifier_fixer.rs
@@ -111,8 +111,8 @@ impl vir::ExprFolder for Optimizer {
             for (expr, variable) in replacer.map.into_iter().sorted_unstable() {
                 forall = vir::Expr::LetExpr(vir::LetExpr {
                     variable,
-                    def: box expr,
-                    body: box forall,
+                    def: Box::new(expr),
+                    body: Box::new(forall),
                     position,
                 });
             }
@@ -335,7 +335,7 @@ impl vir::ExprFolder for UnfoldingExtractor {
             forall = vir::Expr::Unfolding(vir::Unfolding {
                 predicate: typ,
                 arguments: args,
-                base: box forall,
+                base: Box::new(forall),
                 permission: perm_amount,
                 variant,
                 position,
diff --git a/prusti-contracts/prusti-specs/src/lib.rs b/prusti-contracts/prusti-specs/src/lib.rs
index 6f124f4cb01..e2383573575 100644
--- a/prusti-contracts/prusti-specs/src/lib.rs
+++ b/prusti-contracts/prusti-specs/src/lib.rs
@@ -1,7 +1,6 @@
 #![deny(unused_must_use)]
 #![feature(drain_filter)]
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 #![feature(proc_macro_span)]
 #![feature(if_let_guard)]
 #![feature(assert_matches)]
@@ -645,7 +644,11 @@ pub fn trusted(attr: TokenStream, tokens: TokenStream) -> TokenStream {
 
         let item: syn::DeriveInput = handle_result!(syn::parse2(tokens));
         let item_span = item.span();
+
+        // clippy false positive (https://github.com/rust-lang/rust-clippy/issues/10577)
+        #[allow(clippy::redundant_clone)]
         let item_ident = item.ident.clone();
+
         let item_name = syn::Ident::new(
             &format!("prusti_trusted_item_{item_ident}_{spec_id}"),
             item_span,
@@ -714,7 +717,11 @@ pub fn invariant(attr: TokenStream, tokens: TokenStream) -> TokenStream {
 
     let item: syn::DeriveInput = handle_result!(syn::parse2(tokens));
     let item_span = item.span();
+
+    // clippy false positive (https://github.com/rust-lang/rust-clippy/issues/10577)
+    #[allow(clippy::redundant_clone)]
     let item_ident = item.ident.clone();
+
     let item_name = syn::Ident::new(
         &format!("prusti_invariant_item_{item_ident}_{spec_id}"),
         item_span,
@@ -734,7 +741,10 @@ pub fn invariant(attr: TokenStream, tokens: TokenStream) -> TokenStream {
         }
     };
 
+    // clippy false positive (https://github.com/rust-lang/rust-clippy/issues/10577)
+    #[allow(clippy::redundant_clone)]
     let generics = item.generics.clone();
+
     let generics_idents = generics
         .params
         .iter()
diff --git a/prusti-contracts/prusti-specs/src/print_counterexample.rs b/prusti-contracts/prusti-specs/src/print_counterexample.rs
index 6fd85cf7253..d224deedc59 100644
--- a/prusti-contracts/prusti-specs/src/print_counterexample.rs
+++ b/prusti-contracts/prusti-specs/src/print_counterexample.rs
@@ -97,7 +97,11 @@ fn rewrite_internal_struct(
     if !args2.empty_or_trailing() {
         args2.push_punct(<syn::Token![,]>::default());
     }
+
+    // clippy false positive (https://github.com/rust-lang/rust-clippy/issues/10577)
+    #[allow(clippy::redundant_clone)]
     let typ = item_struct.ident.clone();
+
     let spec_item = match item_struct.fields {
         Fields::Named(_) => {
             let spec_item: syn::ItemFn = parse_quote_spanned! {item_span=>
diff --git a/prusti-contracts/prusti-specs/src/specifications/preparser.rs b/prusti-contracts/prusti-specs/src/specifications/preparser.rs
index 8617883a86c..3bfebc60992 100644
--- a/prusti-contracts/prusti-specs/src/specifications/preparser.rs
+++ b/prusti-contracts/prusti-specs/src/specifications/preparser.rs
@@ -174,7 +174,7 @@ impl PrustiTokenStream {
                 (TokenTree::Group(group), _, _, _) => PrustiToken::Group(
                     group.span(),
                     group.delimiter(),
-                    box Self::new(group.stream()),
+                    Box::new(Self::new(group.stream())),
                 ),
                 (token, _, _, _) => PrustiToken::Token(token.clone()),
             });
diff --git a/prusti-interface/src/environment/mir_body/graphviz.rs b/prusti-interface/src/environment/mir_body/graphviz.rs
index 5c595e1f69f..132ef24ae45 100644
--- a/prusti-interface/src/environment/mir_body/graphviz.rs
+++ b/prusti-interface/src/environment/mir_body/graphviz.rs
@@ -185,8 +185,7 @@ fn visit_terminator(graph: &mut Graph, bb: mir::BasicBlock, terminator: &mir::Te
         TerminatorKind::Unreachable => {
             graph.add_exit_edge(bb.to_text(), "unreachable".to_text());
         }
-        TerminatorKind::DropAndReplace { target, unwind, .. }
-        | TerminatorKind::Drop { target, unwind, .. } => {
+        TerminatorKind::Drop { target, unwind, .. } => {
             graph.add_regular_edge(bb.to_text(), target.to_text());
             if let Some(target) = unwind {
                 graph.add_unwind_edge(bb.to_text(), target.to_text());
diff --git a/prusti-interface/src/environment/mir_utils/all_places.rs b/prusti-interface/src/environment/mir_utils/all_places.rs
index 89cfe162953..24daedecbab 100644
--- a/prusti-interface/src/environment/mir_utils/all_places.rs
+++ b/prusti-interface/src/environment/mir_utils/all_places.rs
@@ -1,5 +1,5 @@
 use prusti_rustc_interface::{
-    index::vec::Idx,
+    abi::FieldIdx,
     middle::{mir, ty},
 };
 
@@ -16,7 +16,7 @@ impl<'tcx> AllPlaces<'tcx> for mir::Local {
         let ty = mir.local_decls[self].ty;
         if let ty::TyKind::Tuple(types) = ty.kind() {
             for (i, ty) in types.iter().enumerate() {
-                let field = mir::Field::new(i);
+                let field = FieldIdx::from_usize(i);
                 let place = tcx.mk_place_field(self.into(), field, ty);
                 places.push(place);
             }
diff --git a/prusti-interface/src/environment/mir_utils/real_edges.rs b/prusti-interface/src/environment/mir_utils/real_edges.rs
index ea472668bd7..1be11280e8b 100644
--- a/prusti-interface/src/environment/mir_utils/real_edges.rs
+++ b/prusti-interface/src/environment/mir_utils/real_edges.rs
@@ -58,8 +58,7 @@ fn real_targets(terminator: &mir::Terminator) -> Vec<mir::BasicBlock> {
         | TerminatorKind::GeneratorDrop
         | TerminatorKind::Unreachable => vec![],
 
-        TerminatorKind::DropAndReplace { ref target, .. }
-        | TerminatorKind::Drop { ref target, .. } => vec![*target],
+        TerminatorKind::Drop { ref target, .. } => vec![*target],
 
         TerminatorKind::Call { target, .. } => match target {
             Some(target) => vec![target],
diff --git a/prusti-interface/src/environment/mir_utils/split_aggregate_assignment.rs b/prusti-interface/src/environment/mir_utils/split_aggregate_assignment.rs
index 731003b841d..5a4c8ef8050 100644
--- a/prusti-interface/src/environment/mir_utils/split_aggregate_assignment.rs
+++ b/prusti-interface/src/environment/mir_utils/split_aggregate_assignment.rs
@@ -1,6 +1,6 @@
 use super::{SliceOrArrayRef, TupleItemsForTy};
 use prusti_rustc_interface::{
-    index::vec::Idx,
+    abi::FieldIdx,
     middle::{mir, ty},
 };
 
@@ -53,7 +53,7 @@ impl<'tcx> SplitAggregateAssignment<'tcx> for mir::Statement<'tcx> {
                     .zip(items_ty.into_iter())
                     .enumerate()
                     .map(|(i, (rhs, ty))| {
-                        let field = mir::Field::new(i);
+                        let field = FieldIdx::from_usize(i);
                         let lhs = tcx.mk_place_field(local.into(), field, ty);
                         let rhs = mir::Rvalue::Use(rhs);
                         (lhs, rhs)
@@ -74,7 +74,7 @@ impl<'tcx> SplitAggregateAssignment<'tcx> for mir::Statement<'tcx> {
         atomic_assignments
             .into_iter()
             .map(|(lhs, rhs)| {
-                let kind = mir::StatementKind::Assign(box (lhs, rhs));
+                let kind = mir::StatementKind::Assign(Box::new((lhs, rhs)));
                 mir::Statement { source_info, kind }
             })
             .collect()
diff --git a/prusti-interface/src/lib.rs b/prusti-interface/src/lib.rs
index 34112b46050..0b077ce0921 100644
--- a/prusti-interface/src/lib.rs
+++ b/prusti-interface/src/lib.rs
@@ -10,7 +10,6 @@
 #![deny(unsafe_op_in_unsafe_fn)]
 #![warn(clippy::disallowed_types)]
 #![feature(rustc_private)]
-#![feature(box_syntax)]
 #![feature(box_patterns)]
 #![feature(control_flow_enum)]
 #![feature(min_specialization)]
diff --git a/prusti-interface/src/specs/cross_crate.rs b/prusti-interface/src/specs/cross_crate.rs
index 70aed477300..aa4041a0dae 100644
--- a/prusti-interface/src/specs/cross_crate.rs
+++ b/prusti-interface/src/specs/cross_crate.rs
@@ -1,5 +1,4 @@
 use prusti_rustc_interface::{
-    metadata::creader::CStore,
     serialize::{Decodable, Encodable},
     span::DUMMY_SP,
 };
@@ -48,7 +47,6 @@ impl CrossCrateSpecs {
 
     #[tracing::instrument(level = "debug", skip_all)]
     fn import_specs(env: &mut Environment, def_spec: &mut DefSpecificationMap) {
-        let cstore = CStore::from_tcx(env.tcx());
         // TODO: atm one needs to write `extern crate extern_spec_lib` to import the specs
         // from a crate which is not used in the current crate (e.g. an `#[extern_spec]` only crate)
         // Otherwise the crate doesn't show up in `tcx.crates()`.  Is there some better way
@@ -58,8 +56,8 @@ impl CrossCrateSpecs {
             if let Some(extern_crate) = env.tcx().extern_crate(crate_num.as_def_id()) {
                 if extern_crate.is_direct() {
                     let crate_name = env.tcx().crate_name(*crate_num);
-                    let cs = cstore.crate_source_untracked(*crate_num);
-                    let mut source = cs.paths().next().unwrap().clone();
+                    let crate_source = env.tcx().used_crate_source(*crate_num);
+                    let mut source = crate_source.paths().next().unwrap().clone();
                     source.set_extension("specs");
                     if source.is_file() {
                         if let Err(e) =
diff --git a/prusti-launch/src/bin/cargo-prusti.rs b/prusti-launch/src/bin/cargo-prusti.rs
index 67576a500ad..d3ebce4ea57 100644
--- a/prusti-launch/src/bin/cargo-prusti.rs
+++ b/prusti-launch/src/bin/cargo-prusti.rs
@@ -4,7 +4,6 @@
 // License, v. 2.0. If a copy of the MPL was not distributed with this
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
 #![feature(let_chains)]
-#![feature(option_result_contains)]
 
 use prusti_utils::{config, launch};
 use std::{env, fs, io, path::PathBuf, process::Command};
diff --git a/prusti-rustc-interface/src/lib.rs b/prusti-rustc-interface/src/lib.rs
index 626308e06f3..d8a1415b539 100644
--- a/prusti-rustc-interface/src/lib.rs
+++ b/prusti-rustc-interface/src/lib.rs
@@ -7,6 +7,7 @@
 extern crate rustc_smir;
 
 pub extern crate polonius_engine as polonius_engine;
+pub extern crate rustc_abi as abi;
 pub extern crate rustc_ast as ast;
 pub extern crate rustc_ast_pretty as ast_pretty;
 pub extern crate rustc_attr as attr;
diff --git a/prusti-tests/tests/cargo_verify/failing_crate/output.stderr b/prusti-tests/tests/cargo_verify/failing_crate/output.stderr
index 99481cdb3f1..2a6b4bd199f 100644
--- a/prusti-tests/tests/cargo_verify/failing_crate/output.stderr
+++ b/prusti-tests/tests/cargo_verify/failing_crate/output.stderr
@@ -10,4 +10,4 @@ note: the failing assertion is here
 3 | #[requires(x > 999)]
   |            ^^^^^^^
 
-error: could not compile `failing_crate` due to previous error
+error: could not compile `failing_crate` (bin "failing_crate") due to previous error
diff --git a/prusti-tests/tests/cargo_verify/failing_stable_toolchain/output.stderr b/prusti-tests/tests/cargo_verify/failing_stable_toolchain/output.stderr
index a429ccf5f0d..17aaad2f6f8 100644
--- a/prusti-tests/tests/cargo_verify/failing_stable_toolchain/output.stderr
+++ b/prusti-tests/tests/cargo_verify/failing_stable_toolchain/output.stderr
@@ -18,4 +18,4 @@ note: the failing assertion is here
 3 | #[requires(x > 123)]
   |            ^^^^^^^
 
-error: could not compile `failing_stable_toolchain` due to previous error; 1 warning emitted
+error: could not compile `failing_stable_toolchain` (bin "failing_stable_toolchain") due to previous error; 1 warning emitted
diff --git a/prusti-tests/tests/cargo_verify/overflow_checks/output.stderr b/prusti-tests/tests/cargo_verify/overflow_checks/output.stderr
index 73837cc6e92..0542a0f0486 100644
--- a/prusti-tests/tests/cargo_verify/overflow_checks/output.stderr
+++ b/prusti-tests/tests/cargo_verify/overflow_checks/output.stderr
@@ -4,4 +4,4 @@ error: [Prusti: verification error] assertion might fail with "attempt to add wi
 2 |     x + 1
   |     ^^^^^
 
-error: could not compile `overflow_checks` due to previous error
+error: could not compile `overflow_checks` (bin "overflow_checks") due to previous error
diff --git a/prusti-tests/tests/cargo_verify/prusti_toml/output.stderr b/prusti-tests/tests/cargo_verify/prusti_toml/output.stderr
index 0a366fb1031..a6ccff489c2 100644
--- a/prusti-tests/tests/cargo_verify/prusti_toml/output.stderr
+++ b/prusti-tests/tests/cargo_verify/prusti_toml/output.stderr
@@ -24,4 +24,4 @@ error: [Prusti: verification error] assertion might fail with "attempt to subtra
 11 |     let _y: usize = 1-x;
    |                     ^^^
 
-error: could not compile `prusti_toml` due to 3 previous errors
+error: could not compile `prusti_toml` (lib) due to 3 previous errors
diff --git a/prusti-tests/tests/cargotest.rs b/prusti-tests/tests/cargotest.rs
index 19d9f1c9a9c..55e1e683d3f 100644
--- a/prusti-tests/tests/cargotest.rs
+++ b/prusti-tests/tests/cargotest.rs
@@ -72,7 +72,7 @@ fn simple_assert_false() {
   = note: this error originates in the macro `assert` (in Nightly builds, run with -Z macro-backtrace for more info)
 
 warning: `foo` (bin \"foo\") generated 1 warning
-error: could not compile `foo` due to previous error; 1 warning emitted
+error: could not compile `foo` (bin \"foo\") due to previous error; 1 warning emitted
 ",
         )
         .run();
diff --git a/prusti-tests/tests/verify/fail/assert-false/list-sound.rs b/prusti-tests/tests/verify/fail/assert-false/list-sound.rs
index 3bc19a46cc5..6bebead593c 100644
--- a/prusti-tests/tests/verify/fail/assert-false/list-sound.rs
+++ b/prusti-tests/tests/verify/fail/assert-false/list-sound.rs
@@ -1,6 +1,5 @@
 #![feature(nll)]
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 use prusti_contracts::*;
 
@@ -8,7 +7,7 @@ enum List {
     Nil,
     Const {
         val: i32,
-        next: Box<List>
+        next: Box<List>,
     },
 }
 
@@ -59,7 +58,7 @@ fn empty_list(val: i32) -> List {
 fn singleton_list(val: i32) -> List {
     let ret = List::Const {
         val,
-        next: box List::Nil
+        next: Box::new(List::Nil),
     };
     assert!(false);  //~ ERROR the asserted expression might not hold
     ret
@@ -68,7 +67,7 @@ fn singleton_list(val: i32) -> List {
 fn prepend(val: i32, list: List) -> List {
     let ret = List::Const {
         val,
-        next: box list
+        next: Box::new(list),
     };
     assert!(false);  //~ ERROR the asserted expression might not hold
     ret
@@ -78,11 +77,11 @@ fn append(new_val: i32, list: List) -> List {
     let ret = match list {
         List::Nil => List::Const {
             val: new_val,
-            next: box List::Nil
+            next: Box::new(List::Nil),
         },
         List::Const { val, box next } => List::Const {
             val: val,
-            next: box append(new_val, next)
+            next: Box::new(append(new_val, next)),
         },
     };
     assert!(false);  //~ ERROR the asserted expression might not hold
@@ -92,7 +91,7 @@ fn append(new_val: i32, list: List) -> List {
 fn revert(list: List) -> List {
     let ret = match list {
         List::Nil => List::Nil,
-        List::Const { val, box next } => append(val, revert(next))
+        List::Const { val, box next } => append(val, revert(next)),
     };
     assert!(false);  //~ ERROR the asserted expression might not hold
     ret
diff --git a/prusti-tests/tests/verify/fail/demos/append-error.rs b/prusti-tests/tests/verify/fail/demos/append-error.rs
index ff0d3cbcf90..0aa5b1eab32 100644
--- a/prusti-tests/tests/verify/fail/demos/append-error.rs
+++ b/prusti-tests/tests/verify/fail/demos/append-error.rs
@@ -1,9 +1,10 @@
-#![feature(box_patterns, box_syntax)]
+#![feature(box_patterns)]
+
 use prusti_contracts::*;
 
 struct List {
     val: i32,
-    next: Option<Box<List>>
+    next: Option<Box<List>>,
 }
 
 impl List {
@@ -11,7 +12,7 @@ impl List {
     fn len(&self) -> usize {
         match self.next {
             None => 1,
-            Some(box ref tail) => tail.len() + 1
+            Some(box ref tail) => tail.len() + 1,
         }
     }
 }
@@ -20,10 +21,10 @@ fn append(a: &mut List, v: i32) {
     if let Some(box ref mut tail) = a.next {
         append(tail, v);
     } else {
-        a.next = Some(box List {
+        a.next = Some(Box::new(List {
             val: v,
-            next: None
-        });
+            next: None,
+        }));
     }
 }
 
diff --git a/prusti-tests/tests/verify/fail/demos/append-sorted-error-3.rs b/prusti-tests/tests/verify/fail/demos/append-sorted-error-3.rs
index 62a8ae6e32d..e1eb4b7e650 100644
--- a/prusti-tests/tests/verify/fail/demos/append-sorted-error-3.rs
+++ b/prusti-tests/tests/verify/fail/demos/append-sorted-error-3.rs
@@ -1,9 +1,10 @@
-#![feature(box_patterns, box_syntax)]
+#![feature(box_patterns)]
+
 use prusti_contracts::*;
 
 struct List {
     val: i32,
-    next: Option<Box<List>>
+    next: Option<Box<List>>,
 }
 
 impl List {
@@ -48,10 +49,10 @@ fn append(a: &mut List, v: i32) {
     if let Some(box ref mut tail) = a.next {
         append(tail, v);
     } else {
-        a.next = Some(box List {
+        a.next = Some(Box::new(List {
             val: v,
-            next: None
-        });
+            next: None,
+        }));
     }
 }
 
diff --git a/prusti-tests/tests/verify/fail/loops/havock_loop_vars.rs b/prusti-tests/tests/verify/fail/loops/havock_loop_vars.rs
index 1ffdf54cf89..727fb84cd93 100644
--- a/prusti-tests/tests/verify/fail/loops/havock_loop_vars.rs
+++ b/prusti-tests/tests/verify/fail/loops/havock_loop_vars.rs
@@ -1,5 +1,3 @@
-#![feature(box_syntax)]
-
 use prusti_contracts::*;
 
 #[trusted]
@@ -12,7 +10,7 @@ fn test() {
     let mut z = None;
 
     loop {
-        let x = box 5;
+        let x = Box::new(5);
         if random() {
             y = Some(x);
         } else {
diff --git a/prusti-tests/tests/verify/fail/loops/tmp_in_loop_condition.rs b/prusti-tests/tests/verify/fail/loops/tmp_in_loop_condition.rs
index 4a06c8a5112..e165e0a516c 100644
--- a/prusti-tests/tests/verify/fail/loops/tmp_in_loop_condition.rs
+++ b/prusti-tests/tests/verify/fail/loops/tmp_in_loop_condition.rs
@@ -1,5 +1,3 @@
-#![feature(box_syntax)]
-
 use prusti_contracts::*;
 
 #[trusted]
@@ -8,51 +6,51 @@ fn random() -> u32 {
 }
 
 fn test1() {
-    let mut tmp = box box random();
+    let mut tmp = Box::new(Box::new(random()));
     let tmp_ref = &tmp;
     let tmp_ref_mut = &mut tmp;
 
     while {
         let guard = random() < 55;
 
-        let mut tmp = box box random();
+        let mut tmp = Box::new(Box::new(random()));
         let tmp_ref = &tmp;
         let tmp_ref_mut = &mut tmp;
 
         guard
     } {
-        let mut tmp = box box random();
+        let mut tmp = Box::new(Box::new(random()));
         let tmp_ref = &tmp;
         let tmp_ref_mut = &mut tmp;
     }
 
-    let mut tmp = box box random();
+    let mut tmp = Box::new(Box::new(random()));
     let tmp_ref = &tmp;
     let tmp_ref_mut = &mut tmp;
     assert!(false); //~ ERROR
 }
 
 fn test2() {
-    let mut tmp = box box random();
+    let mut tmp = Box::new(Box::new(random()));
     let tmp_ref = &tmp;
     let tmp_ref_mut = &mut tmp;
 
     while {
         let guard = random() < 55;
 
-        let mut tmp = box box random();
+        let mut tmp = Box::new(Box::new(random()));
         let tmp_ref = &tmp;
         let tmp_ref_mut = &mut tmp;
 
         guard
     } {
-        let mut tmp = box box random();
+        let mut tmp = Box::new(Box::new(random()));
         let tmp_ref = &tmp;
         let tmp_ref_mut = &mut tmp;
         assert!(false); //~ ERROR
     }
 
-    let mut tmp = box box random();
+    let mut tmp = Box::new(Box::new(random()));
     let tmp_ref = &tmp;
     let tmp_ref_mut = &mut tmp;
 }
diff --git a/prusti-tests/tests/verify/fail/no-annotations/predicate-old-expr.rs b/prusti-tests/tests/verify/fail/no-annotations/predicate-old-expr.rs
index 7427a1bb7c9..6ec15273d90 100644
--- a/prusti-tests/tests/verify/fail/no-annotations/predicate-old-expr.rs
+++ b/prusti-tests/tests/verify/fail/no-annotations/predicate-old-expr.rs
@@ -1,6 +1,5 @@
 #![feature(nll)]
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 use std::borrow::BorrowMut;
 
diff --git a/prusti-tests/tests/verify/fail/pure-fn/panic-in-fn.rs b/prusti-tests/tests/verify/fail/pure-fn/panic-in-fn.rs
index 4e75d5a8349..6b0c495fca3 100644
--- a/prusti-tests/tests/verify/fail/pure-fn/panic-in-fn.rs
+++ b/prusti-tests/tests/verify/fail/pure-fn/panic-in-fn.rs
@@ -1,6 +1,5 @@
 #![feature(nll)]
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 use prusti_contracts::*;
 
diff --git a/prusti-tests/tests/verify/fail/pure-fn/wrong-quantifiers.rs b/prusti-tests/tests/verify/fail/pure-fn/wrong-quantifiers.rs
index 433b6356142..f1590232805 100644
--- a/prusti-tests/tests/verify/fail/pure-fn/wrong-quantifiers.rs
+++ b/prusti-tests/tests/verify/fail/pure-fn/wrong-quantifiers.rs
@@ -1,6 +1,5 @@
 #![feature(nll)]
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 use prusti_contracts::*;
 
diff --git a/prusti-tests/tests/verify/fail/pure-fn/wrong-ref-mut-arg.rs b/prusti-tests/tests/verify/fail/pure-fn/wrong-ref-mut-arg.rs
index 6b63d443351..20226f01770 100644
--- a/prusti-tests/tests/verify/fail/pure-fn/wrong-ref-mut-arg.rs
+++ b/prusti-tests/tests/verify/fail/pure-fn/wrong-ref-mut-arg.rs
@@ -1,6 +1,5 @@
 #![feature(nll)]
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 #![feature(never_type)]
 #![allow(unconditional_recursion)]
 
diff --git a/prusti-tests/tests/verify/pass/demos/append.rs b/prusti-tests/tests/verify/pass/demos/append.rs
index ce7d25a595f..742525060bd 100644
--- a/prusti-tests/tests/verify/pass/demos/append.rs
+++ b/prusti-tests/tests/verify/pass/demos/append.rs
@@ -1,4 +1,5 @@
-#![feature(box_patterns, box_syntax)]
+#![feature(box_patterns)]
+
 use prusti_contracts::*;
 
 struct List {
@@ -20,10 +21,10 @@ fn append(a: &mut List, v: i32) {
     if let Some(box ref mut tail) = a.next {
         append(tail, v);
     } else {
-        a.next = Some(box List {
+        a.next = Some(Box::new(List {
             val: v,
             next: None
-        });
+        }));
     }
 }
 
diff --git a/prusti-tests/tests/verify/pass/expiring-loans/pure-fn-loan-2.rs b/prusti-tests/tests/verify/pass/expiring-loans/pure-fn-loan-2.rs
index e37da81a3c8..28028d05da6 100644
--- a/prusti-tests/tests/verify/pass/expiring-loans/pure-fn-loan-2.rs
+++ b/prusti-tests/tests/verify/pass/expiring-loans/pure-fn-loan-2.rs
@@ -1,6 +1,5 @@
 #![feature(nll)]
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 use prusti_contracts::*;
 
diff --git a/prusti-tests/tests/verify/pass/expiring-loans/pure-fn-loan.rs b/prusti-tests/tests/verify/pass/expiring-loans/pure-fn-loan.rs
index ae76b9768e9..a8c73033970 100644
--- a/prusti-tests/tests/verify/pass/expiring-loans/pure-fn-loan.rs
+++ b/prusti-tests/tests/verify/pass/expiring-loans/pure-fn-loan.rs
@@ -1,6 +1,5 @@
 #![feature(nll)]
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 use prusti_contracts::*;
 
diff --git a/prusti-tests/tests/verify/pass/gitlab-issues/issue-118-1.rs b/prusti-tests/tests/verify/pass/gitlab-issues/issue-118-1.rs
index bb710ff9f60..9c0e9a5f1e5 100644
--- a/prusti-tests/tests/verify/pass/gitlab-issues/issue-118-1.rs
+++ b/prusti-tests/tests/verify/pass/gitlab-issues/issue-118-1.rs
@@ -1,6 +1,5 @@
 #![feature(nll)]
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 use prusti_contracts::*;
 
diff --git a/prusti-tests/tests/verify/pass/gitlab-issues/issue-118.rs b/prusti-tests/tests/verify/pass/gitlab-issues/issue-118.rs
index ce79a93ec2c..53c3bdf7f12 100644
--- a/prusti-tests/tests/verify/pass/gitlab-issues/issue-118.rs
+++ b/prusti-tests/tests/verify/pass/gitlab-issues/issue-118.rs
@@ -1,6 +1,5 @@
 #![feature(nll)]
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 use prusti_contracts::*;
 
diff --git a/prusti-tests/tests/verify/pass/gitlab-issues/issue-39.rs b/prusti-tests/tests/verify/pass/gitlab-issues/issue-39.rs
index 2a5ddda7995..6b4c6086ca9 100644
--- a/prusti-tests/tests/verify/pass/gitlab-issues/issue-39.rs
+++ b/prusti-tests/tests/verify/pass/gitlab-issues/issue-39.rs
@@ -2,11 +2,9 @@
 
 #![feature(nll)]
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 use prusti_contracts::*;
 
-
 struct List {
     value: u32,
     next: Option<Box<List>>,
diff --git a/prusti-tests/tests/verify/pass/loop-invs/framing_after_break.rs b/prusti-tests/tests/verify/pass/loop-invs/framing_after_break.rs
index 00bbf54222e..6bcaf9c5ec1 100644
--- a/prusti-tests/tests/verify/pass/loop-invs/framing_after_break.rs
+++ b/prusti-tests/tests/verify/pass/loop-invs/framing_after_break.rs
@@ -1,5 +1,3 @@
-#![feature(box_syntax)]
-
 use prusti_contracts::*;
 
 #[trusted]
@@ -21,7 +19,7 @@ fn test() {
             break;
         }
 
-        let y = box x;
+        let y = Box::new(x);
     }
 
     assert!(x == 123);
@@ -44,7 +42,7 @@ fn test2() {
             break;
         }
 
-        let y = box x;
+        let y = Box::new(x);
     }
 
     assert!(x == 123);
@@ -69,7 +67,7 @@ fn test3() {
 
         x = 567;
 
-        let y = box x;
+        let y = Box::new(x);
     }
 
     assert!(x == 123);
diff --git a/prusti-tests/tests/verify/pass/loop-invs/initialize_in_loop_condition.rs b/prusti-tests/tests/verify/pass/loop-invs/initialize_in_loop_condition.rs
index 2e492f74b3d..dcd1c4074cc 100644
--- a/prusti-tests/tests/verify/pass/loop-invs/initialize_in_loop_condition.rs
+++ b/prusti-tests/tests/verify/pass/loop-invs/initialize_in_loop_condition.rs
@@ -1,5 +1,3 @@
-#![feature(box_syntax)]
-
 use prusti_contracts::*;
 
 #[trusted]
@@ -11,7 +9,7 @@ fn test() {
     let mut x: Box<u32>;
 
     'myloop: while {
-        x = box random();
+        x = Box::new(random());
         if *x == 0 {
             break 'myloop;
         }
diff --git a/prusti-tests/tests/verify/pass/loop-invs/tmp_in_loop_condition.rs b/prusti-tests/tests/verify/pass/loop-invs/tmp_in_loop_condition.rs
index 451bee949e6..f0398aec07d 100644
--- a/prusti-tests/tests/verify/pass/loop-invs/tmp_in_loop_condition.rs
+++ b/prusti-tests/tests/verify/pass/loop-invs/tmp_in_loop_condition.rs
@@ -1,5 +1,3 @@
-#![feature(box_syntax)]
-
 use prusti_contracts::*;
 
 #[trusted]
@@ -8,25 +6,25 @@ fn random() -> u32 {
 }
 
 fn test() {
-    let mut tmp = box box random();
+    let mut tmp = Box::new(Box::new(random()));
     let tmp_ref = &tmp;
     let tmp_ref_mut = &mut tmp;
 
     while {
         let guard = random() < 55;
 
-        let mut tmp = box box random();
+        let mut tmp = Box::new(Box::new(random()));
         let tmp_ref = &tmp;
         let tmp_ref_mut = &mut tmp;
 
         guard
     } {
-        let mut tmp = box box random();
+        let mut tmp = Box::new(Box::new(random()));
         let tmp_ref = &tmp;
         let tmp_ref_mut = &mut tmp;
     }
 
-    let mut tmp = box box random();
+    let mut tmp = Box::new(Box::new(random()));
     let tmp_ref = &tmp;
     let tmp_ref_mut = &mut tmp;
 
diff --git a/prusti-tests/tests/verify/pass/no-annotations/create-box.rs b/prusti-tests/tests/verify/pass/no-annotations/create-box.rs
index a3218a54243..8f05a3f2238 100644
--- a/prusti-tests/tests/verify/pass/no-annotations/create-box.rs
+++ b/prusti-tests/tests/verify/pass/no-annotations/create-box.rs
@@ -1,7 +1,4 @@
-//! Currently unsupported because `Box` and `Option` use a type parameter
-
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 fn use_box(v: i32) -> Box<i32> {
     let x = Box::new(v);
@@ -9,7 +6,7 @@ fn use_box(v: i32) -> Box<i32> {
     assert!(v == y);
     let z = Box::new(y);
     assert!(v == *z);
-    box *z
+    Box::new(*z)
 }
 
 fn main() {}
diff --git a/prusti-tests/tests/verify/pass/no-annotations/either.rs b/prusti-tests/tests/verify/pass/no-annotations/either.rs
index 3daf77c40ed..5b5a0ce2d7d 100644
--- a/prusti-tests/tests/verify/pass/no-annotations/either.rs
+++ b/prusti-tests/tests/verify/pass/no-annotations/either.rs
@@ -1,7 +1,4 @@
-//! Currently unsupported because `Box` and `Option` use a type parameter
-
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 enum Either {
     Left(i32),
diff --git a/prusti-tests/tests/verify/pass/no-annotations/list.rs b/prusti-tests/tests/verify/pass/no-annotations/list.rs
index 7bfb3c6285d..38a37e4834c 100644
--- a/prusti-tests/tests/verify/pass/no-annotations/list.rs
+++ b/prusti-tests/tests/verify/pass/no-annotations/list.rs
@@ -1,13 +1,12 @@
 //! Example of linked list
 
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 enum List {
     Nil,
     Const {
         val: i32,
-        next: Box<List>
+        next: Box<List>,
     },
 }
 
@@ -49,14 +48,14 @@ fn empty_list(val: i32) -> List {
 fn singleton_list(val: i32) -> List {
     List::Const {
         val,
-        next: box List::Nil
+        next: Box::new(List::Nil),
     }
 }
 
 fn prepend(val: i32, list: List) -> List {
     List::Const {
         val,
-        next: box list
+        next: Box::new(list),
     }
 }
 
@@ -64,11 +63,11 @@ fn append(new_val: i32, list: List) -> List {
     match list {
         List::Nil => List::Const {
             val: new_val,
-            next: box List::Nil
+            next: Box::new(List::Nil),
         },
         List::Const { val, box next } => List::Const {
             val: val,
-            next: box append(new_val, next)
+            next: Box::new(append(new_val, next)),
         },
     }
 }
diff --git a/prusti-tests/tests/verify/pass/no-annotations/option.rs b/prusti-tests/tests/verify/pass/no-annotations/option.rs
index cbc91d7b304..6f826c2b121 100644
--- a/prusti-tests/tests/verify/pass/no-annotations/option.rs
+++ b/prusti-tests/tests/verify/pass/no-annotations/option.rs
@@ -1,7 +1,4 @@
-//! Currently unsupported because `Box` and `Option` use a type parameter
-
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 fn main() {
     let x = 123;
diff --git a/prusti-tests/tests/verify/pass/no-annotations/reassignment.rs b/prusti-tests/tests/verify/pass/no-annotations/reassignment.rs
index b6e62e7db59..e534a1c384f 100644
--- a/prusti-tests/tests/verify/pass/no-annotations/reassignment.rs
+++ b/prusti-tests/tests/verify/pass/no-annotations/reassignment.rs
@@ -1,7 +1,6 @@
 //! Example of reassignment
 
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 struct InfiniteList {
     val: i32,
diff --git a/prusti-tests/tests/verify/pass/no-annotations/use-box.rs b/prusti-tests/tests/verify/pass/no-annotations/use-box.rs
index db36f60569e..3a94612a3eb 100644
--- a/prusti-tests/tests/verify/pass/no-annotations/use-box.rs
+++ b/prusti-tests/tests/verify/pass/no-annotations/use-box.rs
@@ -1,7 +1,4 @@
-//! Currently unsupported because `Box` and `Option` use a type parameter
-
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 fn use_box(x: Box<i32>) -> i32 {
     *x
diff --git a/prusti-tests/tests/verify/pass/paper-examples/ownership_align.rs b/prusti-tests/tests/verify/pass/paper-examples/ownership_align.rs
index 6a301c774f0..58911023365 100644
--- a/prusti-tests/tests/verify/pass/paper-examples/ownership_align.rs
+++ b/prusti-tests/tests/verify/pass/paper-examples/ownership_align.rs
@@ -1,5 +1,3 @@
-#![feature(box_syntax)]
-
 use prusti_contracts::*;
 
 struct Point {
@@ -9,7 +7,7 @@ struct Point {
 #[ensures(old((*p).x + s) == (*result).x)]
 #[ensures(old((*p).y) == (*result).y)]
 fn shift_x(p: Box<Point>, s:i32) -> Box<Point> {
-  box Point { x: (*p).x + s, y: (*p).y }
+  Box::new(Point { x: (*p).x + s, y: (*p).y })
 }
 
 fn compress(mut segm: (Box<Point>, Box<Point>))
diff --git a/prusti-tests/tests/verify/pass/paper-examples/routes.rs b/prusti-tests/tests/verify/pass/paper-examples/routes.rs
index 8d67d5a9a11..2a54db73ffb 100644
--- a/prusti-tests/tests/verify/pass/paper-examples/routes.rs
+++ b/prusti-tests/tests/verify/pass/paper-examples/routes.rs
@@ -1,4 +1,4 @@
-#![feature(box_syntax, box_patterns)]
+#![feature(box_patterns)]
 
 use prusti_contracts::*;
 
diff --git a/prusti-tests/tests/verify/pass/pure-fn/issue-27.rs b/prusti-tests/tests/verify/pass/pure-fn/issue-27.rs
index 441585583c5..9a0864bf262 100644
--- a/prusti-tests/tests/verify/pass/pure-fn/issue-27.rs
+++ b/prusti-tests/tests/verify/pass/pure-fn/issue-27.rs
@@ -1,6 +1,5 @@
 #![feature(nll)]
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 /// See issue #27
 
diff --git a/prusti-tests/tests/verify/pass/pure-fn/len-lookup.rs b/prusti-tests/tests/verify/pass/pure-fn/len-lookup.rs
index ce18b014e6a..5e8a1e2abc4 100644
--- a/prusti-tests/tests/verify/pass/pure-fn/len-lookup.rs
+++ b/prusti-tests/tests/verify/pass/pure-fn/len-lookup.rs
@@ -1,6 +1,5 @@
 #![feature(nll)]
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 use prusti_contracts::*;
 
diff --git a/prusti-tests/tests/verify/pass/pure-fn/quantifiers.rs b/prusti-tests/tests/verify/pass/pure-fn/quantifiers.rs
index dd5b6146cc4..f6497affb56 100644
--- a/prusti-tests/tests/verify/pass/pure-fn/quantifiers.rs
+++ b/prusti-tests/tests/verify/pass/pure-fn/quantifiers.rs
@@ -1,6 +1,5 @@
 #![feature(nll)]
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 use prusti_contracts::*;
 
diff --git a/prusti-tests/tests/verify/pass/pure-fn/recursive-pure-fn.rs b/prusti-tests/tests/verify/pass/pure-fn/recursive-pure-fn.rs
index 3719c0551ae..f3c981c60aa 100644
--- a/prusti-tests/tests/verify/pass/pure-fn/recursive-pure-fn.rs
+++ b/prusti-tests/tests/verify/pass/pure-fn/recursive-pure-fn.rs
@@ -1,6 +1,5 @@
 #![feature(nll)]
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 use prusti_contracts::*;
 
diff --git a/prusti-tests/tests/verify/pass/pure-fn/ref-mut-arg.rs b/prusti-tests/tests/verify/pass/pure-fn/ref-mut-arg.rs
index 4b39fecc108..12afe23f96c 100644
--- a/prusti-tests/tests/verify/pass/pure-fn/ref-mut-arg.rs
+++ b/prusti-tests/tests/verify/pass/pure-fn/ref-mut-arg.rs
@@ -1,6 +1,5 @@
 #![feature(nll)]
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 #![feature(never_type)]
 #![allow(unconditional_recursion)]
 
diff --git a/prusti-tests/tests/verify/pass/quick/routes.rs b/prusti-tests/tests/verify/pass/quick/routes.rs
index e61d28b896b..ea303352af2 100644
--- a/prusti-tests/tests/verify/pass/quick/routes.rs
+++ b/prusti-tests/tests/verify/pass/quick/routes.rs
@@ -1,4 +1,4 @@
-#![feature(box_syntax, box_patterns)]
+#![feature(box_patterns)]
 
 use prusti_contracts::*;
 
diff --git a/prusti-tests/tests/verify_overflow/pass/initialization/deref.rs b/prusti-tests/tests/verify_overflow/pass/initialization/deref.rs
index fbe4c455016..de55fb4934d 100644
--- a/prusti-tests/tests/verify_overflow/pass/initialization/deref.rs
+++ b/prusti-tests/tests/verify_overflow/pass/initialization/deref.rs
@@ -2,7 +2,6 @@
 
 #![feature(nll)]
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 use prusti_contracts::*;
 
diff --git a/prusti-tests/tests/verify_overflow/pass/simple-specs/ownership1.rs b/prusti-tests/tests/verify_overflow/pass/simple-specs/ownership1.rs
index aded0adbeec..cf1b9280297 100644
--- a/prusti-tests/tests/verify_overflow/pass/simple-specs/ownership1.rs
+++ b/prusti-tests/tests/verify_overflow/pass/simple-specs/ownership1.rs
@@ -1,5 +1,5 @@
 #![feature(nll)]
-#![feature(box_patterns, box_syntax)]
+#![feature(box_patterns)]
 
 use prusti_contracts::*;
 
diff --git a/prusti-tests/tests/verify_overflow/pass/simple-specs/ownership2.rs b/prusti-tests/tests/verify_overflow/pass/simple-specs/ownership2.rs
index a5ebc008add..2f726522520 100644
--- a/prusti-tests/tests/verify_overflow/pass/simple-specs/ownership2.rs
+++ b/prusti-tests/tests/verify_overflow/pass/simple-specs/ownership2.rs
@@ -1,6 +1,5 @@
 #![feature(nll)]
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 use prusti_contracts::*;
 
@@ -11,7 +10,7 @@ struct Point {
 
 #[requires(u32::MAX - *a >= b)]
 #[ensures(*result == old(*a) + old(b))]
-fn add(a: Box<u32>, b: u32) -> Box<u32> { box (*a + b) }
+fn add(a: Box<u32>, b: u32) -> Box<u32> { Box::new(*a + b) }
 
 #[requires(u32::MAX - *p.x >= s)]
 #[ensures(*result.x == old(*p.x) + old(s))]
@@ -24,4 +23,4 @@ fn shift_x(p: Point, s: u32) -> Point {
     pp
 }
 
-fn main(){}
+fn main() {}
diff --git a/prusti-utils/src/lib.rs b/prusti-utils/src/lib.rs
index f2296bb6579..12116a3fe0f 100644
--- a/prusti-utils/src/lib.rs
+++ b/prusti-utils/src/lib.rs
@@ -5,7 +5,6 @@
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 #![deny(unused_must_use)]
 #![warn(clippy::disallowed_types)]
 
diff --git a/prusti-utils/src/report/log.rs b/prusti-utils/src/report/log.rs
index 1f4a4d6d535..41c852086c7 100644
--- a/prusti-utils/src/report/log.rs
+++ b/prusti-utils/src/report/log.rs
@@ -65,13 +65,13 @@ pub fn build_writer<S: ToString>(namespace: &str, name: S) -> io::Result<Box<dyn
             let name_path = PathBuf::from(name_string);
             debug_assert!(!name_path.is_absolute(), "The name cannot be absolute");
             path.push(name_path);
-            box fs::File::create(path)?
+            Box::new(fs::File::create(path)?)
         }
         // fallback
         None => {
             let mut stdout = io::stdout();
             write!(stdout, "# {}: {}\n\n", namespace, name.to_string())?;
-            box stdout
+            Box::new(stdout)
         }
     })
 }
diff --git a/prusti-viper/src/encoder/counterexamples/counterexample.rs b/prusti-viper/src/encoder/counterexamples/counterexample.rs
index 513cd5813cf..bf8661f520d 100644
--- a/prusti-viper/src/encoder/counterexamples/counterexample.rs
+++ b/prusti-viper/src/encoder/counterexamples/counterexample.rs
@@ -125,8 +125,8 @@ impl Entry {
             (Entry::Float(x), _) => Entry::Float(x.clone()),
             (Entry::Bool(x), _) => Entry::Bool(*x),
             (Entry::Char(x), _) => Entry::Char(*x),
-            (Entry::Ref(entry), _) => Entry::Ref(box entry.merge(other)),
-            (Entry::Box(entry), _) => Entry::Box(box entry.merge(other)),
+            (Entry::Ref(entry), _) => Entry::Ref(Box::new(entry.merge(other))),
+            (Entry::Box(entry), _) => Entry::Box(Box::new(entry.merge(other))),
             (
                 Entry::Struct {
                     name: name1,
diff --git a/prusti-viper/src/encoder/counterexamples/counterexample_translation.rs b/prusti-viper/src/encoder/counterexamples/counterexample_translation.rs
index aff35fdc22f..c211eecedd5 100644
--- a/prusti-viper/src/encoder/counterexamples/counterexample_translation.rs
+++ b/prusti-viper/src/encoder/counterexamples/counterexample_translation.rs
@@ -293,17 +293,16 @@ impl<'ce, 'tcx> CounterexampleTranslator<'ce, 'tcx> {
                 let value = value_str.parse::<u32>().ok()?;
                 Entry::Char(char::from_u32(value)?)
             }
-            (ty::TyKind::Ref(_, typ, _), Some(ModelEntry::Ref(_, map))) => Entry::Ref(
-                box self
-                    .translate_silicon_entry(
-                        *typ,
-                        map.get("val_ref"),
-                        format!("{vir_name}.val_ref"),
-                        silicon_ce_entries,
-                    )
-                    .unwrap_or_default(),
-            ),
-            (ty::TyKind::Ref(..), _) => Entry::Ref(box Entry::Unknown),
+            (ty::TyKind::Ref(_, typ, _), Some(ModelEntry::Ref(_, map))) => Entry::Ref(Box::new(
+                self.translate_silicon_entry(
+                    *typ,
+                    map.get("val_ref"),
+                    format!("{vir_name}.val_ref"),
+                    silicon_ce_entries,
+                )
+                .unwrap_or_default(),
+            )),
+            (ty::TyKind::Ref(..), _) => Entry::Ref(Box::new(Entry::Unknown)),
             (ty::TyKind::Tuple(subst), Some(ModelEntry::Ref(_, map))) => {
                 let len = subst.len();
                 let mut fields = vec![];
@@ -336,9 +335,11 @@ impl<'ce, 'tcx> CounterexampleTranslator<'ce, 'tcx> {
                         silicon_ce_entries,
                     )
                     .unwrap_or_default();
-                Entry::Box(box entry)
+                Entry::Box(Box::new(entry))
+            }
+            (ty::TyKind::Adt(adt_def, _), _) if adt_def.is_box() => {
+                Entry::Box(Box::new(Entry::Unknown))
             }
-            (ty::TyKind::Adt(adt_def, _), _) if adt_def.is_box() => Entry::Box(box Entry::Unknown),
             (ty::TyKind::Adt(adt_def, subst), _) if adt_def.is_struct() => {
                 let variant = adt_def.variants().iter().next().unwrap();
                 let struct_name = variant.ident(self.tcx).name.to_ident_string();
@@ -589,20 +590,19 @@ impl<'ce, 'tcx> CounterexampleTranslator<'ce, 'tcx> {
                         if let Some(encoded_typ) = encoded_typ_option {
                             let new_encoded_typ = Some(encoded_typ.replacen("ref$", "", 1)); //remove a ref
                             let sil_entry = map.get("val_ref");
-                            Entry::Ref(
-                                box self
-                                    .translate_silicon_entry_with_snapshot(
-                                        *typ,
-                                        sil_entry,
-                                        new_encoded_typ,
-                                    )
-                                    .unwrap_or_default(),
-                            )
+                            Entry::Ref(Box::new(
+                                self.translate_silicon_entry_with_snapshot(
+                                    *typ,
+                                    sil_entry,
+                                    new_encoded_typ,
+                                )
+                                .unwrap_or_default(),
+                            ))
                         } else {
-                            Entry::Ref(box Entry::Unknown)
+                            Entry::Ref(Box::new(Entry::Unknown))
                         }
                     }
-                    _ => Entry::Ref(box Entry::Unknown),
+                    _ => Entry::Ref(Box::new(Entry::Unknown)),
                 }
             }
             ty::TyKind::Tuple(subst) => match snapshot_var {
@@ -642,7 +642,7 @@ impl<'ce, 'tcx> CounterexampleTranslator<'ce, 'tcx> {
                         encoded_typ_option,
                     )
                     .unwrap_or_default();
-                Entry::Box(box entry)
+                Entry::Box(Box::new(entry))
             }
             ty::TyKind::Adt(adt_def, subst) if adt_def.is_struct() => {
                 let variant = adt_def.variants().iter().next().unwrap();
diff --git a/prusti-viper/src/encoder/counterexamples/counterexample_translation_refactored.rs b/prusti-viper/src/encoder/counterexamples/counterexample_translation_refactored.rs
index be1f56f967a..994c89dd651 100644
--- a/prusti-viper/src/encoder/counterexamples/counterexample_translation_refactored.rs
+++ b/prusti-viper/src/encoder/counterexamples/counterexample_translation_refactored.rs
@@ -355,13 +355,13 @@ impl<'ce, 'tcx, 'v> CounterexampleTranslator<'ce, 'tcx, 'v> {
                     .get(domain_name)
                     .unwrap();
                 let sil_fn_name = format!("destructor${domain_name}$$target_current");
-                Entry::Ref(box self.extract_field_value(
+                Entry::Ref(Box::new(self.extract_field_value(
                     &sil_fn_name,
                     Some(*typ),
                     model_entry,
                     sil_domain,
                     model,
-                ))
+                )))
             }
             (Some(ModelEntry::DomainValue(domain_name, _)), Some(ty::TyKind::Tuple(subst))) => {
                 let sil_domain = self
@@ -400,13 +400,13 @@ impl<'ce, 'tcx, 'v> CounterexampleTranslator<'ce, 'tcx, 'v> {
                     .unwrap();
                 let sil_fn_name = format!("destructor${domain_name}$$val_ref");
                 let new_typ = subst.type_at(0);
-                Entry::Box(box self.extract_field_value(
+                Entry::Box(Box::new(self.extract_field_value(
                     &sil_fn_name,
                     Some(new_typ),
                     model_entry,
                     sil_domain,
                     model,
-                ))
+                )))
             }
 
             (
@@ -423,7 +423,7 @@ impl<'ce, 'tcx, 'v> CounterexampleTranslator<'ce, 'tcx, 'v> {
                         .unwrap();
                     let sil_fn_name = format!("destructor${domain_name}$$value");
                     let variant = adt_def.variants().iter().next().unwrap();
-                    let int_typ = Some(variant.fields[0].ty(self.tcx, subst));
+                    let int_typ = Some(variant.fields[0usize.into()].ty(self.tcx, subst));
                     return self.extract_field_value(
                         &sil_fn_name,
                         int_typ,
@@ -491,11 +491,12 @@ impl<'ce, 'tcx, 'v> CounterexampleTranslator<'ce, 'tcx, 'v> {
                         let super_name = format!("{adt_def:?}");
                         let disc_value_int = disc_value.parse::<usize>().unwrap();
                         let variant = adt_def.variants().iter().next().unwrap();
-                        let variant_name = variant.fields[disc_value_int]
+                        let variant_name = variant.fields[disc_value_int.into()]
                             .ident(self.tcx)
                             .name
                             .to_ident_string();
-                        let field_typ = Some(variant.fields[disc_value_int].ty(self.tcx, subst));
+                        let field_typ =
+                            Some(variant.fields[disc_value_int.into()].ty(self.tcx, subst));
 
                         let destructor_sil_name =
                             format!("destructor${}${}$value", domain_name, &variant_name);
@@ -521,19 +522,19 @@ impl<'ce, 'tcx, 'v> CounterexampleTranslator<'ce, 'tcx, 'v> {
                                 );
                                 return Entry::Union {
                                     name: super_name,
-                                    field_entry: (variant_name, box field_entry),
+                                    field_entry: (variant_name, Box::new(field_entry)),
                                 };
                             }
                             return Entry::Union {
                                 name: super_name,
-                                field_entry: (variant_name, box Entry::Unknown),
+                                field_entry: (variant_name, Box::new(Entry::Unknown)),
                             };
                         }
                     }
                 }
                 Entry::Union {
                     name: format!("{adt_def:?}"),
-                    field_entry: ("?".to_string(), box Entry::Unknown),
+                    field_entry: ("?".to_string(), Box::new(Entry::Unknown)),
                 }
             }
             (
diff --git a/prusti-viper/src/encoder/encoder.rs b/prusti-viper/src/encoder/encoder.rs
index 08e5966d17f..c6ff636ec35 100644
--- a/prusti-viper/src/encoder/encoder.rs
+++ b/prusti-viper/src/encoder/encoder.rs
@@ -523,8 +523,8 @@ impl<'v, 'tcx> Encoder<'v, 'tcx> {
             let slice_cons = self.encode_snapshot(dst_ty, None, vec![array_uncons.clone()])?;
             let data_len = vir::Expr::ContainerOp(vir::ContainerOp {
                 op_kind: vir::ContainerOpKind::SeqLen,
-                left: box array_uncons,
-                right: box true.into(), // unused
+                left: Box::new(array_uncons),
+                right: Box::new(true.into()), // unused
                 position: vir::Position::default(),
             });
             let result = vir::Expr::from(vir_local!{ __result: {dst_snap_ty.clone()} });
diff --git a/prusti-viper/src/encoder/foldunfold/mod.rs b/prusti-viper/src/encoder/foldunfold/mod.rs
index 0535306f98c..e80b23f9ec3 100644
--- a/prusti-viper/src/encoder/foldunfold/mod.rs
+++ b/prusti-viper/src/encoder/foldunfold/mod.rs
@@ -882,7 +882,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> vir::CfgReplacer<PathCtxt<'p>, ActionVec> for FoldUnf
                 }
                 if perm_amount == vir::PermAmount::Write {
                     let access = vir::Expr::FieldAccessPredicate(vir::FieldAccessPredicate {
-                        base: box place.clone(),
+                        base: Box::new(place.clone()),
                         permission: vir::PermAmount::Remaining,
                         position: vir::Position::default(),
                     });
@@ -899,7 +899,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> vir::CfgReplacer<PathCtxt<'p>, ActionVec> for FoldUnf
                 let new_place = place.replace_place(source, target);
                 trace!("    new place: {}", new_place);
                 let lhs_read_access = vir::Expr::FieldAccessPredicate(vir::FieldAccessPredicate {
-                    base: box new_place,
+                    base: Box::new(new_place),
                     permission: vir::PermAmount::Read,
                     position: vir::Position::default(),
                 });
@@ -931,7 +931,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> vir::CfgReplacer<PathCtxt<'p>, ActionVec> for FoldUnf
                     let access =
                         vir::Expr::PredicateAccessPredicate(vir::PredicateAccessPredicate {
                             predicate_type: predicate_type.clone(),
-                            argument: box place.clone(),
+                            argument: Box::new(place.clone()),
                             permission: vir::PermAmount::Remaining,
                             position: place.pos(),
                         });
@@ -950,7 +950,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> vir::CfgReplacer<PathCtxt<'p>, ActionVec> for FoldUnf
                 let lhs_read_access =
                     vir::Expr::PredicateAccessPredicate(vir::PredicateAccessPredicate {
                         predicate_type,
-                        argument: box new_place,
+                        argument: Box::new(new_place),
                         permission: vir::PermAmount::Read,
                         position: vir::Position::default(),
                     });
diff --git a/prusti-viper/src/encoder/foldunfold/semantics.rs b/prusti-viper/src/encoder/foldunfold/semantics.rs
index a35c6cba526..17534e4cbc8 100644
--- a/prusti-viper/src/encoder/foldunfold/semantics.rs
+++ b/prusti-viper/src/encoder/foldunfold/semantics.rs
@@ -347,9 +347,12 @@ impl ApplyOnState for vir::Stmt {
                         if this_label == target_label {
                             if let vir::Expr::LabelledOld(repl_labelled) = replacement {
                                 return vir::Expr::LabelledOld(vir::LabelledOld {
-                                    base: box this_base
-                                        .clone()
-                                        .replace_place(target_base, repl_labelled.base.as_ref()),
+                                    base: Box::new(
+                                        this_base.clone().replace_place(
+                                            target_base,
+                                            repl_labelled.base.as_ref(),
+                                        ),
+                                    ),
                                     label: repl_labelled.label.clone(),
                                     position: repl_labelled.position,
                                 });
diff --git a/prusti-viper/src/encoder/high/lower/ty.rs b/prusti-viper/src/encoder/high/lower/ty.rs
index 17a72a0a56d..02cf6358cf0 100644
--- a/prusti-viper/src/encoder/high/lower/ty.rs
+++ b/prusti-viper/src/encoder/high/lower/ty.rs
@@ -18,11 +18,11 @@ impl IntoPolymorphic<vir_poly::Type> for vir_high::Type {
             vir_high::Type::Bool => vir_poly::Type::typed_ref("bool"),
             vir_high::Type::Int(int) => vir_poly::Type::typed_ref(int.to_string().to_lowercase()),
             vir_high::Type::Sequence(ty) => vir_poly::Type::Seq(vir_poly::SeqType {
-                typ: box ty.element_type.lower(encoder),
+                typ: Box::new(ty.element_type.lower(encoder)),
             }),
             vir_high::Type::Map(ty) => vir_poly::Type::Map(vir_poly::MapType {
-                key_type: box ty.key_type.lower(encoder),
-                val_type: box ty.val_type.lower(encoder),
+                key_type: Box::new(ty.key_type.lower(encoder)),
+                val_type: Box::new(ty.val_type.lower(encoder)),
             }),
             vir_high::Type::Float(float) => {
                 vir_poly::Type::typed_ref(float.to_string().to_lowercase())
diff --git a/prusti-viper/src/encoder/mir/contracts/borrows.rs b/prusti-viper/src/encoder/mir/contracts/borrows.rs
index b9bf189a107..39182d84716 100644
--- a/prusti-viper/src/encoder/mir/contracts/borrows.rs
+++ b/prusti-viper/src/encoder/mir/contracts/borrows.rs
@@ -9,8 +9,8 @@ use crate::{
     utils::type_visitor::{self, TypeVisitor},
 };
 use prusti_rustc_interface::{
+    abi::FieldIdx,
     hir::{self as hir, Mutability},
-    index::vec::Idx,
     middle::{
         mir,
         ty::{self, Ty, TyCtxt, TyKind},
@@ -176,7 +176,7 @@ impl<'tcx> TypeVisitor<'tcx> for BorrowInfoCollectingVisitor<'tcx> {
     ) -> Result<(), Self::Error> {
         let old_path = self.current_path.take().unwrap();
         let ty = field.ty(self.tcx(), substs);
-        let field_id = mir::Field::new(index);
+        let field_id = FieldIdx::from_usize(index);
         let new_path = self.tcx.mk_place_field(old_path, field_id, ty);
         self.current_path = Some(new_path);
         // self.current_path = Some(old_path.clone().field(field_id, ty));
@@ -214,7 +214,7 @@ impl<'tcx> TypeVisitor<'tcx> for BorrowInfoCollectingVisitor<'tcx> {
     fn visit_tuple(&mut self, types: &'tcx ty::List<ty::Ty<'tcx>>) -> Result<(), Self::Error> {
         let old_path = self.current_path.take().unwrap();
         for (i, ty) in types.into_iter().enumerate() {
-            let field = mir::Field::new(i);
+            let field = FieldIdx::from_usize(i);
             self.current_path = Some(self.tcx().mk_place_field(old_path, field, ty));
             self.visit_ty(ty)?;
         }
diff --git a/prusti-viper/src/encoder/mir/places/interface.rs b/prusti-viper/src/encoder/mir/places/interface.rs
index 5428b62deeb..80e2e901785 100644
--- a/prusti-viper/src/encoder/mir/places/interface.rs
+++ b/prusti-viper/src/encoder/mir/places/interface.rs
@@ -324,7 +324,11 @@ impl<'v, 'tcx: 'v> PlacesEncoderInterface<'tcx> for super::super::super::Encoder
         right: vir_high::Expression,
         ty: &vir_high::Type,
     ) -> EncodingResult<vir_high::Expression> {
-        if !op.is_checkable() || !prusti_common::config::check_overflows() {
+        if !matches!(
+            op,
+            mir::BinOp::Add | mir::BinOp::Sub | mir::BinOp::Mul | mir::BinOp::Shl | mir::BinOp::Shr
+        ) || !prusti_common::config::check_overflows()
+        {
             Ok(false.into())
         } else {
             let result = self.encode_binary_op_high(op, left, right.clone(), ty)?;
diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/builtin_function_encoder.rs b/prusti-viper/src/encoder/mir/procedures/encoder/builtin_function_encoder.rs
index 70fde0e2809..4f2b3f9d56c 100644
--- a/prusti-viper/src/encoder/mir/procedures/encoder/builtin_function_encoder.rs
+++ b/prusti-viper/src/encoder/mir/procedures/encoder/builtin_function_encoder.rs
@@ -269,7 +269,8 @@ impl<'p, 'v, 'tcx> BuiltinFuncAppEncoder<'p, 'v, 'tcx> for super::ProcedureEncod
                 if matches!(
                     lhs.get_type(),
                     vir_high::Type::Reference(vir_high::ty::Reference {
-                        target_type: box vir_high::Type::Int(vir_high::ty::Int::Unbounded)
+                        target_type:
+                            box vir_high::Type::Int(vir_high::ty::Int::Unbounded)
                             | box vir_high::Type::Sequence(..)
                             | box vir_high::Type::Map(..),
                         ..
diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_dataflow.rs b/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_dataflow.rs
index 02a48722131..ae27c065786 100644
--- a/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_dataflow.rs
+++ b/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_dataflow.rs
@@ -14,6 +14,7 @@
 use log::debug;
 use prusti_interface::environment::mir_body::patch::MirPatch;
 use prusti_rustc_interface::{
+    abi::FieldIdx,
     dataflow::elaborate_drops::{DropFlagMode, DropStyle, Unwind},
     hir,
     hir::lang_items::LangItem,
@@ -95,7 +96,7 @@ pub trait DropElaborator<'a, 'tcx>: fmt::Debug {
     /// Returns the subpath of a field of `path` (or `None` if there is no dedicated subpath).
     ///
     /// If this returns `None`, `field` will not get a dedicated drop flag.
-    fn field_subpath(&self, path: Self::Path, field: Field) -> Option<Self::Path>;
+    fn field_subpath(&self, path: Self::Path, field: FieldIdx) -> Option<Self::Path>;
 
     /// Returns the subpath of a dereference of `path` (or `None` if there is no dedicated subpath).
     ///
@@ -243,7 +244,7 @@ where
             .iter()
             .enumerate()
             .map(|(i, f)| {
-                let field = Field::new(i);
+                let field = FieldIdx::from_usize(i);
                 let subpath = self.elaborator.field_subpath(variant_path, field);
                 let tcx = self.tcx();
 
@@ -383,8 +384,10 @@ where
             .enumerate()
             .map(|(i, &ty)| {
                 (
-                    self.tcx().mk_place_field(self.place, Field::new(i), ty),
-                    self.elaborator.field_subpath(self.path, Field::new(i)),
+                    self.tcx()
+                        .mk_place_field(self.place, FieldIdx::from_usize(i), ty),
+                    self.elaborator
+                        .field_subpath(self.path, FieldIdx::from_usize(i)),
                 )
             })
             .collect();
@@ -981,7 +984,7 @@ where
             .iter()
             .enumerate()
             .map(|(i, f)| {
-                let field = Field::new(i);
+                let field = FieldIdx::from_usize(i);
                 let field_ty = f.ty(tcx, substs);
                 Operand::Move(tcx.mk_place_field(self.place, field, field_ty))
             })
diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_transform.rs b/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_transform.rs
index bf931ee50fc..b8f2bbb33a7 100644
--- a/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_transform.rs
+++ b/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_transform.rs
@@ -14,6 +14,7 @@ use super::mir_dataflow::{elaborate_drop, DropElaborator};
 use log::debug;
 use prusti_interface::environment::mir_body::patch::MirPatch;
 use prusti_rustc_interface::{
+    abi::FieldIdx,
     data_structures::fx::FxHashMap,
     dataflow::{
         elaborate_drops::{DropFlagMode, DropFlagState, DropStyle, Unwind},
@@ -142,11 +143,6 @@ pub(in super::super) fn remove_dead_unwinds<'tcx>(
                 ref place,
                 unwind: Some(_),
                 ..
-            }
-            | TerminatorKind::DropAndReplace {
-                ref place,
-                unwind: Some(_),
-                ..
             } => und.derefer(place.as_ref(), body).unwrap_or(*place),
             _ => continue,
         };
@@ -277,7 +273,7 @@ impl<'a, 'tcx> DropElaborator<'a, 'tcx> for Elaborator<'a, '_, 'tcx> {
         }
     }
 
-    fn field_subpath(&self, path: Self::Path, field: Field) -> Option<Self::Path> {
+    fn field_subpath(&self, path: Self::Path, field: FieldIdx) -> Option<Self::Path> {
         prusti_rustc_interface::dataflow::move_path_children_matching(
             self.ctxt.move_data(),
             path,
@@ -389,8 +385,7 @@ impl<'b, 'tcx> ElaborateDropsCtxt<'b, 'tcx> {
             }
             let terminator = data.terminator();
             let place = match terminator.kind {
-                TerminatorKind::Drop { ref place, .. }
-                | TerminatorKind::DropAndReplace { ref place, .. } => self
+                TerminatorKind::Drop { ref place, .. } => self
                     .un_derefer
                     .derefer(place.as_ref(), self.body)
                     .unwrap_or(*place),
@@ -498,130 +493,11 @@ impl<'b, 'tcx> ElaborateDropsCtxt<'b, 'tcx> {
                         }
                     }
                 }
-                TerminatorKind::DropAndReplace {
-                    mut place,
-                    ref value,
-                    target,
-                    unwind,
-                } => {
-                    assert!(!data.is_cleanup);
-
-                    if let Some(new_place) = self.un_derefer.derefer(place.as_ref(), self.body) {
-                        place = new_place;
-                    }
-                    self.elaborate_replace(loc, place, value, target, unwind);
-                }
                 _ => continue,
             }
         }
     }
 
-    /// Elaborate a MIR `replace` terminator. This instruction
-    /// is not directly handled by codegen, and therefore
-    /// must be desugared.
-    ///
-    /// The desugaring drops the location if needed, and then writes
-    /// the value (including setting the drop flag) over it in *both* arms.
-    ///
-    /// The `replace` terminator can also be called on places that
-    /// are not tracked by elaboration (for example,
-    /// `replace x[i] <- tmp0`). The borrow checker requires that
-    /// these locations are initialized before the assignment,
-    /// so we just generate an unconditional drop.
-    fn elaborate_replace(
-        &mut self,
-        loc: Location,
-        place: Place<'tcx>,
-        value: &Operand<'tcx>,
-        target: BasicBlock,
-        unwind: Option<BasicBlock>,
-    ) {
-        let bb = loc.block;
-        let data = &self.body[bb];
-        let terminator = data.terminator();
-        assert!(
-            !data.is_cleanup,
-            "DropAndReplace in unwind path not supported"
-        );
-
-        let assign = Statement {
-            kind: StatementKind::Assign(Box::new((place, Rvalue::Use(value.clone())))),
-            source_info: terminator.source_info,
-        };
-
-        let unwind = unwind.unwrap_or_else(|| self.patch.resume_block());
-        let unwind = self.patch.new_block(BasicBlockData {
-            statements: vec![assign.clone()],
-            terminator: Some(Terminator {
-                kind: TerminatorKind::Goto { target: unwind },
-                ..*terminator
-            }),
-            is_cleanup: true,
-        });
-
-        let target = self.patch.new_block(BasicBlockData {
-            statements: vec![assign],
-            terminator: Some(Terminator {
-                kind: TerminatorKind::Goto { target },
-                ..*terminator
-            }),
-            is_cleanup: false,
-        });
-
-        match self.move_data().rev_lookup.find(place.as_ref()) {
-            LookupResult::Exact(path) => {
-                debug!(
-                    "elaborate_drop_and_replace({:?}) - tracked {:?}",
-                    terminator, path
-                );
-                self.init_data.seek_before(loc);
-                elaborate_drop(
-                    &mut Elaborator { ctxt: self },
-                    terminator.source_info,
-                    place,
-                    path,
-                    target,
-                    Unwind::To(unwind),
-                    bb,
-                );
-                on_all_children_bits(self.tcx, self.body, self.move_data(), path, |child| {
-                    self.set_drop_flag(
-                        Location {
-                            block: target,
-                            statement_index: 0,
-                        },
-                        child,
-                        DropFlagState::Present,
-                    );
-                    self.set_drop_flag(
-                        Location {
-                            block: unwind,
-                            statement_index: 0,
-                        },
-                        child,
-                        DropFlagState::Present,
-                    );
-                });
-            }
-            LookupResult::Parent(parent) => {
-                // drop and replace behind a pointer/array/whatever. The location
-                // must be initialized.
-                debug!(
-                    "elaborate_drop_and_replace({:?}) - untracked {:?}",
-                    terminator, parent
-                );
-                self.patch.patch_terminator(
-                    bb,
-                    TerminatorKind::Drop {
-                        place,
-                        target,
-                        unwind: Some(unwind),
-                    },
-                );
-            }
-        }
-    }
-
     fn constant_bool(&self, span: Span, val: bool) -> Rvalue<'tcx> {
         Rvalue::Use(Operand::Constant(Box::new(Constant {
             span,
@@ -700,22 +576,12 @@ impl<'b, 'tcx> ElaborateDropsCtxt<'b, 'tcx> {
             debug!("drop_flags_for_locs({:?})", data);
             for i in 0..(data.statements.len() + 1) {
                 debug!("drop_flag_for_locs: stmt {}", i);
-                let mut allow_initializations = true;
                 if i == data.statements.len() {
                     match data.terminator().kind {
                         TerminatorKind::Drop { .. } => {
                             // drop elaboration should handle that by itself
                             continue;
                         }
-                        TerminatorKind::DropAndReplace { .. } => {
-                            // this contains the move of the source and
-                            // the initialization of the destination. We
-                            // only want the former - the latter is handled
-                            // by the elaboration code and must be done
-                            // *after* the destination is dropped.
-                            assert!(self.patch.is_patched(bb));
-                            allow_initializations = false;
-                        }
                         TerminatorKind::Resume => {
                             // It is possible for `Resume` to be patched
                             // (in particular it can be patched to be replaced with
@@ -735,11 +601,7 @@ impl<'b, 'tcx> ElaborateDropsCtxt<'b, 'tcx> {
                     self.body,
                     self.env,
                     loc,
-                    |path, ds| {
-                        if ds == DropFlagState::Absent || allow_initializations {
-                            self.set_drop_flag(loc, path, ds)
-                        }
-                    },
+                    |path, ds| self.set_drop_flag(loc, path, ds),
                 )
             }
 
diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/mod.rs b/prusti-viper/src/encoder/mir/procedures/encoder/mod.rs
index 68ad418a783..6013c273f81 100644
--- a/prusti-viper/src/encoder/mir/procedures/encoder/mod.rs
+++ b/prusti-viper/src/encoder/mir/procedures/encoder/mod.rs
@@ -857,7 +857,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                     assert!(ty.is_union());
                     let adt_def = tcx.adt_def(*adt_did);
                     let variant_def = adt_def.non_enum_variant();
-                    let field_name = variant_def.fields[*active_field_index]
+                    let field_name = variant_def.fields[(*active_field_index).into()]
                         .ident(tcx)
                         .to_string();
                     ty = ty.variant(field_name.into());
diff --git a/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_high.rs b/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_high.rs
index 24299d94ddb..44f37bc2bdd 100644
--- a/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_high.rs
+++ b/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_high.rs
@@ -940,8 +940,6 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx>
                 self.apply_switch_int_terminator(switch_ty, discr, targets, states, span)?
             }
 
-            TerminatorKind::DropAndReplace { .. } => unimplemented!(),
-
             TerminatorKind::Call {
                 args,
                 destination,
@@ -1054,7 +1052,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx>
         match &statement.kind {
             mir::StatementKind::StorageLive(..)
             | mir::StatementKind::StorageDead(..)
-            | mir::StatementKind::FakeRead(..) => {
+            | mir::StatementKind::FakeRead(..)
+            | mir::StatementKind::PlaceMention(..) => {
                 // Nothing to do
             }
             mir::StatementKind::Assign(box (lhs, rhs)) => {
diff --git a/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_poly.rs b/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_poly.rs
index d5f2c6fa481..a660f2146e4 100644
--- a/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_poly.rs
+++ b/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_poly.rs
@@ -156,7 +156,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionBackwardInterpreter<'p, 'v, 'tcx> {
             PlaceEncoding::Variant { box base, field } => {
                 let postprocessed_base = self.postprocess_place_encoding(base)?;
                 vir::Expr::Variant(vir::Variant {
-                    base: box postprocessed_base,
+                    base: Box::new(postprocessed_base),
                     variant_index: field,
                     position: vir::Position::default(),
                 })
@@ -785,8 +785,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx>
                 }
             }
 
-            TerminatorKind::DropAndReplace { .. }
-            | TerminatorKind::Yield { .. }
+            TerminatorKind::Yield { .. }
             | TerminatorKind::GeneratorDrop
             | TerminatorKind::InlineAsm { .. } => {
                 return Err(SpannedEncodingError::internal(
@@ -832,6 +831,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx>
             // | mir::StatementKind::ReadForMatch(..)
             // | mir::StatementKind::EndRegion(..)
             | mir::StatementKind::AscribeUserType(..)
+            | mir::StatementKind::PlaceMention(..)
              => {
                 // Nothing to do
             }
@@ -1023,7 +1023,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx>
                                 let encoded_elem_ty = self.encoder.encode_snapshot_type(elem_ty)
                                     .with_span(span)?;
                                 let elems = vir::Expr::Seq( vir::Seq {
-                                    typ: vir::Type::Seq( vir::SeqType {typ: box encoded_elem_ty} ),
+                                    typ: vir::Type::Seq( vir::SeqType {typ: Box::new(encoded_elem_ty)} ),
                                     elements: encoded_operands,
                                     position: vir::Position::default(),
                                 });
@@ -1256,7 +1256,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx>
                         let encoded_elem_ty = self.encoder.encode_snapshot_type(elem_ty)
                             .with_span(span)?;
                         let elems = vir::Expr::Seq(vir::Seq {
-                            typ: vir::Type::Seq(vir::SeqType{ typ: box encoded_elem_ty }),
+                            typ: vir::Type::Seq(vir::SeqType{ typ: Box::new(encoded_elem_ty) }),
                             elements: (0..len).map(|_| encoded_operand.clone()).collect(),
                             position: vir::Position::default(),
                         });
diff --git a/prusti-viper/src/encoder/mir/types/interface.rs b/prusti-viper/src/encoder/mir/types/interface.rs
index 738aee05447..1b26bdf00b8 100644
--- a/prusti-viper/src/encoder/mir/types/interface.rs
+++ b/prusti-viper/src/encoder/mir/types/interface.rs
@@ -5,6 +5,7 @@ use crate::encoder::{
     mir::types::interface::ty::SubstsRef,
 };
 use prusti_rustc_interface::{
+    abi::FieldIdx,
     errors::MultiSpan,
     middle::{mir, ty},
     span::Span,
@@ -33,7 +34,7 @@ pub(crate) trait MirTypeEncoderInterface<'tcx> {
     fn encode_field(
         &self,
         ty: &vir_high::Type,
-        index: mir::Field,
+        index: FieldIdx,
         use_span: Option<Span>,
         declaration_span: Span,
     ) -> SpannedEncodingResult<vir_high::FieldDecl>;
@@ -119,7 +120,7 @@ impl<'v, 'tcx: 'v> MirTypeEncoderInterface<'tcx> for super::super::super::Encode
     fn encode_field(
         &self,
         ty: &vir_high::Type,
-        field: mir::Field,
+        field: FieldIdx,
         use_span: Option<Span>,
         declaration_span: Span,
     ) -> SpannedEncodingResult<vir_high::FieldDecl> {
diff --git a/prusti-viper/src/encoder/mir_encoder/mod.rs b/prusti-viper/src/encoder/mir_encoder/mod.rs
index 665eb2c6b17..7be46484647 100644
--- a/prusti-viper/src/encoder/mir_encoder/mod.rs
+++ b/prusti-viper/src/encoder/mir_encoder/mod.rs
@@ -142,7 +142,7 @@ pub trait PlaceEncoder<'v, 'tcx: 'v> {
                         } else {
                             encoded_base
                         };
-                        let field = &variant_def.fields[field.index()];
+                        let field = &variant_def.fields[*field];
                         let field_ty = *proj_field_ty;
                         if utils::is_reference(field_ty) {
                             error_unsupported!("access to reference-typed fields is not supported");
@@ -245,7 +245,7 @@ pub trait PlaceEncoder<'v, 'tcx: 'v> {
                     ty::TyKind::Array(elem_ty, _) => {
                         (
                             PlaceEncoding::ArrayAccess {
-                                base: box encoded_base,
+                                base: Box::new(encoded_base),
                                 index,
                                 encoded_elem_ty: self.encoder().encode_type(*elem_ty)?,
                                 rust_array_ty: base_ty,
@@ -257,7 +257,7 @@ pub trait PlaceEncoder<'v, 'tcx: 'v> {
                     ty::TyKind::Slice(elem_ty) => {
                         (
                             PlaceEncoding::SliceAccess {
-                                base: box encoded_base,
+                                base: Box::new(encoded_base),
                                 index,
                                 encoded_elem_ty: self.encoder().encode_type(*elem_ty)?,
                                 rust_slice_ty: base_ty,
@@ -552,7 +552,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> MirEncoder<'p, 'v, 'tcx> {
         right: vir::Expr,
         ty: ty::Ty<'tcx>,
     ) -> EncodingResult<vir::Expr> {
-        if !op.is_checkable() || !config::check_overflows() {
+        if !matches!(op, mir::BinOp::Add | mir::BinOp::Sub | mir::BinOp::Mul | mir::BinOp::Shl | mir::BinOp::Shr) || !config::check_overflows() {
             Ok(false.into())
         } else {
             let result = self.encode_bin_op_expr(op, left, right.clone(), ty)?;
diff --git a/prusti-viper/src/encoder/mir_encoder/place_encoding.rs b/prusti-viper/src/encoder/mir_encoder/place_encoding.rs
index 4147202ca51..23af5ecdb89 100644
--- a/prusti-viper/src/encoder/mir_encoder/place_encoding.rs
+++ b/prusti-viper/src/encoder/mir_encoder/place_encoding.rs
@@ -80,7 +80,7 @@ impl<'tcx> PlaceEncoding<'tcx> {
             PlaceEncoding::Variant { base, field } => {
                 match base.into_array_base() {
                     ExprOrArrayBase::Expr(e) => ExprOrArrayBase::Expr(
-                        vir::Expr::Variant( vir::Variant {base: box e, variant_index: field, position: vir::Position::default()} )
+                        vir::Expr::Variant( vir::Variant {base: Box::new(e), variant_index: field, position: vir::Position::default()} )
                     ),
                     base@ExprOrArrayBase::ArrayBase(_) => base,
                     base@ExprOrArrayBase::SliceBase(_) => base,
@@ -106,7 +106,7 @@ impl<'tcx> PlaceEncoding<'tcx> {
     }
 
     pub fn field(self, field: vir::Field) -> Self {
-        PlaceEncoding::FieldAccess { base: box self, field }
+        PlaceEncoding::FieldAccess { base: Box::new(self), field }
     }
 
     pub fn get_type(&self) -> &vir::Type {
@@ -124,7 +124,7 @@ impl<'tcx> PlaceEncoding<'tcx> {
         let field_name = format!("enum_{index}");
         let field = vir::Field::new(field_name, self.get_type().clone().variant(index));
 
-        PlaceEncoding::Variant { base: box self, field }
+        PlaceEncoding::Variant { base: Box::new(self), field }
     }
 }
 
diff --git a/prusti-viper/src/encoder/mirror_function_encoder.rs b/prusti-viper/src/encoder/mirror_function_encoder.rs
index e04ccb15bfd..1c09951cc30 100644
--- a/prusti-viper/src/encoder/mirror_function_encoder.rs
+++ b/prusti-viper/src/encoder/mirror_function_encoder.rs
@@ -76,7 +76,7 @@ impl MirrorEncoder {
         // add postcondition to the original function
         // [result == mirror(args), true]
         function.posts.push(vir::Expr::InhaleExhale( vir::InhaleExhale {
-            inhale_expr: box vir::Expr::eq_cmp(
+            inhale_expr: Box::new(vir::Expr::eq_cmp(
                 vir::Expr::local(
                     vir::LocalVar::new("__result", function.return_type.clone()),
                 ),
@@ -87,8 +87,8 @@ impl MirrorEncoder {
                         .map(vir::Expr::local)
                         .collect(),
                 ),
-            ),
-            exhale_expr: box true.into(),
+            )),
+            exhale_expr: Box::new(true.into()),
             position: vir::Position::default(),
         }));
 
diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs
index 6d823998555..34c8992a83c 100644
--- a/prusti-viper/src/encoder/procedure_encoder.rs
+++ b/prusti-viper/src/encoder/procedure_encoder.rs
@@ -1453,6 +1453,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             | mir::StatementKind::FakeRead(..)
             | mir::StatementKind::AscribeUserType(..)
             | mir::StatementKind::Coverage(..)
+            | mir::StatementKind::PlaceMention(..)
             | mir::StatementKind::Nop => vec![],
 
             mir::StatementKind::Assign(box (lhs, ref rhs)) => {
@@ -2182,8 +2183,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 );
                 // Inhale the magic wand.
                 let magic_wand = vir::Expr::MagicWand( vir::MagicWand {
-                    left: box lhs.clone(),
-                    right: box rhs.clone(),
+                    left: Box::new(lhs.clone()),
+                    right: Box::new(rhs.clone()),
                     borrow: Some(loan.index().into()),
                     position: pos,
                 });
@@ -2454,20 +2455,6 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 (stmts, MirSuccessor::Goto(real_target))
             }
 
-            TerminatorKind::DropAndReplace {
-                target,
-                place: lhs,
-                ref value,
-                ..
-            } => {
-                let (encoded_lhs, pre_stmts, _, _) = self.encode_place(lhs, ArrayAccessKind::Mutable(None, location), location)?;
-                stmts.extend(pre_stmts);
-                stmts.extend(
-                    self.encode_assign_operand(&encoded_lhs, value, location)?
-                );
-                (stmts, MirSuccessor::Goto(target))
-            }
-
             TerminatorKind::Call {
                 ref args,
                 destination,
@@ -5003,8 +4990,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         let tmp_var = self.get_pure_var_for_preserving_value(loop_head, place);
         vir::Expr::BinOp ( vir::BinOp {
             op_kind: vir::BinaryOpKind::EqCmp,
-            left: box tmp_var.into(),
-            right: box place.clone(),
+            left: Box::new(tmp_var.into()),
+            right: Box::new(place.clone()),
             position: vir::Position::default(),
         })
     }
@@ -6215,14 +6202,14 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         let val_ref_field = self.encoder.encode_value_field(ty).with_span(span)?;
         let slice_expr = encoded_lhs.field(val_ref_field);
         stmts.push(vir_stmt!{ inhale [vir::Expr::FieldAccessPredicate( vir::FieldAccessPredicate {
-            base: box slice_expr.clone(),
+            base: Box::new(slice_expr.clone()),
             permission: vir::PermAmount::Write,
             position: vir::Position::default(),
         })]});
 
         let slice_perm = vir::Expr::PredicateAccessPredicate( vir::PredicateAccessPredicate {
             predicate_type: slice_types.sequence_pred_type.clone(),
-            argument: box slice_expr.clone(),
+            argument: Box::new(slice_expr.clone()),
             permission: if is_mut { vir::PermAmount::Write } else { vir::PermAmount::Read },
             position: vir::Position::default(),
         });
@@ -6960,7 +6947,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
             PlaceEncoding::Variant { box base, field } => {
                 let (expr, stmts) = self.postprocess_place_encoding(base, array_encode_kind)?;
                 (vir::Expr::Variant( vir::Variant {
-                    base: box expr,
+                    base: Box::new(expr),
                     variant_index: field,
                     position: vir::Position::default(),
                 }),
diff --git a/prusti-viper/src/encoder/snapshot/encoder.rs b/prusti-viper/src/encoder/snapshot/encoder.rs
index 2e557ab10d0..7f72c402ebc 100644
--- a/prusti-viper/src/encoder/snapshot/encoder.rs
+++ b/prusti-viper/src/encoder/snapshot/encoder.rs
@@ -812,7 +812,7 @@ impl SnapshotEncoder {
                 let domain_name = format!("Snap${}", &array_types.sequence_pred_type.name());
                 let snap_type = array_types.sequence_pred_type.convert_to_snapshot();
                 let seq_type = Type::Seq(vir::SeqType {
-                    typ: box elem_snap_ty.clone(),
+                    typ: Box::new(elem_snap_ty.clone()),
                 });
 
                 let cons = vir::DomainFunc {
@@ -963,8 +963,8 @@ impl SnapshotEncoder {
 
                     let seq_lookup = Expr::ContainerOp(vir::ContainerOp {
                         op_kind: ContainerOpKind::SeqIndex,
-                        left: box data.clone().into(),
-                        right: box idx.clone().into(),
+                        left: Box::new(data.clone().into()),
+                        right: Box::new(idx.clone().into()),
                         position: vir::Position::default(),
                     });
                     vir::DomainAxiom {
@@ -1042,7 +1042,7 @@ impl SnapshotEncoder {
                 let slice_snap_ty = slice_types.sequence_pred_type.convert_to_snapshot();
                 let elem_snap_ty = self.encode_type(encoder, *elem_ty)?;
                 let seq_type = Type::Seq(vir::SeqType {
-                    typ: box elem_snap_ty.clone(),
+                    typ: Box::new(elem_snap_ty.clone()),
                 });
 
                 let cons = vir::DomainFunc {
@@ -1132,13 +1132,13 @@ impl SnapshotEncoder {
                     )],
                     posts: vec![
                         Expr::InhaleExhale(vir::InhaleExhale {
-                            inhale_expr: box read_eq_lookup,
-                            exhale_expr: box true.into(),
+                            inhale_expr: Box::new(read_eq_lookup),
+                            exhale_expr: Box::new(true.into()),
                             position: vir::Position::default(),
                         }),
                         Expr::InhaleExhale(vir::InhaleExhale {
-                            inhale_expr: box snap_len_eq_call_len,
-                            exhale_expr: box true.into(),
+                            inhale_expr: Box::new(snap_len_eq_call_len),
+                            exhale_expr: Box::new(true.into()),
                             position: vir::Position::default(),
                         }),
                     ],
@@ -1218,8 +1218,8 @@ impl SnapshotEncoder {
 
                     let seq_lookup = Expr::ContainerOp(vir::ContainerOp {
                         op_kind: ContainerOpKind::SeqIndex,
-                        left: box data.clone().into(),
-                        right: box idx.clone().into(),
+                        left: Box::new(data.clone().into()),
+                        right: Box::new(idx.clone().into()),
                         position: vir::Position::default(),
                     });
 
@@ -1242,8 +1242,8 @@ impl SnapshotEncoder {
                     let len_call = len.apply(vec![cons_call]);
                     let seq_len = Expr::ContainerOp(vir::ContainerOp {
                         op_kind: ContainerOpKind::SeqLen,
-                        left: box data.into(),
-                        right: box true.into(), // unused
+                        left: Box::new(data.into()),
+                        right: Box::new(true.into()), // unused
                         position: vir::Position::default(),
                     });
 
@@ -1374,7 +1374,7 @@ impl SnapshotEncoder {
 
         let self_expr: Expr = vir_local! { self: {seq_pred_ty.clone()} }.into();
         let seq_type = Type::Seq(vir::SeqType {
-            typ: box elem_snap_ty.clone(),
+            typ: Box::new(elem_snap_ty.clone()),
         });
         let start = vir_local! { start: Int };
         let start_expr: Expr = start.clone().into();
@@ -1392,20 +1392,20 @@ impl SnapshotEncoder {
         let start_lt_len = vir_expr! { [start_expr] < [seq_len] };
         let result_len = Expr::ContainerOp(vir::ContainerOp {
             op_kind: ContainerOpKind::SeqLen,
-            left: box result_expr.clone(),
-            right: box Expr::from(0),
+            left: Box::new(result_expr.clone()),
+            right: Box::new(Expr::from(0)),
             position: vir::Position::default(),
         });
         let result_0 = Expr::ContainerOp(vir::ContainerOp {
             op_kind: ContainerOpKind::SeqIndex,
-            left: box result_expr.clone(),
-            right: box Expr::from(0),
+            left: Box::new(result_expr.clone()),
+            right: Box::new(Expr::from(0)),
             position: vir::Position::default(),
         });
         let result_j = Expr::ContainerOp(vir::ContainerOp {
             op_kind: ContainerOpKind::SeqIndex,
-            left: box result_expr.clone(),
-            right: box j_expr.clone(),
+            left: Box::new(result_expr.clone()),
+            right: Box::new(j_expr.clone()),
             position: vir::Position::default(),
         });
         let slice_lookup_i = lookup_pure(self_expr.clone(), i_expr.clone(), elem_snap_ty.clone());
@@ -1456,7 +1456,7 @@ impl SnapshotEncoder {
                 }),
                 Expr::ContainerOp(vir::ContainerOp {
                     op_kind: ContainerOpKind::SeqConcat,
-                    left: box Expr::Seq(vir::Seq {
+                    left: Box::new(Expr::Seq(vir::Seq {
                         typ: seq_type.clone(),
                         elements: vec![lookup_pure(
                             self_expr.clone(),
@@ -1464,15 +1464,15 @@ impl SnapshotEncoder {
                             elem_snap_ty,
                         )],
                         position: vir::Position::default(),
-                    }),
-                    right: box Expr::func_app(
+                    })),
+                    right: Box::new(Expr::func_app(
                         seq_collect_funcname,
                         Vec::new(), // FIXME: This is most likely wrong.
                         vec![self_expr, vir_expr! { [start_expr] + [Expr::from(1)] }],
                         vec![vir_local! { slice: {seq_pred_ty} }, start],
                         seq_type,
                         vir::Position::default(),
-                    ),
+                    )),
                     position: vir::Position::default(),
                 }),
             )),
@@ -1490,7 +1490,7 @@ impl SnapshotEncoder {
 
         let self_expr: Expr = vir_local! { self: {self_snap_ty.clone()} }.into();
         let seq_type = Type::Seq(vir::SeqType {
-            typ: box elem_snap_ty.clone(),
+            typ: Box::new(elem_snap_ty),
         });
 
         let lo = vir_local! { lo: Int };
@@ -1506,20 +1506,20 @@ impl SnapshotEncoder {
 
         let result_len = Expr::ContainerOp(vir::ContainerOp {
             op_kind: ContainerOpKind::SeqLen,
-            left: box result_expr.clone(),
-            right: box Expr::from(0),
+            left: Box::new(result_expr.clone()),
+            right: Box::new(Expr::from(0)),
             position: vir::Position::default(),
         });
         let result_0 = Expr::ContainerOp(vir::ContainerOp {
             op_kind: ContainerOpKind::SeqIndex,
-            left: box result_expr.clone(),
-            right: box Expr::from(0),
+            left: Box::new(result_expr.clone()),
+            right: Box::new(Expr::from(0)),
             position: vir::Position::default(),
         });
         let result_j = Expr::ContainerOp(vir::ContainerOp {
             op_kind: ContainerOpKind::SeqIndex,
-            left: box result_expr.clone(),
-            right: box j_expr.clone(),
+            left: Box::new(result_expr),
+            right: Box::new(j_expr.clone()),
             position: vir::Position::default(),
         });
 
@@ -1566,12 +1566,12 @@ impl SnapshotEncoder {
                 }),
                 Expr::ContainerOp(vir::ContainerOp {
                     op_kind: ContainerOpKind::SeqConcat,
-                    left: box Expr::Seq(vir::Seq {
+                    left: Box::new(Expr::Seq(vir::Seq {
                         typ: seq_type.clone(),
                         elements: vec![read_lo],
                         position: vir::Position::default(),
-                    }),
-                    right: box Expr::func_app(
+                    })),
+                    right: Box::new(Expr::func_app(
                         slice_helper_name,
                         vec![self_snap_ty.clone()],
                         vec![
@@ -1582,7 +1582,7 @@ impl SnapshotEncoder {
                         vec![vir_local! { slice: {self_snap_ty} }, lo, hi],
                         seq_type,
                         vir::Position::default(),
-                    ),
+                    )),
                     position: vir::Position::default(),
                 }),
             )),
diff --git a/prusti-viper/src/encoder/snapshot/patcher.rs b/prusti-viper/src/encoder/snapshot/patcher.rs
index 66fb5a21f9e..e4dac602369 100644
--- a/prusti-viper/src/encoder/snapshot/patcher.rs
+++ b/prusti-viper/src/encoder/snapshot/patcher.rs
@@ -115,11 +115,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> FallibleExprFolder for SnapshotPatcher<'p, 'v, 'tcx>
                         field,
                     ),
                     _ => Ok(vir::Expr::Field(vir::FieldExpr {
-                        base: box vir::Expr::Variant(vir::Variant {
+                        base: Box::new(vir::Expr::Variant(vir::Variant {
                             base: receiver,
                             variant_index: variant,
                             position: pos2,
-                        }),
+                        })),
                         field,
                         position,
                     })),
@@ -163,7 +163,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> FallibleExprFolder for SnapshotPatcher<'p, 'v, 'tcx>
         Ok(vir::Expr::ForAll(vir::ForAll {
             variables: patched_vars,
             triggers,
-            body: box expr,
+            body: Box::new(expr),
             position,
         }))
     }
@@ -181,7 +181,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> FallibleExprFolder for SnapshotPatcher<'p, 'v, 'tcx>
         Ok(vir::Expr::Exists(vir::Exists {
             variables: patched_vars,
             triggers,
-            body: box expr,
+            body: Box::new(expr),
             position,
         }))
     }
@@ -200,8 +200,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> FallibleExprFolder for SnapshotPatcher<'p, 'v, 'tcx>
             Ok(base)
         } else {
             Ok(vir::Expr::Downcast(vir::DowncastExpr {
-                base: box base,
-                enum_place: box enum_expr,
+                base: Box::new(base),
+                enum_place: Box::new(enum_expr),
                 field,
             }))
         }
diff --git a/prusti-viper/src/lib.rs b/prusti-viper/src/lib.rs
index f423994ada7..77d9f8a80c3 100644
--- a/prusti-viper/src/lib.rs
+++ b/prusti-viper/src/lib.rs
@@ -6,7 +6,6 @@
 
 #![feature(rustc_private)]
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 #![feature(try_blocks)]
 #![feature(never_type)]
 #![feature(btree_drain_filter)]
diff --git a/prusti/src/driver.rs b/prusti/src/driver.rs
index 8f11f730094..729476a40d6 100644
--- a/prusti/src/driver.rs
+++ b/prusti/src/driver.rs
@@ -7,7 +7,6 @@
 #![feature(rustc_private)]
 #![feature(proc_macro_internals)]
 #![feature(decl_macro)]
-#![feature(box_syntax)]
 #![deny(unused_must_use)]
 
 mod arg_value;
@@ -30,7 +29,7 @@ const BUG_REPORT_URL: &str = "https://github.com/viperproject/prusti-dev/issues/
 lazy_static! {
     static ref ICE_HOOK: Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static> = {
         let hook = panic::take_hook();
-        panic::set_hook(box |info| report_prusti_ice(info, BUG_REPORT_URL));
+        panic::set_hook(Box::new(|info| report_prusti_ice(info, BUG_REPORT_URL)));
         hook
     };
 }
@@ -57,17 +56,19 @@ fn report_prusti_ice(info: &panic::PanicInfo<'_>, bug_report_url: &str) {
         prusti_rustc_interface::driver::DEFAULT_LOCALE_RESOURCES.to_vec(),
         false,
     );
-    let emitter = box prusti_rustc_interface::errors::emitter::EmitterWriter::stderr(
-        prusti_rustc_interface::errors::ColorConfig::Auto,
-        None,
-        None,
-        fallback_bundle,
-        false,
-        false,
-        None,
-        false,
-        false,
-        prusti_rustc_interface::errors::TerminalUrl::Auto,
+    let emitter = Box::new(
+        prusti_rustc_interface::errors::emitter::EmitterWriter::stderr(
+            prusti_rustc_interface::errors::ColorConfig::Auto,
+            None,
+            None,
+            fallback_bundle,
+            false,
+            false,
+            None,
+            false,
+            false,
+            prusti_rustc_interface::errors::TerminalUrl::Auto,
+        ),
     );
     let handler = prusti_rustc_interface::errors::Handler::with_emitter(true, None, emitter);
 
diff --git a/rust-toolchain b/rust-toolchain
index 638d203885a..dba307748c3 100644
--- a/rust-toolchain
+++ b/rust-toolchain
@@ -1,4 +1,4 @@
 [toolchain]
-channel = "nightly-2023-03-08"
+channel = "nightly-2023-04-01"
 components = [ "rustc-dev", "llvm-tools-preview", "rust-std", "rustfmt", "clippy" ]
 profile = "minimal"
diff --git a/test-crates/src/main.rs b/test-crates/src/main.rs
index ec61eddfb13..c8a21a42cc3 100644
--- a/test-crates/src/main.rs
+++ b/test-crates/src/main.rs
@@ -194,6 +194,9 @@ fn main() -> Result<(), Box<dyn Error>> {
     let guest_viper_home = Path::new("/opt/rustwide/viper-home");
     let guest_z3_home = Path::new("/opt/rustwide/z3-home");
     // Map JAVA at exactly the same location on the guest so that symlinks work.
+
+    // clippy false positive (https://github.com/rust-lang/rust-clippy/issues/10577)
+    #[allow(clippy::redundant_clone)]
     let guest_java_home = host_java_home.clone();
 
     info!("Using host's Java home {:?}", host_java_home);
diff --git a/viper-toolchain b/viper-toolchain
index f693ba55360..e29b60ea05b 100644
--- a/viper-toolchain
+++ b/viper-toolchain
@@ -1 +1 @@
-v-2023-03-10-1726
+v-2023-03-29-1448
diff --git a/vir/defs/polymorphic/ast/expr_transformers.rs b/vir/defs/polymorphic/ast/expr_transformers.rs
index c6fe744b85f..3b6cb6ac191 100644
--- a/vir/defs/polymorphic/ast/expr_transformers.rs
+++ b/vir/defs/polymorphic/ast/expr_transformers.rs
@@ -68,7 +68,7 @@ pub trait ExprFolder: Sized {
     }
 
     fn fold_boxed(&mut self, e: Box<Expr>) -> Box<Expr> {
-        box self.fold(*e)
+        Box::new(self.fold(*e))
     }
 
     fn fold_local(&mut self, local: Local) -> Expr {
@@ -739,7 +739,7 @@ pub trait FallibleExprFolder: Sized {
     }
 
     fn fallible_fold_boxed(&mut self, e: Box<Expr>) -> Result<Box<Expr>, Self::Error> {
-        Ok(box self.fallible_fold(*e)?)
+        Ok(Box::new(self.fallible_fold(*e)?))
     }
 
     fn fallible_fold_local(&mut self, local: Local) -> Result<Expr, Self::Error> {
diff --git a/vir/src/legacy/ast/expr.rs b/vir/src/legacy/ast/expr.rs
index 32e2824fc8f..14876f6a800 100644
--- a/vir/src/legacy/ast/expr.rs
+++ b/vir/src/legacy/ast/expr.rs
@@ -450,12 +450,12 @@ impl Expr {
 
     pub fn predicate_access_predicate<S: ToString>(name: S, place: Expr, perm: PermAmount) -> Self {
         let pos = place.pos();
-        Expr::PredicateAccessPredicate(name.to_string(), box place, perm, pos)
+        Expr::PredicateAccessPredicate(name.to_string(), Box::new(place), perm, pos)
     }
 
     pub fn field_access_predicate(place: Expr, perm: PermAmount) -> Self {
         let pos = place.pos();
-        Expr::FieldAccessPredicate(box place, perm, pos)
+        Expr::FieldAccessPredicate(Box::new(place), perm, pos)
     }
 
     pub fn pred_permission(place: Expr, perm: PermAmount) -> Option<Self> {
@@ -465,27 +465,27 @@ impl Expr {
     }
 
     pub fn acc_permission(place: Expr, perm: PermAmount) -> Self {
-        Expr::FieldAccessPredicate(box place, perm, Position::default())
+        Expr::FieldAccessPredicate(Box::new(place), perm, Position::default())
     }
 
     pub fn labelled_old(label: &str, expr: Expr) -> Self {
-        Expr::LabelledOld(label.to_string(), box expr, Position::default())
+        Expr::LabelledOld(label.to_string(), Box::new(expr), Position::default())
     }
 
     #[allow(clippy::should_implement_trait)]
     pub fn not(expr: Expr) -> Self {
-        Expr::UnaryOp(UnaryOpKind::Not, box expr, Position::default())
+        Expr::UnaryOp(UnaryOpKind::Not, Box::new(expr), Position::default())
     }
 
     pub fn minus(expr: Expr) -> Self {
-        Expr::UnaryOp(UnaryOpKind::Minus, box expr, Position::default())
+        Expr::UnaryOp(UnaryOpKind::Minus, Box::new(expr), Position::default())
     }
 
     pub fn gt_cmp(left: Expr, right: Expr) -> Self {
         Expr::BinOp(
             BinaryOpKind::GtCmp,
-            box left,
-            box right,
+            Box::new(left),
+            Box::new(right),
             Position::default(),
         )
     }
@@ -493,8 +493,8 @@ impl Expr {
     pub fn ge_cmp(left: Expr, right: Expr) -> Self {
         Expr::BinOp(
             BinaryOpKind::GeCmp,
-            box left,
-            box right,
+            Box::new(left),
+            Box::new(right),
             Position::default(),
         )
     }
@@ -502,8 +502,8 @@ impl Expr {
     pub fn lt_cmp(left: Expr, right: Expr) -> Self {
         Expr::BinOp(
             BinaryOpKind::LtCmp,
-            box left,
-            box right,
+            Box::new(left),
+            Box::new(right),
             Position::default(),
         )
     }
@@ -511,8 +511,8 @@ impl Expr {
     pub fn le_cmp(left: Expr, right: Expr) -> Self {
         Expr::BinOp(
             BinaryOpKind::LeCmp,
-            box left,
-            box right,
+            Box::new(left),
+            Box::new(right),
             Position::default(),
         )
     }
@@ -520,8 +520,8 @@ impl Expr {
     pub fn eq_cmp(left: Expr, right: Expr) -> Self {
         Expr::BinOp(
             BinaryOpKind::EqCmp,
-            box left,
-            box right,
+            Box::new(left),
+            Box::new(right),
             Position::default(),
         )
     }
@@ -532,26 +532,51 @@ impl Expr {
 
     #[allow(clippy::should_implement_trait)]
     pub fn add(left: Expr, right: Expr) -> Self {
-        Expr::BinOp(BinaryOpKind::Add, box left, box right, Position::default())
+        Expr::BinOp(
+            BinaryOpKind::Add,
+            Box::new(left),
+            Box::new(right),
+            Position::default(),
+        )
     }
 
     #[allow(clippy::should_implement_trait)]
     pub fn sub(left: Expr, right: Expr) -> Self {
-        Expr::BinOp(BinaryOpKind::Sub, box left, box right, Position::default())
+        Expr::BinOp(
+            BinaryOpKind::Sub,
+            Box::new(left),
+            Box::new(right),
+            Position::default(),
+        )
     }
 
     #[allow(clippy::should_implement_trait)]
     pub fn mul(left: Expr, right: Expr) -> Self {
-        Expr::BinOp(BinaryOpKind::Mul, box left, box right, Position::default())
+        Expr::BinOp(
+            BinaryOpKind::Mul,
+            Box::new(left),
+            Box::new(right),
+            Position::default(),
+        )
     }
 
     #[allow(clippy::should_implement_trait)]
     pub fn div(left: Expr, right: Expr) -> Self {
-        Expr::BinOp(BinaryOpKind::Div, box left, box right, Position::default())
+        Expr::BinOp(
+            BinaryOpKind::Div,
+            Box::new(left),
+            Box::new(right),
+            Position::default(),
+        )
     }
 
     pub fn modulo(left: Expr, right: Expr) -> Self {
-        Expr::BinOp(BinaryOpKind::Mod, box left, box right, Position::default())
+        Expr::BinOp(
+            BinaryOpKind::Mod,
+            Box::new(left),
+            Box::new(right),
+            Position::default(),
+        )
     }
 
     #[allow(clippy::should_implement_trait)]
@@ -575,11 +600,21 @@ impl Expr {
     }
 
     pub fn and(left: Expr, right: Expr) -> Self {
-        Expr::BinOp(BinaryOpKind::And, box left, box right, Position::default())
+        Expr::BinOp(
+            BinaryOpKind::And,
+            Box::new(left),
+            Box::new(right),
+            Position::default(),
+        )
     }
 
     pub fn or(left: Expr, right: Expr) -> Self {
-        Expr::BinOp(BinaryOpKind::Or, box left, box right, Position::default())
+        Expr::BinOp(
+            BinaryOpKind::Or,
+            Box::new(left),
+            Box::new(right),
+            Position::default(),
+        )
     }
 
     pub fn xor(left: Expr, right: Expr) -> Self {
@@ -589,8 +624,8 @@ impl Expr {
     pub fn implies(left: Expr, right: Expr) -> Self {
         Expr::BinOp(
             BinaryOpKind::Implies,
-            box left,
-            box right,
+            Box::new(left),
+            Box::new(right),
             Position::default(),
         )
     }
@@ -600,7 +635,7 @@ impl Expr {
             !vars.is_empty(),
             "A quantifier must have at least one variable."
         );
-        Expr::ForAll(vars, triggers, box body, Position::default())
+        Expr::ForAll(vars, triggers, Box::new(body), Position::default())
     }
 
     pub fn exists(vars: Vec<LocalVar>, triggers: Vec<Trigger>, body: Expr) -> Self {
@@ -608,11 +643,16 @@ impl Expr {
             !vars.is_empty(),
             "A quantifier must have at least one variable."
         );
-        Expr::Exists(vars, triggers, box body, Position::default())
+        Expr::Exists(vars, triggers, Box::new(body), Position::default())
     }
 
     pub fn ite(guard: Expr, left: Expr, right: Expr) -> Self {
-        Expr::Cond(box guard, box left, box right, Position::default())
+        Expr::Cond(
+            Box::new(guard),
+            Box::new(left),
+            Box::new(right),
+            Position::default(),
+        )
     }
 
     pub fn unfolding(
@@ -625,7 +665,7 @@ impl Expr {
         Expr::Unfolding(
             pred_name,
             args,
-            box expr,
+            Box::new(expr),
             perm,
             variant,
             Position::default(),
@@ -636,7 +676,14 @@ impl Expr {
     pub fn wrap_in_unfolding(arg: Expr, body: Expr) -> Expr {
         let type_name = arg.get_type().name();
         let pos = body.pos();
-        Expr::Unfolding(type_name, vec![arg], box body, PermAmount::Read, None, pos)
+        Expr::Unfolding(
+            type_name,
+            vec![arg],
+            Box::new(body),
+            PermAmount::Read,
+            None,
+            pos,
+        )
     }
 
     pub fn func_app(
@@ -654,15 +701,15 @@ impl Expr {
     }
 
     pub fn magic_wand(lhs: Expr, rhs: Expr, borrow: Option<Borrow>) -> Self {
-        Expr::MagicWand(box lhs, box rhs, borrow, Position::default())
+        Expr::MagicWand(Box::new(lhs), Box::new(rhs), borrow, Position::default())
     }
 
     pub fn downcast(base: Expr, enum_place: Expr, variant_field: Field) -> Self {
-        Expr::Downcast(box base, box enum_place, variant_field)
+        Expr::Downcast(Box::new(base), Box::new(enum_place), variant_field)
     }
 
     pub fn snap_app(expr: Expr) -> Self {
-        Expr::SnapApp(box expr, Position::default())
+        Expr::SnapApp(Box::new(expr), Position::default())
     }
 
     pub fn find(&self, sub_target: &Expr) -> bool {
@@ -740,8 +787,8 @@ impl Expr {
         components
             .into_iter()
             .fold(self, |acc, component| match component {
-                PlaceComponent::Variant(variant, pos) => Expr::Variant(box acc, variant, pos),
-                PlaceComponent::Field(field, pos) => Expr::Field(box acc, field, pos),
+                PlaceComponent::Variant(variant, pos) => Expr::Variant(Box::new(acc), variant, pos),
+                PlaceComponent::Field(field, pos) => Expr::Field(Box::new(acc), field, pos),
             })
     }
 
@@ -757,18 +804,22 @@ impl Expr {
         let field_name = format!("enum_{index}");
         let typ = self.get_type();
         let variant = Field::new(field_name, typ.clone().variant(index));
-        Expr::Variant(box self, variant, Position::default())
+        Expr::Variant(Box::new(self), variant, Position::default())
     }
 
     #[must_use]
     pub fn field(self, field: Field) -> Self {
-        Expr::Field(box self, field, Position::default())
+        Expr::Field(Box::new(self), field, Position::default())
     }
 
     #[must_use]
     pub fn addr_of(self) -> Self {
         let type_name = self.get_type().name();
-        Expr::AddrOf(box self, Type::TypedRef(type_name), Position::default())
+        Expr::AddrOf(
+            Box::new(self),
+            Type::TypedRef(type_name),
+            Position::default(),
+        )
     }
 
     pub fn is_only_permissions(&self) -> bool {
@@ -908,7 +959,7 @@ impl Expr {
                 */
                 self
             }
-            _ => Expr::LabelledOld(label.to_string(), box self, Position::default()),
+            _ => Expr::LabelledOld(label.to_string(), Box::new(self), Position::default()),
         }
     }
 
@@ -1746,13 +1797,13 @@ impl Expr {
         impl ExprWalker for Collector {
             fn walk_variant(&mut self, e: &Expr, v: &Field, p: &Position) {
                 self.walk(e);
-                let expr = Expr::Variant(box e.clone(), v.clone(), *p);
+                let expr = Expr::Variant(Box::new(e.clone()), v.clone(), *p);
                 let perm = Expr::acc_permission(expr, self.perm_amount);
                 self.perms.push(perm);
             }
             fn walk_field(&mut self, e: &Expr, f: &Field, p: &Position) {
                 self.walk(e);
-                let expr = Expr::Field(box e.clone(), f.clone(), *p);
+                let expr = Expr::Field(Box::new(e.clone()), f.clone(), *p);
                 let perm = Expr::acc_permission(expr, self.perm_amount);
                 self.perms.push(perm);
             }
diff --git a/vir/src/legacy/ast/expr_transformers.rs b/vir/src/legacy/ast/expr_transformers.rs
index aa490dd0e8f..86958617ee2 100644
--- a/vir/src/legacy/ast/expr_transformers.rs
+++ b/vir/src/legacy/ast/expr_transformers.rs
@@ -101,7 +101,7 @@ pub trait ExprFolder: Sized {
 
     #[allow(clippy::boxed_local)]
     fn fold_boxed(&mut self, e: Box<Expr>) -> Box<Expr> {
-        box self.fold(*e)
+        Box::new(self.fold(*e))
     }
 
     fn fold_local(&mut self, v: LocalVar, p: Position) -> Expr {
@@ -653,7 +653,7 @@ pub trait FallibleExprFolder: Sized {
 
     #[allow(clippy::boxed_local)]
     fn fallible_fold_boxed(&mut self, e: Box<Expr>) -> Result<Box<Expr>, Self::Error> {
-        Ok(box self.fallible_fold(*e)?)
+        Ok(Box::new(self.fallible_fold(*e)?))
     }
 
     fn fallible_fold_local(&mut self, v: LocalVar, p: Position) -> Result<Expr, Self::Error> {
diff --git a/vir/src/legacy/ast/predicate.rs b/vir/src/legacy/ast/predicate.rs
index a46bff16904..b752608da41 100644
--- a/vir/src/legacy/ast/predicate.rs
+++ b/vir/src/legacy/ast/predicate.rs
@@ -204,7 +204,7 @@ impl StructPredicate {
     pub fn construct_access(&self, this: Expr, perm_amount: PermAmount) -> Expr {
         Expr::PredicateAccessPredicate(
             self.name.clone(),
-            box this,
+            Box::new(this),
             perm_amount,
             Position::default(),
         )
diff --git a/vir/src/legacy/ast/stmt.rs b/vir/src/legacy/ast/stmt.rs
index 444bbe4988d..6c1e6c36671 100644
--- a/vir/src/legacy/ast/stmt.rs
+++ b/vir/src/legacy/ast/stmt.rs
@@ -287,7 +287,7 @@ impl Stmt {
         pos: Position,
     ) -> Self {
         Stmt::PackageMagicWand(
-            Expr::MagicWand(box lhs, box rhs, None, pos),
+            Expr::MagicWand(Box::new(lhs), Box::new(rhs), None, pos),
             stmts,
             label,
             vars,
diff --git a/vir/src/lib.rs b/vir/src/lib.rs
index 758dff65741..d7caf3f60a9 100644
--- a/vir/src/lib.rs
+++ b/vir/src/lib.rs
@@ -1,5 +1,4 @@
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 #![feature(decl_macro)]
 #![allow(unused_imports)]
 #![deny(unused_must_use)]