diff --git a/z3/src/solver.rs b/z3/src/solver.rs
index a78e1fcb..5ba1360b 100644
--- a/z3/src/solver.rs
+++ b/z3/src/solver.rs
@@ -176,7 +176,7 @@ impl<'ctx> Solver<'ctx> {
     }
 
     // Return a vector of assumptions in the solver.
-    pub fn get_assertions(&self) -> Vec<ast::Bool> {
+    pub fn get_assertions(&self) -> Vec<ast::Bool<'ctx>> {
         let z3_vec = unsafe { Z3_solver_get_assertions(self.ctx.z3_ctx, self.z3_slv) };
 
         (0..unsafe { Z3_ast_vector_size(self.ctx.z3_ctx, z3_vec) })
diff --git a/z3/tests/lib.rs b/z3/tests/lib.rs
index 50a1d896..e1332955 100644
--- a/z3/tests/lib.rs
+++ b/z3/tests/lib.rs
@@ -124,6 +124,26 @@ fn test_cloning_ast() {
     assert_eq!(yv, 0);
 }
 
+fn get_some_solver_assertions(ctx: &Context) -> Vec<ast::Bool> {
+    let s = Solver::new(ctx);
+    let x = ast::Int::new_const(ctx, "x");
+    let y = ast::Int::new_const(ctx, "y");
+    s.assert(&x.gt(&y));
+    s.get_assertions()
+}
+
+#[test]
+fn test_solver_get_assertions_lifetime() {
+    // This makes sure that the assertions created in the function
+    // using the solver have the lifetime of the context rather
+    // than the solver.
+    let _ = env_logger::try_init();
+    let cfg = Config::new();
+    let ctx = Context::new(&cfg);
+    let assertions = get_some_solver_assertions(&ctx);
+    assert_eq!(assertions.len(), 1);
+}
+
 #[test]
 fn test_format() {
     let cfg = Config::new();