diff --git a/.stainless-version b/.stainless-version
index e458cbc7..7a53e6e9 100644
--- a/.stainless-version
+++ b/.stainless-version
@@ -1 +1 @@
-noxt-0.8.0-41-g5e334c2
+noxt-0.8.0-41-g6e0a759
diff --git a/demo/examples/generic_option.rs b/demo/examples/generic_option.rs
index 392036f3..3c19afa1 100644
--- a/demo/examples/generic_option.rs
+++ b/demo/examples/generic_option.rs
@@ -1,3 +1,5 @@
+extern crate stainless;
+
 enum Maybe<T> {
   Nothing,
   Just(T),
@@ -21,11 +23,11 @@ fn get_or_else<T>(maybe: Maybe<T>, default: T) -> T {
 fn flatten<T>(maybemaybe: Maybe<Maybe<T>>) -> Maybe<T> {
   match maybemaybe {
     Maybe::Nothing => Maybe::Nothing,
-    Maybe::Just(maybe) => maybe
+    Maybe::Just(maybe) => maybe,
   }
 }
 
-fn main() -> () {
+pub fn main() -> () {
   let x = 123;
   let maybe_x = just(x);
   get_or_else(maybe_x, 0);
diff --git a/demo/examples/insertion_sort.rs b/demo/examples/insertion_sort.rs
index ed2894df..1b558b68 100644
--- a/demo/examples/insertion_sort.rs
+++ b/demo/examples/insertion_sort.rs
@@ -30,8 +30,8 @@ impl List<i32> {
   #[measure(self)]
   pub fn contents(&self) -> Set<i32> {
     match self {
-      List::Nil => Set::empty(),
-      List::Cons(head, tail) => tail.contents().add(*head),
+      List::Nil => Set::new(),
+      List::Cons(head, tail) => tail.contents().insert(*head),
     }
   }
 
@@ -69,8 +69,8 @@ impl List<i32> {
   #[post(
     ret.size() == self.size() + 1 &&
     ret.is_sorted() &&
-    ret.contents().is_subset_of(&self.contents().add(e)) &&
-    self.contents().add(e).is_subset_of(&ret.contents())
+    ret.contents().is_subset(&self.contents().insert(e)) &&
+    self.contents().insert(e).is_subset(&ret.contents())
   )]
   pub fn sorted_insert(self, e: i32) -> List<i32> {
     match self {
@@ -85,8 +85,8 @@ impl List<i32> {
   #[post(
     ret.size() == self.size() &&
     ret.is_sorted() &&
-    ret.contents().is_subset_of(&self.contents()) &&
-    self.contents().is_subset_of(&ret.contents())
+    ret.contents().is_subset(&self.contents()) &&
+    self.contents().is_subset(&ret.contents())
   )]
   pub fn sort(self) -> List<i32> {
     match self {
diff --git a/demo/examples/list_binary_search.rs b/demo/examples/list_binary_search.rs
index 87a5a7a7..108dfd89 100644
--- a/demo/examples/list_binary_search.rs
+++ b/demo/examples/list_binary_search.rs
@@ -33,6 +33,15 @@ impl<T> List<T> {
     }
   }
 
+  // Check that we can have a measure where the parameter is consumed.
+  #[measure(self)]
+  pub fn consume(self) -> () {
+    match self {
+      List::Nil => (),
+      List::Cons(..) => (),
+    }
+  }
+
   #[pre(index < self.size())]
   #[post(ret.is_some())]
   pub fn get(&self, index: u32) -> Option<&T> {
diff --git a/demo/examples/mut_local_fields.rs b/demo/examples/mut_local_fields.rs
new file mode 100644
index 00000000..a8da1976
--- /dev/null
+++ b/demo/examples/mut_local_fields.rs
@@ -0,0 +1,35 @@
+#![allow(dead_code, unused_assignments)]
+
+extern crate stainless;
+use stainless::*;
+
+#[var(field)]
+struct S {
+  field: i32,
+}
+
+fn set_field(s: S) -> S {
+  // current work-around for anti-aliasing
+  let mut s = S { ..s };
+  s.field = 789;
+  s
+}
+
+fn set_int(mut s: i32) -> i32 {
+  s = 1000;
+  s
+}
+
+pub fn main() {
+  // field assignment
+  let mut s = S { field: 123 };
+  assert!(s.field == 123);
+  s.field = 456;
+  assert!(s.field == 456);
+
+  let s = set_field(s);
+  assert!(s.field == 789);
+
+  let i = set_int(12);
+  assert!(i == 1000);
+}
diff --git a/demo/examples/mut_local_params.rs b/demo/examples/mut_local_params.rs
new file mode 100644
index 00000000..bb791e2e
--- /dev/null
+++ b/demo/examples/mut_local_params.rs
@@ -0,0 +1,26 @@
+#![allow(unused)]
+
+extern crate stainless;
+use stainless::*;
+
+// This should pass because place is only locally mutable.
+pub fn change<'a, T>(mut place: &'a T, new: &'a T) -> &'a T {
+  place = new;
+  place
+}
+
+#[pre(a > 0)]
+#[post(ret > 0)]
+pub fn with_spec(mut a: i32) -> i32 {
+  a
+}
+
+pub fn main() {
+  // Here, we don't modify anything locally.
+  let y = 10;
+  let z = 5;
+  assert!(z == 5);
+  let res = change(&z, &y);
+  assert!(z == 5);
+  assert!(*res == y);
+}
diff --git a/stainless_extraction/src/flags.rs b/stainless_extraction/src/flags.rs
index 4c70b223..b69baec2 100644
--- a/stainless_extraction/src/flags.rs
+++ b/stainless_extraction/src/flags.rs
@@ -24,18 +24,12 @@ pub(super) enum Flag {
   Measure,
 }
 
-#[derive(Clone, Debug)]
+#[derive(Clone, Debug, Default)]
 pub(super) struct Flags {
   set: HashSet<Flag>,
 }
 
 impl Flags {
-  fn new() -> Self {
-    Self {
-      set: HashSet::new(),
-    }
-  }
-
   pub(super) fn add(&mut self, flag: Flag) {
     self.set.insert(flag);
   }
@@ -124,7 +118,7 @@ pub(super) fn extract_flag(
 impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
   pub(super) fn extract_flags(&self, carrier_hid: HirId) -> (Flags, HashMap<Symbol, Flags>) {
     let attrs = self.tcx.hir().attrs(carrier_hid);
-    let mut carrier_flags = Flags::new();
+    let mut carrier_flags = Flags::default();
     let mut flags_by_symbol: HashMap<Symbol, Flags> = HashMap::new();
 
     for attr in attrs {
@@ -140,7 +134,7 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
       let mut add_by_symbol = |symbol: Symbol| {
         flags_by_symbol
           .entry(symbol)
-          .or_insert_with(Flags::new)
+          .or_insert_with(Flags::default)
           .add(flag)
       };
 
diff --git a/stainless_extraction/src/krate.rs b/stainless_extraction/src/krate.rs
index 6f887d70..b399d054 100644
--- a/stainless_extraction/src/krate.rs
+++ b/stainless_extraction/src/krate.rs
@@ -466,7 +466,7 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
   pub(super) fn get_or_extract_adt(&mut self, def_id: DefId) -> &'l st::ADTSort<'l> {
     self
       .get_id_from_def(def_id)
-      .and_then(|id| self.with_extraction(|xt| xt.adts.get(id).copied()))
+      .and_then(|id| self.get_adt(id))
       .unwrap_or_else(|| {
         let adt = self.extract_adt(def_id);
         self.add_adt(adt);
@@ -474,7 +474,7 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
       })
   }
 
-  pub(super) fn extract_adt(&mut self, def_id: DefId) -> &'l st::ADTSort<'l> {
+  fn extract_adt(&mut self, def_id: DefId) -> &'l st::ADTSort<'l> {
     let f = self.factory();
     let adt_id = self.get_or_register_def(def_id);
     let adt_def = self.tcx.adt_def(def_id);
diff --git a/stainless_extraction/src/lib.rs b/stainless_extraction/src/lib.rs
index a8e97d71..43572257 100644
--- a/stainless_extraction/src/lib.rs
+++ b/stainless_extraction/src/lib.rs
@@ -249,6 +249,10 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
     })
   }
 
+  fn get_adt(&self, id: StainlessSymId<'l>) -> Option<&'l st::ADTSort<'l>> {
+    self.with_extraction(|xt| xt.adts.get(id).copied())
+  }
+
   fn add_function_ref(&mut self, def_id: DefId) {
     self.with_extraction_mut(|xt| {
       assert!(xt.function_refs.insert(def_id));
diff --git a/stainless_frontend/tests/extraction_tests.rs b/stainless_frontend/tests/extraction_tests.rs
index 9b35cfe8..413178ae 100644
--- a/stainless_frontend/tests/extraction_tests.rs
+++ b/stainless_frontend/tests/extraction_tests.rs
@@ -143,6 +143,7 @@ define_tests!(
   fail_extraction: double_measure_impl,
   fail_verification: liskov_rectangle,
   fail_extraction: mut_borrow_ref,
+  crash_verification: mut_immutable_field,
   fail_extraction: mut_params,
   crash_verification: return_in_cond,
   crash_verification: return_in_guard,
diff --git a/stainless_frontend/tests/fail/mut_immutable_field.rs b/stainless_frontend/tests/fail/mut_immutable_field.rs
new file mode 100644
index 00000000..882c458e
--- /dev/null
+++ b/stainless_frontend/tests/fail/mut_immutable_field.rs
@@ -0,0 +1,10 @@
+extern crate stainless;
+
+struct A {
+  b: bool,
+}
+
+fn set_false(mut a: A) -> A {
+  a.b = false;
+  a
+}
diff --git a/stainless_frontend/tests/pass/mut_local_fields.rs b/stainless_frontend/tests/pass/mut_local_fields.rs
index ce00c647..a8da1976 100644
--- a/stainless_frontend/tests/pass/mut_local_fields.rs
+++ b/stainless_frontend/tests/pass/mut_local_fields.rs
@@ -1,3 +1,5 @@
+#![allow(dead_code, unused_assignments)]
+
 extern crate stainless;
 use stainless::*;
 
@@ -6,10 +8,28 @@ struct S {
   field: i32,
 }
 
+fn set_field(s: S) -> S {
+  // current work-around for anti-aliasing
+  let mut s = S { ..s };
+  s.field = 789;
+  s
+}
+
+fn set_int(mut s: i32) -> i32 {
+  s = 1000;
+  s
+}
+
 pub fn main() {
   // field assignment
   let mut s = S { field: 123 };
   assert!(s.field == 123);
   s.field = 456;
   assert!(s.field == 456);
+
+  let s = set_field(s);
+  assert!(s.field == 789);
+
+  let i = set_int(12);
+  assert!(i == 1000);
 }