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] 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);