Use predicate_must_hold_modulo_regions when resolving ghost constrain…

…ts to account for references in associated types

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

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 = <Self as B<'a>>::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);
+}