From ae6589d9b4e3f67ed373271b0e52da9e39d291fa Mon Sep 17 00:00:00 2001 From: Jonas Hansen Date: Thu, 28 Apr 2022 17:01:56 +0200 Subject: [PATCH] Erase regions in constraint solving --- .../src/encoder/mir/specifications/constraints.rs | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) 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) {