diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs index d6806a31038..4caf1132e51 100644 --- a/prusti-interface/src/environment/mod.rs +++ b/prusti-interface/src/environment/mod.rs @@ -549,7 +549,7 @@ impl<'tcx> Environment<'tcx> { ); self.tcx.infer_ctxt().enter(|infcx| { - infcx.predicate_must_hold_considering_regions(&obligation) + infcx.predicate_must_hold_modulo_regions(&obligation) }) } diff --git a/prusti-tests/tests/verify_overflow/pass/ghost-constraints/associated-types-6.rs b/prusti-tests/tests/verify_overflow/pass/ghost-constraints/associated-types-6.rs new file mode 100644 index 00000000000..33a93a7b64e --- /dev/null +++ b/prusti-tests/tests/verify_overflow/pass/ghost-constraints/associated-types-6.rs @@ -0,0 +1,38 @@ +// compile-flags: -Penable_ghost_constraints=true + +use prusti_contracts::*; + +trait A<'a> { + type AType; +} + +trait B<'a> { + type BType; + + #[ghost_constraint(Self: A<'a, AType = >::BType> , [ + ensures(*result > 0) + ])] + #[trusted] + fn foo(&'a self) -> &'a i32; +} + +struct S { + val: i32, +} +impl<'a> A<'a> for S { + type AType = &'a i32; +} + +impl<'a> B<'a> for S { + type BType = &'a i32; + + #[trusted] + fn foo(&'a self) -> &'a i32 { &self.val } +} + +fn main() { + let s = S { + val: 42 + }; + assert!(*s.foo() > 0); +} \ No newline at end of file