Split tests for field and var assignment.

stainless_frontend/tests/extraction_tests.rs

@@ -91,6 +91,7 @@ define_tests!(
   pass: let_type,
   pass: list_binary_search,
   pass: monoid,
+  pass: mut_local_fields,
   pass: mut_local_lets,
   pass: mut_local_params,
   pass: mut_ref_immut_borrow,

stainless_frontend/tests/pass/mut_local_fields.rs

@@ -0,0 +1,15 @@
+extern crate stainless;
+use stainless::*;
+
+#[var(field)]
+struct S {
+  field: i32,
+}
+
+pub fn main() {
+  // field assignment
+  let mut s = S { field: 123 };
+  assert!(s.field == 123);
+  s.field = 456;
+  assert!(s.field == 456);
+}

stainless_frontend/tests/pass/mut_local_lets.rs

@@ -7,10 +7,6 @@ pub enum IntOption {
   Some(i32),
 }
 
-struct S {
-  field: i32,
-}
-
 pub fn main() {
   // Local mutation is ok.
   let mut x = 1;
@@ -24,10 +20,4 @@ pub fn main() {
   let mut option = IntOption::None;
   option2 = option;
   option = IntOption::Some(123);
-
-  // field assignment
-  let mut s = S { field: 123 };
-  assert!(s.field == 123);
-  s.field = 456;
-  assert!(s.field == 456);
 }