Skip to content

Commit 1670345

Browse files
committed
Move predicate normalization in constraint solver for better debugging
1 parent 47c5a0b commit 1670345

File tree

1 file changed

+9
-9
lines changed

1 file changed

+9
-9
lines changed

prusti-viper/src/encoder/mir/specifications/constraints.rs

+9-9
Original file line numberDiff line numberDiff line change
@@ -161,15 +161,7 @@ pub mod trait_bounds {
161161
let all_bounds_satisfied = param_env_constraint
162162
.caller_bounds()
163163
.iter()
164-
.all(|predicate| {
165-
// Normalize any associated type projections.
166-
// This needs to be done because ghost constraints might contain "deeply nested"
167-
// associated types, e.g. `T: A<SomeAssocType = <Self as B>::OtherAssocType`
168-
// where `<Self as B>::OtherAssocType` can be normalized to some concrete type.
169-
let normalized_predicate = env.normalize_to(predicate);
170-
171-
env.evaluate_predicate(normalized_predicate, param_env_lookup)
172-
});
164+
.all(|predicate| env.evaluate_predicate(predicate, param_env_lookup));
173165

174166
trace!("Constraint fulfilled: {all_bounds_satisfied}");
175167
all_bounds_satisfied
@@ -208,6 +200,14 @@ pub mod trait_bounds {
208200
param_env
209201
);
210202

203+
// Normalize any associated type projections.
204+
// This needs to be done because ghost constraints might contain "deeply nested"
205+
// associated types, e.g. `T: A<SomeAssocType = <Self as B>::OtherAssocType`
206+
// where `<Self as B>::OtherAssocType` can be normalized to some concrete type.
207+
let param_env = env.normalize_to(param_env);
208+
209+
trace!("Constraints after normalization: {:#?}", param_env);
210+
211211
param_env
212212
}
213213

0 commit comments

Comments
 (0)