From 0879a168c933a8c52be7d6450f6feeb8fbf1da01 Mon Sep 17 00:00:00 2001
From: Mark <mark.denhoed@cs.ox.ac.uk>
Date: Mon, 30 Sep 2024 11:43:02 +0100
Subject: [PATCH 1/7] Update emscripten

---
 .github/workflows/rust.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml
index 21341d23..03ef09ea 100644
--- a/.github/workflows/rust.yml
+++ b/.github/workflows/rust.yml
@@ -10,7 +10,7 @@ env:
   CARGO_INCREMENTAL: 0
   CARGO_REGISTRIES_CRATES_IO_PROTOCOL: sparse
   RUSTFLAGS: "-D warnings"
-  EMSCRIPTEN_VERSION: "3.1.59" # Change back to `latest` once Z3 4.13.1 or later is out.
+  EMSCRIPTEN_VERSION: "latest"
 
 jobs:
   check-formatting:

From 9e4b455386d26e9b340afbc7f94f155b7af8730b Mon Sep 17 00:00:00 2001
From: Mark <mark.denhoed@cs.ox.ac.uk>
Date: Mon, 30 Sep 2024 12:02:19 +0100
Subject: [PATCH 2/7] Bump z3 submodule to new release

---
 z3-sys/z3 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/z3-sys/z3 b/z3-sys/z3
index 3049f578..9a8ff749 160000
--- a/z3-sys/z3
+++ b/z3-sys/z3
@@ -1 +1 @@
-Subproject commit 3049f578a8f98a0b0992eca193afe57a73b30ca3
+Subproject commit 9a8ff74924561557f2b0e748f95a7764540e866a

From ee4e584ba14ab5e61b9cc84670aff02bf6a4d274 Mon Sep 17 00:00:00 2001
From: Mark <mark.denhoed@cs.ox.ac.uk>
Date: Mon, 2 Dec 2024 16:27:30 +0000
Subject: [PATCH 3/7] Pin to cc 1.1 for now

---
 z3-sys/Cargo.toml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/z3-sys/Cargo.toml b/z3-sys/Cargo.toml
index 36f62fe6..84208b33 100644
--- a/z3-sys/Cargo.toml
+++ b/z3-sys/Cargo.toml
@@ -17,6 +17,7 @@ repository = "https://github.com/prove-rs/z3.rs.git"
 
 [build-dependencies]
 bindgen = { version = "0.70", default-features = false, features = ["runtime"] }
+cc = "~1.1"
 cmake = { version = "0.1.49", optional = true }
 pkg-config = "0.3.27"
 vcpkg = { version = "0.2.15", optional = true }

From 0eb903d6f6920f702861988809dd12416781b452 Mon Sep 17 00:00:00 2001
From: Mark <mark.denhoed@cs.ox.ac.uk>
Date: Mon, 9 Dec 2024 09:45:33 +0000
Subject: [PATCH 4/7] Add expect lint annotation

---
 z3/src/ast.rs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/z3/src/ast.rs b/z3/src/ast.rs
index 577cfe74..6507abff 100644
--- a/z3/src/ast.rs
+++ b/z3/src/ast.rs
@@ -2317,6 +2317,7 @@ pub fn exists_const<'ctx>(
 /// let f_f_3: ast::Int = f.apply(&[&f.apply(&[&ast::Int::from_u64(&ctx, 3)])]).try_into().unwrap();
 /// assert_eq!(3, model.eval(&f_f_3, true).unwrap().as_u64().unwrap());
 /// ```
+#[expect(clippy::too_many_arguments)]
 pub fn quantifier_const<'ctx>(
     ctx: &'ctx Context,
     is_forall: bool,

From 419643b10a8e03458e4b6ef574098124d93dd6b2 Mon Sep 17 00:00:00 2001
From: Mark <mark.denhoed@cs.ox.ac.uk>
Date: Mon, 9 Dec 2024 09:48:39 +0000
Subject: [PATCH 5/7] Elide lifetimes

