Fix lifetime on Solver::get_assertions() result.

The return value was missing a lifetime annotation connecting it
to the context's lifetime `'ctx`, this left the Rust compiler to
tie it to the lifetime of the `Solver` reference, which was too
short.

Fixes #262.

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) })

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