diff --git a/prusti-contracts/prusti-specs/src/specifications/preparser.rs b/prusti-contracts/prusti-specs/src/specifications/preparser.rs
index afbe05c0c55..171785912d7 100644
--- a/prusti-contracts/prusti-specs/src/specifications/preparser.rs
+++ b/prusti-contracts/prusti-specs/src/specifications/preparser.rs
@@ -878,20 +878,25 @@ impl PrustiBinaryOp {
         }
     }
 
-    fn translate(&self, span: Span, lhs: TokenStream, rhs: TokenStream) -> TokenStream {
+    fn translate(&self, span: Span, raw_lhs: TokenStream, raw_rhs: TokenStream) -> TokenStream {
+        let lhs = quote_spanned! { raw_lhs.span() => (#raw_lhs) };
+        let rhs = quote_spanned! { raw_rhs.span() => (#raw_rhs) };
         match self {
-            Self::Rust(op) => op.translate(span, lhs, rhs),
+            Self::Rust(op) => op.translate(span, raw_lhs, raw_rhs),
             // implication is desugared into this form to avoid evaluation
             // order issues: `f(a, b)` makes Rust evaluate both `a` and `b`
             // before the `f` call
             Self::Implies => {
                 // preserve span of LHS
-                let not_lhs = quote_spanned! { lhs.span() => !(#lhs) };
-                quote_spanned! { span => (#not_lhs || (#rhs)) }
+                let not_lhs = quote_spanned! { lhs.span() => !#lhs };
+                quote_spanned! { span => #not_lhs || #rhs }
+            }
+            Self::Or => quote_spanned! { span => #lhs || #rhs },
+            Self::And => quote_spanned! { span => #lhs && #rhs },
+            Self::SnapEq => {
+                let joined_span = join_spans(lhs.span(), rhs.span());
+                quote_spanned! { joined_span => snapshot_equality(&#lhs, &#rhs) }
             }
-            Self::Or => quote_spanned! { span => (#lhs) || (#rhs) },
-            Self::And => quote_spanned! { span => (#lhs) && (#rhs) },
-            Self::SnapEq => quote_spanned! { span => snapshot_equality(&(#lhs), &(#rhs)) },
         }
     }
 }
diff --git a/prusti-tests/tests/parse/ui/composite.stdout b/prusti-tests/tests/parse/ui/composite.stdout
index 7647d4db054..be327541e13 100644
--- a/prusti-tests/tests/parse/ui/composite.stdout
+++ b/prusti-tests/tests/parse/ui/composite.stdout
@@ -42,7 +42,7 @@ use prusti_contracts::*;
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test1_$(NUM_UUID)() -> bool {
-    !!(((!((true) && (true)) || ((true) && (true)))): bool)
+    !!((!((true) && (true)) || ((true) && (true))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -51,7 +51,7 @@ fn test1() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test2_$(NUM_UUID)() -> bool {
-    !!(((((true) && (((!(true) || (true))))) && (((true) || (true)))) &&
+    !!(((((true) && ((!(true) || (true)))) && (((true) || (true)))) &&
                             (true)): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
@@ -61,7 +61,7 @@ fn test2() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test3_$(NUM_UUID)() -> bool {
-    !!(((!(((true) && (true))) || (true))): bool)
+    !!((!(((true) && (true))) || (true)): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -70,7 +70,7 @@ fn test3() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test4_$(NUM_UUID)() -> bool {
-    !!(((!((((!(true) || (true)))) && (true)) || (true))): bool)
+    !!((!(((!(true) || (true))) && (true)) || (true)): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -79,8 +79,8 @@ fn test4() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test5_$(NUM_UUID)() -> bool {
-    !!(((((!(true) || (true)))) &&
-                            (((!(true) || ((true) && (((true) || (true)))))))): bool)
+    !!((((!(true) || (true))) &&
+                            ((!(true) || ((true) && (((true) || (true))))))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -89,8 +89,8 @@ fn test5() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test6_$(NUM_UUID)() -> bool {
-    !!(((!(((true) && (true))) ||
-                                ((!(true) || ((!(true) || ((!(true) || (true))))))))): bool)
+    !!((!(((true) && (true))) ||
+                            (!(true) || (!(true) || (!(true) || (true))))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -99,8 +99,8 @@ fn test6() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test7_$(NUM_UUID)() -> bool {
-    !!(((!(((true) && (true))) ||
-                                ((!(((true) && (true))) || (((true) && (true))))))): bool)
+    !!((!(((true) && (true))) ||
+                            (!(((true) && (true))) || (((true) && (true))))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -109,7 +109,7 @@ fn test7() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test8_$(NUM_UUID)() -> bool {
-    !!(((!(((true) || (true))) || (((true) || (true))))): bool)
+    !!((!(((true) || (true))) || (((true) || (true)))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -118,8 +118,8 @@ fn test8() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test9_$(NUM_UUID)() -> bool {
-    !!(((!(((true) || (true))) ||
-                                (((true) || (((true) && (((true) || (true))))))))): bool)
+    !!((!(((true) || (true))) ||
+                            (((true) || (((true) && (((true) || (true)))))))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -151,10 +151,10 @@ fn test12() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test13_$(NUM_UUID)() -> bool {
-    !!(((!(true) ||
-                                ((!(forall((),
-                                                        #[prusti::spec_only] |a: i32, b: i32| -> bool
-                                                            { ((a == 5): bool) })) || (true))))): bool)
+    !!((!(true) ||
+                            (!(forall((),
+                                                #[prusti::spec_only] |a: i32, b: i32| -> bool
+                                                    { ((a == 5): bool) })) || (true))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -163,10 +163,10 @@ fn test13() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test14_$(NUM_UUID)() -> bool {
-    !!(((!(true) ||
-                                (forall((),
-                                        #[prusti::spec_only] |a: i32| -> bool
-                                            { ((a == 5): bool) })))): bool)
+    !!((!(true) ||
+                            (forall((),
+                                    #[prusti::spec_only] |a: i32| -> bool
+                                        { ((a == 5): bool) }))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -175,9 +175,9 @@ fn test14() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test15_$(NUM_UUID)() -> bool {
-    !!(((!(forall((),
-                                            #[prusti::spec_only] |a: i32| -> bool { ((a == 5): bool) }))
-                                || (true))): bool)
+    !!((!(forall((),
+                                        #[prusti::spec_only] |a: i32| -> bool { ((a == 5): bool) }))
+                            || (true)): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -186,13 +186,13 @@ fn test15() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test16_$(NUM_UUID)() -> bool {
-    !!(((!(forall((),
-                                            #[prusti::spec_only] |b: i32| -> bool
-                                                { ((b == 10): bool) })) ||
-                                ((!(true) ||
-                                            (forall((),
-                                                    #[prusti::spec_only] |a: u32, b: u32| -> bool
-                                                        { ((a == 5): bool) })))))): bool)
+    !!((!(forall((),
+                                        #[prusti::spec_only] |b: i32| -> bool
+                                            { ((b == 10): bool) })) ||
+                            (!(true) ||
+                                    (forall((),
+                                            #[prusti::spec_only] |a: u32, b: u32| -> bool
+                                                { ((a == 5): bool) })))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -224,10 +224,10 @@ fn test19() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test20_$(NUM_UUID)() -> bool {
-    !!(((!(true) ||
-                                ((!(exists((),
-                                                        #[prusti::spec_only] |a: i32, b: i32| -> bool
-                                                            { ((a == 5): bool) })) || (true))))): bool)
+    !!((!(true) ||
+                            (!(exists((),
+                                                #[prusti::spec_only] |a: i32, b: i32| -> bool
+                                                    { ((a == 5): bool) })) || (true))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -236,10 +236,10 @@ fn test20() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test21_$(NUM_UUID)() -> bool {
-    !!(((!(true) ||
-                                (exists((),
-                                        #[prusti::spec_only] |a: i32| -> bool
-                                            { ((a == 5): bool) })))): bool)
+    !!((!(true) ||
+                            (exists((),
+                                    #[prusti::spec_only] |a: i32| -> bool
+                                        { ((a == 5): bool) }))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -248,9 +248,9 @@ fn test21() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test22_$(NUM_UUID)() -> bool {
-    !!(((!(exists((),
-                                            #[prusti::spec_only] |a: i32| -> bool { ((a == 5): bool) }))
-                                || (true))): bool)
+    !!((!(exists((),
+                                        #[prusti::spec_only] |a: i32| -> bool { ((a == 5): bool) }))
+                            || (true)): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -259,13 +259,13 @@ fn test22() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test23_$(NUM_UUID)() -> bool {
-    !!(((!(exists((),
-                                            #[prusti::spec_only] |b: i32| -> bool
-                                                { ((b == 10): bool) })) ||
-                                ((!(true) ||
-                                            (exists((),
-                                                    #[prusti::spec_only] |a: u32, b: u32| -> bool
-                                                        { ((a == 5): bool) })))))): bool)
+    !!((!(exists((),
+                                        #[prusti::spec_only] |b: i32| -> bool
+                                            { ((b == 10): bool) })) ||
+                            (!(true) ||
+                                    (exists((),
+                                            #[prusti::spec_only] |a: u32, b: u32| -> bool
+                                                { ((a == 5): bool) })))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
diff --git a/prusti-tests/tests/parse/ui/exists.stdout b/prusti-tests/tests/parse/ui/exists.stdout
index 65b45f7a091..3c3a7db3a33 100644
--- a/prusti-tests/tests/parse/ui/exists.stdout
+++ b/prusti-tests/tests/parse/ui/exists.stdout
@@ -50,8 +50,7 @@ fn test2() {}
 fn prusti_pre_item_test3_$(NUM_UUID)() -> bool {
     !!((exists((),
                             #[prusti::spec_only] |a: i32, b: i32| -> bool
-                                { (((!(a + b == a + b) || (a + b == a + b))): bool) })):
-                    bool)
+                                { ((!(a + b == a + b) || (a + b == a + b)): bool) })): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -92,8 +91,7 @@ fn prusti_pre_item_test6_$(NUM_UUID)() -> bool {
                                     #[prusti::spec_only] |a: i32, b: i32| (2)),
                                 (#[prusti::spec_only] |a: i32, b: i32| (1),)),
                             #[prusti::spec_only] |a: i32, b: i32| -> bool
-                                { (((!(a + b == a + b) || (a + b == a + b))): bool) })):
-                    bool)
+                                { ((!(a + b == a + b) || (a + b == a + b)): bool) })): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
diff --git a/prusti-tests/tests/parse/ui/forall.stdout b/prusti-tests/tests/parse/ui/forall.stdout
index e1ecb7f4782..0a2a103053a 100644
--- a/prusti-tests/tests/parse/ui/forall.stdout
+++ b/prusti-tests/tests/parse/ui/forall.stdout
@@ -50,8 +50,7 @@ fn test2() {}
 fn prusti_pre_item_test3_$(NUM_UUID)() -> bool {
     !!((forall((),
                             #[prusti::spec_only] |a: i32, b: i32| -> bool
-                                { (((!(a + b == a + b) || (a + b == a + b))): bool) })):
-                    bool)
+                                { ((!(a + b == a + b) || (a + b == a + b)): bool) })): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -92,8 +91,7 @@ fn prusti_pre_item_test6_$(NUM_UUID)() -> bool {
                                     #[prusti::spec_only] |a: i32, b: i32| (2)),
                                 (#[prusti::spec_only] |a: i32, b: i32| (1),)),
                             #[prusti::spec_only] |a: i32, b: i32| -> bool
-                                { (((!(a + b == a + b) || (a + b == a + b))): bool) })):
-                    bool)
+                                { ((!(a + b == a + b) || (a + b == a + b)): bool) })): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
diff --git a/prusti-tests/tests/parse/ui/implies.stdout b/prusti-tests/tests/parse/ui/implies.stdout
index 4caacc7707f..697e793846e 100644
--- a/prusti-tests/tests/parse/ui/implies.stdout
+++ b/prusti-tests/tests/parse/ui/implies.stdout
@@ -28,7 +28,7 @@ use prusti_contracts::*;
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test1_$(NUM_UUID)() -> bool {
-    !!(((!(true) || (true))): bool)
+    !!((!(true) || (true)): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -37,7 +37,7 @@ fn test1() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test2_$(NUM_UUID)() -> bool {
-    !!(((!(true) || ((!(true) || (true))))): bool)
+    !!((!(true) || (!(true) || (true))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -46,7 +46,7 @@ fn test2() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test3_$(NUM_UUID)() -> bool {
-    !!(((!(true) || (((!(true) || (true)))))): bool)
+    !!((!(true) || ((!(true) || (true)))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -55,7 +55,7 @@ fn test3() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test4_$(NUM_UUID)() -> bool {
-    !!(((!(((!(true) || (true)))) || (true))): bool)
+    !!((!((!(true) || (true))) || (true)): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -64,7 +64,7 @@ fn test4() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test5_$(NUM_UUID)() -> bool {
-    !!(((!(((!(true) || (true)))) || (((!(true) || (true)))))): bool)
+    !!((!((!(true) || (true))) || ((!(true) || (true)))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -73,7 +73,7 @@ fn test5() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test21_$(NUM_UUID)() -> bool {
-    !!(((!(true) || (true))): bool)
+    !!((!(true) || (true)): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -82,7 +82,7 @@ fn test21() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test22_$(NUM_UUID)() -> bool {
-    !!(((!(true) || ((!(true) || (true))))): bool)
+    !!((!(true) || (!(true) || (true))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -91,7 +91,7 @@ fn test22() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test23_$(NUM_UUID)() -> bool {
-    !!(((!(true) || (((!(true) || (true)))))): bool)
+    !!((!(true) || ((!(true) || (true)))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -100,7 +100,7 @@ fn test23() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test24_$(NUM_UUID)() -> bool {
-    !!(((!(((!(true) || (true)))) || (true))): bool)
+    !!((!((!(true) || (true))) || (true)): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -109,7 +109,7 @@ fn test24() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test25_$(NUM_UUID)() -> bool {
-    !!(((!(((!(true) || (true)))) || (((!(true) || (true)))))): bool)
+    !!((!((!(true) || (true))) || ((!(true) || (true)))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
diff --git a/prusti-tests/tests/parse/ui/predicates.stdout b/prusti-tests/tests/parse/ui/predicates.stdout
index 756b4bc5ad7..e4681fb552e 100644
--- a/prusti-tests/tests/parse/ui/predicates.stdout
+++ b/prusti-tests/tests/parse/ui/predicates.stdout
@@ -79,7 +79,7 @@ fn prusti_pred_item_forall_implication_$(NUM_UUID)()
     -> bool {
     !!((forall((),
                             #[prusti::spec_only] |x: usize| -> bool
-                                { (((!((x != 0)) || (x * 2 != 0))): bool) })): bool)
+                                { ((!((x != 0)) || (x * 2 != 0)): bool) })): bool)
 }
 #[allow(unused_must_use, unused_variables, dead_code)]
 #[prusti::pred_spec_id_ref = "$(NUM_UUID)"]
@@ -96,7 +96,7 @@ fn prusti_pred_item_exists_implication_$(NUM_UUID)()
     -> bool {
     !!((exists((),
                             #[prusti::spec_only] |x: usize| -> bool
-                                { (((!((x != 0)) || (x * 2 != 0))): bool) })): bool)
+                                { ((!((x != 0)) || (x * 2 != 0)): bool) })): bool)
 }
 #[allow(unused_must_use, unused_variables, dead_code)]
 #[prusti::pred_spec_id_ref = "$(NUM_UUID)"]
diff --git a/prusti-tests/tests/typecheck/ui/nested_forall.stdout b/prusti-tests/tests/typecheck/ui/nested_forall.stdout
index a2fc02dba9a..992be64f226 100644
--- a/prusti-tests/tests/typecheck/ui/nested_forall.stdout
+++ b/prusti-tests/tests/typecheck/ui/nested_forall.stdout
@@ -45,7 +45,7 @@ fn prusti_pre_item_test2_$(NUM_UUID)() -> bool {
                                 {
                                     ((forall((),
                                                     #[prusti::spec_only] |b: i32| -> bool
-                                                        { (((!(a == a) || (b == b))): bool) })): bool)
+                                                        { ((!(a == a) || (b == b)): bool) })): bool)
                                 })): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
@@ -94,7 +94,7 @@ fn prusti_pre_item_test5_$(NUM_UUID)() -> bool {
                                 {
                                     ((exists((),
                                                     #[prusti::spec_only] |b: i32| -> bool
-                                                        { (((!(a == a) || (b == b))): bool) })): bool)
+                                                        { ((!(a == a) || (b == b)): bool) })): bool)
                                 })): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
diff --git a/prusti-tests/tests/verify/ui/calls.stdout b/prusti-tests/tests/verify/ui/calls.stdout
index 31eb59cd5fc..413a40572c9 100644
--- a/prusti-tests/tests/verify/ui/calls.stdout
+++ b/prusti-tests/tests/verify/ui/calls.stdout
@@ -59,7 +59,7 @@ fn test_max2() {
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_post_item_test_max3_$(NUM_UUID)(result: i32)
     -> bool {
-    !!((((true) && (((!(true) || (result == 3))))) && (((true) || (false)))):
+    !!((((true) && ((!(true) || (result == 3)))) && (((true) || (false)))):
                     bool)
 }
 #[prusti::post_spec_id_ref = "$(NUM_UUID)"]
diff --git a/prusti-tests/tests/verify/ui/failing-postcondition.rs b/prusti-tests/tests/verify/ui/failing-postcondition.rs
index 866eb1d5ae4..3eeff1ecce4 100644
--- a/prusti-tests/tests/verify/ui/failing-postcondition.rs
+++ b/prusti-tests/tests/verify/ui/failing-postcondition.rs
@@ -10,10 +10,17 @@ fn client(a: u32) {}
 
 #[pure]
 #[ensures(result)]
-fn test1() -> bool { false }
+fn test1() -> bool {
+    false
+}
 
 #[pure]
 #[ensures(x)]
-fn test2(x: bool) -> bool { x }
+fn test2(x: bool) -> bool {
+    x
+}
+
+#[ensures(a === b)]
+fn test3<T>(a: T, b: T) {}
 
 fn main() {}
diff --git a/prusti-tests/tests/verify/ui/failing-postcondition.stderr b/prusti-tests/tests/verify/ui/failing-postcondition.stderr
index 8b0671f40fe..54424aa4380 100644
--- a/prusti-tests/tests/verify/ui/failing-postcondition.stderr
+++ b/prusti-tests/tests/verify/ui/failing-postcondition.stderr
@@ -1,8 +1,8 @@
 error: [Prusti: verification error] postcondition might not hold.
- --> $DIR/failing-postcondition.rs:8:28
+ --> $DIR/failing-postcondition.rs:8:11
   |
 8 | #[ensures(something_true() && false)]
-  |                            ^^
+  |           ^^^^^^^^^^^^^^^^^^^^^^^^^
   |
 note: the error originates here
  --> $DIR/failing-postcondition.rs:9:1
@@ -19,20 +19,36 @@ error: [Prusti: verification error] postcondition might not hold.
 note: the error originates here
   --> $DIR/failing-postcondition.rs:13:1
    |
-13 | fn test1() -> bool { false }
-   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+13 | / fn test1() -> bool {
+14 | |     false
+15 | | }
+   | |_^
 
 error: [Prusti: verification error] postcondition might not hold.
-  --> $DIR/failing-postcondition.rs:16:11
+  --> $DIR/failing-postcondition.rs:18:11
    |
-16 | #[ensures(x)]
+18 | #[ensures(x)]
    |           ^
    |
 note: the error originates here
-  --> $DIR/failing-postcondition.rs:17:1
+  --> $DIR/failing-postcondition.rs:19:1
    |
-17 | fn test2(x: bool) -> bool { x }
-   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+19 | / fn test2(x: bool) -> bool {
+20 | |     x
+21 | | }
+   | |_^
 
-error: aborting due to 3 previous errors
+error: [Prusti: verification error] postcondition might not hold.
+  --> $DIR/failing-postcondition.rs:23:11
+   |
+23 | #[ensures(a === b)]
+   |           ^^^^^^^
+   |
+note: the error originates here
+  --> $DIR/failing-postcondition.rs:24:1
+   |
+24 | fn test3<T>(a: T, b: T) {}
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: aborting due to 4 previous errors
 
diff --git a/prusti-tests/tests/verify/ui/predicates/abstract-predicate-with-body.stderr b/prusti-tests/tests/verify/ui/predicates/abstract-predicate-with-body.stderr
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/prusti-tests/tests/verify/ui/pure.stdout b/prusti-tests/tests/verify/ui/pure.stdout
index bb513935b86..ae0203eb800 100644
--- a/prusti-tests/tests/verify/ui/pure.stdout
+++ b/prusti-tests/tests/verify/ui/pure.stdout
@@ -67,7 +67,7 @@ fn test_max2() {
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_post_item_test_max3_$(NUM_UUID)(result: i32)
     -> bool {
-    !!((((true) && (((!(true) || (result == 3))))) && (((true) || (false)))):
+    !!((((true) && ((!(true) || (result == 3)))) && (((true) || (false)))):
                     bool)
 }
 #[prusti::post_spec_id_ref = "$(NUM_UUID)"]