From fb69747c323aa41afff467e66b7284b13740e4dc Mon Sep 17 00:00:00 2001
From: hermanventer <herman@endor.ai>
Date: Mon, 1 Jul 2024 10:02:57 -0700
Subject: [PATCH] Update dependencies

---
 .github/workflows/mirai_on_mirai.yml |   4 +-
 .github/workflows/rust.yml           |  32 +--
 Cargo.lock                           | 405 +++++++++++++--------------
 binaries/summary_store.tar           | Bin 3085312 -> 3195904 bytes
 checker/Cargo.toml                   |   9 +-
 checker/src/cargo_mirai.rs           |   4 +-
 checker/src/z3_solver.rs             |   5 +-
 7 files changed, 227 insertions(+), 232 deletions(-)

diff --git a/.github/workflows/mirai_on_mirai.yml b/.github/workflows/mirai_on_mirai.yml
index 536a6cd5..a242c56f 100644
--- a/.github/workflows/mirai_on_mirai.yml
+++ b/.github/workflows/mirai_on_mirai.yml
@@ -10,14 +10,14 @@ jobs:
   build_with_vcpkg_installed_z3:
     strategy:
       matrix:
-        build: [linux, macos, windows]
+        build: [ linux, macos, windows ]
         include:
           - build: linux
             os: ubuntu-latest
             vcpkg_triplet: x64-linux
           - build: macos
             os: macos-latest
-            vcpkg_triplet: x64-osx
+            vcpkg_triplet: arm64-osx
           - build: windows
             os: windows-latest
             vcpkg_triplet: x64-windows-static-md
diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml
index 5690343e..41d333d1 100644
--- a/.github/workflows/rust.yml
+++ b/.github/workflows/rust.yml
@@ -31,7 +31,7 @@ jobs:
         id: vcpkg
         with:
           pkgs: z3
-          triplet: x64-osx
+          triplet: arm64-osx
           cache-key: macos-latest
           revision: master
           token: ${{ github.token }}
@@ -39,25 +39,25 @@ jobs:
 
       - name: Execute tests
         run: |
-          cargo test --all --no-default-features --features=vcpkg -- --test-threads=1
+          cargo test --all -- --test-threads=1
         env:
           CARGO_INCREMENTAL: 0
           RUSTFLAGS: "-Zprofile -Ccodegen-units=1 -Copt-level=0 -Clink-dead-code -Coverflow-checks=off -Zpanic_abort_tests"
 
-      - name: Setup grcov
-        run: |
-          cargo install grcov
-
-      - name: Run grcov
-        run: |
-          zip -0 cov.zip $(find . -name "mirai*.gc*" -print)
-          grcov cov.zip -s . -t lcov --llvm --ignore-not-existing --ignore "/*" -o lcov.info
-
-      - name: Upload coverage data to codecov.io
-        uses: codecov/codecov-action@v3
-        with:
-          token: ${{ secrets.CODECOV_TOKEN }}
-          files: "lcov.info"
+#      - name: Setup grcov
+#        run: |
+#          cargo install grcov
+#
+#      - name: Run grcov
+#        run: |
+#          zip -0 cov.zip $(find . -name "mirai*.gc*" -print)
+#          grcov cov.zip -s . -t lcov --llvm --ignore-not-existing --ignore "/*" -o lcov.info
+#
+#      - name: Upload coverage data to codecov.io
+#        uses: codecov/codecov-action@v3
+#        with:
+#          token: ${{ secrets.CODECOV_TOKEN }}
+#          files: "lcov.info"
 
   mirai_on_mirai_ubuntu:
     runs-on: ubuntu-latest
diff --git a/Cargo.lock b/Cargo.lock
index f12d7096..606a5ef5 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -4,56 +4,57 @@ version = 3
 
 [[package]]
 name = "aho-corasick"
-version = "1.1.2"
+version = "1.1.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b2969dcb958b36655471fc61f7e416fa76033bdd4bfed0678d8fee1e2d07a1f0"
+checksum = "8e60d3430d3a69478ad0993f19238d2df97c507009a52b3c10addcd7f6bcb916"
 dependencies = [
  "memchr",
 ]
 
 [[package]]
 name = "anstream"
-version = "0.6.4"
+version = "0.6.14"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2ab91ebe16eb252986481c5b62f6098f3b698a45e34b5b98200cf20dd2484a44"
+checksum = "418c75fa768af9c03be99d17643f93f79bbba589895012a80e3452a19ddda15b"
 dependencies = [
  "anstyle",
  "anstyle-parse",
  "anstyle-query",
  "anstyle-wincon",
  "colorchoice",
+ "is_terminal_polyfill",
  "utf8parse",
 ]
 
 [[package]]
 name = "anstyle"
-version = "1.0.4"
+version = "1.0.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7079075b41f533b8c61d2a4d073c4676e1f8b249ff94a393b0595db304e0dd87"
+checksum = "038dfcf04a5feb68e9c60b21c9625a54c2c0616e79b72b0fd87075a056ae1d1b"
 
 [[package]]
 name = "anstyle-parse"
-version = "0.2.2"
+version = "0.2.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "317b9a89c1868f5ea6ff1d9539a69f45dffc21ce321ac1fd1160dfa48c8e2140"
+checksum = "c03a11a9034d92058ceb6ee011ce58af4a9bf61491aa7e1e59ecd24bd40d22d4"
 dependencies = [
  "utf8parse",
 ]
 
 [[package]]
 name = "anstyle-query"
-version = "1.0.0"
+version = "1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5ca11d4be1bab0c8bc8734a9aa7bf4ee8316d462a08c6ac5052f888fef5b494b"
+checksum = "ad186efb764318d35165f1758e7dcef3b10628e26d41a44bc5550652e6804391"
 dependencies = [
  "windows-sys",
 ]
 
 [[package]]
 name = "anstyle-wincon"
