Convert trait predicate tests to Rust syntax

Now that named struct-field resolution is on main (#118), flip the trait
predicate tests (annot_preds_trait, annot_preds_trait_multi; pass and fail)
from raw SMT-LIB2 bodies to Rust-expression bodies using `self.x`.

https://claude.ai/code/session_01WdLyxyy4ieAxrexj83X5MX

Author: claude

tests/ui/fail/annot_preds_trait.rs

@@ -25,15 +25,10 @@ trait Double {
 
 #[thrust_macros::context]
 impl Double for A {
-    // Write concrete definitions for predicates in `impl` blocks
+    // self.x * 3 (this isn't actually doubled!) does not comply with the trait.
     #[thrust_macros::predicate]
     fn is_double(self, doubled: Self) -> bool {
-        // (tuple_proj<Int>.0 self) is equivalent to self.x
-        // self.x * 3 == doubled.x (this isn't actually doubled!) is written as following:
-        "(=
-            (* (tuple_proj<Int>.0 self_) 3)
-            (tuple_proj<Int>.0 doubled)
-        )"; true // This definition does not comply with annotations in trait!
+        self.x * 3 == doubled.x
     }
 
     // Check if this method complies with annotations in

tests/ui/fail/annot_preds_trait_multi.rs

@@ -26,11 +26,7 @@ impl thrust_models::Model for A {
 impl Double for A {
     #[thrust_macros::predicate]
     fn is_double(self, doubled: Self) -> bool {
-        // self.x * 2 == doubled.x
-        "(=
-            (* (tuple_proj<Int>.0 self_) 2)
-            (tuple_proj<Int>.0 doubled)
-        )"; true
+        self.x * 2 == doubled.x
     }
 
     fn double(&mut self) {
@@ -50,19 +46,10 @@ impl thrust_models::Model for B {
 
 #[thrust_macros::context]
 impl Double for B {
+    // self.x * 3 (this isn't actually doubled!) does not comply with the trait.
     #[thrust_macros::predicate]
     fn is_double(self, doubled: Self) -> bool {
-        // self.x * 3 == doubled.x && self.y * 2 == doubled.y (this isn't actually doubled!)
-        "(and
-            (=
-                (* (tuple_proj<Int-Int>.0 self_) 3)
-                (tuple_proj<Int-Int>.0 doubled)
-            )
-            (=
-                (* (tuple_proj<Int-Int>.1 self_) 2)
-                (tuple_proj<Int-Int>.1 doubled)
-            )
-        )"; true // This definition does not comply with annotations in trait!
+        self.x * 3 == doubled.x && self.y * 2 == doubled.y
     }
 
     fn double(&mut self) {

tests/ui/pass/annot_preds_trait.rs

@@ -25,15 +25,10 @@ trait Double {
 
 #[thrust_macros::context]
 impl Double for A {
-    // Write concrete definitions for predicates in `impl` blocks
+    // Write concrete definitions for predicates in `impl` blocks, in Rust syntax.
     #[thrust_macros::predicate]
     fn is_double(self, doubled: Self) -> bool {
-        // (tuple_proj<Int>.0 self) is equivalent to self.x
-        // self.x * 2 == doubled.x is written as following:
-        "(=
-            (* (tuple_proj<Int>.0 self_) 2)
-            (tuple_proj<Int>.0 doubled)
-        )"; true
+        self.x * 2 == doubled.x
     }
 
     // Check if this method complies with annotations in

tests/ui/pass/annot_preds_trait_multi.rs

@@ -26,11 +26,7 @@ impl thrust_models::Model for A {
 impl Double for A {
     #[thrust_macros::predicate]
     fn is_double(self, doubled: Self) -> bool {
-        // self.x * 2 == doubled.x
-        "(=
-            (* (tuple_proj<Int>.0 self_) 2)
-            (tuple_proj<Int>.0 doubled)
-        )"; true
+        self.x * 2 == doubled.x
     }
 
     fn double(&mut self) {
@@ -52,17 +48,7 @@ impl thrust_models::Model for B {
 impl Double for B {
     #[thrust_macros::predicate]
     fn is_double(self, doubled: Self) -> bool {
-        // self.x * 2 == doubled.x && self.y * 2 == doubled.y
-        "(and
-            (=
-                (* (tuple_proj<Int-Int>.0 self_) 2)
-                (tuple_proj<Int-Int>.0 doubled)
-            )
-            (=
-                (* (tuple_proj<Int-Int>.1 self_) 2)
-                (tuple_proj<Int-Int>.1 doubled)
-            )
-        )"; true
+        self.x * 2 == doubled.x && self.y * 2 == doubled.y
     }
 
     fn double(&mut self) {