diff --git a/prusti-viper/src/encoder/mir/specifications/constraints.rs b/prusti-viper/src/encoder/mir/specifications/constraints.rs index 51fcb67df35..1473a3ad26f 100644 --- a/prusti-viper/src/encoder/mir/specifications/constraints.rs +++ b/prusti-viper/src/encoder/mir/specifications/constraints.rs @@ -153,15 +153,18 @@ pub mod trait_bounds { // contain a behavioral subtyping check which will be performed on the // resolved spec. let param_env_lookup = if let Some(caller_def_id) = context.caller_proc_def_id { - env.tcx().param_env(caller_def_id) + env.tcx().param_env_reveal_all_normalized(caller_def_id) } else { - env.tcx().param_env(context.proc_def_id) + env.tcx().param_env_reveal_all_normalized(context.proc_def_id) }; let all_bounds_satisfied = param_env_constraint .caller_bounds() .iter() - .all(|predicate| env.evaluate_predicate(predicate, param_env_lookup)); + .all(|predicate| { + let predicate = env.tcx().erase_regions(predicate); + env.evaluate_predicate(predicate, param_env_lookup) + }); trace!("Constraint fulfilled: {all_bounds_satisfied}"); all_bounds_satisfied @@ -228,7 +231,7 @@ pub mod trait_bounds { .cloned() .unwrap_or_default(); for spec_id in pres.iter().chain(posts.iter()) { - let param_env = env.tcx().param_env(spec_id.to_def_id()); + let param_env = env.tcx().param_env_reveal_all_normalized(spec_id.to_def_id()); let spec_span = env.tcx().def_span(spec_id.to_def_id()); let attrs = env.tcx().get_attrs(spec_id.to_def_id()); if has_trait_bounds_ghost_constraint(attrs) {