From 3ee584dc66df2b25003823c2aba00e5a51ad2d16 Mon Sep 17 00:00:00 2001
From: Jonas Hansen <ganymed92@gmail.com>
Date: Wed, 27 Apr 2022 17:08:37 +0200
Subject: [PATCH] Move predicate normalization in constraint solver for better
 debugging

---
 .../encoder/mir/specifications/constraints.rs | 19 ++++++++++++-------
 1 file changed, 12 insertions(+), 7 deletions(-)

diff --git a/prusti-viper/src/encoder/mir/specifications/constraints.rs b/prusti-viper/src/encoder/mir/specifications/constraints.rs
index 58c8cf70ea3..87f2143117f 100644
--- a/prusti-viper/src/encoder/mir/specifications/constraints.rs
+++ b/prusti-viper/src/encoder/mir/specifications/constraints.rs
@@ -162,13 +162,7 @@ pub mod trait_bounds {
             .caller_bounds()
             .iter()
             .all(|predicate| {
-                // Normalize any associated type projections.
-                // This needs to be done because ghost constraints might contain "deeply nested"
-                // associated types, e.g. `T: A<SomeAssocType = <Self as B>::OtherAssocType`
-                // where `<Self as B>::OtherAssocType` can be normalized to some concrete type.
-                let normalized_predicate = env.normalize_to(predicate);
-
-                env.evaluate_predicate(normalized_predicate, param_env_lookup)
+                env.evaluate_predicate(predicate, param_env_lookup)
             });
 
         trace!("Constraint fulfilled: {all_bounds_satisfied}");
@@ -208,6 +202,17 @@ pub mod trait_bounds {
             param_env
         );
 
+        // Normalize any associated type projections.
+        // This needs to be done because ghost constraints might contain "deeply nested"
+        // associated types, e.g. `T: A<SomeAssocType = <Self as B>::OtherAssocType`
+        // where `<Self as B>::OtherAssocType` can be normalized to some concrete type.
+        let param_env = env.normalize_to(param_env);
+
+        trace!(
+            "Constraints after normalization: {:#?}",
+            param_env
+        );
+
         param_env
     }