---
 z3/src/context.rs       |  6 +++---
 z3/src/func_decl.rs     |  6 +++---
 z3/src/func_entry.rs    |  6 +++---
 z3/src/func_interp.rs   |  6 +++---
 z3/src/goal.rs          |  8 ++++----
 z3/src/model.rs         |  8 ++++----
 z3/src/optimize.rs      |  6 +++---
 z3/src/params.rs        |  6 +++---
 z3/src/pattern.rs       |  6 +++---
 z3/src/probe.rs         |  8 ++++----
 z3/src/rec_func_decl.rs |  6 +++---
 z3/src/solver.rs        |  6 +++---
 z3/src/sort.rs          | 12 ++++++------
 z3/src/statistics.rs    |  8 ++++----
 z3/src/tactic.rs        |  8 ++++----
 15 files changed, 53 insertions(+), 53 deletions(-)

diff --git a/z3/src/context.rs b/z3/src/context.rs
index 65a362ef..eaa51a2b 100644
--- a/z3/src/context.rs
+++ b/z3/src/context.rs
@@ -59,7 +59,7 @@ impl Context {
     }
 }
 
-impl<'ctx> ContextHandle<'ctx> {
+impl ContextHandle<'_> {
     /// Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.
     pub fn interrupt(&self) {
         unsafe {
@@ -68,8 +68,8 @@ impl<'ctx> ContextHandle<'ctx> {
     }
 }
 
-unsafe impl<'ctx> Sync for ContextHandle<'ctx> {}
-unsafe impl<'ctx> Send for ContextHandle<'ctx> {}
+unsafe impl Sync for ContextHandle<'_> {}
+unsafe impl Send for ContextHandle<'_> {}
 
 impl Drop for Context {
     fn drop(&mut self) {
diff --git a/z3/src/func_decl.rs b/z3/src/func_decl.rs
index 0d4f73e9..307e13eb 100644
--- a/z3/src/func_decl.rs
+++ b/z3/src/func_decl.rs
@@ -99,7 +99,7 @@ impl<'ctx> FuncDecl<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Display for FuncDecl<'ctx> {
+impl fmt::Display for FuncDecl<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         let p = unsafe { Z3_func_decl_to_string(self.ctx.z3_ctx, self.z3_func_decl) };
         if p.is_null() {
@@ -112,13 +112,13 @@ impl<'ctx> fmt::Display for FuncDecl<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Debug for FuncDecl<'ctx> {
+impl fmt::Debug for FuncDecl<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Display>::fmt(self, f)
     }
 }
 
-impl<'ctx> Drop for FuncDecl<'ctx> {
+impl Drop for FuncDecl<'_> {
     fn drop(&mut self) {
         unsafe {
             Z3_dec_ref(
diff --git a/z3/src/func_entry.rs b/z3/src/func_entry.rs
index a1e2f33d..2d287db2 100644
--- a/z3/src/func_entry.rs
+++ b/z3/src/func_entry.rs
@@ -41,7 +41,7 @@ impl<'ctx> FuncEntry<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Display for FuncEntry<'ctx> {
+impl fmt::Display for FuncEntry<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         write!(f, "[")?;
         self.get_args()
@@ -52,13 +52,13 @@ impl<'ctx> fmt::Display for FuncEntry<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Debug for FuncEntry<'ctx> {
+impl fmt::Debug for FuncEntry<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Display>::fmt(self, f)
     }
 }
 
-impl<'ctx> Drop for FuncEntry<'ctx> {
+impl Drop for FuncEntry<'_> {
     fn drop(&mut self) {
         unsafe {
             Z3_func_entry_dec_ref(self.ctx.z3_ctx, self.z3_func_entry);
diff --git a/z3/src/func_interp.rs b/z3/src/func_interp.rs
index 889a896c..41042ff0 100644
--- a/z3/src/func_interp.rs
+++ b/z3/src/func_interp.rs
@@ -68,7 +68,7 @@ impl<'ctx> FuncInterp<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Display for FuncInterp<'ctx> {
+impl fmt::Display for FuncInterp<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         write!(f, "[")?;
         self.get_entries().into_iter().try_for_each(|e| {
@@ -95,13 +95,13 @@ impl<'ctx> fmt::Display for FuncInterp<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Debug for FuncInterp<'ctx> {
+impl fmt::Debug for FuncInterp<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Display>::fmt(self, f)
     }
 }
 
-impl<'ctx> Drop for FuncInterp<'ctx> {
+impl Drop for FuncInterp<'_> {
     fn drop(&mut self) {
         unsafe {
             Z3_func_interp_dec_ref(self.ctx.z3_ctx, self.z3_func_interp);
diff --git a/z3/src/goal.rs b/z3/src/goal.rs
index 66a9e951..7788914f 100644
--- a/z3/src/goal.rs
+++ b/z3/src/goal.rs
@@ -5,7 +5,7 @@ use z3_sys::*;
 
 use crate::{ast, ast::Ast, Context, Goal};
 
-impl<'ctx> Clone for Goal<'ctx> {
+impl Clone for Goal<'_> {
     fn clone(&self) -> Self {
         Self {
             ctx: self.ctx,
@@ -109,7 +109,7 @@ impl<'ctx> Goal<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Display for Goal<'ctx> {
+impl fmt::Display for Goal<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         let p = unsafe { Z3_goal_to_string(self.ctx.z3_ctx, self.z3_goal) };
         if p.is_null() {
@@ -122,13 +122,13 @@ impl<'ctx> fmt::Display for Goal<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Debug for Goal<'ctx> {
+impl fmt::Debug for Goal<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Display>::fmt(self, f)
     }
 }
 
-impl<'ctx> Drop for Goal<'ctx> {
+impl Drop for Goal<'_> {
     fn drop(&mut self) {
         unsafe {
             Z3_goal_dec_ref(self.ctx.z3_ctx, self.z3_goal);
diff --git a/z3/src/model.rs b/z3/src/model.rs
index 811eb98c..6c97ce41 100644
--- a/z3/src/model.rs
+++ b/z3/src/model.rs
@@ -135,7 +135,7 @@ impl<'ctx> Model<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Display for Model<'ctx> {
+impl fmt::Display for Model<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         let p = unsafe { Z3_model_to_string(self.ctx.z3_ctx, self.z3_mdl) };
         if p.is_null() {
@@ -148,13 +148,13 @@ impl<'ctx> fmt::Display for Model<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Debug for Model<'ctx> {
+impl fmt::Debug for Model<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Display>::fmt(self, f)
     }
 }
 
-impl<'ctx> Drop for Model<'ctx> {
+impl Drop for Model<'_> {
     fn drop(&mut self) {
         unsafe { Z3_model_dec_ref(self.ctx.z3_ctx, self.z3_mdl) };
     }
@@ -181,7 +181,7 @@ impl<'a, 'ctx> IntoIterator for &'a Model<'ctx> {
     }
 }
 
-impl<'a, 'ctx> Iterator for ModelIter<'a, 'ctx> {
+impl<'ctx> Iterator for ModelIter<'_, 'ctx> {
     type Item = FuncDecl<'ctx>;
 
     fn next(&mut self) -> Option<Self::Item> {
diff --git a/z3/src/optimize.rs b/z3/src/optimize.rs
index 49ffb5b0..70a8dc09 100644
--- a/z3/src/optimize.rs
+++ b/z3/src/optimize.rs
@@ -274,7 +274,7 @@ impl<'ctx> Optimize<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Display for Optimize<'ctx> {
+impl fmt::Display for Optimize<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         let p = unsafe { Z3_optimize_to_string(self.ctx.z3_ctx, self.z3_opt) };
         if p.is_null() {
@@ -287,13 +287,13 @@ impl<'ctx> fmt::Display for Optimize<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Debug for Optimize<'ctx> {
+impl fmt::Debug for Optimize<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Display>::fmt(self, f)
     }
 }
 
-impl<'ctx> Drop for Optimize<'ctx> {
+impl Drop for Optimize<'_> {
     fn drop(&mut self) {
         unsafe { Z3_optimize_dec_ref(self.ctx.z3_ctx, self.z3_opt) };
     }
diff --git a/z3/src/params.rs b/z3/src/params.rs
index 2166b957..6a7618c1 100644
--- a/z3/src/params.rs
+++ b/z3/src/params.rs
@@ -99,7 +99,7 @@ pub fn reset_all_global_params() {
     unsafe { Z3_global_param_reset_all() };
 }
 
-impl<'ctx> fmt::Display for Params<'ctx> {
+impl fmt::Display for Params<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         let p = unsafe { Z3_params_to_string(self.ctx.z3_ctx, self.z3_params) };
         if p.is_null() {
@@ -112,13 +112,13 @@ impl<'ctx> fmt::Display for Params<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Debug for Params<'ctx> {
+impl fmt::Debug for Params<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Display>::fmt(self, f)
     }
 }
 
-impl<'ctx> Drop for Params<'ctx> {
+impl Drop for Params<'_> {
     fn drop(&mut self) {
         unsafe { Z3_params_dec_ref(self.ctx.z3_ctx, self.z3_params) };
     }
diff --git a/z3/src/pattern.rs b/z3/src/pattern.rs
index 9d869720..5f1bc8b3 100644
--- a/z3/src/pattern.rs
+++ b/z3/src/pattern.rs
@@ -46,7 +46,7 @@ impl<'ctx> Pattern<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Debug for Pattern<'ctx> {
+impl fmt::Debug for Pattern<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         let p = unsafe { Z3_pattern_to_string(self.ctx.z3_ctx, self.z3_pattern) };
         if p.is_null() {
@@ -59,13 +59,13 @@ impl<'ctx> fmt::Debug for Pattern<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Display for Pattern<'ctx> {
+impl fmt::Display for Pattern<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Debug>::fmt(self, f)
     }
 }
 
-impl<'ctx> Drop for Pattern<'ctx> {
+impl Drop for Pattern<'_> {
     fn drop(&mut self) {
         unsafe {
             Z3_dec_ref(self.ctx.z3_ctx, self.z3_pattern as Z3_ast);
diff --git a/z3/src/probe.rs b/z3/src/probe.rs
index 2fa44e55..62a924fc 100644
--- a/z3/src/probe.rs
+++ b/z3/src/probe.rs
@@ -167,25 +167,25 @@ impl<'ctx> Probe<'ctx> {
     }
 }
 
-impl<'ctx> Clone for Probe<'ctx> {
+impl Clone for Probe<'_> {
     fn clone(&self) -> Self {
         unsafe { Self::wrap(self.ctx, self.z3_probe) }
     }
 }
 
-impl<'ctx> fmt::Display for Probe<'ctx> {
+impl fmt::Display for Probe<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         write!(f, "<z3.probe>")
     }
 }
 
-impl<'ctx> fmt::Debug for Probe<'ctx> {
+impl fmt::Debug for Probe<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Display>::fmt(self, f)
     }
 }
 
-impl<'ctx> Drop for Probe<'ctx> {
+impl Drop for Probe<'_> {
     fn drop(&mut self) {
         unsafe {
             Z3_probe_dec_ref(self.ctx.z3_ctx, self.z3_probe);
diff --git a/z3/src/rec_func_decl.rs b/z3/src/rec_func_decl.rs
index f1dd65b6..b43eee85 100644
--- a/z3/src/rec_func_decl.rs
+++ b/z3/src/rec_func_decl.rs
@@ -94,7 +94,7 @@ impl<'ctx> RecFuncDecl<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Display for RecFuncDecl<'ctx> {
+impl fmt::Display for RecFuncDecl<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         let p = unsafe { Z3_func_decl_to_string(self.ctx.z3_ctx, self.z3_func_decl) };
         if p.is_null() {
@@ -107,13 +107,13 @@ impl<'ctx> fmt::Display for RecFuncDecl<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Debug for RecFuncDecl<'ctx> {
+impl fmt::Debug for RecFuncDecl<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Display>::fmt(self, f)
     }
 }
 
-impl<'ctx> Drop for RecFuncDecl<'ctx> {
+impl Drop for RecFuncDecl<'_> {
     fn drop(&mut self) {
         unsafe {
             Z3_dec_ref(
diff --git a/z3/src/solver.rs b/z3/src/solver.rs
index 19bccfbc..143aa3cc 100644
--- a/z3/src/solver.rs
+++ b/z3/src/solver.rs
@@ -400,7 +400,7 @@ impl<'ctx> Solver<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Display for Solver<'ctx> {
+impl fmt::Display for Solver<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         let p = unsafe { Z3_solver_to_string(self.ctx.z3_ctx, self.z3_slv) };
         if p.is_null() {
@@ -413,13 +413,13 @@ impl<'ctx> fmt::Display for Solver<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Debug for Solver<'ctx> {
+impl fmt::Debug for Solver<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Display>::fmt(self, f)
     }
 }
 
-impl<'ctx> Drop for Solver<'ctx> {
+impl Drop for Solver<'_> {
     fn drop(&mut self) {
         unsafe { Z3_solver_dec_ref(self.ctx.z3_ctx, self.z3_slv) };
     }
diff --git a/z3/src/sort.rs b/z3/src/sort.rs
index bf462e0f..cd12903c 100644
--- a/z3/src/sort.rs
+++ b/z3/src/sort.rs
@@ -274,13 +274,13 @@ impl<'ctx> Sort<'ctx> {
     }
 }
 
-impl<'ctx> Clone for Sort<'ctx> {
+impl Clone for Sort<'_> {
     fn clone(&self) -> Self {
         unsafe { Self::wrap(self.ctx, self.z3_sort) }
     }
 }
 
-impl<'ctx> fmt::Display for Sort<'ctx> {
+impl fmt::Display for Sort<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         let p = unsafe { Z3_sort_to_string(self.ctx.z3_ctx, self.z3_sort) };
         if p.is_null() {
@@ -293,7 +293,7 @@ impl<'ctx> fmt::Display for Sort<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Debug for Sort<'ctx> {
+impl fmt::Debug for Sort<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Display>::fmt(self, f)
     }
@@ -305,9 +305,9 @@ impl<'ctx> PartialEq<Sort<'ctx>> for Sort<'ctx> {
     }
 }
 
-impl<'ctx> Eq for Sort<'ctx> {}
+impl Eq for Sort<'_> {}
 
-impl<'ctx> Drop for Sort<'ctx> {
+impl Drop for Sort<'_> {
     fn drop(&mut self) {
         unsafe {
             Z3_dec_ref(
@@ -332,7 +332,7 @@ impl<'ctx> SortDiffers<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Display for SortDiffers<'ctx> {
+impl fmt::Display for SortDiffers<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         write!(
             f,
diff --git a/z3/src/statistics.rs b/z3/src/statistics.rs
index db3b1885..ae09d6e4 100644
--- a/z3/src/statistics.rs
+++ b/z3/src/statistics.rs
@@ -79,19 +79,19 @@ impl<'ctx> Statistics<'ctx> {
     }
 }
 
-impl<'ctx> Clone for Statistics<'ctx> {
+impl Clone for Statistics<'_> {
     fn clone(&self) -> Self {
         unsafe { Self::wrap(self.ctx, self.z3_stats) }
     }
 }
 
-impl<'ctx> fmt::Display for Statistics<'ctx> {
+impl fmt::Display for Statistics<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         write!(f, "<z3.stats>")
     }
 }
 
-impl<'ctx> fmt::Debug for Statistics<'ctx> {
+impl fmt::Debug for Statistics<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         let mut s = f.debug_struct("Statistics");
         for e in self.entries() {
@@ -104,7 +104,7 @@ impl<'ctx> fmt::Debug for Statistics<'ctx> {
     }
 }
 
-impl<'ctx> Drop for Statistics<'ctx> {
+impl Drop for Statistics<'_> {
     fn drop(&mut self) {
         unsafe {
             Z3_stats_dec_ref(self.ctx.z3_ctx, self.z3_stats);
diff --git a/z3/src/tactic.rs b/z3/src/tactic.rs
index 57bfbb2f..5b79e6f9 100644
--- a/z3/src/tactic.rs
+++ b/z3/src/tactic.rs
@@ -31,7 +31,7 @@ impl<'ctx> ApplyResult<'ctx> {
     }
 }
 
-impl<'ctx> Drop for ApplyResult<'ctx> {
+impl Drop for ApplyResult<'_> {
     fn drop(&mut self) {
         unsafe {
             Z3_apply_result_dec_ref(self.ctx.z3_ctx, self.z3_apply_result);
@@ -239,7 +239,7 @@ impl<'ctx> Tactic<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Display for Tactic<'ctx> {
+impl fmt::Display for Tactic<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         let p = unsafe { Z3_tactic_get_help(self.ctx.z3_ctx, self.z3_tactic) };
         if p.is_null() {
@@ -252,13 +252,13 @@ impl<'ctx> fmt::Display for Tactic<'ctx> {
     }
 }
 
-impl<'ctx> fmt::Debug for Tactic<'ctx> {
+impl fmt::Debug for Tactic<'_> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         <Self as fmt::Display>::fmt(self, f)
     }
 }
 
-impl<'ctx> Drop for Tactic<'ctx> {
+impl Drop for Tactic<'_> {
     fn drop(&mut self) {
         unsafe {
             Z3_tactic_dec_ref(self.ctx.z3_ctx, self.z3_tactic);

From 531708c4d37f1dc0623f95e42eafb7b73b71ec32 Mon Sep 17 00:00:00 2001
From: Mark <mark.denhoed@cs.ox.ac.uk>
Date: Mon, 9 Dec 2024 09:58:02 +0000
Subject: [PATCH 6/7] Add note on cc pinning

---
 z3-sys/Cargo.toml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/z3-sys/Cargo.toml b/z3-sys/Cargo.toml
index 84208b33..4633a492 100644
--- a/z3-sys/Cargo.toml
+++ b/z3-sys/Cargo.toml
@@ -17,6 +17,8 @@ repository = "https://github.com/prove-rs/z3.rs.git"
 
 [build-dependencies]
 bindgen = { version = "0.70", default-features = false, features = ["runtime"] }
+# Temporarily pinning cc to 1.1 as 1.2 and later use -fno-exceptions, which
+# breaks the z3 build. See https://github.com/prove-rs/z3.rs/issues/328
 cc = "~1.1"
 cmake = { version = "0.1.49", optional = true }
 pkg-config = "0.3.27"

From f000c8a16e70c14a14d677306489aa146f1f696e Mon Sep 17 00:00:00 2001
From: Mark <mark.denhoed@cs.ox.ac.uk>
Date: Mon, 9 Dec 2024 10:00:19 +0000
Subject: [PATCH 7/7] Use allow instead of expect to avoid de-facto MSRV bump

---
 z3/src/ast.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/z3/src/ast.rs b/z3/src/ast.rs
index 6507abff..d04e9984 100644
--- a/z3/src/ast.rs
+++ b/z3/src/ast.rs
@@ -2317,7 +2317,7 @@ pub fn exists_const<'ctx>(
 /// let f_f_3: ast::Int = f.apply(&[&f.apply(&[&ast::Int::from_u64(&ctx, 3)])]).try_into().unwrap();
 /// assert_eq!(3, model.eval(&f_f_3, true).unwrap().as_u64().unwrap());
 /// ```
-#[expect(clippy::too_many_arguments)]
+#[allow(clippy::too_many_arguments)]
 pub fn quantifier_const<'ctx>(
     ctx: &'ctx Context,
     is_forall: bool,