From eb5796f1c6832d2695b6668303f712261b40d29b Mon Sep 17 00:00:00 2001
From: Samuel Thomas <sgpthomas@gmail.com>
Date: Mon, 25 Nov 2024 21:04:34 -0600
Subject: [PATCH] Adjust lifetimes on `ModelIter` to make them more permissive
 (#324)

---
 z3/src/model.rs | 12 ++++++------
 z3/tests/lib.rs | 29 +++++++++++++++++++++++++++++
 2 files changed, 35 insertions(+), 6 deletions(-)

diff --git a/z3/src/model.rs b/z3/src/model.rs
index 5cf4b318..811eb98c 100644
--- a/z3/src/model.rs
+++ b/z3/src/model.rs
@@ -130,7 +130,7 @@ impl<'ctx> Model<'ctx> {
         }
     }
 
-    pub fn iter(&'ctx self) -> ModelIter<'ctx> {
+    pub fn iter<'a>(&'a self) -> ModelIter<'a, 'ctx> {
         self.into_iter()
     }
 }
@@ -162,15 +162,15 @@ impl<'ctx> Drop for Model<'ctx> {
 
 #[derive(Debug)]
 /// <https://z3prover.github.io/api/html/classz3py_1_1_model_ref.html#a7890b7c9bc70cf2a26a343c22d2c8367>
-pub struct ModelIter<'ctx> {
-    model: &'ctx Model<'ctx>,
+pub struct ModelIter<'a, 'ctx> {
+    model: &'a Model<'ctx>,
     idx: u32,
     len: u32,
 }
 
-impl<'ctx> IntoIterator for &'ctx Model<'ctx> {
+impl<'a, 'ctx> IntoIterator for &'a Model<'ctx> {
     type Item = FuncDecl<'ctx>;
-    type IntoIter = ModelIter<'ctx>;
+    type IntoIter = ModelIter<'a, 'ctx>;
 
     fn into_iter(self) -> Self::IntoIter {
         ModelIter {
@@ -181,7 +181,7 @@ impl<'ctx> IntoIterator for &'ctx Model<'ctx> {
     }
 }
 
-impl<'ctx> Iterator for ModelIter<'ctx> {
+impl<'a, 'ctx> Iterator for ModelIter<'a, 'ctx> {
     type Item = FuncDecl<'ctx>;
 
     fn next(&mut self) -> Option<Self::Item> {
diff --git a/z3/tests/lib.rs b/z3/tests/lib.rs
index 0f206684..465065dd 100644
--- a/z3/tests/lib.rs
+++ b/z3/tests/lib.rs
@@ -1973,3 +1973,32 @@ fn test_atleast() {
     assert!(matches!(solver.check(), SatResult::Unsat));
     solver.pop(1);
 }
+
+#[test]
+fn test_model_iter() {
+    let cfg = Config::new();
+    let ctx = Context::new(&cfg);
+    let solver = Solver::new(&ctx);
+
+    let a = ast::Int::new_const(&ctx, "a");
+    let two = ast::Int::from_u64(&ctx, 2);
+    solver.assert(&a._eq(&two));
+    solver.check();
+
+    let model = solver.get_model().unwrap();
+
+    // consume a model and return some asts constructed from it
+    // this didn't compile before pr#324
+    fn consume_model(model: Model) -> Vec<ast::Dynamic> {
+        let mut asts = vec![];
+        for func in &model {
+            asts.push(func.apply(&[]));
+        }
+        asts
+    }
+
+    assert_eq!(
+        consume_model(model),
+        vec![ast::Dynamic::new_const(&ctx, "a", &Sort::int(&ctx))]
+    );
+}