-version = "3.0.1"
+version = "3.0.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f0699d10d2f4d628a98ee7b57b289abbc98ff3bad977cb3152709d4bf2330628"
+checksum = "61a38449feb7068f52bb06c12759005cf459ee52bb4adc1d5a7c4322d716fb19"
 dependencies = [
  "anstyle",
  "windows-sys",
@@ -61,9 +62,9 @@ dependencies = [
 
 [[package]]
 name = "archery"
-version = "1.1.0"
+version = "1.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "487955f60962765486ce000015a3492ca45c34a2ebbf12bc0aa2b5110ca6e7d2"
+checksum = "8967cd1cc9e9e1954f644e14fbd6042fe9a37da96c52a67e44a2ac18261f8561"
 dependencies = [
  "static_assertions",
  "triomphe",
@@ -71,9 +72,9 @@ dependencies = [
 
 [[package]]
 name = "autocfg"
-version = "1.1.0"
+version = "1.3.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa"
+checksum = "0c4b4d0bd25bd0b74681c0ad21497610ce1b7c91b1022cd21c80c6fbdd9476b0"
 
 [[package]]
 name = "bincode"
@@ -86,22 +87,22 @@ dependencies = [
 
 [[package]]
 name = "bindgen"
-version = "0.68.1"
+version = "0.69.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "726e4313eb6ec35d2730258ad4e15b547ee75d6afaa1361a922e78e59b7d8078"
+checksum = "a00dc851838a2120612785d195287475a3ac45514741da670b735818822129a0"
 dependencies = [
- "bitflags 2.4.1",
+ "bitflags 2.6.0",
  "cexpr",
  "clang-sys",
+ "itertools 0.12.1",
  "lazy_static",
  "lazycell",
- "peeking_take_while",
  "proc-macro2",
  "quote",
  "regex",
  "rustc-hash",
  "shlex",
- "syn 2.0.39",
+ "syn 2.0.68",
 ]
 
 [[package]]
@@ -112,9 +113,9 @@ checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a"
 
 [[package]]
 name = "bitflags"
-version = "2.4.1"
+version = "2.6.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "327762f6e5a765692301e5bb513e0d9fef63be86bbc14528052b1cd3e6f03e07"
+checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de"
 
 [[package]]
 name = "byteorder"
@@ -124,18 +125,18 @@ checksum = "1fd0f2584146f6f2ef48085050886acf353beff7305ebd1ae69500e27c67f64b"
 
 [[package]]
 name = "camino"
-version = "1.1.6"
+version = "1.1.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c59e92b5a388f549b863a7bea62612c09f24c8393560709a54558a9abdfb3b9c"
+checksum = "e0ec6b951b160caa93cc0c7b209e5a3bff7aae9062213451ac99493cd844c239"
 dependencies = [
  "serde",
 ]
 
 [[package]]
 name = "cargo-platform"
-version = "0.1.4"
+version = "0.1.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "12024c4645c97566567129c204f65d5815a8c9aecf30fcbe682b2fe034996d36"
+checksum = "ceed8ef69d8518a5dda55c07425450b58a4e1946f4951eab6d7191ee86c2443d"
 dependencies = [
  "serde",
 ]
@@ -156,12 +157,9 @@ dependencies = [
 
 [[package]]
 name = "cc"
-version = "1.0.84"
+version = "1.0.104"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0f8e7c90afad890484a21653d08b6e209ae34770fb5ee298f9c699fcc1e5c856"
-dependencies = [
- "libc",
-]
+checksum = "74b6a57f98764a267ff415d50a25e6e166f3831a5071af4995296ea97d210490"
 
 [[package]]
 name = "cexpr"
@@ -180,9 +178,9 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
 
 [[package]]
 name = "clang-sys"
-version = "1.6.1"
+version = "1.8.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c688fc74432808e3eb684cae8830a86be1d66a2bd58e1f248ed0960a590baf6f"
+checksum = "0b023947811758c97c59bf9d1c188fd619ad4718dcaa767947df1cadb14f39f4"
 dependencies = [
  "glob",
  "libc",
@@ -227,9 +225,9 @@ dependencies = [
 
 [[package]]
 name = "colorchoice"
-version = "1.0.0"
+version = "1.0.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "acbf1af155f9b9ef647e42cdc158db4b64a1b61f743629225fde6f3e0be2a7c7"
+checksum = "0b6a852b24ab71dffc585bcb46eaf7959d175cb865a7152e35b348d1b2960422"
 
 [[package]]
 name = "contracts"
@@ -244,45 +242,37 @@ dependencies = [
 
 [[package]]
 name = "crc32fast"
-version = "1.3.2"
+version = "1.4.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b540bd8bc810d3885c6ea91e2018302f68baba2129ab3e88f32389ee9370880d"
+checksum = "a97769d94ddab943e4510d138150169a2758b5ef3eb191a9ee688de3e23ef7b3"
 dependencies = [
  "cfg-if",
 ]
 
 [[package]]
 name = "crossbeam-deque"
-version = "0.8.3"
+version = "0.8.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ce6fd6f855243022dcecf8702fef0c297d4338e226845fe067f6341ad9fa0cef"
+checksum = "613f8cc01fe9cf1a3eb3d7f488fd2fa8388403e97039e2f73692932e291a770d"
 dependencies = [
- "cfg-if",
  "crossbeam-epoch",
  "crossbeam-utils",
 ]
 
 [[package]]
 name = "crossbeam-epoch"
-version = "0.9.15"
+version = "0.9.18"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ae211234986c545741a7dc064309f67ee1e5ad243d0e48335adc0484d960bcc7"
+checksum = "5b82ac4a3c2ca9c3460964f020e1402edd5753411d7737aa39c3714ad1b5420e"
 dependencies = [
- "autocfg",
- "cfg-if",
  "crossbeam-utils",
- "memoffset",
- "scopeguard",
 ]
 
 [[package]]
 name = "crossbeam-utils"
-version = "0.8.16"
+version = "0.8.20"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5a22b2d63d4d1dc0b7f1b6b2747dd0088008a9be28b6ddf0b1e7d335e3037294"
-dependencies = [
- "cfg-if",
-]
+checksum = "22ec99545bb0ed0ea7bb9b8e1e9122ea386ff8a48c0922e43f36d45ab09e0e80"
 
 [[package]]
 name = "darling"
@@ -321,21 +311,31 @@ dependencies = [
 
 [[package]]
 name = "either"
-version = "1.9.0"
+version = "1.13.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a26ae43d7bcc3b814de94796a5e736d4029efb0ee900c12e2d54c993ad1a1e07"
+checksum = "60b1af1c220855b6ceac025d3f6ecdd2b7c4894bfe9cd9bda4fbb4bc7c0d4cf0"
+
+[[package]]
+name = "env_filter"
+version = "0.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a009aa4810eb158359dda09d0c87378e4bbb89b5a801f016885a4707ba24f7ea"
+dependencies = [
+ "log",
+ "regex",
+]
 
 [[package]]
 name = "env_logger"
-version = "0.10.1"
+version = "0.11.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "95b3f3e67048839cb0d0781f445682a35113da7121f7c949db0e2be96a4fbece"
+checksum = "38b35839ba51819680ba087cd351788c9a3c476841207e0b8cee0b04722343b9"
 dependencies = [
+ "anstream",
+ "anstyle",
+ "env_filter",
  "humantime",
- "is-terminal",
  "log",
- "regex",
- "termcolor",
 ]
 
 [[package]]
@@ -346,9 +346,9 @@ checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5"
 
 [[package]]
 name = "errno"
-version = "0.3.6"
+version = "0.3.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7c18ee0ed65a5f1f81cac6b1d213b69c35fa47d4252ad41f1486dbd8226fe36e"
+checksum = "534c5cf6194dfab3db3242765c03bbe257cf92f22b38f6bc0c58d59108a820ba"
 dependencies = [
  "libc",
  "windows-sys",
@@ -356,19 +356,19 @@ dependencies = [
 
 [[package]]
 name = "fastrand"
-version = "2.0.1"
+version = "2.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "25cbce373ec4653f1a01a31e8a5e5ec0c622dc27ff9c4e6606eefef5cbbed4a5"
+checksum = "9fc0510504f03c51ada170672ac806f1f105a88aa97a5281117e1ddc3368e51a"
 
 [[package]]
 name = "filetime"
-version = "0.2.22"
+version = "0.2.23"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d4029edd3e734da6fe05b6cd7bd2960760a616bd2ddd0d59a0124746d6272af0"
+checksum = "1ee447700ac8aa0b2f2bd7bc4462ad686ba06baa6727ac149a2d6277f0d240fd"
 dependencies = [
  "cfg-if",
  "libc",
- "redox_syscall 0.3.5",
+ "redox_syscall 0.4.1",
  "windows-sys",
 ]
 
@@ -405,9 +405,9 @@ dependencies = [
 
 [[package]]
 name = "getrandom"
-version = "0.2.11"
+version = "0.2.15"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "fe9006bed769170c11f845cf00c7c1e9092aeb3f268e007c3e760ac68008070f"
+checksum = "c4567c8db10ae91089c99af84c68c38da3ec2f087c3f82960bcdbf3656b6f4d7"
 dependencies = [
  "cfg-if",
  "libc",
@@ -422,15 +422,9 @@ checksum = "d2fabcfbdc87f4758337ca535fb41a6d701b65693ce38287d856d1674551ec9b"
 
 [[package]]
 name = "hashbrown"
-version = "0.14.2"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f93e7192158dbcda357bdec5fb5788eebf8bbac027f3f33e719d29135ae84156"
-
-[[package]]
-name = "hermit-abi"
-version = "0.3.3"
+version = "0.14.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d77f7ec81a6d05a3abb01ab6eb7590f6083d08449fe5a1c8b1e620283546ccb7"
+checksum = "e5274423e17b7c9fc20b6e7e208532f9b19825d82dfd615708b70edd83df41f1"
 
 [[package]]
 name = "humantime"
@@ -446,9 +440,9 @@ checksum = "b9e0384b61958566e926dc50660321d12159025e767c18e043daf26b70104c39"
 
 [[package]]
 name = "indexmap"
-version = "2.1.0"
+version = "2.2.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d530e1a18b1cb4c484e6e34556a0d948706958449fca0cab753d649f2bce3d1f"
+checksum = "168fb715dda47215e360912c096649d23d58bf392ac62f73919e831745e40f26"
 dependencies = [
  "equivalent",
  "hashbrown",
@@ -456,44 +450,48 @@ dependencies = [
 
 [[package]]
 name = "instant"
-version = "0.1.12"
+version = "0.1.13"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7a5bbe824c507c5da5956355e86a746d82e0e1464f65d862cc5e71da70e94b2c"
+checksum = "e0242819d153cba4b4b05a5a8f2a7e9bbf97b6055b2a002b395c96b5ff3c0222"
 dependencies = [
  "cfg-if",
 ]
 
 [[package]]
-name = "is-terminal"
-version = "0.4.9"
+name = "is_terminal_polyfill"
+version = "1.70.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f8478577c03552c21db0e2724ffb8986a5ce7af88107e6be5d2ee6e158c12800"
+
+[[package]]
+name = "itertools"
+version = "0.12.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "cb0889898416213fab133e1d33a0e5858a48177452750691bde3666d0fdbaf8b"
+checksum = "ba291022dbbd398a455acf126c1e341954079855bc60dfdda641363bd6922569"
 dependencies = [
- "hermit-abi",
- "rustix",
- "windows-sys",
+ "either",
 ]
 
 [[package]]
 name = "itertools"
-version = "0.11.0"
+version = "0.13.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b1c173a5686ce8bfa551b3563d0c2170bf24ca44da99c7ca4bfdab5418c3fe57"
+checksum = "413ee7dfc52ee1a4949ceeb7dbc8a33f2d6c088194d9f922fb8318faf1f01186"
 dependencies = [
  "either",
 ]
 
 [[package]]
 name = "itoa"
-version = "1.0.9"
+version = "1.0.11"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "af150ab688ff2122fcef229be89cb50dd66af9e01a4ff320cc137eecc9bacc38"
+checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b"
 
 [[package]]
 name = "lazy_static"
-version = "1.4.0"
+version = "1.5.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646"
+checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe"
 
 [[package]]
 name = "lazycell"
@@ -503,31 +501,31 @@ checksum = "830d08ce1d1d941e6b30645f1a0eb5643013d835ce3779a5fc208261dbe10f55"
 
 [[package]]
 name = "libc"
-version = "0.2.150"
+version = "0.2.155"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "89d92a4743f9a61002fae18374ed11e7973f530cb3a3255fb354818118b2203c"
+checksum = "97b3888a4aecf77e811145cadf6eef5901f4782c53886191b2f693f24761847c"
 
 [[package]]
 name = "libloading"
-version = "0.7.4"
+version = "0.8.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b67380fd3b2fbe7527a606e18729d21c6f3951633d0500574c4dc22d2d638b9f"
+checksum = "e310b3a6b5907f99202fcdb4960ff45b93735d7c7d96b760fcff8db2dc0e103d"
 dependencies = [
  "cfg-if",
- "winapi",
+ "windows-targets",
 ]
 
 [[package]]
 name = "linux-raw-sys"
-version = "0.4.11"
+version = "0.4.14"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "969488b55f8ac402214f3f5fd243ebb7206cf82de60d3172994707a4bcc2b829"
+checksum = "78b3ae25bc7c8c38cec158d1f2757ee79e9b3740fbc7ccf0e59e4b08d793fa89"
 
 [[package]]
 name = "lock_api"
-version = "0.4.11"
+version = "0.4.12"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3c168f8615b12bc01f9c17e2eb0cc07dcae1940121185446edc3744920e8ef45"
+checksum = "07af8b9cdd281b7915f413fa73f29ebd5d55d0d3f0155584dade1ff18cea1b17"
 dependencies = [
  "autocfg",
  "scopeguard",
@@ -535,9 +533,9 @@ dependencies = [
 
 [[package]]
 name = "log"
-version = "0.4.20"
+version = "0.4.22"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b5e6163cb8c49088c2c36f57875e58ccd8c87c7427f7fbd50ea6710b2f3f2e8f"
+checksum = "a7a70ba024b9dc04c27ea2f0c0548feb474ec5c54bba33a7f72f873a39d07b24"
 
 [[package]]
 name = "log-derive"
@@ -553,18 +551,9 @@ dependencies = [
 
 [[package]]
 name = "memchr"
-version = "2.6.4"
+version = "2.7.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f665ee40bc4a3c5590afb1e9677db74a508659dfd71e126420da8274909a0167"
-
-[[package]]
-name = "memoffset"
-version = "0.9.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5a634b1c61a95585bd15607c6ab0c4e5b226e695ff2800ba0cdccddf208c406c"
-dependencies = [
- "autocfg",
-]
+checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3"
 
 [[package]]
 name = "minimal-lexical"
@@ -582,7 +571,7 @@ dependencies = [
  "contracts",
  "env_logger",
  "fs2",
- "itertools",
+ "itertools 0.13.0",
  "lazy_static",
  "log",
  "log-derive",
@@ -599,6 +588,7 @@ dependencies = [
  "sled",
  "tar",
  "tempfile",
+ "triomphe",
  "walkdir",
  "z3-sys",
 ]
@@ -649,22 +639,22 @@ dependencies = [
  "winapi",
 ]
 
-[[package]]
-name = "peeking_take_while"
-version = "0.1.2"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "19b17cddbe7ec3f8bc800887bab5e717348c95ea2ca0b1bf0837fb964dc67099"
-
 [[package]]
 name = "petgraph"
-version = "0.6.4"
+version = "0.6.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e1d3afd2628e69da2be385eb6f2fd57c8ac7977ceeff6dc166ff1657b0e386a9"
+checksum = "b4c5cc86750666a3ed20bdaf5ca2a0344f9c67674cae0515bec2da16fbaa47db"
 dependencies = [
  "fixedbitset",
  "indexmap",
 ]
 
+[[package]]
+name = "pkg-config"
+version = "0.3.30"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d231b230927b5e4ad203db57bbcbee2802f6bce620b1e4a9024a07d94e2907ec"
+
 [[package]]
 name = "ppv-lite86"
 version = "0.2.17"
@@ -673,18 +663,18 @@ checksum = "5b40af805b3121feab8a3c29f04d8ad262fa8e0561883e7653e024ae4479e6de"
 
 [[package]]
 name = "proc-macro2"
-version = "1.0.69"
+version = "1.0.86"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "134c189feb4956b20f6f547d2cf727d4c0fe06722b20a0eec87ed445a97f92da"
+checksum = "5e719e8df665df0d1c8fbfd238015744736151d4445ec0836b8e628aae103b77"
 dependencies = [
  "unicode-ident",
 ]
 
 [[package]]
 name = "quote"
-version = "1.0.33"
+version = "1.0.36"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5267fca4496028628a95160fc423a33e8b2e6af8a5302579e322e4b520293cae"
+checksum = "0fa76aaf39101c457836aec0ce2316dbdc3ab723cdda1c6bd4e6ad4208acaca7"
 dependencies = [
  "proc-macro2",
 ]
@@ -721,9 +711,9 @@ dependencies = [
 
 [[package]]
 name = "rayon"
-version = "1.8.0"
+version = "1.10.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9c27db03db7734835b3f53954b534c91069375ce6ccaa2e065441e07d9b6cdb1"
+checksum = "b418a60154510ca1a002a752ca9714984e21e4241e804d32555251faf8b78ffa"
 dependencies = [
  "either",
  "rayon-core",
@@ -731,9 +721,9 @@ dependencies = [
 
 [[package]]
 name = "rayon-core"
-version = "1.12.0"
+version = "1.12.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5ce3fb6ad83f861aac485e76e1985cd109d9a3713802152be56c3b1f0e0658ed"
+checksum = "1465873a3dfdaa8ae7cb14b4383657caab0b3e8a0aa9ae8e04b044854c8dfce2"
 dependencies = [
  "crossbeam-deque",
  "crossbeam-utils",
@@ -748,15 +738,6 @@ dependencies = [
  "bitflags 1.3.2",
 ]
 
-[[package]]
-name = "redox_syscall"
-version = "0.3.5"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "567664f262709473930a4bf9e51bf2ebf3348f2e748ccc50dea20646858f8f29"
-dependencies = [
- "bitflags 1.3.2",
-]
-
 [[package]]
 name = "redox_syscall"
 version = "0.4.1"
@@ -768,9 +749,9 @@ dependencies = [
 
 [[package]]
 name = "regex"
-version = "1.10.2"
+version = "1.10.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "380b951a9c5e80ddfd6136919eef32310721aa4aacd4889a8d39124b026ab343"
+checksum = "b91213439dad192326a0d7c6ee3955910425f441d7038e0d6933b0aec5c4517f"
 dependencies = [
  "aho-corasick",
  "memchr",
@@ -780,9 +761,9 @@ dependencies = [
 
 [[package]]
 name = "regex-automata"
-version = "0.4.3"
+version = "0.4.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5f804c7828047e88b2d32e2d7fe5a105da8ee3264f01902f796c8e067dc2483f"
+checksum = "38caf58cc5ef2fed281f89292ef23f6365465ed9a41b7a7754eb4e26496c92df"
 dependencies = [
  "aho-corasick",
  "memchr",
@@ -791,9 +772,9 @@ dependencies = [
 
 [[package]]
 name = "regex-syntax"
-version = "0.8.2"
+version = "0.8.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c08c74e62047bb2de4ff487b251e4a92e24f48745648451635cec7d591162d9f"
+checksum = "7a66a03ae7c801facd77a29370b4faec201768915ac14a721ba36f20bc9c209b"
 
 [[package]]
 name = "rpds"
@@ -819,11 +800,11 @@ checksum = "8ba09476327c4b70ccefb6180f046ef588c26a24cf5d269a9feba316eb4f029f"
 
 [[package]]
 name = "rustix"
-version = "0.38.21"
+version = "0.38.34"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2b426b0506e5d50a7d8dafcf2e81471400deb602392c7dd110815afb4eaf02a3"
+checksum = "70dc5ec042f7a43c4a73241207cecc9873a06d45debb38b329f8541d85c2730f"
 dependencies = [
- "bitflags 2.4.1",
+ "bitflags 2.6.0",
  "errno",
  "libc",
  "linux-raw-sys",
@@ -832,9 +813,9 @@ dependencies = [
 
 [[package]]
 name = "ryu"
-version = "1.0.15"
+version = "1.0.18"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1ad4cc8da4ef723ed60bced201181d83791ad433213d8c24efffda1eec85d741"
+checksum = "f3cb5ba0dc43242ce17de99c180e96db90b235b8a9fdc9543c96d2209116bd9f"
 
 [[package]]
 name = "same-file"
@@ -877,14 +858,14 @@ checksum = "d6c7207fbec9faa48073f3e3074cbe553af6ea512d7c21ba46e434e70ea9fbc1"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.39",
+ "syn 2.0.68",
 ]
 
 [[package]]
 name = "serde_json"
-version = "1.0.108"
+version = "1.0.109"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3d1c7e3eac408d115102c4c24ad393e0821bb3a5df4d506a80f85f7a742a526b"
+checksum = "cb0652c533506ad7a2e353cce269330d6afd8bdfb6d75e0ace5b35aacbd7b9e9"
 dependencies = [
  "itoa",
  "ryu",
@@ -903,9 +884,9 @@ dependencies = [
 
 [[package]]
 name = "shlex"
-version = "1.2.0"
+version = "1.3.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a7cee0529a6d40f580e7a5e6c495c8fbfe21b7b52795ed4bb5e62cdf92bc6380"
+checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64"
 
 [[package]]
 name = "shopping_cart"
@@ -933,9 +914,15 @@ dependencies = [
 
 [[package]]
 name = "smallvec"
-version = "1.11.2"
+version = "1.13.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4dccd0940a2dcdf68d092b8cbab7dc0ad8fa938bf95787e1b916b0e3d0e8e970"
+checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67"
+
+[[package]]
+name = "stable_deref_trait"
+version = "1.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a8f112729512f8e442d81f95a8a7ddf2b7c6b8a1a6f509a95864142b30cab2d3"
 
 [[package]]
 name = "static_assertions"
@@ -968,9 +955,9 @@ dependencies = [
 
 [[package]]
 name = "syn"
-version = "2.0.39"
+version = "2.0.68"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "23e78b90f2fcf45d3e842032ce32e3f2d1545ba6636271dcbf24fa306d87be7a"
+checksum = "901fa70d88b9d6c98022e23b4136f9f3e54e4662c3bc1bd1d84a42a9a0f0c1e9"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -993,9 +980,9 @@ dependencies = [
 
 [[package]]
 name = "tar"
-version = "0.4.40"
+version = "0.4.41"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b16afcea1f22891c49a00c751c7b63b2233284064f11a200fc624137c51e2ddb"
+checksum = "cb797dad5fb5b76fcf519e702f4a589483b5ef06567f160c392832c1f5e44909"
 dependencies = [
  "filetime",
  "libc",
@@ -1004,44 +991,34 @@ dependencies = [
 
 [[package]]
 name = "tempfile"
-version = "3.8.1"
+version = "3.10.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7ef1adac450ad7f4b3c28589471ade84f25f731a7a0fe30d71dfa9f60fd808e5"
+checksum = "85b77fafb263dd9d05cbeac119526425676db3784113aa9295c88498cbf8bff1"
 dependencies = [
  "cfg-if",
  "fastrand",
- "redox_syscall 0.4.1",
  "rustix",
  "windows-sys",
 ]
 
-[[package]]
-name = "termcolor"
-version = "1.3.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6093bad37da69aab9d123a8091e4be0aa4a03e4d601ec641c327398315f62b64"
-dependencies = [
- "winapi-util",
-]
-
 [[package]]
 name = "thiserror"
-version = "1.0.50"
+version = "1.0.61"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f9a7210f5c9a7156bb50aa36aed4c95afb51df0df00713949448cf9e97d382d2"
+checksum = "c546c80d6be4bc6a00c0f01730c08df82eaa7a7a61f11d656526506112cc1709"
 dependencies = [
  "thiserror-impl",
 ]
 
 [[package]]
 name = "thiserror-impl"
-version = "1.0.50"
+version = "1.0.61"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "266b2e40bc00e5a6c09c3584011e08b06f123c00362c92b975ba9843aaaa14b8"
+checksum = "46c3384250002a6d5af4d114f2845d37b57521033f30d5c3f46c4d70e1197533"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.39",
+ "syn 2.0.68",
 ]
 
 [[package]]
@@ -1064,6 +1041,10 @@ name = "triomphe"
 version = "0.1.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "0eee8098afad3fb0c54a9007aab6804558410503ad676d4633f9c2559a00ac0f"
+dependencies = [
+ "serde",
+ "stable_deref_trait",
+]
 
 [[package]]
 name = "unicode-ident"
@@ -1080,9 +1061,9 @@ dependencies = [
 
 [[package]]
 name = "utf8parse"
-version = "0.2.1"
+version = "0.2.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "711b9620af191e0cdc7468a8d14e709c3dcdb115b36f838e601583af800a370a"
+checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821"
 
 [[package]]
 name = "vcpkg"
@@ -1099,9 +1080,9 @@ dependencies = [
 
 [[package]]
 name = "walkdir"
-version = "2.4.0"
+version = "2.5.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d71d857dc86794ca4c280d616f7da00d2dbfd8cd788846559a6813e6aa4b54ee"
+checksum = "29790946404f91d9c5d06f9874efddea1dc06c5efe94541a7d6863108e3a5e4b"
 dependencies = [
  "same-file",
  "winapi-util",
@@ -1131,11 +1112,11 @@ checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6"
 
 [[package]]
 name = "winapi-util"
-version = "0.1.6"
+version = "0.1.8"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f29e6f9198ba0d26b4c9f07dbe6f9ed633e1f3d5b8b414090084349e46a52596"
+checksum = "4d4cc384e1e73b93bafa6fb4f1df8c41695c8a91cf9c4c64358067d15a7b6c6b"
 dependencies = [
- "winapi",
+ "windows-sys",
 ]
 
 [[package]]
@@ -1146,22 +1127,23 @@ checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f"
 
 [[package]]
 name = "windows-sys"
-version = "0.48.0"
+version = "0.52.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9"
+checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d"
 dependencies = [
  "windows-targets",
 ]
 
 [[package]]
 name = "windows-targets"
-version = "0.48.5"
+version = "0.52.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9a2fa6e2155d7247be68c096456083145c183cbbbc2764150dda45a87197940c"
+checksum = "6f0713a46559409d202e70e28227288446bf7841d3211583a4b53e3f6d96e7eb"
 dependencies = [
  "windows_aarch64_gnullvm",
  "windows_aarch64_msvc",
  "windows_i686_gnu",
+ "windows_i686_gnullvm",
  "windows_i686_msvc",
  "windows_x86_64_gnu",
  "windows_x86_64_gnullvm",
@@ -1170,61 +1152,70 @@ dependencies = [
 
 [[package]]
 name = "windows_aarch64_gnullvm"
-version = "0.48.5"
+version = "0.52.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2b38e32f0abccf9987a4e3079dfb67dcd799fb61361e53e2882c3cbaf0d905d8"
+checksum = "7088eed71e8b8dda258ecc8bac5fb1153c5cffaf2578fc8ff5d61e23578d3263"
 
 [[package]]
 name = "windows_aarch64_msvc"
-version = "0.48.5"
+version = "0.52.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "dc35310971f3b2dbbf3f0690a219f40e2d9afcf64f9ab7cc1be722937c26b4bc"
+checksum = "9985fd1504e250c615ca5f281c3f7a6da76213ebd5ccc9561496568a2752afb6"
 
 [[package]]
 name = "windows_i686_gnu"
-version = "0.48.5"
+version = "0.52.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a75915e7def60c94dcef72200b9a8e58e5091744960da64ec734a6c6e9b3743e"
+checksum = "88ba073cf16d5372720ec942a8ccbf61626074c6d4dd2e745299726ce8b89670"
+
+[[package]]
+name = "windows_i686_gnullvm"
+version = "0.52.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "87f4261229030a858f36b459e748ae97545d6f1ec60e5e0d6a3d32e0dc232ee9"
 
 [[package]]
 name = "windows_i686_msvc"
-version = "0.48.5"
+version = "0.52.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8f55c233f70c4b27f66c523580f78f1004e8b5a8b659e05a4eb49d4166cca406"
+checksum = "db3c2bf3d13d5b658be73463284eaf12830ac9a26a90c717b7f771dfe97487bf"
 
 [[package]]
 name = "windows_x86_64_gnu"
-version = "0.48.5"
+version = "0.52.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "53d40abd2583d23e4718fddf1ebec84dbff8381c07cae67ff7768bbf19c6718e"
+checksum = "4e4246f76bdeff09eb48875a0fd3e2af6aada79d409d33011886d3e1581517d9"
 
 [[package]]
 name = "windows_x86_64_gnullvm"
-version = "0.48.5"
+version = "0.52.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0b7b52767868a23d5bab768e390dc5f5c55825b6d30b86c844ff2dc7414044cc"
+checksum = "852298e482cd67c356ddd9570386e2862b5673c85bd5f88df9ab6802b334c596"
 
 [[package]]
 name = "windows_x86_64_msvc"
-version = "0.48.5"
+version = "0.52.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538"
+checksum = "bec47e5bfd1bff0eeaf6d8b485cc1074891a197ab4225d504cb7a1ab88b02bf0"
 
 [[package]]
 name = "xattr"
-version = "1.0.1"
+version = "1.3.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f4686009f71ff3e5c4dbcf1a282d0a44db3f021ba69350cd42086b3e5f1c6985"
+checksum = "8da84f1a25939b27f6820d92aed108f83ff920fdf11a7b19366c27c4cda81d4f"
 dependencies = [
  "libc",
+ "linux-raw-sys",
+ "rustix",
 ]
 
 [[package]]
 name = "z3-sys"
 version = "0.8.1"
-source = "git+https://github.com/prove-rs/z3.rs.git#26ddf7fb90ea62509bb235286024fc7f76319591"
+source = "git+https://github.com/prove-rs/z3.rs.git?rev=cb7b79a61433673a5e6b07559cc661a97b5a84cf#cb7b79a61433673a5e6b07559cc661a97b5a84cf"
 dependencies = [
  "bindgen",
  "cmake",
+ "pkg-config",
  "vcpkg",
 ]
diff --git a/binaries/summary_store.tar b/binaries/summary_store.tar
index a319a86964fc2da78487b48603f3b2ed5faa2a0a..c7cb12299dd5c25244b318449f7d5b87cc92e4a8 100644
GIT binary patch
delta 7544
zcmbtZcT`l@)}MiU=iWKfVCV=^2JW31m|>7&o6s#-5MvZjq(nr)h8Qav#g2#+m92m%
zQ4=*{BYL7lg=jRz*kc#;MU5u05U`Am?_4mxytmf3zCS(|dog$K-`QvH-`=OpWx=*@
z#0!=m6PK|o>_UT0A>D(5x&?Wf0z*TCgG8PorC!mcCa*fN)K0wGUOnSKAl<tM2md$3
zZK8W{U{JTv(C(gr!GHS;CjPp2Gnqu5rcQs0#O}+)?qVWVM68KWL}(%sA`B6hh?EE-
zA|oOvq9CFqq9S5L#FmJfh#e7oA`V0xi8v8)CgMWGl}HyNZbXDRyAtsr;)%uXUTO1O
z&h)$VKw?XYRH>=cCXUTWP0bjanLd5uC)PN<!mG+&I(^&@H(E@IMflAwuRD&cgRVyw
z+jgD8JAcuhqVVnSyiV9F2hWKAk+rZM6h(_flGXXSJcftbJ2q^4(B*n`hMEH{v)o)^
z({(QuzH-g$usu8V_dAGfolotXl4Fh6KK6QIuXtIXe1L5$rzDI>B!c`zu@37Dx+DrO
zp}c4HR*EghY1SfXq8L`N*F?!(@$!MXJu3Vr+*{_r=B1Y<v90?kd^S_J*_xU(;&uh>
zO7M2Vn&IA~qNJ1eH;!Q~qVZJS?(<1f{3&>McTm0@bL$0b(Tt^#OeA99T!`2O+pX92
z@Tc~idwC2zvb`Pf>7Cw-BiL>I+6S}G2UA#V6o)bR!-w8u9N5HxiyyLW^C_4-S{#b2
zUh8^Mc)yj#=&q>nxb+j;I*(GQM53;6Zi2W!4)3D(vc|u9XeK%+#$3DEmu($NDb*s8
z3Tl>$V{zGZ@lz`tAEJqnD=Z%4%GlOVDV0(f-7-NOk53QMyISLtNKKxDVv^13pV`)0
z%EneON6r>U<4vRVBdoD3LGx0sSlRuHOYC3Cl&wNA*W}Sr*pMlfSYbLtv&ezXQtXan
z+Y%`JW~shEg_qCPyp<|O{(6SEET-)2MItG*fW!x%-l|Wq#!DAzHaN)Y=3Pi)E!vrs
zgBP5gEa?SLZph5|^jG>PCahVnxxy;%$S&U|2q((XO(Zfv=|}3R`w#k+neeL`4R(+Q
zq+7MI7X3pCH-F&Q6eM5u<ApOQj#?y=2X!m|MiUH09vVl?eywR&OTVk*J|M0fC<wSr
zPsfi}`jwh6^ONR+gY;<Hs*$Y45JJJq8tYkj^iO`fLh!X)ns2Q=Hfb$J)T*NviqzA4
z7_+9O=1iG6HaB%jX6h$1r?lEZAoAwmsEv<3#5?<#A!4hC95=LS#*1No?7QdkRt*bh
zVtrydtin@ywFd>=|I$o^*grHi3TKCy8SL`~)RM&_kv)`-^9jcOe`=;#Tm8TNufDQc
z2MxD1&N%0pCdXQqb>QkX!hs#->HtR*{7qm}D~rN|-26*S_?AWU&_Q}FNiAb7{?93V
zIKlsZ2>h(_*}<H0tM7%LA((ID<7D-;wIgXvlKzIqjH}OPF<QQ>dj<QVFST?DDEs=j
z!@+PL7yL&TpRVHngo9S^6A2`ih}D~_%;0I!Xv!AToe|FDeg3kNvd+u}Qi>!B8cp;p
z{Cb=J`4F6?_hB8S17^GQU@hJ3D6ri}&%h%e_^;}Pr$+dc(M;3IFMeZRlw(<6pK<@&
zlw-;kGmw+->-c{DWu71UV9yVI@8&T-j{NDh)l3SS-E2zS9pB0?w6|YwCqMJ^K5y>$
zn^T=gwj!mH#>&&a?T*Zt>-~?T5j5D}^-W+dJ~-)%l4!`i>pPN-iJ8<BCDNtP$a3~@
z|E_P0)Wex6MC0jF5!gQP<stc=Zv^__#0fFVCOR$H$~aeOxaS)uJwJJGI2tPe(;xWy
zK=0ptBbXlL%bQRZ4e9rN-C@%MUj^(WYP4}SU57FW)CU5Cc~5Y>?;FF6O5J<;9X6ZY
z7V2NhwuaL9!hK)f8YR8{Vj0`|lrAlUz!SbPFvLmE;30qduD6z652|n{$vM)v<*_g0
z#H_emm?OApmvGsPX_VCpG>(QGh8xdZSo4G<nLsncWieChJvIoiAuNHVt3>f6ZD?S*
zBxd0jOPN4OzLax<(=v{MFeztdc38_6zEh8sJ{nOQg%ap85o{Fle=7i<K0i1cO{XCe
zaWmNKb9%31TSI7k6mgt2yRSWZHru+I#t#+TVr%Kv@1<cR=AJa3W6SBC7+1SZlraC7
zS~CA^Z@ar_APq7dH;74gkXNE%G^FUbk5F)~DF{uZSBs2b(sS-`RmTlxbdH)BG=T<#
zo}0+FGSLdul0xGeJvT%wGtHRz0=0ZZMx=l^i0covL7XEb`Ez$<2eu!(hgv=)rqP|I
z5(D>w?e?&4J8DUzafy)|Dwf@2qrFf|A_1j!g5t9|XBcGS?#a?qR+5=AiD_J?$rQqQ
zz?MMnA=}7L&1YZipz-={TqTPve-8MPZCy^UUIUGY^TlI&b01numyA5~icnyt@sTjj
z;3U&D#`Q-n@$?!|a;Lwr5!^FbN<{flA%Qi2C(t#GB(NcYByg>AT`g*fBc@SMn#RS#
zr)iuTeoN$Tvnl#M$*3in#%Ghb!D89mJ80kEP6#p%zD(zA1SjE8@|8~n1a#+EIFiYY
zM%Pa%@1U0P#3z)baanLPnR|qm%-HLUmJwYnJgVS&fhvU?$i%t1xuHVR*eTpfR6F~#
zwP-0p^oMx`#A{w9Cx!4-&a9xaG#{`pM$v1@@hpOte0~5vpUS;ql;;%gWJ!v3^crFk
zL*QcVAgmkD{UDXv;;hdJG0SNDYAQF&i5WO|{Y<o+hB*aXfi!F3*EMJoaR>8Ha3(OX
zAbsb%fA}5J6)=AVH%Y28j^)u|0T9s0CBx7{E=?A)_LIY?#h)m9LH=T`A9yx$DtK1N
z-C`#XzVSI~(a^YQC1)>2!y{*xq83gV-dM_oK;SCw7W$#i@tc1u{ow3L4nce|v261X
z>hn*_*b?q{c8}FGav-?SIH8n7jDk{~+rYlKL$57=$G~7*zm8kPVpE3UrB;1?T#_5f
zwve_K7$Q`x!8Mb#&5jW8HMd5(bCY2cYw1e*dG~lUghxk4z9#L!(d8ZS>A`f8lY!Mi
z5=!%TSNs0c;&_Pr10`N|zK;H~6W~oJI4usU=dOvRK^`0bK(hp8VI$WYx*g@rsJK4c
z9hDPZB9!Lq;^6LKt}ojD_|16)M42QgKZ1fITqHBbD)TL>qT$>TZUfSf2wIIQ31W07
z;?z;D4?1<yBtjdBGF?y(hnxnkKfA3WU@rT#n8pna+yYwZzS-&$xp}Rp%Yh^fjrX_!
zJnsZILW*ZzGh7LhzV7MpgwXOejc=UcwmadouEr5Ob9&nkm1Kv7mA`SB=*OYcs!#?E
zB5x@Ejq3`o_qiBEeGr&}CKIIz!XI+JP;{T`Cv~ulZ9@l$62cyGvth&ol5p1rR8K+z
zkd`1oa_Bwal4R1$-yA}Vh_X*EguC)F;P{F+%Z_tNwrB;>4$6hIu6$28?8>WQ`5&BF
zcCue`Iw~TjAswc;4lOg5TDl+2rs1bQxH;^OqYc4qTOExD|H*Bk6wkCeE&Gh3VV%(S
zHNpHsyr6}fOyk+3joE?frp=!pWi2Yz`*tW7+9BNu?6h1dq;2!3v2nd|t2Z++)Y@B^
z<E@gP!z8L6T|lK|1*mwkbAPc>MwZArQ2><Kkh7(?4L^{nTXEnEVG$MC@CA(J(Dngn
z0}bxBd^P&nrg=14Md0xQJOX};;BBCn9dAa<Pi)F0t9l(-)g6{fH6Me-1$7!!Oq4@m
zfgL}z1IeVeyW|TF=h^YqEcc<PiEW!hV~ssOfl_qI8#j%8s-xGf?^x#{+7xVY<}rnJ
zmyK6-(nIs7E+Gj!)A*n}FLhQf?z^j;Tw&U2Ump=Eq8E*3S&8Hjk?3CpC6uik<`nsv
zA;%)!g0JqD{$&j|kNunQVh_}24e|eCoAE;lYPE)jQ_^O9NhW+W{X{q6BQ^rSbD4A+
zp74!ypc~4*1eeiTdc7#2GdX!EKTP_tx}HXJi4xp<^Wk7t@n&X=J2eL_q~Z5aevx$T
z+}FXRwF#i6H~%qQ=}rI_Cmj2kc!DlH_;OS~Rz;Ijb-l<B0zcrrpnV*V;9d{H=F+IJ
z*JKx6Pj*paiG;B6JPXr%@@DC!(+v;EiXu+WnfX+3=|yxuJRh<H)d)J%2mB^>n|pa8
z+cuBJlHUAeirx76cZ=Azn>3yq&Yz}~akmejBG;}yH0LQ2>7Yd=Ptl6xs`N2ar)TAk
zP0bxUF@4t942S=EPEE}U?A8M&_eI%Yzui9z9Qz?NnD(%naebvgTnDo|H@#=}9`~Nv
zlY@}24cwARH{*?4i5BlkMq8wvRG%(?Pjz@N)GSul?C3>Gs?xsi>2*R+&vJr`qxf~w
zdFlhRSWEBIG#oyPrhBMlB;3D4w*ANFci{##pb;?nf&VhHK&{MBvQD-c5Al)x9j;j?
z`@0b;8qst6^0VU4u-^DyS>zx<JGx_ztMIX-J2E{4Ku33crIs~|p(KZNQn4q~>9!fq
zyw7~cqT|o~-=LLrg(yxaVShN1%txWsPpxl|1yMm3L}NN13&Te9F-%FY+X7N-s2<HP
zN2;#|7L#48Lc|NhoS}aTKTz7^&jMGpnJD4h$9yKN%OEYXa$&<$(p?o~<9wXTkA%-s
z`Do^Cp9z6vi-kW^`6@<y?@@`c-xR0utI&om@;zkbR*;o@Za?1#iZb|qY?EgMV%tv9
zxIUdfOtB~USFvo{4H_@V<bS55_M2S?k?+e}$a(UEY^_TD(z`L0lxEud(ySLs^Q{wj
zE#lY9vaj`xW-ZJFTIUaE@{}4d)w)Dli4dH9q;`SI2*m&!)%3|zax=!}3NHzScESsT
z<*{;sb>IidZ@}4KWX&)+QhuHJ?z4rLgk7|85nm{+aMyoEww6i}3@sp>RWBy%XxTSU
zYtb4SZZGE7O1rL_sU(Yv09p$8#7=se%9hrWU9M6zOvpDF&J^(OFnK8-hS1TqPXDyD
zW1if}5AZbfT0$0+d5(4vD(i5zf*;=L?9A)hr-Z!9PV$0*3~_^;rKAeQk8U`ldBhS9
z>6`UhXei`|DMootnZ&jor>lfB8q&}6{cv0XpGC2u7bMl}QyIDE7V)nsnaTB_n6*el
zXuTiU&QfdO>`s>mE0GK$DO)Y{Eb@zlD#}&`M=u+@fbp24nS?3Z0!8~}*C5BrX6k;0
ze1ug8eFN;?(T640az~~^=jI^4fp1CWhs5eXzW6+sRIdJg<tl{ANuA-+4!%OxyS48M
z)<S(t`{_EuD6e%1$2%X(hA7aH0*647UR7s$ey|{dSHh5+yaWz@NwQD31cah##2g}I
zuLs>uz8~79c(NV+K$L|rWgnjpuXgf%(Px{lyh104a(SonR4pGZUDH4JDf*TuVe&qH
z32fL!3VZ%W$#pcJhFiP%1<0W(DTAE5Rpi{ATF2`kwT`!iExSpTT4rq<igJXZIdyyx
z%xfk?Lp&}#Cc#4L9{y9s_qz@bVA~$j8#-#x;;i?_j(ho9N)hmBNd((=j;<mW8=*MU
zaP$Fw0HwUKWhH5MI)U~#h{$m$R@r3W!Yp~SLLGiAFNV-}|2=(`0(~LQaPd4}shrz%
zo+XWcm^KEAM80q?!hX#E(e`&E6a{iHt&wkrb4iL{;Ym-$Eojv!{)HArN(Z1%Nzf6U
z34797CpdV4B$xhu-CE(^nsbr&1+R;If2R1g->i3<NvNn&nTJl2fdvqGiSGvUuJQ?x
z^9!lbvxv4Na!uJF>eFet{|i5axv2W`E;+j(>=HkZxzc4r!MlgvFj=CNfc0fE@S<a)
z5iKSI`*se@yUfQkgRfV$y~74VudC$rx4Xid6~i^tpR;W<>FN%)Z&`RhyzC0!gHr4~
zmgK~?-KIAXiw%%6Bw)==eg-A2x?W0HqbVATkIA1Z)b=T}y;+Nm{d<n91dh|3LH3fb
zQtq!Bf=G-0N}B?NLo2^VF$&9`$v;srRhC~1$<_$FUh-Q|Ui`3QXe)_g95l9*)3N>)
zxr8{DL`9J=AJwA4u=gczf=y9cXUK`t(lFvRNz?mcygRw<REq|@H@m_;!SdNJSz8Hn
z)r7f@fi_WETbT5QkB}by<>O~$N2(S<wpber?QaOW**7$W>=D&ukC-6VhQW+zts2(8
zC8cxS_b3{TqT$M0J{jdu-J*~{R8Kh9L+cI^R@y{G_R)+QwylKT*g>CosWxrDr`C;9
zOn8~Nk8Qh8R}%v{K?$v}DMg!xFH+iAN|}8qwSiDrLkD&fZa?Bk`%EAWtHnht73~Ua
z-&H%sMYhEJ(R9}0w15uoE-Y>zINQZGOz6*iP=@?tk2%y^WyWW_D!-M(+!B=v?<iK4
zTY+bs>M^Y7rcz=Y`0m+^HwCK_$N?CqGQ%F7l`}j!tE_~_(+J3InyP_8$-Q4vD4!$~
zEu`oVucEcXu)K%XTPZDWI_|?-TxQbnbDlCoj9@`m=PW2WEOUmWOobV2_9^zkp6`?@
z+;m*oIe!kM$&{XOD?^zEr*oAG{Br6$iy26~bzsR?DlwO@tYM&bo$XD?K0=1CJFHyV
z5xyDU(kpG0*w|NF?IPocYg|~1dITLB4Ebwpd|;1<st4R$V>1|Ux~;5o#ivrW#}v}m
z6Nkvlv##WeOKprQLoA0b7wy8}Rf2OEXtUpiiKADmwsuVM?+8;5M5(rPPTLV1zP-2u
zGtucLBo+`>mo8V4u$~OF&4rt><auVS%1PW2_JNhEweLng;Z=1odJy4r#X!|;H7=f{
zJ>(*r_eZ@iSs*TSk5JehqtZf}Rvm<Km8#Ym$1c;(b&{U->v@{B$Ro-5{i~{*18%C;
zo^fGmr=us)82U5VRH7XKiicVk>~&DP$PLfBru|)w^WJJNxZo3AbOu|zFi_Xzf_se8
zmB{e4Y~4K<TwkOMl;MHj=@hQG`kt=AVgDt)y(>=Zs^4jYM|9J7amDwC=*P?OvlM+l
zS6r5-A0xwk3iXMusPfA|ck<S2hsYmlw(Grc{C52tgpb_S&vnHE1N{o+`0!M}uUzqh
z!+yyMEED@5cf~gb`CmbJYmxsYSA4q3Ux8T9j|=~@df`Lk09Vg*)}^N4|KG2Zd*-su
zaqaDAI^Oh&L{~cB_$`?DJ8QAMBf%{i!!NFA+*iRb&@{<za;)Y5>K_2@VTLFaW4cE+
zV4^faX_P?=)53}J%3txpXgpEs1tbsm!VTffzWI+2p$QW3k1$MRJUyOVMx!LKF~X26
z9sR<)5PeMG5Wd#n3t7FjW@gbXo1f5d2~3PMj376e<5y9V0N5C9aD(3>4Q6Ir&9SK{
zQ3CoXLlV1X{}=9TYcB~dj57FHv#ra%KgG7rmf$0O4B6Jwyj1h|q`j3A92je8cV)h>
z-|;cZmq1{VVIhh(JkCYgl0Bp#0jmt&&|GBb%Tx}!Tuu@I|5b)8#Hou-WcEFxF6G4r
zCpfUm5W!5}A#xICf3wPv#8^sY&rz}jMi(1KGt1}9`5vW7pt0DHj*d0dbt5_NA#d&j
zFBzTTk(1E@l1dC_bV6Nhi<S~gf58$Bv&#&TY=+m&HEe5?1pAd5f~?V0H&605?i<OT
zy-*Zo@W*S`80K56ci%kkL9$Ux{(jrByW`g4f*U^fSBW7$*%$=hUp4GTJ%4+$7A=?T
zC0jU|A_jIj8>7%i55BrY=H1&lZyzwKjNxov)m2ZlNU|5st}*t3Ln>n!BY$>zCCZaP
zyUIA1DSnK@-aVM%h>bBq>QnLdUuY(A15@pdq40q%(S5O~I{v+`7c|%!&C(6WTpytf
z0r#c7kq3XZ(aacoy1hb~5}2Ykj$^}XU;m43lS^=u+W5v=fj!1`XIo!O_U;pjtYAU1
zF%}0p88=!>&n`2N*W&6V2@Z%d4(P(<44Sh9jg`RftBje9SMII}=pzXv6dQ*#)8n+&
zXs870ij5yKnw3v}Kp#p#USb@^JU`y$r2xw;A+X=Ynp_kofp1HUL!?XC(}&P7$v)Cx
zWkyFZm69;sqiL<+XId%o^T}vFO{n*&QezT3u~;6<{`I*88_JAeg=S>_oX)mQmF%m7
zTWS)p(^{hwB^`4yuz&=dEWtPGjf1-|Coc6>q0thMiUU#@wzU6wlpul0;($bk^*l`8
zSxew&aX>b+KJC{NXoLj9tO634NgJY0zI$+i{Z;|X%H;w7`OnnuA%UUq|M`i<ihy>>
F{{Z_lx(omS

delta 8778
zcmeHNcUV-{wx5A>IOl8_q<3U!dZsXQ=$26_(xeEA3N}E+F5Ma%Y6QE8xDYEbma9oD
z7`N9FYpfA$xzQ*_jmFp#5n@7O!dnC0XuP@ay?@^K^1koQ=lUFe>$lflzrFU}r|g+s
zdO|*X+abBVE<;y1al(YGf~gsWMY#ppy2A0<Bg#A@%Os1k5lZKPpg^U6P;fv{KxjaS
ze~?o050#`~nNn({c$UlMEjk(Nz{yNxvc#<6%HDmIY06h0BPJ8j0?_i&jDK$`^Xy<1
zo|@VRzZ*ZB&??LG-5kYA{AMnb*$>a1pv%h38=tMqE6AOcos*R_JX<C=kzKH}`hJX=
zLr!bYL1ogL{~X+tv!=vmXN|}%(EmF<OsgJ$>5qB>q~O3nnR3c&J+lHO<%FU!6SBMc
zhji}TDKIoJAV}xmIVdC~FvLHA1cxdU;v&NPM8?MTkJ3%aDk>__{aMQ0!c*eHr}arm
z2@Mz*6Fnh_1a(&S#YPF~|5+o{Dg09?`7@>dD@^Rl>?Ya1S(1>DAe0c?CZR?yx0Q3c
zjA7$*hZVL$W`A190Lfnp`Rf%D<+XcV%U2@8|GaemA%Q{vt<nXChWbmL{{p33_=mcM
zh6Z8&Z`O^`WsDfsS~LMh9FqQY{RM`E{w2$1@w#lS8esS#$<sODUlyFdzdvpu|J8!)
z6pA_ngF1!$?^lhP?H(8$5)c^jFI%C1=<5|USI(BmSvi^snkgECX2i_UI5ZwjKqF}8
zXclM+G)uI0XjW*}Xf|lJXm)7!XbxzOXijL(Xf9~3Xl`ikXzkHF(3DipdS=d`)8=@t
zwWA*3dC!4<vB&e29n%u{#X%^$?&(J#T=P6^N8K7cpV`qh#A`}d`naE$xjn7U@tPDt
zrylSMwWsY~daVni&m+Bu+tUj}ymjt0f2Q|%d)g7a!!77nTfE<~-*?peXA9c9&U>ys
zS*aNuOa?Q>vi6WAX&qqaGjAStobWNw`47FT1iI~o_d0vVQS;~@Ful8v6TRHc=MZmm
zcvy59-)wQ1F*RNVWHNa%ZP?=d*bc%ZZD;s=u}?AWcFd=rEv;sKuh^SE>1r~B#4&SZ
z<`bd%gikbWO7YD%^%zm>IF!8j7;&44opfUgGxBmLXBTATj?5^Uocm$}_!oP1faFKM
zcCg`&uK~iAcv#SkA-=Os9ONF@>D#7&hM(kJTWNqa9xhh8^B^sgGqAYQLs>4lTD3WM
z4)L{u<y$-%&@PknaDIqyLb<-D1ti!g-(Y17Mb<j1dlllQ>dg>GGJGvSdg9AK>LaB6
zA-~abxgE?-^WDn-c4OOmzS+cr>e78bG&T7@E-AdUgC35g`8rW$rf;4pUANNrsXe@N
z+jqNHsN1^5q*(@7O52J4A#c~RSvIS+m=ue7i2YBichp$!KNb#-KK1n}&%|2(p=J^o
zxhrD%-)q-KoYj+mt8A?}SlPE{UYCqw$#!9(sOJOUzsdQ!ldhexQdj7uZ+!>IP5;6P
z1D2treB(R=+<xxuy<$AuRuZAX_qhp8Qg`4TEMAyxD<Qp^`7-Ok0C;xHC!QX7r$bkk
zPd(|Y<C{&r>C4$2M*XElmY_%)UfNNdA^7i%yuvqIS~Aq#Ol)!BydL$fC;b`lb{7Y5
z71wSWNIC<>?&3h6oj6HJ(wH*17$(}mkM3emVW`S&1sTnh$w28Tc7$>5#V|7c$9g9+
z7BLY#Jw*>V8Z8P?j~<~sV|xdZZDi+piayZGLk#1lZY@7e#xPLkA&w=tV%u*gBaz?(
z4Lw99_$tMooJ-F3+E)yBxLqhJph_u*@ejGsQob>Sp?8&HM^oPE!lCti;|~nA_7T4^
z6{<{%8C2!K>=Q-Kkw1TR`526`0`irjHykMx&7e~c>^*<1b2%Bsz^oqPXl}*k$30LC
zeAh!9!%GX9d9PcvE5a6~Vc0_1-8Bve0qVlUbnZmO-9^UXSspGrLVcvjL1MUQ;2sB9
zt$76x<aUnQH;4>ipdnmL<My6<FOy7UAUQ&u#8<^Di}}W2hSo-i9ZdPg+O$l*v7DhV
zqr`cp!o6mjj;NqBLl?w}YDaF6*Fkq<#|JX8<4(5xOA^n3OO}|xx%)WIA$=K`kR_&)
ziIEyL8PAl<bkJj%=nfahiq_DaB^rd$9Xkyn<In?l#)>)^KTI_6dqUFeNW)Nu?iwcc
zmYe6tOuj=JQjs$h{Kt#25LPWZz~~X;J@X$cueFedKIj@^bR~jvyl4e`v&FCZ!kgQ6
zk%ml$ZWt-1$j!HQPU}P((vX>HWX3_}dpJ6SMvLE=D{}$68;Pz_ZLY8hVtc3=BR=J4
zJB+R5f7;H_ZDYkXJlS8LvWIUhWy)8=#R$=t78HtoOofx<uHMBlF);MPB+<{&eAu&o
zDWoBpSt%RbmT%%x@rAiZ{*o<56)RE2?)Ox2psN(^;e%zUV$Jrsdr3nQx&}eRCCqI}
zrDy{$mWy|I57(hlq+u{azbX?G<>uW!x8Cv3AjnLD1FKOl2I&F6?dcE(-E&2L)irSl
zU-hf~ucTo#LyK36>2mI5%yu~`Vc<@MSSqyh<5;o?dxMvkF~reTqJcb#{rh4vAF)_i
zd<>&Sff%KTO6%mq|1^lHFkbB8PPM)ly#wN}oaJ(Z8Lm#bidl&+Ieb;EPoSMPif08O
zd49nW9E%c$lI`LYM~)=U$swf-EI1}E5X72I`^f|h2l;133F41q{YT78`W0seV%29w
zywDi2B#)Wh$zdb5JWe$jGEaz^r0D(J_eq1cm3U6<3hYVoHqlQ%eS|c48^OF}RRDN?
zilANIuu{^{!3bXJtqO*)QwWyMQEYw<YCt+C6394>o`>$@;5R)*XT(Q*L*VFK{zqqq
zjyx+8P7&4p+&uoLdrZZuR|Anq&s`Mf@<LVr2o~ioVra67YPut78TSB-+<{ru+P50g
z!c~vS`ljO<Z-SE}5On^=^f-BLYh?E5trF?VNY$5ep+Gn9IhkSvpTw!U!k#FVfz&R{
zXUHnV(xAAPDhZ;aRng?zTi=`~fMB{2Ood0$s&L{JIO73Xi{MZrm<CH?R1w0sQQ|_f
z#u##TFV#>8iN%mhUTB=j2E?);D?r;1mS0p^Ks|c+hdY9@`5%@s)H6;so3$Lg!nuxb
zmaS%1fl;}CfL2d$C8_!gHivo3hp2r2@ArZgZTEr{?*)}6pxUIW;FhhvJO_7Ha6PXY
zNfu>}ewU13K;{MQ&#T(Q-_EOgk|+yx49P)Ig4&BJU+_p#n?uLXR0bjS%*>}`A9~=z
zMb%Wej~L0=?V-fc0a+I#+Z~RisNEs^0<vSj*}93$HL{B@siNT-V&?BUM(|`IVhIJ1
z(?{JI@@iE{=JO}TOd(4U?cItdfn%M@!1)BP`+!VkU|^kU8vl6d4L`oAhM_m>RPQqi
ziqAv*3x)xF*&&C9gW5T?-RG(tR@kuO@D{$gT{~v$Gjp{QM>wah#u#g()zbv$?mwI(
zWlSZ`gLri+e0osVO;|P024{bzOb^uwY9(BcQOA?#2S5A-*GHwSmk|tuoLF_Vuz%5>
zzGR)T@x}yoCb-9`4cubSlRe2&1~TK+%Y?H(9-M`%6$vSc>NtqZl?)_o|F$k<8Dc4I
zk%q>rt>IcPwLxfKYf|}pxNtznAb!+v*VBB{G=?6FSC3;91A9#$%m1KaDpwmd7JsK1
zN+DTI8R3_tv1?JI6GNq0YQc$U9xSdU70hbcfVN(yUr_fIKG?a@jZ8-nmRwf%fG?vl
z-}_pR;babuXsvp#a5eFPAI>)<SYJ^OgV;JGR1Ca!6(hl-I`t~@bE=&iUe{L3G*Eq2
z?Fmn>s0sAHh{>NW^u3Qe7dDl5)kQ%4MRiXBT5deUd5&24Rdog|xP-jYQ>iti+K6qu
zs@}*y)Gi6<n`SU{(q(lH!{35iReV!DL!bOZUCY?qUgNn8Rf)e(-pbdLcZmtiRcR{8
zyQf0$k;P1vEXkNsEClCjBDl*Zoj%1uhMBpV<-#SFTaBqzy-F=TPt#LKdN+9$PI<(X
z6Ez~#=4lMv)cO^sWD^6{`I`61g_;{ra44#9=~++G41`_BG%U0)&~z7$6y=GyP_e1i
zB+XDbQJ}%1e(}QsoUK)|-r%{yFA9<hHPQUd3dg_URH%Zi1DX&xdR*fM?IvpsiVfC-
zZ26|om^H22H4axVT3n>bVH70}x0Cs%n@kmY6yV=qpHBNt)#Nh5LEA5*aU2R6I&O((
zgcF%pzPb*V%o<rjTX%E!X(GuDt^YxsY-{k+fH_2i1J!gVr<Q!Tm#jpvKO8%(35DAI
z8W-3}HQ^-V$aqJr>l&OPuRZbmH4$XPrgeL9O{|gi{oRvB;+HP9d<`bG#h4Kv*pIA0
zW~z~y1jgpv(hK{Zw61^ynq@-mSEuD<1~S0<6U}tq#k#17Z#v1)=?66*Gm6P~-Ani%
z%$YT7Wil({#3`e7M>QiEVf(7X<52KHhEDiG^MRAlvfom~Fl$@Gs9^auwGBA`rU~bi
zXM*&kkb$h<G)3fl!{c4#EV35Ct`^OF$ZkQ#*DFrkC8rqputjs4d_Hx|6LK6G^Nft*
ziWY4TQvP(&aWV_BaIn6kbAVh{tAPb_t%0O|A29>>v9-95p+^Nj$+d}OS6odj$wM%p
z4Qyex0z67adXetTi`FE27(Hs}yh3XaPow+{iUk|q>&rJiW!AM;{8E3tmcC=E{gB~v
zdM`@nn=aw1<+aBdVdnG9At?J>h9<abuRD?Bc{Y8?Ol%g`)>peIZC|2n-nJO8#Ov@L
ztu^1kWUUiaMPUN97o@B=JujlPsoZDV?T3-m45UPB&u}#V`!M7FtBldk<0`uEdWqWs
z=wr2A;b^?p44%Yj4cuz={N=CU8Kk0PWGI=3okhb(G1>t5HddR=Sv)FvYGm|?)6P)X
z+2nl3H%(^Nw`waZ(`sl_oVF9Ac=|lTl5e`htV53#py&Z~d6IS#BlOE1)|GFzvSX+s
zOUpWw`ZGVRz;(A?mJKNjv=ZFjq}RcKQf(yHB`fwzvYCPEQtcLQKy~^cyd8q11=_{j
z@cZ$M@qXpb0__6s>w5)<jH>b%qN?BSP5mC10lZwOEg|de{9<q}u9qc4%R+5;xcNwH
z1NDng<)FDg3?zeaBo=E26aQe<AYzoz87@8dvxSTIv;^8e*1Exw#ae?xvvk&ezG*qL
zp;cn_x7tiPdWqJJ;nn9OckoSEuEk~A>kMz(#dn}dv-uUALSoq;U!uSHLjC{0zcm6n
zJ7MjMF)b}$wBTpf+K;|!{eRzPZLTwYcuTv(lCoBQ>z&Ds!V6!JUF=3#fw4@^)FH}m
zqk<+(^E=>7oj>%O?&!R9(uHSc)~u{uMuzdMB_m@*_Q<S><BLq`#p`}`&O%WC-7Jf5
z5@mElqu+OKic}}>Jih4$Yr<e@%Zs-wsq~TOR)#LI(mk@Vw1|nv+h^W`WmuWath{(&
z$C?+0dscL^x9*BFFWqRd<r`<Qdj{a!mR{X-e%6YE3uAWjO{-Wl4#Polm|Rs8G%cN>
zlaq9}oQ1G6U%BzkX17@C7VTBnj`;o3^*WixzArOCW|+>8E*`B*H|M(~F9_os_pmj!
zTQ-@}`-Qr1oCW>7FQ?({-Ds97cYCD^^!yT?zq#eXKEK@Io4vDHf=4?XG)(23=@)fg
zowW32rB30(Kb&+gmH#o3rE&*(ca91*x})~I^Rx|3eA6rza-!rRv^?Fr3q#MI(b>5u
zZs>lw%s0+p742mBy75w9c`QwS$J^7C*5B2AV5RVSd@6%)Okpi;WU_Wpog<H<fh)b6
zOz46}ovRDKUpIXb-#C+{d7Hd*O-Vz~bEPDo-6ji!@OwIMxb1+C9`2U<?}<X|S$dUk
z{E)S>Hue*qC6A=r4|(@Dr54Wm7#GC_vqN?K^TDjO!sxCZ&PGtbB)ORh?Hi~cZmtjw
zdk64M16UhdnT&;exrvsV-}iQ8=)UgyG#7>I<*OKc8Eb2Y$79ei%gl%7uaXZirIzV>
z(Oh_*a3+jz7ALbb$--x}KMfh7pYCG0xyxriA?nCFxXEOGP-d{nr-~S#6%zU7{4NEV
z$nKDZLUD;c7(5o}yHouvy`_balkEJIZ&p8LX~q(tTY<FOBK=+$Vcwi>J{ZcL1^p3r
zBDMP5r%a*^oArYg!fz=Rk$kgXFiU5+`gRDRi8cC@E|y}+@e|m<mUXe0$+S>>(ma<c
zM))q5sCBLW8nIk6TCm}pwLh}1E=K>QJ4_zsclZ_t(}&me|8NoFRBq=mYB~$YoY*OJ
zdXw+vV0xrcuONbXtcfSz9AL|Wbrm~_eje6gX&0g9O87Cp+4>%fFKndGUC8?noUf2V
zcBd>D)+b6GSE(c(G@eofDH(qL6EYqhI-^5`4MxzldWHuXji9=f4K`j<50bAvUPi_t
z=m(cd^-j<|NwSAhFUcT$olyUh3_=g&`AY5Ku@PIpquoX_%!uVDNxtx4zs|sg)pWZ}
z`ms>yE%g`b>mNQR=|;jwNs=4b`e37R&%YZ;(u~--B*_&D5mSu%W?=~5*oEEIwkz+K
zRP?@&^s5OkUA_N+Z=A}~M;)cHrow&;>#zA{8%vfB(MT;WH1WFlv&fl$TM|c#Sr{HI
z%^|aA9#1D@F_IRtVk9qE)Jr1Z8Y3CFG>@MTqhJ^sBaPwihrj2FnL%xgG?3fZ>}SA~
z@aie0b6t*ixJd@Huq;*@LgG~ez9yL%%?mEYNlsuHCq)xkIc{L%5X3<;g3l)6AT5f+
zF4*w*x{&!8HBKtww-yXM!Z$`>uDzr{Q^lU%iWt7}5W8!)aYL!zFKOx7L}|Jy{mfaF
z)=?P0v?U0o+2C|ekxX5M+xZz2a8BN0A>$;ULwBU9vI5D^d+YJhh24#hF4%J<?3^S;
z^7umHSL}2*)Wu0rpqn6tll^r~=43ANqS|<eCP>}6y3IdtCGW5x&yl8c35TleU;SZ#
zqd8I-d2sg1Suz>hbcRpzB?-FZN>OCQ#hQ2C1pkhpFm!q7r(^^&;ll!{Bk1x_`O~rf
z7s*Im#d*>w{^f6%&hkwbEWMp4{c37ml+eqKZ+yw_-h*e`CPf8pNm2iaQne}lWRt3Y
zN5S^04417<I!kX%k$Sn(8DFZ#`g1iN13n_zENE9sBe}btbHhj~3#(U3{e*q)?8hX9
z-Gi?yK(Yh#3QXblSM_&E9~P1-q`q7bgj_PRw^c~}I8`6Zbdtp4v%Az=h#vHH8R=_m
zdIuy2m>VxQaJQ^PQw#?muaf$3)RM#-XM-h3>HN-{p2PU(TUeS45}5EG2jA|+H|4X`
zvPv4p&}ZK2&0fOB61Vp-`N1rmx?W0jrAhtN*Hs+*?l>PZgoO)#mxglZk7qZN0W1U@
zkkYvGh09-(F)WlFkj8QY18bj>{w!o3l$^o!AlB)l+T16vkd1HLd5C!AYo^N>o|`kW
z_2iTLw<n*W0e{VtPs`UQpKU54UP+Kb-}<qEe^AI<KQ;*H{O3P5@DB+N{hvSjyuiQu
cQN^GB)*xWjA?d9X>tO%aC!SP(SZXo*581Mk=>Px#

diff --git a/checker/Cargo.toml b/checker/Cargo.toml
index 1a932dac..8442e621 100644
--- a/checker/Cargo.toml
+++ b/checker/Cargo.toml
@@ -29,7 +29,7 @@ doctest = false # and no doc tests
 [dependencies]
 bincode = { version = "*", features = ["i128"] }
 cargo_metadata = "*"
-clap = "*"
+clap = "=4.4.8"
 env_logger = "*"
 fs2 = "*"
 itertools = "*"
@@ -43,13 +43,14 @@ rayon = "*"
 regex = "1.5.6"
 rpds = { version = "*", features = ["serde"] }
 rustc_tools_util = "*"
-serde = { version = "*", features = ["derive", "alloc", "rc"] }
+serde = { version = "=1.0.192", features = ["derive", "alloc", "rc"] }
 serde_json = "*"
 shellwords = "*"
 sled = "*"
 tar = "0.4.38"
 tempfile = "*"
-z3-sys = { version = "*", git="https://github.com/prove-rs/z3.rs.git", optional = true }
+triomphe = "=0.1.9"
+z3-sys = { version = "*", git = "https://github.com/prove-rs/z3.rs.git", rev = "cb7b79a61433673a5e6b07559cc661a97b5a84cf", optional = true }
 
 [dev-dependencies]
 walkdir = "*"
@@ -59,7 +60,7 @@ walkdir = "*"
 # of the cargo command using it, e.g.
 # `--extern contracts=$PROJECT_DIR$/target/debug/deps/libcontracts-c8ea818f33e46907.dylib`
 # or similar, and to integration_tests.rs (search for extern_deps there).
-# We set the dep to a specific revision so we don't get paths as above not longer working after update of the repo
+# We set the dep to a specific revision, so we don't get paths as above no longer working after update of the repo
 # and the Cargo.lock.
 contracts = { version = "0.6.0", features = ["mirai_assertions"] }
 
diff --git a/checker/src/cargo_mirai.rs b/checker/src/cargo_mirai.rs
index c97ecd97..e11eb3f5 100644
--- a/checker/src/cargo_mirai.rs
+++ b/checker/src/cargo_mirai.rs
@@ -33,11 +33,11 @@ pub fn main() {
     }
 
     match std::env::args().nth(1).as_ref().map(AsRef::<str>::as_ref) {
-        Some(s) if s.ends_with("mirai") => {
+        Some(s) if s.ends_with("mirai") || s.ends_with("mirai.exe") => {
             // Get here for the top level cargo execution, i.e. "cargo mirai".
             call_cargo();
         }
-        Some(s) if s.ends_with("rustc") => {
+        Some(s) if s.ends_with("rustc") || s.ends_with("rustc.exe") => {
             // 'cargo rustc ..' redirects here because RUSTC_WRAPPER points to this binary.
             // execute rustc with MIRAI applicable parameters for dependencies and call MIRAI
             // to analyze targets in the current package.
diff --git a/checker/src/z3_solver.rs b/checker/src/z3_solver.rs
index 0a8be055..b40043c6 100644
--- a/checker/src/z3_solver.rs
+++ b/checker/src/z3_solver.rs
@@ -1139,7 +1139,10 @@ impl Z3Solver {
             Expression::TaggedExpression { operand, .. } => {
                 self.get_as_numeric_z3_ast(&operand.expression)
             }
-            Expression::Transmute { operand, target_type } => {
+            Expression::Transmute {
+                operand,
+                target_type,
+            } => {
                 if target_type.is_integer() || target_type.is_floating_point_number() {
                     self.numeric_cast(&operand.expression, *target_type)
                 } else {