diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml
index 19e5ff1ad..dac659b50 100644
--- a/engine/lib/dependencies.ml
+++ b/engine/lib/dependencies.ml
@@ -41,7 +41,15 @@ module Make (F : Features.T) = struct
 
   module ItemGraph = struct
     module G = Graph.Persistent.Digraph.Concrete (Concrete_ident)
-    module Topological = Graph.Topological.Make_stable (G)
+
+    module StableG = struct
+      include Graph.Persistent.Digraph.Concrete (Int)
+
+      let empty () = empty
+    end
+
+    module Topological = Graph.Topological.Make_stable (StableG)
+    module GMap = Graph.Gmap.Edge (G) (StableG)
     module Oper = Graph.Oper.P (G)
 
     let vertices_of_item (i : item) : G.V.t list =
@@ -270,13 +278,55 @@ module Make (F : Features.T) = struct
     let g =
       ItemGraph.of_items ~original_items:items items |> ItemGraph.Oper.mirror
     in
-    let lookup (name : concrete_ident) =
-      List.find ~f:(ident_of >> Concrete_ident.equal name) items
+    let items_array = Array.of_list items in
+    let name_index =
+      items
+      |> List.mapi ~f:(fun i item -> (item.ident, i))
+      |> Map.of_alist_exn (module Concrete_ident)
+    in
+
+    let lookup (index : int) = items_array.(index) in
+    let stable_g =
+      ItemGraph.GMap.filter_map
+        (fun ((name1, name2) : concrete_ident * concrete_ident) ->
+          let to_index = Map.find name_index in
+          let i1, i2 = (to_index name1, to_index name2) in
+
+          Option.both i1 i2)
+        g
+    in
+    let stable_g =
+      List.foldi items ~init:stable_g ~f:(fun i g _ ->
+          ItemGraph.StableG.add_vertex g i)
+    in
+    let items' =
+      ItemGraph.Topological.fold List.cons stable_g [] |> List.map ~f:lookup
+    in
+    (* Stable topological sort doesn't guarantee to group cycles together.
+       We make this correction to ensure mutually recursive items are grouped. *)
+    let cycles =
+      ItemGraph.MutRec.SCC.scc_list g
+      |> List.filter ~f:(fun cycle -> List.length cycle > 1)
     in
     let items' =
-      ItemGraph.Topological.fold List.cons g []
-      |> List.filter_map ~f:lookup |> List.rev
+      List.fold items' ~init:[] ~f:(fun acc item ->
+          match
+            List.find cycles ~f:(fun cycle ->
+                List.mem cycle item.ident ~equal:[%eq: concrete_ident])
+          with
+          | Some _
+            when List.exists acc ~f:(fun els ->
+                     List.mem els item ~equal:[%eq: item]) ->
+              [] :: acc
+          | Some cycle ->
+              List.map cycle ~f:(fun ident ->
+                  List.find_exn items ~f:(fun item ->
+                      [%eq: concrete_ident] item.ident ident))
+              :: acc
+          | None -> [ item ] :: acc)
+      |> List.concat
     in
+
     assert (
       let of_list =
         List.map ~f:ident_of >> Set.of_list (module Concrete_ident)
diff --git a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap
index 6454004a7..2ab239bdb 100644
--- a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap	
@@ -35,20 +35,37 @@ module Attribute_opaque
 open Core
 open FStar.Mul
 
+assume
+val t_OpaqueStruct': v_X: usize -> v_T: Type0 -> v_U: Type0 -> eqtype
+
+let t_OpaqueStruct (v_X: usize) (v_T v_U: Type0) = t_OpaqueStruct' v_X v_T v_U
+
 assume
 val t_OpaqueEnum': v_X: usize -> v_T: Type0 -> v_U: Type0 -> eqtype
 
 let t_OpaqueEnum (v_X: usize) (v_T v_U: Type0) = t_OpaqueEnum' v_X v_T v_U
 
 assume
-val t_OpaqueStruct': v_X: usize -> v_T: Type0 -> v_U: Type0 -> eqtype
+val ff_generic': v_X: usize -> #v_T: Type0 -> #v_U: Type0 -> x: v_U
+  -> Prims.Pure (t_OpaqueEnum v_X v_T v_U) Prims.l_True (fun _ -> Prims.l_True)
 
-let t_OpaqueStruct (v_X: usize) (v_T v_U: Type0) = t_OpaqueStruct' v_X v_T v_U
+let ff_generic (v_X: usize) (#v_T #v_U: Type0) = ff_generic' v_X #v_T #v_U
 
 assume
-val impl__S1__f_s1': Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
+val f': x: bool -> y: bool -> Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True)
 
-let impl__S1__f_s1 = impl__S1__f_s1'
+let f = f'
+
+assume
+val ff_pre_post': x: bool -> y: bool
+  -> Prims.Pure bool
+      (requires x)
+      (ensures
+        fun result ->
+          let result:bool = result in
+          result =. y)
+
+let ff_pre_post = ff_pre_post'
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 assume
@@ -57,37 +74,20 @@ val impl_2': #v_U: Type0 -> {| i1: Core.Clone.t_Clone v_U |} -> t_TrGeneric i32
 let impl_2 (#v_U: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_U) =
   impl_2' #v_U #i1
 
-assume
-val impl__S2__f_s2': Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
-
-let impl__S2__f_s2 = impl__S2__f_s2'
-
 assume
 val v_C': u8
 
 let v_C = v_C'
 
 assume
-val f': x: bool -> y: bool -> Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True)
-
-let f = f'
-
-assume
-val ff_generic': v_X: usize -> #v_T: Type0 -> #v_U: Type0 -> x: v_U
-  -> Prims.Pure (t_OpaqueEnum v_X v_T v_U) Prims.l_True (fun _ -> Prims.l_True)
+val impl__S1__f_s1': Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
 
-let ff_generic (v_X: usize) (#v_T #v_U: Type0) = ff_generic' v_X #v_T #v_U
+let impl__S1__f_s1 = impl__S1__f_s1'
 
 assume
-val ff_pre_post': x: bool -> y: bool
-  -> Prims.Pure bool
-      (requires x)
-      (ensures
-        fun result ->
-          let result:bool = result in
-          result =. y)
+val impl__S2__f_s2': Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
 
-let ff_pre_post = ff_pre_post'
+let impl__S2__f_s2 = impl__S2__f_s2'
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 assume
@@ -101,13 +101,22 @@ module Attribute_opaque
 open Core
 open FStar.Mul
 
-type t_S1 = | S1 : t_S1
-
-type t_S2 = | S2 : t_S2
+val t_OpaqueStruct (v_X: usize) (v_T v_U: Type0) : eqtype
 
 val t_OpaqueEnum (v_X: usize) (v_T v_U: Type0) : eqtype
 
-val t_OpaqueStruct (v_X: usize) (v_T v_U: Type0) : eqtype
+val ff_generic (v_X: usize) (#v_T #v_U: Type0) (x: v_U)
+    : Prims.Pure (t_OpaqueEnum v_X v_T v_U) Prims.l_True (fun _ -> Prims.l_True)
+
+val f (x y: bool) : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True)
+
+val ff_pre_post (x y: bool)
+    : Prims.Pure bool
+      (requires x)
+      (ensures
+        fun result ->
+          let result:bool = result in
+          result =. y)
 
 class t_TrGeneric (v_Self: Type0) (v_U: Type0) = {
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_13225137425257751668:Core.Clone.t_Clone v_U;
@@ -116,27 +125,18 @@ class t_TrGeneric (v_Self: Type0) (v_U: Type0) = {
   f_f:x0: v_U -> Prims.Pure v_Self (f_f_pre x0) (fun result -> f_f_post x0 result)
 }
 
-val impl__S1__f_s1: Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
-
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl_2 (#v_U: Type0) {| i1: Core.Clone.t_Clone v_U |} : t_TrGeneric i32 v_U
 
-val impl__S2__f_s2: Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
-
 val v_C:u8
 
-val f (x y: bool) : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True)
+type t_S1 = | S1 : t_S1
 
-val ff_generic (v_X: usize) (#v_T #v_U: Type0) (x: v_U)
-    : Prims.Pure (t_OpaqueEnum v_X v_T v_U) Prims.l_True (fun _ -> Prims.l_True)
+val impl__S1__f_s1: Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
 
-val ff_pre_post (x y: bool)
-    : Prims.Pure bool
-      (requires x)
-      (ensures
-        fun result ->
-          let result:bool = result in
-          result =. y)
+type t_S2 = | S2 : t_S2
+
+val impl__S2__f_s2: Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
 
 class t_T (v_Self: Type0) = {
   f_U:Type0;
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index 03baa5eff..7fbe766fd 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
@@ -104,6 +104,8 @@ val impl': Core.Marker.t_Copy t_Int
 
 let impl = impl'
 
+unfold let add x y = x + y
+
 unfold instance impl: Core.Ops.Arith.t_Sub t_Int t_Int =
   {
     f_Output = t_Int;
@@ -111,8 +113,6 @@ unfold instance impl: Core.Ops.Arith.t_Sub t_Int t_Int =
     f_sub_post = (fun (self: t_Int) (other: t_Int) (out: t_Int) -> true);
     f_sub = fun (self: t_Int) (other: t_Int) -> self + other
   }
-
-unfold let add x y = x + y
 '''
 "Attributes.Nested_refinement_elim.fst" = '''
 module Attributes.Nested_refinement_elim
@@ -134,6 +134,11 @@ let v_MAX: usize = sz 10
 
 type t_SafeIndex = { f_i:f_i: usize{f_i <. v_MAX} }
 
+let impl__SafeIndex__new (i: usize) : Core.Option.t_Option t_SafeIndex =
+  if i <. v_MAX
+  then Core.Option.Option_Some ({ f_i = i } <: t_SafeIndex) <: Core.Option.t_Option t_SafeIndex
+  else Core.Option.Option_None <: Core.Option.t_Option t_SafeIndex
+
 let impl__SafeIndex__as_usize (self: t_SafeIndex) : usize = self.f_i
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
@@ -144,11 +149,6 @@ let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (sz 10)) t_SafeIn
     f_index_post = (fun (self: t_Array v_T (sz 10)) (index: t_SafeIndex) (out: v_T) -> true);
     f_index = fun (self: t_Array v_T (sz 10)) (index: t_SafeIndex) -> self.[ index.f_i ]
   }
-
-let impl__SafeIndex__new (i: usize) : Core.Option.t_Option t_SafeIndex =
-  if i <. v_MAX
-  then Core.Option.Option_Some ({ f_i = i } <: t_SafeIndex) <: Core.Option.t_Option t_SafeIndex
-  else Core.Option.Option_None <: Core.Option.t_Option t_SafeIndex
 '''
 "Attributes.Pre_post_on_traits_and_impls.fst" = '''
 module Attributes.Pre_post_on_traits_and_impls
@@ -156,23 +156,6 @@ module Attributes.Pre_post_on_traits_and_impls
 open Core
 open FStar.Mul
 
-type t_ViaAdd = | ViaAdd : t_ViaAdd
-
-type t_ViaMul = | ViaMul : t_ViaMul
-
-class t_TraitWithRequiresAndEnsures (v_Self: Type0) = {
-  f_method_pre:self___: v_Self -> x: u8 -> pred: Type0{x <. 100uy ==> pred};
-  f_method_post:self___: v_Self -> x: u8 -> r: u8 -> pred: Type0{pred ==> r >. 88uy};
-  f_method:x0: v_Self -> x1: u8
-    -> Prims.Pure u8 (f_method_pre x0 x1) (fun result -> f_method_post x0 x1 result)
-}
-
-let test
-      (#v_T: Type0)
-      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_TraitWithRequiresAndEnsures v_T)
-      (x: v_T)
-    : u8 = (f_method #v_T #FStar.Tactics.Typeclasses.solve x 99uy <: u8) -! 88uy
-
 class t_Operation (v_Self: Type0) = {
   f_double_pre:x: u8
     -> pred:
@@ -191,6 +174,10 @@ class t_Operation (v_Self: Type0) = {
   f_double:x0: u8 -> Prims.Pure u8 (f_double_pre x0) (fun result -> f_double_post x0 result)
 }
 
+type t_ViaAdd = | ViaAdd : t_ViaAdd
+
+type t_ViaMul = | ViaMul : t_ViaMul
+
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl: t_Operation t_ViaAdd =
   {
@@ -224,6 +211,19 @@ let impl_1: t_Operation t_ViaMul =
         (Rust_primitives.Hax.Int.from_machine result <: Hax_lib.Int.t_Int));
     f_double = fun (x: u8) -> x *! 2uy
   }
+
+class t_TraitWithRequiresAndEnsures (v_Self: Type0) = {
+  f_method_pre:self___: v_Self -> x: u8 -> pred: Type0{x <. 100uy ==> pred};
+  f_method_post:self___: v_Self -> x: u8 -> r: u8 -> pred: Type0{pred ==> r >. 88uy};
+  f_method:x0: v_Self -> x1: u8
+    -> Prims.Pure u8 (f_method_pre x0 x1) (fun result -> f_method_post x0 x1 result)
+}
+
+let test
+      (#v_T: Type0)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_TraitWithRequiresAndEnsures v_T)
+      (x: v_T)
+    : u8 = (f_method #v_T #FStar.Tactics.Typeclasses.solve x 99uy <: u8) -! 88uy
 '''
 "Attributes.Refined_arithmetic.fst" = '''
 module Attributes.Refined_arithmetic
@@ -259,10 +259,10 @@ module Attributes.Refined_indexes
 open Core
 open FStar.Mul
 
-type t_MyArray = | MyArray : t_Array u8 (sz 10) -> t_MyArray
-
 let v_MAX: usize = sz 10
 
+type t_MyArray = | MyArray : t_Array u8 (sz 10) -> t_MyArray
+
 /// Triple dash comment
 (** Multiline double star comment Maecenas blandit accumsan feugiat.
     Done vitae ullamcorper est.
@@ -300,27 +300,20 @@ module Attributes.Refinement_types
 open Core
 open FStar.Mul
 
-/// Example of a specific constraint on a value
-let t_CompressionFactor = x: u8{x =. 4uy || x =. 5uy || x =. 10uy || x =. 11uy}
-
 let t_BoundedU8 (v_MIN v_MAX: u8) = x: u8{x >=. v_MIN && x <=. v_MAX}
 
-/// A field element
-let t_FieldElement = x: u16{x <=. 2347us}
+let bounded_u8 (x: t_BoundedU8 12uy 15uy) (y: t_BoundedU8 10uy 11uy) : t_BoundedU8 1uy 23uy =
+  (x <: u8) +! (y <: u8) <: t_BoundedU8 1uy 23uy
 
 /// Even `u8` numbers. Constructing pub Even values triggers static
 /// proofs in the extraction.
 let t_Even = x: u8{(x %! 2uy <: u8) =. 0uy}
 
-/// A modular mutliplicative inverse
-let t_ModInverse (v_MOD: u32) =
-  n:
-  u32
-    { (((cast (n <: u32) <: u128) *! (cast (v_MOD <: u32) <: u128) <: u128) %!
-        (cast (v_MOD <: u32) <: u128)
-        <:
-        u128) =.
-      pub_u128 1 }
+let double (x: u8) : Prims.Pure t_Even (requires x <. 127uy) (fun _ -> Prims.l_True) =
+  x +! x <: t_Even
+
+let double_refine (x: u8) : Prims.Pure t_Even (requires x <. 127uy) (fun _ -> Prims.l_True) =
+  x +! x <: t_Even
 
 /// A string that contains no space.
 let t_NoE =
@@ -342,14 +335,21 @@ let t_NoE =
       in
       ~.out }
 
-let double_refine (x: u8) : Prims.Pure t_Even (requires x <. 127uy) (fun _ -> Prims.l_True) =
-  x +! x <: t_Even
+/// A modular mutliplicative inverse
+let t_ModInverse (v_MOD: u32) =
+  n:
+  u32
+    { (((cast (n <: u32) <: u128) *! (cast (v_MOD <: u32) <: u128) <: u128) %!
+        (cast (v_MOD <: u32) <: u128)
+        <:
+        u128) =.
+      pub_u128 1 }
 
-let bounded_u8 (x: t_BoundedU8 12uy 15uy) (y: t_BoundedU8 10uy 11uy) : t_BoundedU8 1uy 23uy =
-  (x <: u8) +! (y <: u8) <: t_BoundedU8 1uy 23uy
+/// A field element
+let t_FieldElement = x: u16{x <=. 2347us}
 
-let double (x: u8) : Prims.Pure t_Even (requires x <. 127uy) (fun _ -> Prims.l_True) =
-  x +! x <: t_Even
+/// Example of a specific constraint on a value
+let t_CompressionFactor = x: u8{x =. 4uy || x =. 5uy || x =. 10uy || x =. 11uy}
 '''
 "Attributes.Requires_mut.fst" = '''
 module Attributes.Requires_mut
@@ -429,6 +429,12 @@ module Attributes.Verifcation_status
 open Core
 open FStar.Mul
 
+#push-options "--admit_smt_queries true"
+
+let a_function_which_only_laxes (_: Prims.unit) : Prims.unit = Hax_lib.v_assert false
+
+#pop-options
+
 let a_panicfree_function (_: Prims.unit)
     : Prims.Pure u8
       Prims.l_True
@@ -453,12 +459,6 @@ let another_panicfree_function (_: Prims.unit)
   let nothing:i32 = 0l in
   let still_not_much:i32 = not_much +! nothing in
   admit () (* Panic freedom *)
-
-#push-options "--admit_smt_queries true"
-
-let a_function_which_only_laxes (_: Prims.unit) : Prims.unit = Hax_lib.v_assert false
-
-#pop-options
 '''
 "Attributes.fst" = '''
 module Attributes
@@ -466,23 +466,20 @@ module Attributes
 open Core
 open FStar.Mul
 
-let inlined_code__V: u8 = 12uy
-
-let issue_844_ (v__x: u8)
-    : Prims.Pure u8
-      Prims.l_True
-      (ensures
-        fun v__x_future ->
-          let v__x_future:u8 = v__x_future in
-          true) = v__x
-
 let u32_max: u32 = 90000ul
 
-type t_Foo = {
-  f_x:u32;
-  f_y:f_y: u32{f_y >. 3ul};
-  f_z:f_z: u32{((f_y +! f_x <: u32) +! f_z <: u32) >. 3ul}
-}
+/// A doc comment on `add3`
+///another doc comment on add3
+let add3 (x y z: u32)
+    : Prims.Pure u32
+      (requires x >. 10ul && y >. 10ul && z >. 10ul && ((x +! y <: u32) +! z <: u32) <. u32_max)
+      (ensures
+        fun result ->
+          let result:u32 = result in
+          Hax_lib.implies true
+            (fun temp_0_ ->
+                let _:Prims.unit = temp_0_ in
+                result >. 32ul <: bool)) = (x +! y <: u32) +! z
 
 let swap_and_mut_req_ens (x y: u32)
     : Prims.Pure (u32 & u32 & u32)
@@ -497,18 +494,13 @@ let swap_and_mut_req_ens (x y: u32)
   let hax_temp_output:u32 = x +! y in
   x, y, hax_temp_output <: (u32 & u32 & u32)
 
-/// A doc comment on `add3`
-///another doc comment on add3
-let add3 (x y z: u32)
-    : Prims.Pure u32
-      (requires x >. 10ul && y >. 10ul && z >. 10ul && ((x +! y <: u32) +! z <: u32) <. u32_max)
+let issue_844_ (v__x: u8)
+    : Prims.Pure u8
+      Prims.l_True
       (ensures
-        fun result ->
-          let result:u32 = result in
-          Hax_lib.implies true
-            (fun temp_0_ ->
-                let _:Prims.unit = temp_0_ in
-                result >. 32ul <: bool)) = (x +! y <: u32) +! z
+        fun v__x_future ->
+          let v__x_future:u8 = v__x_future in
+          true) = v__x
 
 let add3_lemma (x: u32)
     : Lemma Prims.l_True
@@ -516,6 +508,14 @@ let add3_lemma (x: u32)
         x <=. 10ul || x >=. (u32_max /! 3ul <: u32) || (add3 x x x <: u32) =. (x *! 3ul <: u32)) =
   ()
 
+type t_Foo = {
+  f_x:u32;
+  f_y:f_y: u32{f_y >. 3ul};
+  f_z:f_z: u32{((f_y +! f_x <: u32) +! f_z <: u32) >. 3ul}
+}
+
+let inlined_code__V: u8 = 12uy
+
 unfold let some_function _ = "hello from F*"
 
 let before_inlined_code = "example before"
diff --git a/test-harness/src/snapshots/toolchain__constructor-as-closure into-fstar.snap b/test-harness/src/snapshots/toolchain__constructor-as-closure into-fstar.snap
index 6f8919b71..57b89460f 100644
--- a/test-harness/src/snapshots/toolchain__constructor-as-closure into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__constructor-as-closure into-fstar.snap	
@@ -32,15 +32,15 @@ module Constructor_as_closure
 open Core
 open FStar.Mul
 
-type t_Context =
-  | Context_A : i32 -> t_Context
-  | Context_B : i32 -> t_Context
-
 type t_Test = | Test : i32 -> t_Test
 
 let impl__Test__test (x: Core.Option.t_Option i32) : Core.Option.t_Option t_Test =
   Core.Option.impl__map #i32 #t_Test x Test
 
+type t_Context =
+  | Context_A : i32 -> t_Context
+  | Context_B : i32 -> t_Context
+
 let impl__Context__test (x: Core.Option.t_Option i32) : Core.Option.t_Option t_Context =
   Core.Option.impl__map #i32 #t_Context x Context_B
 '''
diff --git a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap
index d964ad67b..bde826973 100644
--- a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap	
@@ -138,16 +138,16 @@ module Cyclic_modules.Enums_a.Cyclic_bundle_1009707801
 open Core
 open FStar.Mul
 
-type t_T_366415196 =
-  | T_366415196_A : t_T_366415196
-  | T_366415196_B : t_T_366415196
-  | T_366415196_C : Alloc.Vec.t_Vec t_T_240131830 Alloc.Alloc.t_Global -> t_T_366415196
-
-and t_U =
+type t_U =
   | U_A : t_U
   | U_B : t_U
   | U_C : Alloc.Vec.t_Vec t_T_240131830 Alloc.Alloc.t_Global -> t_U
 
+and t_T_366415196 =
+  | T_366415196_A : t_T_366415196
+  | T_366415196_B : t_T_366415196
+  | T_366415196_C : Alloc.Vec.t_Vec t_T_240131830 Alloc.Alloc.t_Global -> t_T_366415196
+
 and t_T_240131830 =
   | T_240131830_A : t_T_240131830
   | T_240131830_B : t_T_240131830
@@ -178,14 +178,6 @@ module Cyclic_modules.Enums_b
 open Core
 open FStar.Mul
 
-include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {t_T_366415196 as t_T}
-
-include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {T_366415196_A as T_A}
-
-include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {T_366415196_B as T_B}
-
-include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {T_366415196_C as T_C}
-
 include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {t_U as t_U}
 
 include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {U_A as U_A}
@@ -194,6 +186,14 @@ include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {U_B as U_B}
 
 include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {U_C as U_C}
 
+include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {t_T_366415196 as t_T}
+
+include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {T_366415196_A as T_A}
+
+include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {T_366415196_B as T_B}
+
+include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {T_366415196_C as T_C}
+
 include Cyclic_modules.Enums_a.Cyclic_bundle_1009707801 {f as f}
 '''
 "Cyclic_modules.Late_skip_a.Cyclic_bundle_658016071.fst" = '''
@@ -202,10 +202,10 @@ module Cyclic_modules.Late_skip_a.Cyclic_bundle_658016071
 open Core
 open FStar.Mul
 
-let rec ff_749016415 (_: Prims.unit) : Prims.unit = ff_377825240 ()
-
-and ff_377825240 (_: Prims.unit) : Prims.Pure Prims.unit (requires true) (fun _ -> Prims.l_True) =
+let rec ff_377825240 (_: Prims.unit) : Prims.Pure Prims.unit (requires true) (fun _ -> Prims.l_True) =
   ff_749016415 ()
+
+and ff_749016415 (_: Prims.unit) : Prims.unit = ff_377825240 ()
 '''
 "Cyclic_modules.Late_skip_a.fst" = '''
 module Cyclic_modules.Late_skip_a
@@ -229,12 +229,12 @@ module Cyclic_modules.M1.Cyclic_bundle_892895908
 open Core
 open FStar.Mul
 
+let d (_: Prims.unit) : Prims.unit = ()
+
 let c (_: Prims.unit) : Prims.unit = ()
 
 let a (_: Prims.unit) : Prims.unit = c ()
 
-let d (_: Prims.unit) : Prims.unit = ()
-
 let b (_: Prims.unit) : Prims.unit =
   let _:Prims.unit = a () in
   d ()
@@ -253,10 +253,10 @@ module Cyclic_modules.M2
 open Core
 open FStar.Mul
 
-include Cyclic_modules.M1.Cyclic_bundle_892895908 {c as c}
-
 include Cyclic_modules.M1.Cyclic_bundle_892895908 {d as d}
 
+include Cyclic_modules.M1.Cyclic_bundle_892895908 {c as c}
+
 include Cyclic_modules.M1.Cyclic_bundle_892895908 {b as b}
 '''
 "Cyclic_modules.Rec.fst" = '''
@@ -279,15 +279,15 @@ let rec hf (x: t_T) : t_T =
   | T_t1  -> hf (T_t2 <: t_T)
   | T_t2  -> x
 
-let rec g1 (x: t_T) : t_T =
-  match x <: t_T with
-  | T_t1  -> g2 x
-  | T_t2  -> T_t1 <: t_T
-
-and g2 (x: t_T) : t_T =
+let rec g2 (x: t_T) : t_T =
   match x <: t_T with
   | T_t1  -> g1 x
   | T_t2  -> hf x
+
+and g1 (x: t_T) : t_T =
+  match x <: t_T with
+  | T_t1  -> g2 x
+  | T_t2  -> T_t1 <: t_T
 '''
 "Cyclic_modules.Rec1_same_name.Cyclic_bundle_563905053.fst" = '''
 module Cyclic_modules.Rec1_same_name.Cyclic_bundle_563905053
@@ -295,9 +295,9 @@ module Cyclic_modules.Rec1_same_name.Cyclic_bundle_563905053
 open Core
 open FStar.Mul
 
-let rec ff_533409751 (x: i32) : i32 = ff_91805216 x
+let rec ff_91805216 (x: i32) : i32 = if x >. 0l then ff_533409751 (x -! 1l <: i32) else 0l
 
-and ff_91805216 (x: i32) : i32 = if x >. 0l then ff_533409751 (x -! 1l <: i32) else 0l
+and ff_533409751 (x: i32) : i32 = ff_91805216 x
 '''
 "Cyclic_modules.Rec1_same_name.fst" = '''
 module Cyclic_modules.Rec1_same_name
@@ -329,13 +329,13 @@ let t_T1_cast_to_repr (x: t_T1) : isize = match x <: t_T1 with | T1_T1  -> isz 0
 
 type t_T2 = | T2_T2 : t_T -> t_T2
 
-type t_TRec =
-  | TRec_T : t_T1Rec -> t_TRec
-  | TRec_Empty : t_TRec
+type t_T2Rec = | T2Rec_T2 : t_TRec -> t_T2Rec
 
 and t_T1Rec = | T1Rec_T1 : Alloc.Boxed.t_Box t_T2Rec Alloc.Alloc.t_Global -> t_T1Rec
 
-and t_T2Rec = | T2Rec_T2 : t_TRec -> t_T2Rec
+and t_TRec =
+  | TRec_T : t_T1Rec -> t_TRec
+  | TRec_Empty : t_TRec
 '''
 "Cyclic_modules.Typ_a.fst" = '''
 module Cyclic_modules.Typ_a
@@ -369,13 +369,13 @@ include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {t_T2 as t_T2}
 
 include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {T2_T2 as T2_T2}
 
-include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {t_T1Rec as t_T1Rec}
-
-include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {T1Rec_T1 as T1Rec_T1}
-
 include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {t_T2Rec as t_T2Rec}
 
 include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {T2Rec_T2 as T2Rec_T2}
+
+include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {t_T1Rec as t_T1Rec}
+
+include Cyclic_modules.Typ_a.Cyclic_bundle_830459646 {T1Rec_T1 as T1Rec_T1}
 '''
 "Cyclic_modules.Variant_constructor_a.Cyclic_bundle_748213522.fst" = '''
 module Cyclic_modules.Variant_constructor_a.Cyclic_bundle_748213522
diff --git a/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap b/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap
index bfe3bcc0a..6209a1837 100644
--- a/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap	
@@ -42,11 +42,7 @@ Import RecordSetNotations.
 
 
 
-Definition discriminant_EnumWithRepr_ExplicitDiscr1 : t_u16 :=
-  1.
-
-Definition discriminant_EnumWithRepr_ExplicitDiscr2 : t_u16 :=
-  5.
+(* NotImplementedYet *)
 
 Inductive t_EnumWithRepr : Type :=
 | EnumWithRepr_ExplicitDiscr1
@@ -56,6 +52,12 @@ Inductive t_EnumWithRepr : Type :=
 Arguments t_EnumWithRepr:clear implicits.
 Arguments t_EnumWithRepr.
 
+Definition discriminant_EnumWithRepr_ExplicitDiscr1 : t_u16 :=
+  1.
+
+Definition discriminant_EnumWithRepr_ExplicitDiscr2 : t_u16 :=
+  5.
+
 Definition t_EnumWithRepr_cast_to_repr (x : t_EnumWithRepr) : t_u16 :=
   match x with
   | EnumWithRepr_ExplicitDiscr1 =>
@@ -68,8 +70,6 @@ Definition t_EnumWithRepr_cast_to_repr (x : t_EnumWithRepr) : t_u16 :=
     t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) (2)
   end.
 
-(* NotImplementedYet *)
-
 Definition f (_ : unit) : t_u32 :=
   let v__x := cast (t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) (0)) in
   t_Add_f_add (cast (t_EnumWithRepr_cast_to_repr (EnumWithRepr_ImplicitDiscrEmptyTuple))) (cast (t_EnumWithRepr_cast_to_repr (EnumWithRepr_ImplicitDiscrEmptyStruct))).
@@ -77,9 +77,9 @@ Definition f (_ : unit) : t_u32 :=
 Definition ff__CONST : t_u16 :=
   cast (t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr1) (0)).
 
-Definition get_casted_repr (x : t_EnumWithRepr) : t_u64 :=
-  cast (t_EnumWithRepr_cast_to_repr (x)).
-
 Definition get_repr (x : t_EnumWithRepr) : t_u16 :=
   t_EnumWithRepr_cast_to_repr (x).
+
+Definition get_casted_repr (x : t_EnumWithRepr) : t_u64 :=
+  cast (t_EnumWithRepr_cast_to_repr (x)).
 '''
diff --git a/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap b/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap
index 30788080c..2a5977c0b 100644
--- a/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap	
@@ -33,16 +33,16 @@ module Enum_repr
 open Core
 open FStar.Mul
 
-let discriminant_EnumWithRepr_ExplicitDiscr1: u16 = 1us
-
-let discriminant_EnumWithRepr_ExplicitDiscr2: u16 = 5us
-
 type t_EnumWithRepr =
   | EnumWithRepr_ExplicitDiscr1 : t_EnumWithRepr
   | EnumWithRepr_ExplicitDiscr2 : t_EnumWithRepr
   | EnumWithRepr_ImplicitDiscrEmptyTuple : t_EnumWithRepr
   | EnumWithRepr_ImplicitDiscrEmptyStruct : t_EnumWithRepr
 
+let discriminant_EnumWithRepr_ExplicitDiscr1: u16 = 1us
+
+let discriminant_EnumWithRepr_ExplicitDiscr2: u16 = 5us
+
 let t_EnumWithRepr_cast_to_repr (x: t_EnumWithRepr) : u16 =
   match x <: t_EnumWithRepr with
   | EnumWithRepr_ExplicitDiscr1  -> discriminant_EnumWithRepr_ExplicitDiscr1
@@ -64,7 +64,7 @@ let f (_: Prims.unit) : u32 =
 
 let ff__CONST: u16 = cast (discriminant_EnumWithRepr_ExplicitDiscr1 +! 0us <: u16) <: u16
 
-let get_casted_repr (x: t_EnumWithRepr) : u64 = cast (t_EnumWithRepr_cast_to_repr x <: u16) <: u64
-
 let get_repr (x: t_EnumWithRepr) : u16 = t_EnumWithRepr_cast_to_repr x
+
+let get_casted_repr (x: t_EnumWithRepr) : u64 = cast (t_EnumWithRepr_cast_to_repr x <: u16) <: u64
 '''
diff --git a/test-harness/src/snapshots/toolchain__enum-repr into-ssprove.snap b/test-harness/src/snapshots/toolchain__enum-repr into-ssprove.snap
index d1e4e4c09..613f21e5e 100644
--- a/test-harness/src/snapshots/toolchain__enum-repr into-ssprove.snap	
+++ b/test-harness/src/snapshots/toolchain__enum-repr into-ssprove.snap	
@@ -54,15 +54,7 @@ Import choice.Choice.Exports.
 
 Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.
 
-Equations discriminant_EnumWithRepr_ExplicitDiscr1 {L : {fset Location}} {I : Interface} : both L I int16 :=
-  discriminant_EnumWithRepr_ExplicitDiscr1  :=
-    solve_lift (ret_both (1 : int16)) : both L I int16.
-Fail Next Obligation.
-
-Equations discriminant_EnumWithRepr_ExplicitDiscr2 {L : {fset Location}} {I : Interface} : both L I int16 :=
-  discriminant_EnumWithRepr_ExplicitDiscr2  :=
-    solve_lift (ret_both (5 : int16)) : both L I int16.
-Fail Next Obligation.
+(*Not implemented yet? todo(item)*)
 
 Definition t_EnumWithRepr : choice_type :=
   ('unit ∐ 'unit ∐ 'unit ∐ 'unit).
@@ -87,6 +79,16 @@ Equations EnumWithRepr_ImplicitDiscrEmptyStruct {L : {fset Location}} {I : Inter
     solve_lift (ret_both (inr (tt : 'unit) : t_EnumWithRepr)) : both L I t_EnumWithRepr.
 Fail Next Obligation.
 
+Equations discriminant_EnumWithRepr_ExplicitDiscr1 {L : {fset Location}} {I : Interface} : both L I int16 :=
+  discriminant_EnumWithRepr_ExplicitDiscr1  :=
+    solve_lift (ret_both (1 : int16)) : both L I int16.
+Fail Next Obligation.
+
+Equations discriminant_EnumWithRepr_ExplicitDiscr2 {L : {fset Location}} {I : Interface} : both L I int16 :=
+  discriminant_EnumWithRepr_ExplicitDiscr2  :=
+    solve_lift (ret_both (5 : int16)) : both L I int16.
+Fail Next Obligation.
+
 Equations t_EnumWithRepr_cast_to_repr {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 t_EnumWithRepr) : both L1 I1 int16 :=
   t_EnumWithRepr_cast_to_repr x  :=
     matchb x with
@@ -101,8 +103,6 @@ Equations t_EnumWithRepr_cast_to_repr {L1 : {fset Location}} {I1 : Interface} (x
     end : both L1 I1 int16.
 Fail Next Obligation.
 
-(*Not implemented yet? todo(item)*)
-
 Equations f {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 int32 :=
   f _  :=
     letb v__x := cast_int (WS2 := _) (discriminant_EnumWithRepr_ExplicitDiscr2 .+ (ret_both (0 : int16))) in
@@ -114,13 +114,13 @@ Equations ff__CONST {L : {fset Location}} {I : Interface} : both L I int16 :=
     solve_lift (cast_int (WS2 := _) (discriminant_EnumWithRepr_ExplicitDiscr1 .+ (ret_both (0 : int16)))) : both L I int16.
 Fail Next Obligation.
 
-Equations get_casted_repr {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 t_EnumWithRepr) : both L1 I1 int64 :=
-  get_casted_repr x  :=
-    solve_lift (cast_int (WS2 := _) (t_EnumWithRepr_cast_to_repr x)) : both L1 I1 int64.
-Fail Next Obligation.
-
 Equations get_repr {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 t_EnumWithRepr) : both L1 I1 int16 :=
   get_repr x  :=
     solve_lift (t_EnumWithRepr_cast_to_repr x) : both L1 I1 int16.
 Fail Next Obligation.
+
+Equations get_casted_repr {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 t_EnumWithRepr) : both L1 I1 int64 :=
+  get_casted_repr x  :=
+    solve_lift (cast_int (WS2 := _) (t_EnumWithRepr_cast_to_repr x)) : both L1 I1 int64.
+Fail Next Obligation.
 '''
diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap
index 26fe6fce5..0fc420b27 100644
--- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap	
@@ -45,25 +45,25 @@ open FStar.Mul
 
 type t_Test = | Test : t_Test
 
-let impl__Test__set_alpn_protocols
+let impl__Test__set_ciphersuites
       (#v_S #impl_995885649_: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i2: Core.Convert.t_AsRef v_S string)
       (#[FStar.Tactics.Typeclasses.tcresolve ()]
           i3:
           Core.Iter.Traits.Collect.t_IntoIterator impl_995885649_)
       (self: t_Test)
-      (v__protocols: impl_995885649_)
+      (ciphers: impl_995885649_)
     : Core.Result.t_Result Prims.unit Prims.unit =
   Core.Result.Result_Ok (() <: Prims.unit) <: Core.Result.t_Result Prims.unit Prims.unit
 
-let impl__Test__set_ciphersuites
+let impl__Test__set_alpn_protocols
       (#v_S #impl_995885649_: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i2: Core.Convert.t_AsRef v_S string)
       (#[FStar.Tactics.Typeclasses.tcresolve ()]
           i3:
           Core.Iter.Traits.Collect.t_IntoIterator impl_995885649_)
       (self: t_Test)
-      (ciphers: impl_995885649_)
+      (v__protocols: impl_995885649_)
     : Core.Result.t_Result Prims.unit Prims.unit =
   Core.Result.Result_Ok (() <: Prims.unit) <: Core.Result.t_Result Prims.unit Prims.unit
 '''
@@ -73,26 +73,6 @@ module Generics
 open Core
 open FStar.Mul
 
-let impl__Bar__inherent_impl_generics (#v_T: Type0) (v_N: usize) (x: t_Array v_T v_N) : Prims.unit =
-  ()
-
-type t_Bar = | Bar : t_Bar
-
-class t_Foo (v_Self: Type0) = {
-  f_const_add_pre:v_N: usize -> v_Self -> Type0;
-  f_const_add_post:v_N: usize -> v_Self -> usize -> Type0;
-  f_const_add:v_N: usize -> x0: v_Self
-    -> Prims.Pure usize (f_const_add_pre v_N x0) (fun result -> f_const_add_post v_N x0 result)
-}
-
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_Foo_for_usize: t_Foo usize =
-  {
-    f_const_add_pre = (fun (v_N: usize) (self: usize) -> true);
-    f_const_add_post = (fun (v_N: usize) (self: usize) (out: usize) -> true);
-    f_const_add = fun (v_N: usize) (self: usize) -> self +! v_N
-  }
-
 let dup
       (#v_T: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_T)
@@ -103,6 +83,30 @@ let dup
   <:
   (v_T & v_T)
 
+let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize =
+  let acc:usize = v_LEN +! sz 9 in
+  let acc:usize =
+    Rust_primitives.Hax.Folds.fold_range (sz 0)
+      v_LEN
+      (fun acc temp_1_ ->
+          let acc:usize = acc in
+          let _:usize = temp_1_ in
+          true)
+      acc
+      (fun acc i ->
+          let acc:usize = acc in
+          let i:usize = i in
+          acc +! (arr.[ i ] <: usize) <: usize)
+  in
+  acc
+
+let repeat
+      (v_LEN: usize)
+      (#v_T: Type0)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Marker.t_Copy v_T)
+      (x: v_T)
+    : t_Array v_T v_LEN = Rust_primitives.Hax.repeat x v_LEN
+
 let f (v_N x: usize) : usize = (v_N +! v_N <: usize) +! x
 
 let call_f (_: Prims.unit) : usize = (f (sz 10) (sz 3) <: usize) +! sz 3
@@ -140,27 +144,23 @@ let call_g (_: Prims.unit) : usize =
     usize) +!
   sz 3
 
-let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize =
-  let acc:usize = v_LEN +! sz 9 in
-  let acc:usize =
-    Rust_primitives.Hax.Folds.fold_range (sz 0)
-      v_LEN
-      (fun acc temp_1_ ->
-          let acc:usize = acc in
-          let _:usize = temp_1_ in
-          true)
-      acc
-      (fun acc i ->
-          let acc:usize = acc in
-          let i:usize = i in
-          acc +! (arr.[ i ] <: usize) <: usize)
-  in
-  acc
+class t_Foo (v_Self: Type0) = {
+  f_const_add_pre:v_N: usize -> v_Self -> Type0;
+  f_const_add_post:v_N: usize -> v_Self -> usize -> Type0;
+  f_const_add:v_N: usize -> x0: v_Self
+    -> Prims.Pure usize (f_const_add_pre v_N x0) (fun result -> f_const_add_post v_N x0 result)
+}
 
-let repeat
-      (v_LEN: usize)
-      (#v_T: Type0)
-      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Marker.t_Copy v_T)
-      (x: v_T)
-    : t_Array v_T v_LEN = Rust_primitives.Hax.repeat x v_LEN
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl_Foo_for_usize: t_Foo usize =
+  {
+    f_const_add_pre = (fun (v_N: usize) (self: usize) -> true);
+    f_const_add_post = (fun (v_N: usize) (self: usize) (out: usize) -> true);
+    f_const_add = fun (v_N: usize) (self: usize) -> self +! v_N
+  }
+
+type t_Bar = | Bar : t_Bar
+
+let impl__Bar__inherent_impl_generics (#v_T: Type0) (v_N: usize) (x: t_Array v_T v_N) : Prims.unit =
+  ()
 '''
diff --git a/test-harness/src/snapshots/toolchain__guards into-coq.snap b/test-harness/src/snapshots/toolchain__guards into-coq.snap
index abd2a3274..7755eb3aa 100644
--- a/test-harness/src/snapshots/toolchain__guards into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__guards into-coq.snap	
@@ -43,7 +43,7 @@ Import RecordSetNotations.
 
 (* NotImplementedYet *)
 
-Definition equivalent (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 :=
+Definition if_let_guard (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 :=
   match x with
   | Option_None =>
     0
@@ -59,8 +59,8 @@ Definition equivalent (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 :=
     | _ =>
       Option_None
     end with
-    | Option_Some (y) =>
-      y
+    | Option_Some (x) =>
+      x
     | Option_None =>
       match x with
       | Option_Some (Result_Err (y)) =>
@@ -71,25 +71,7 @@ Definition equivalent (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 :=
     end
   end.
 
-Definition if_guard (x : t_Option ((t_i32))) : t_i32 :=
-  match match x with
-  | Option_Some (v) =>
-    match t_PartialOrd_f_gt (v) (0) with
-    | true =>
-      Option_Some (v)
-    | _ =>
-      Option_None
-    end
-  | _ =>
-    Option_None
-  end with
-  | Option_Some (x) =>
-    x
-  | Option_None =>
-    0
-  end.
-
-Definition if_let_guard (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 :=
+Definition equivalent (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 :=
   match x with
   | Option_None =>
     0
@@ -105,8 +87,8 @@ Definition if_let_guard (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32
     | _ =>
       Option_None
     end with
-    | Option_Some (x) =>
-      x
+    | Option_Some (y) =>
+      y
     | Option_None =>
       match x with
       | Option_Some (Result_Err (y)) =>
@@ -159,4 +141,22 @@ Definition multiple_guards (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i
       end
     end
   end.
+
+Definition if_guard (x : t_Option ((t_i32))) : t_i32 :=
+  match match x with
+  | Option_Some (v) =>
+    match t_PartialOrd_f_gt (v) (0) with
+    | true =>
+      Option_Some (v)
+    | _ =>
+      Option_None
+    end
+  | _ =>
+    Option_None
+  end with
+  | Option_Some (x) =>
+    x
+  | Option_None =>
+    0
+  end.
 '''
diff --git a/test-harness/src/snapshots/toolchain__guards into-fstar.snap b/test-harness/src/snapshots/toolchain__guards into-fstar.snap
index cf6aebabc..729bf71af 100644
--- a/test-harness/src/snapshots/toolchain__guards into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__guards into-fstar.snap	
@@ -32,7 +32,7 @@ module Guards
 open Core
 open FStar.Mul
 
-let equivalent (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i32 =
+let if_let_guard (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i32 =
   match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
   | Core.Option.Option_None  -> 0l
   | _ ->
@@ -46,27 +46,13 @@ let equivalent (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i32 =
       <:
       Core.Option.t_Option i32
     with
-    | Core.Option.Option_Some y -> y
+    | Core.Option.Option_Some x -> x
     | Core.Option.Option_None  ->
       match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
       | Core.Option.Option_Some (Core.Result.Result_Err y) -> y
       | _ -> 1l
 
-let if_guard (x: Core.Option.t_Option i32) : i32 =
-  match
-    (match x <: Core.Option.t_Option i32 with
-      | Core.Option.Option_Some v ->
-        (match v >. 0l <: bool with
-          | true -> Core.Option.Option_Some v <: Core.Option.t_Option i32
-          | _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
-      | _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
-    <:
-    Core.Option.t_Option i32
-  with
-  | Core.Option.Option_Some x -> x
-  | Core.Option.Option_None  -> 0l
-
-let if_let_guard (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i32 =
+let equivalent (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i32 =
   match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
   | Core.Option.Option_None  -> 0l
   | _ ->
@@ -80,7 +66,7 @@ let if_let_guard (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i32
       <:
       Core.Option.t_Option i32
     with
-    | Core.Option.Option_Some x -> x
+    | Core.Option.Option_Some y -> y
     | Core.Option.Option_None  ->
       match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
       | Core.Option.Option_Some (Core.Result.Result_Err y) -> y
@@ -117,4 +103,18 @@ let multiple_guards (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i
         match x <: Core.Option.t_Option (Core.Result.t_Result i32 i32) with
         | Core.Option.Option_Some (Core.Result.Result_Err y) -> y
         | _ -> 1l
+
+let if_guard (x: Core.Option.t_Option i32) : i32 =
+  match
+    (match x <: Core.Option.t_Option i32 with
+      | Core.Option.Option_Some v ->
+        (match v >. 0l <: bool with
+          | true -> Core.Option.Option_Some v <: Core.Option.t_Option i32
+          | _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
+      | _ -> Core.Option.Option_None <: Core.Option.t_Option i32)
+    <:
+    Core.Option.t_Option i32
+  with
+  | Core.Option.Option_Some x -> x
+  | Core.Option.Option_None  -> 0l
 '''
diff --git a/test-harness/src/snapshots/toolchain__guards into-ssprove.snap b/test-harness/src/snapshots/toolchain__guards into-ssprove.snap
index 57b079118..a499287d3 100644
--- a/test-harness/src/snapshots/toolchain__guards into-ssprove.snap	
+++ b/test-harness/src/snapshots/toolchain__guards into-ssprove.snap	
@@ -55,8 +55,8 @@ Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.
 
 (*Not implemented yet? todo(item)*)
 
-Equations equivalent {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_Option (t_Result int32 int32))) : both L1 I1 int32 :=
-  equivalent x  :=
+Equations if_let_guard {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_Option (t_Result int32 int32))) : both L1 I1 int32 :=
+  if_let_guard x  :=
     matchb x with
     | Option_None_case  =>
       solve_lift (ret_both (0 : int32))
@@ -74,9 +74,9 @@ Equations equivalent {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_
       | _ =>
         Option_None
       end with
-      | Option_Some_case y =>
-        letb y := ret_both ((y) : (int32)) in
-        solve_lift y
+      | Option_Some_case x =>
+        letb x := ret_both ((x) : (int32)) in
+        solve_lift x
       | Option_None_case  =>
         matchb x with
         | Option_Some_case Result_Err y =>
@@ -89,30 +89,8 @@ Equations equivalent {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_
     end : both L1 I1 int32.
 Fail Next Obligation.
 
-Equations if_guard {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_Option int32)) : both L1 I1 int32 :=
-  if_guard x  :=
-    matchb matchb x with
-    | Option_Some_case v =>
-      letb v := ret_both ((v) : (int32)) in
-      matchb v >.? (ret_both (0 : int32)) with
-      | true =>
-        Option_Some (solve_lift v)
-      | _ =>
-        Option_None
-      end
-    | _ =>
-      Option_None
-    end with
-    | Option_Some_case x =>
-      letb x := ret_both ((x) : (int32)) in
-      solve_lift x
-    | Option_None_case  =>
-      solve_lift (ret_both (0 : int32))
-    end : both L1 I1 int32.
-Fail Next Obligation.
-
-Equations if_let_guard {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_Option (t_Result int32 int32))) : both L1 I1 int32 :=
-  if_let_guard x  :=
+Equations equivalent {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_Option (t_Result int32 int32))) : both L1 I1 int32 :=
+  equivalent x  :=
     matchb x with
     | Option_None_case  =>
       solve_lift (ret_both (0 : int32))
@@ -130,9 +108,9 @@ Equations if_let_guard {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (
       | _ =>
         Option_None
       end with
-      | Option_Some_case x =>
-        letb x := ret_both ((x) : (int32)) in
-        solve_lift x
+      | Option_Some_case y =>
+        letb y := ret_both ((y) : (int32)) in
+        solve_lift y
       | Option_None_case  =>
         matchb x with
         | Option_Some_case Result_Err y =>
@@ -196,4 +174,26 @@ Equations multiple_guards {L1 : {fset Location}} {I1 : Interface} (x : both L1 I
       end
     end : both L1 I1 int32.
 Fail Next Obligation.
+
+Equations if_guard {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_Option int32)) : both L1 I1 int32 :=
+  if_guard x  :=
+    matchb matchb x with
+    | Option_Some_case v =>
+      letb v := ret_both ((v) : (int32)) in
+      matchb v >.? (ret_both (0 : int32)) with
+      | true =>
+        Option_Some (solve_lift v)
+      | _ =>
+        Option_None
+      end
+    | _ =>
+      Option_None
+    end with
+    | Option_Some_case x =>
+      letb x := ret_both ((x) : (int32)) in
+      solve_lift x
+    | Option_None_case  =>
+      solve_lift (ret_both (0 : int32))
+    end : both L1 I1 int32.
+Fail Next Obligation.
 '''
diff --git a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap
index c86f3b275..04abbc64e 100644
--- a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap	
@@ -41,6 +41,8 @@ Import RecordSetNotations.
 
 
 
+(* NotImplementedYet *)
+
 Record t_Foo : Type :=
   {
   }.
@@ -60,14 +62,24 @@ Instance t_Trait_254780795 : t_Trait ((t_Foo)) :=
   {
   }.
 
-(* NotImplementedYet *)
-
 Definition main_a_a (_ : unit) : unit :=
   tt.
 
+Definition main_b_a (_ : unit) : unit :=
+  tt.
+
+Definition main_c_a (_ : unit) : unit :=
+  tt.
+
 Definition main_a_b (_ : unit) : unit :=
   tt.
 
+Definition main_b_b (_ : unit) : unit :=
+  tt.
+
+Definition main_c_b (_ : unit) : unit :=
+  tt.
+
 Definition main_a_c (_ : unit) : unit :=
   tt.
 
@@ -77,12 +89,6 @@ Definition main_a `{v_T : Type} `{t_Sized (v_T)} `{t_Trait (v_T)} (x : v_T) : un
   let _ := main_a_c (tt) in
   tt.
 
-Definition main_b_a (_ : unit) : unit :=
-  tt.
-
-Definition main_b_b (_ : unit) : unit :=
-  tt.
-
 Definition main_b_c (_ : unit) : unit :=
   tt.
 
@@ -92,12 +98,6 @@ Definition main_b (_ : unit) : unit :=
   let _ := main_b_c (tt) in
   tt.
 
-Definition main_c_a (_ : unit) : unit :=
-  tt.
-
-Definition main_c_b (_ : unit) : unit :=
-  tt.
-
 Definition main_c_c (_ : unit) : unit :=
   tt.
 
diff --git a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap
index 41cd2ac28..de9402027 100644
--- a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap	
@@ -42,8 +42,16 @@ let impl_Trait_for_Foo: t_Trait t_Foo = { __marker_trait = () }
 /// Indirect dependencies
 let main_a_a (_: Prims.unit) : Prims.unit = ()
 
+let main_b_a (_: Prims.unit) : Prims.unit = ()
+
+let main_c_a (_: Prims.unit) : Prims.unit = ()
+
 let main_a_b (_: Prims.unit) : Prims.unit = ()
 
+let main_b_b (_: Prims.unit) : Prims.unit = ()
+
+let main_c_b (_: Prims.unit) : Prims.unit = ()
+
 let main_a_c (_: Prims.unit) : Prims.unit = ()
 
 /// Direct dependencies
@@ -54,10 +62,6 @@ let main_a (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Trait
   let _:Prims.unit = main_a_c () in
   ()
 
-let main_b_a (_: Prims.unit) : Prims.unit = ()
-
-let main_b_b (_: Prims.unit) : Prims.unit = ()
-
 let main_b_c (_: Prims.unit) : Prims.unit = ()
 
 let main_b (_: Prims.unit) : Prims.unit =
@@ -66,10 +70,6 @@ let main_b (_: Prims.unit) : Prims.unit =
   let _:Prims.unit = main_b_c () in
   ()
 
-let main_c_a (_: Prims.unit) : Prims.unit = ()
-
-let main_c_b (_: Prims.unit) : Prims.unit = ()
-
 let main_c_c (_: Prims.unit) : Prims.unit = ()
 
 let main_c (_: Prims.unit) : Prims.unit =
diff --git a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap
index dcdee90a4..edfe10447 100644
--- a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap	
@@ -33,26 +33,23 @@ module Interface_only
 open Core
 open FStar.Mul
 
-type t_Bar = | Bar : t_Bar
-
-type t_Holder (v_T: Type0) = { f_value:Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global }
-
-type t_Param (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE }
+/// This item contains unsafe blocks and raw references, two features
+/// not supported by hax. Thanks to the `-i` flag and the `+:`
+/// modifier, `f` is still extractable as an interface.
+/// Expressions within type are still extracted, as well as pre- and
+/// post-conditions.
+assume
+val f': x: u8
+  -> Prims.Pure (t_Array u8 (sz 4))
+      (requires x <. 254uy)
+      (ensures
+        fun r ->
+          let r:t_Array u8 (sz 4) = r in
+          (r.[ sz 0 ] <: u8) >. x)
 
-class t_T2 (v_Self: Type0) = {
-  f_d_pre:Prims.unit -> Type0;
-  f_d_post:Prims.unit -> Prims.unit -> Type0;
-  f_d:x0: Prims.unit -> Prims.Pure Prims.unit (f_d_pre x0) (fun result -> f_d_post x0 result)
-}
+let f = f'
 
-/// Items can be forced to be transparent
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_T2_for_u8: t_T2 u8 =
-  {
-    f_d_pre = (fun (_: Prims.unit) -> false);
-    f_d_post = (fun (_: Prims.unit) (out: Prims.unit) -> true);
-    f_d = fun (_: Prims.unit) -> ()
-  }
+type t_Bar = | Bar : t_Bar
 
 /// Non-inherent implementations are extracted, their bodies are not
 /// dropped. This might be a bit surprising: see
@@ -75,39 +72,42 @@ val from__from': u8 -> t_Bar
 
 let from__from = from__from'
 
+type t_Holder (v_T: Type0) = { f_value:Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global }
+
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 assume
 val impl_2': #v_T: Type0 -> Core.Convert.t_From (t_Holder v_T) Prims.unit
 
 let impl_2 (#v_T: Type0) = impl_2' #v_T
 
+type t_Param (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE }
+
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 assume
 val impl_3': v_SIZE: usize -> Core.Convert.t_From (t_Param v_SIZE) Prims.unit
 
 let impl_3 (v_SIZE: usize) = impl_3' v_SIZE
 
-/// This item contains unsafe blocks and raw references, two features
-/// not supported by hax. Thanks to the `-i` flag and the `+:`
-/// modifier, `f` is still extractable as an interface.
-/// Expressions within type are still extracted, as well as pre- and
-/// post-conditions.
-assume
-val f': x: u8
-  -> Prims.Pure (t_Array u8 (sz 4))
-      (requires x <. 254uy)
-      (ensures
-        fun r ->
-          let r:t_Array u8 (sz 4) = r in
-          (r.[ sz 0 ] <: u8) >. x)
-
-let f = f'
-
 assume
 val ff_generic': v_X: usize -> #v_U: Type0 -> v__x: v_U -> t_Param v_X
 
 let ff_generic (v_X: usize) (#v_U: Type0) = ff_generic' v_X #v_U
 
+class t_T2 (v_Self: Type0) = {
+  f_d_pre:Prims.unit -> Type0;
+  f_d_post:Prims.unit -> Prims.unit -> Type0;
+  f_d:x0: Prims.unit -> Prims.Pure Prims.unit (f_d_pre x0) (fun result -> f_d_post x0 result)
+}
+
+/// Items can be forced to be transparent
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl_T2_for_u8: t_T2 u8 =
+  {
+    f_d_pre = (fun (_: Prims.unit) -> false);
+    f_d_post = (fun (_: Prims.unit) (out: Prims.unit) -> true);
+    f_d = fun (_: Prims.unit) -> ()
+  }
+
 class t_T (v_Self: Type0) = {
   f_Assoc:Type0;
   f_d_pre:Prims.unit -> Type0;
diff --git a/test-harness/src/snapshots/toolchain__literals into-coq.snap b/test-harness/src/snapshots/toolchain__literals into-coq.snap
index 4ef4fb981..87a42d7cd 100644
--- a/test-harness/src/snapshots/toolchain__literals into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__literals into-coq.snap	
@@ -42,39 +42,10 @@ Import RecordSetNotations.
 
 
 
-From Literals Require Import Hax_lib (t_int).
-Export Hax_lib (t_int).
-
-Record t_Foo : Type :=
-  {
-    f_field : t_u8;
-  }.
-Arguments t_Foo:clear implicits.
-Arguments t_Foo.
-Arguments Build_t_Foo.
-#[export] Instance settable_t_Foo : Settable _ :=
-  settable! (@Build_t_Foo) <f_field>.
-
 (* NotImplementedYet *)
 
-Definition v_CONSTANT : t_Foo :=
-  Build_t_Foo (3).
-
-Definition casts (x8 : t_u8) (x16 : t_u16) (x32 : t_u32) (x64 : t_u64) (xs : t_usize) : unit :=
-  let _ : t_u64 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (x64)) (cast (xs)) in
-  let _ : t_u32 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (x32)) (cast (x64))) (cast (xs)) in
-  let _ : t_u16 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (x16)) (cast (x32))) (cast (x64))) (cast (xs)) in
-  let _ : t_u8 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (x8) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
-  let _ : t_i64 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
-  let _ : t_i32 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
-  let _ : t_i16 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
-  let _ : t_i8 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
-  tt.
-
-Definition fn_pointer_cast (_ : unit) : unit :=
-  let f : t_u32 -> t_u32 := fun x =>
-    x in
-  tt.
+From Literals Require Import Hax_lib (t_int).
+Export Hax_lib (t_int).
 
 Definition math_integers (x : t_Int) `{andb (f_gt (x) (impl__Int___unsafe_from_str ("0"%string))) (f_lt (x) (impl__Int___unsafe_from_str ("16"%string))) = true} : t_u8 :=
   let _ : t_Int := f_lift (3) in
@@ -100,8 +71,27 @@ Definition math_integers (x : t_Int) `{andb (f_gt (x) (impl__Int___unsafe_from_s
   let _ : t_usize := impl__Int__to_usize (x) in
   impl__Int__to_u8 (f_add (x) (f_mul (x) (x))).
 
-Definition null : ascii :=
-  "\000"%char.
+Definition panic_with_msg (_ : unit) : unit :=
+  never_to_any (panic_fmt (impl_2__new_const (["with msg"%string]))).
+
+Record t_Foo : Type :=
+  {
+    f_field : t_u8;
+  }.
+Arguments t_Foo:clear implicits.
+Arguments t_Foo.
+Arguments Build_t_Foo.
+#[export] Instance settable_t_Foo : Settable _ :=
+  settable! (@Build_t_Foo) <f_field>.
+
+
+
+
+
+
+
+Definition v_CONSTANT : t_Foo :=
+  Build_t_Foo (3).
 
 Definition numeric (_ : unit) : unit :=
   let _ : t_usize := 123 in
@@ -132,16 +122,26 @@ Definition patterns (_ : unit) : unit :=
   end in
   tt.
 
-
-
-
-
-
-
-Definition panic_with_msg (_ : unit) : unit :=
-  never_to_any (panic_fmt (impl_2__new_const (["with msg"%string]))).
+Definition casts (x8 : t_u8) (x16 : t_u16) (x32 : t_u32) (x64 : t_u64) (xs : t_usize) : unit :=
+  let _ : t_u64 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (x64)) (cast (xs)) in
+  let _ : t_u32 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (x32)) (cast (x64))) (cast (xs)) in
+  let _ : t_u16 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (x16)) (cast (x32))) (cast (x64))) (cast (xs)) in
+  let _ : t_u8 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (x8) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
+  let _ : t_i64 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
+  let _ : t_i32 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
+  let _ : t_i16 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
+  let _ : t_i8 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in
+  tt.
 
 Definition empty_array (_ : unit) : unit :=
   let _ : t_Slice t_u8 := unsize ([]) in
   tt.
+
+Definition fn_pointer_cast (_ : unit) : unit :=
+  let f : t_u32 -> t_u32 := fun x =>
+    x in
+  tt.
+
+Definition null : ascii :=
+  "\000"%char.
 '''
diff --git a/test-harness/src/snapshots/toolchain__literals into-fstar.snap b/test-harness/src/snapshots/toolchain__literals into-fstar.snap
index 355ca6097..5e0ea4ae5 100644
--- a/test-harness/src/snapshots/toolchain__literals into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__literals into-fstar.snap	
@@ -33,10 +33,104 @@ module Literals
 open Core
 open FStar.Mul
 
+let math_integers (x: Hax_lib.Int.t_Int)
+    : Prims.Pure u8
+      (requires x > (0 <: Hax_lib.Int.t_Int) && x < (16 <: Hax_lib.Int.t_Int))
+      (fun _ -> Prims.l_True) =
+  let _:Hax_lib.Int.t_Int = Rust_primitives.Hax.Int.from_machine (sz 3) in
+  let _:bool =
+    ((-340282366920938463463374607431768211455000) <: Hax_lib.Int.t_Int) >
+    (340282366920938463463374607431768211455000 <: Hax_lib.Int.t_Int)
+  in
+  let _:bool = x < x in
+  let _:bool = x >= x in
+  let _:bool = x <= x in
+  let _:bool = x <> x in
+  let _:bool = x = x in
+  let _:Hax_lib.Int.t_Int = x + x in
+  let _:Hax_lib.Int.t_Int = x - x in
+  let _:Hax_lib.Int.t_Int = x * x in
+  let _:Hax_lib.Int.t_Int = x / x in
+  let _:i16 = Hax_lib.Int.impl__Int__to_i16 x in
+  let _:i32 = Hax_lib.Int.impl__Int__to_i32 x in
+  let _:i64 = Hax_lib.Int.impl__Int__to_i64 x in
+  let _:i128 = Hax_lib.Int.impl__Int__to_i128 x in
+  let _:isize = Hax_lib.Int.impl__Int__to_isize x in
+  let _:u16 = Hax_lib.Int.impl__Int__to_u16 x in
+  let _:u32 = Hax_lib.Int.impl__Int__to_u32 x in
+  let _:u64 = Hax_lib.Int.impl__Int__to_u64 x in
+  let _:u128 = Hax_lib.Int.impl__Int__to_u128 x in
+  let _:usize = Hax_lib.Int.impl__Int__to_usize x in
+  Hax_lib.Int.impl__Int__to_u8 (x + (x * x <: Hax_lib.Int.t_Int) <: Hax_lib.Int.t_Int)
+
+let panic_with_msg (_: Prims.unit) : Prims.unit =
+  Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.impl_2__new_const (sz 1)
+            (let list = ["with msg"] in
+              FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+              Rust_primitives.Hax.array_of_list 1 list)
+          <:
+          Core.Fmt.t_Arguments)
+      <:
+      Rust_primitives.Hax.t_Never)
+
 type t_Foo = { f_field:u8 }
 
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+assume
+val impl': Core.Marker.t_StructuralPartialEq t_Foo
+
+let impl = impl'
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+assume
+val impl_1': Core.Cmp.t_PartialEq t_Foo t_Foo
+
+let impl_1 = impl_1'
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+assume
+val impl_2': Core.Cmp.t_Eq t_Foo
+
+let impl_2 = impl_2'
+
 let v_CONSTANT: t_Foo = { f_field = 3uy } <: t_Foo
 
+let numeric (_: Prims.unit) : Prims.unit =
+  let _:usize = sz 123 in
+  let _:isize = isz (-42) in
+  let _:isize = isz 42 in
+  let _:i32 = (-42l) in
+  let _:u128 = pub_u128 22222222222222222222 in
+  ()
+
+let patterns (_: Prims.unit) : Prims.unit =
+  let _:Prims.unit =
+    match 1uy <: u8 with
+    | 2uy -> () <: Prims.unit
+    | _ -> () <: Prims.unit
+  in
+  let _:Prims.unit =
+    match
+      "hello",
+      (123l,
+        (let list = ["a"; "b"] in
+          FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
+          Rust_primitives.Hax.array_of_list 2 list)
+        <:
+        (i32 & t_Array string (sz 2)))
+      <:
+      (string & (i32 & t_Array string (sz 2)))
+    with
+    | "hello", (123l, v__todo) -> () <: Prims.unit
+    | _ -> () <: Prims.unit
+  in
+  let _:Prims.unit =
+    match { f_field = 4uy } <: t_Foo with
+    | { f_field = 3uy } -> () <: Prims.unit
+    | _ -> () <: Prims.unit
+  in
+  ()
+
 let casts (x8: u8) (x16: u16) (x32: u32) (x64: u64) (xs: usize) : Prims.unit =
   let _:u64 =
     ((((cast (x8 <: u8) <: u64) +! (cast (x16 <: u16) <: u64) <: u64) +! (cast (x32 <: u32) <: u64)
@@ -106,107 +200,6 @@ let casts (x8: u8) (x16: u16) (x32: u32) (x64: u64) (xs: usize) : Prims.unit =
   in
   ()
 
-/// https://github.com/hacspec/hax/issues/500
-let fn_pointer_cast (_: Prims.unit) : Prims.unit =
-  let (f: (u32 -> u32)): u32 -> u32 = fun x -> x in
-  ()
-
-let math_integers (x: Hax_lib.Int.t_Int)
-    : Prims.Pure u8
-      (requires x > (0 <: Hax_lib.Int.t_Int) && x < (16 <: Hax_lib.Int.t_Int))
-      (fun _ -> Prims.l_True) =
-  let _:Hax_lib.Int.t_Int = Rust_primitives.Hax.Int.from_machine (sz 3) in
-  let _:bool =
-    ((-340282366920938463463374607431768211455000) <: Hax_lib.Int.t_Int) >
-    (340282366920938463463374607431768211455000 <: Hax_lib.Int.t_Int)
-  in
-  let _:bool = x < x in
-  let _:bool = x >= x in
-  let _:bool = x <= x in
-  let _:bool = x <> x in
-  let _:bool = x = x in
-  let _:Hax_lib.Int.t_Int = x + x in
-  let _:Hax_lib.Int.t_Int = x - x in
-  let _:Hax_lib.Int.t_Int = x * x in
-  let _:Hax_lib.Int.t_Int = x / x in
-  let _:i16 = Hax_lib.Int.impl__Int__to_i16 x in
-  let _:i32 = Hax_lib.Int.impl__Int__to_i32 x in
-  let _:i64 = Hax_lib.Int.impl__Int__to_i64 x in
-  let _:i128 = Hax_lib.Int.impl__Int__to_i128 x in
-  let _:isize = Hax_lib.Int.impl__Int__to_isize x in
-  let _:u16 = Hax_lib.Int.impl__Int__to_u16 x in
-  let _:u32 = Hax_lib.Int.impl__Int__to_u32 x in
-  let _:u64 = Hax_lib.Int.impl__Int__to_u64 x in
-  let _:u128 = Hax_lib.Int.impl__Int__to_u128 x in
-  let _:usize = Hax_lib.Int.impl__Int__to_usize x in
-  Hax_lib.Int.impl__Int__to_u8 (x + (x * x <: Hax_lib.Int.t_Int) <: Hax_lib.Int.t_Int)
-
-let null: char = '\0'
-
-let numeric (_: Prims.unit) : Prims.unit =
-  let _:usize = sz 123 in
-  let _:isize = isz (-42) in
-  let _:isize = isz 42 in
-  let _:i32 = (-42l) in
-  let _:u128 = pub_u128 22222222222222222222 in
-  ()
-
-let patterns (_: Prims.unit) : Prims.unit =
-  let _:Prims.unit =
-    match 1uy <: u8 with
-    | 2uy -> () <: Prims.unit
-    | _ -> () <: Prims.unit
-  in
-  let _:Prims.unit =
-    match
-      "hello",
-      (123l,
-        (let list = ["a"; "b"] in
-          FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
-          Rust_primitives.Hax.array_of_list 2 list)
-        <:
-        (i32 & t_Array string (sz 2)))
-      <:
-      (string & (i32 & t_Array string (sz 2)))
-    with
-    | "hello", (123l, v__todo) -> () <: Prims.unit
-    | _ -> () <: Prims.unit
-  in
-  let _:Prims.unit =
-    match { f_field = 4uy } <: t_Foo with
-    | { f_field = 3uy } -> () <: Prims.unit
-    | _ -> () <: Prims.unit
-  in
-  ()
-
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-assume
-val impl': Core.Marker.t_StructuralPartialEq t_Foo
-
-let impl = impl'
-
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-assume
-val impl_1': Core.Cmp.t_PartialEq t_Foo t_Foo
-
-let impl_1 = impl_1'
-
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-assume
-val impl_2': Core.Cmp.t_Eq t_Foo
-
-let impl_2 = impl_2'
-
-let panic_with_msg (_: Prims.unit) : Prims.unit =
-  Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.impl_2__new_const (sz 1)
-            (let list = ["with msg"] in
-              FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
-              Rust_primitives.Hax.array_of_list 1 list)
-          <:
-          Core.Fmt.t_Arguments)
-      <:
-      Rust_primitives.Hax.t_Never)
-
 let empty_array (_: Prims.unit) : Prims.unit =
   let _:t_Slice u8 =
     (let list:Prims.list u8 = [] in
@@ -216,4 +209,11 @@ let empty_array (_: Prims.unit) : Prims.unit =
     t_Slice u8
   in
   ()
+
+/// https://github.com/hacspec/hax/issues/500
+let fn_pointer_cast (_: Prims.unit) : Prims.unit =
+  let (f: (u32 -> u32)): u32 -> u32 = fun x -> x in
+  ()
+
+let null: char = '\0'
 '''
diff --git a/test-harness/src/snapshots/toolchain__loops into-fstar.snap b/test-harness/src/snapshots/toolchain__loops into-fstar.snap
index 36eaac7f4..e51648762 100644
--- a/test-harness/src/snapshots/toolchain__loops into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__loops into-fstar.snap	
@@ -84,83 +84,6 @@ module Loops.Control_flow
 open Core
 open FStar.Mul
 
-type t_M = { f_m:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global }
-
-let impl__M__decoded_message (self: t_M)
-    : Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
-  match
-    Rust_primitives.Hax.Folds.fold_range_return (sz 0)
-      (Alloc.Vec.impl_1__len #u8 #Alloc.Alloc.t_Global self.f_m <: usize)
-      (fun temp_0_ temp_1_ ->
-          let _:Prims.unit = temp_0_ in
-          let _:usize = temp_1_ in
-          true)
-      ()
-      (fun temp_0_ i ->
-          let _:Prims.unit = temp_0_ in
-          let i:usize = i in
-          if i >. sz 5 <: bool
-          then
-            Core.Ops.Control_flow.ControlFlow_Break
-            (Core.Ops.Control_flow.ControlFlow_Break
-              (Core.Option.Option_None
-                <:
-                Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
-              <:
-              Core.Ops.Control_flow.t_ControlFlow
-                (Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
-                (Prims.unit & Prims.unit))
-            <:
-            Core.Ops.Control_flow.t_ControlFlow
-              (Core.Ops.Control_flow.t_ControlFlow
-                  (Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
-                  (Prims.unit & Prims.unit)) Prims.unit
-          else
-            Core.Ops.Control_flow.ControlFlow_Continue ()
-            <:
-            Core.Ops.Control_flow.t_ControlFlow
-              (Core.Ops.Control_flow.t_ControlFlow
-                  (Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
-                  (Prims.unit & Prims.unit)) Prims.unit)
-    <:
-    Core.Ops.Control_flow.t_ControlFlow
-      (Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) Prims.unit
-  with
-  | Core.Ops.Control_flow.ControlFlow_Break ret -> ret
-  | Core.Ops.Control_flow.ControlFlow_Continue _ ->
-    Core.Option.Option_Some
-    (Core.Clone.f_clone #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
-        #FStar.Tactics.Typeclasses.solve
-        self.f_m)
-    <:
-    Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
-
-let bigger_power_2_ (x: i32) : i32 =
-  let pow:i32 = 1l in
-  Rust_primitives.f_while_loop_cf (fun pow ->
-        let pow:i32 = pow in
-        pow <. 1000000l <: bool)
-    pow
-    (fun pow ->
-        let pow:i32 = pow in
-        let pow:i32 = pow *! 2l in
-        if pow <. x
-        then
-          let pow:i32 = pow *! 3l in
-          if true
-          then
-            Core.Ops.Control_flow.ControlFlow_Break ((), pow <: (Prims.unit & i32))
-            <:
-            Core.Ops.Control_flow.t_ControlFlow (Prims.unit & i32) i32
-          else
-            Core.Ops.Control_flow.ControlFlow_Continue (pow *! 2l)
-            <:
-            Core.Ops.Control_flow.t_ControlFlow (Prims.unit & i32) i32
-        else
-          Core.Ops.Control_flow.ControlFlow_Continue (pow *! 2l)
-          <:
-          Core.Ops.Control_flow.t_ControlFlow (Prims.unit & i32) i32)
-
 let double_sum (_: Prims.unit) : i32 =
   let sum:i32 = 0l in
   let sum:i32 =
@@ -214,6 +137,38 @@ let double_sum2 (_: Prims.unit) : i32 =
   in
   sum +! sum2
 
+let double_sum_return (v: t_Slice i32) : i32 =
+  let sum:i32 = 0l in
+  match
+    Rust_primitives.Hax.f_fold_return (Core.Iter.Traits.Collect.f_into_iter #(t_Slice i32)
+          #FStar.Tactics.Typeclasses.solve
+          v
+        <:
+        Core.Slice.Iter.t_Iter i32)
+      sum
+      (fun sum i ->
+          let sum:i32 = sum in
+          let i:i32 = i in
+          if i <. 0l <: bool
+          then
+            Core.Ops.Control_flow.ControlFlow_Break
+            (Core.Ops.Control_flow.ControlFlow_Break 0l
+              <:
+              Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & i32))
+            <:
+            Core.Ops.Control_flow.t_ControlFlow
+              (Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & i32)) i32
+          else
+            Core.Ops.Control_flow.ControlFlow_Continue (sum +! i <: i32)
+            <:
+            Core.Ops.Control_flow.t_ControlFlow
+              (Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & i32)) i32)
+    <:
+    Core.Ops.Control_flow.t_ControlFlow i32 i32
+  with
+  | Core.Ops.Control_flow.ControlFlow_Break ret -> ret
+  | Core.Ops.Control_flow.ControlFlow_Continue sum -> sum *! 2l
+
 let double_sum2_return (v: t_Slice i32) : i32 =
   let sum:i32 = 0l in
   let sum2:i32 = 0l in
@@ -248,37 +203,82 @@ let double_sum2_return (v: t_Slice i32) : i32 =
   | Core.Ops.Control_flow.ControlFlow_Break ret -> ret
   | Core.Ops.Control_flow.ControlFlow_Continue (sum, sum2) -> sum +! sum2
 
-let double_sum_return (v: t_Slice i32) : i32 =
-  let sum:i32 = 0l in
+let bigger_power_2_ (x: i32) : i32 =
+  let pow:i32 = 1l in
+  Rust_primitives.f_while_loop_cf (fun pow ->
+        let pow:i32 = pow in
+        pow <. 1000000l <: bool)
+    pow
+    (fun pow ->
+        let pow:i32 = pow in
+        let pow:i32 = pow *! 2l in
+        if pow <. x
+        then
+          let pow:i32 = pow *! 3l in
+          if true
+          then
+            Core.Ops.Control_flow.ControlFlow_Break ((), pow <: (Prims.unit & i32))
+            <:
+            Core.Ops.Control_flow.t_ControlFlow (Prims.unit & i32) i32
+          else
+            Core.Ops.Control_flow.ControlFlow_Continue (pow *! 2l)
+            <:
+            Core.Ops.Control_flow.t_ControlFlow (Prims.unit & i32) i32
+        else
+          Core.Ops.Control_flow.ControlFlow_Continue (pow *! 2l)
+          <:
+          Core.Ops.Control_flow.t_ControlFlow (Prims.unit & i32) i32)
+
+type t_M = { f_m:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global }
+
+let impl__M__decoded_message (self: t_M)
+    : Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
   match
-    Rust_primitives.Hax.f_fold_return (Core.Iter.Traits.Collect.f_into_iter #(t_Slice i32)
-          #FStar.Tactics.Typeclasses.solve
-          v
-        <:
-        Core.Slice.Iter.t_Iter i32)
-      sum
-      (fun sum i ->
-          let sum:i32 = sum in
-          let i:i32 = i in
-          if i <. 0l <: bool
+    Rust_primitives.Hax.Folds.fold_range_return (sz 0)
+      (Alloc.Vec.impl_1__len #u8 #Alloc.Alloc.t_Global self.f_m <: usize)
+      (fun temp_0_ temp_1_ ->
+          let _:Prims.unit = temp_0_ in
+          let _:usize = temp_1_ in
+          true)
+      ()
+      (fun temp_0_ i ->
+          let _:Prims.unit = temp_0_ in
+          let i:usize = i in
+          if i >. sz 5 <: bool
           then
             Core.Ops.Control_flow.ControlFlow_Break
-            (Core.Ops.Control_flow.ControlFlow_Break 0l
+            (Core.Ops.Control_flow.ControlFlow_Break
+              (Core.Option.Option_None
+                <:
+                Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
               <:
-              Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & i32))
+              Core.Ops.Control_flow.t_ControlFlow
+                (Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
+                (Prims.unit & Prims.unit))
             <:
             Core.Ops.Control_flow.t_ControlFlow
-              (Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & i32)) i32
+              (Core.Ops.Control_flow.t_ControlFlow
+                  (Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
+                  (Prims.unit & Prims.unit)) Prims.unit
           else
-            Core.Ops.Control_flow.ControlFlow_Continue (sum +! i <: i32)
+            Core.Ops.Control_flow.ControlFlow_Continue ()
             <:
             Core.Ops.Control_flow.t_ControlFlow
-              (Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & i32)) i32)
+              (Core.Ops.Control_flow.t_ControlFlow
+                  (Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
+                  (Prims.unit & Prims.unit)) Prims.unit)
     <:
-    Core.Ops.Control_flow.t_ControlFlow i32 i32
+    Core.Ops.Control_flow.t_ControlFlow
+      (Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) Prims.unit
   with
   | Core.Ops.Control_flow.ControlFlow_Break ret -> ret
-  | Core.Ops.Control_flow.ControlFlow_Continue sum -> sum *! 2l
+  | Core.Ops.Control_flow.ControlFlow_Continue _ ->
+    Core.Option.Option_Some
+    (Core.Clone.f_clone #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+        #FStar.Tactics.Typeclasses.solve
+        self.f_m)
+    <:
+    Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
 
 let nested (_: Prims.unit) : i32 =
   let sum:i32 = 0l in
@@ -384,7 +384,94 @@ module Loops.For_loops
 open Core
 open FStar.Mul
 
-let bool_returning (x: u8) : bool = x <. 10uy
+let range1 (_: Prims.unit) : usize =
+  let acc:usize = sz 0 in
+  let acc:usize =
+    Rust_primitives.Hax.Folds.fold_range (sz 0)
+      (sz 15)
+      (fun acc temp_1_ ->
+          let acc:usize = acc in
+          let _:usize = temp_1_ in
+          true)
+      acc
+      (fun acc i ->
+          let acc:usize = acc in
+          let i:usize = i in
+          acc +! i <: usize)
+  in
+  acc
+
+let range2 (n: usize) : usize =
+  let acc:usize = sz 0 in
+  let acc:usize =
+    Rust_primitives.Hax.Folds.fold_range (sz 0)
+      (n +! sz 10 <: usize)
+      (fun acc temp_1_ ->
+          let acc:usize = acc in
+          let _:usize = temp_1_ in
+          true)
+      acc
+      (fun acc i ->
+          let acc:usize = acc in
+          let i:usize = i in
+          (acc +! i <: usize) +! sz 1 <: usize)
+  in
+  acc
+
+let composed_range (n: usize) : usize =
+  let acc:usize = sz 0 in
+  let acc:usize =
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Chain.t_Chain
+              (Core.Ops.Range.t_Range usize) (Core.Ops.Range.t_Range usize))
+          #FStar.Tactics.Typeclasses.solve
+          (Core.Iter.Traits.Iterator.f_chain #(Core.Ops.Range.t_Range usize)
+              #FStar.Tactics.Typeclasses.solve
+              #(Core.Ops.Range.t_Range usize)
+              ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n }
+                <:
+                Core.Ops.Range.t_Range usize)
+              ({
+                  Core.Ops.Range.f_start = n +! sz 10 <: usize;
+                  Core.Ops.Range.f_end = n +! sz 50 <: usize
+                }
+                <:
+                Core.Ops.Range.t_Range usize)
+            <:
+            Core.Iter.Adapters.Chain.t_Chain (Core.Ops.Range.t_Range usize)
+              (Core.Ops.Range.t_Range usize))
+        <:
+        Core.Iter.Adapters.Chain.t_Chain (Core.Ops.Range.t_Range usize)
+          (Core.Ops.Range.t_Range usize))
+      acc
+      (fun acc i ->
+          let acc:usize = acc in
+          let i:usize = i in
+          (acc +! i <: usize) +! sz 1 <: usize)
+  in
+  acc
+
+let rev_range (n: usize) : usize =
+  let acc:usize = sz 0 in
+  let acc:usize =
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Rev.t_Rev
+            (Core.Ops.Range.t_Range usize))
+          #FStar.Tactics.Typeclasses.solve
+          (Core.Iter.Traits.Iterator.f_rev #(Core.Ops.Range.t_Range usize)
+              #FStar.Tactics.Typeclasses.solve
+              ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n }
+                <:
+                Core.Ops.Range.t_Range usize)
+            <:
+            Core.Iter.Adapters.Rev.t_Rev (Core.Ops.Range.t_Range usize))
+        <:
+        Core.Iter.Adapters.Rev.t_Rev (Core.Ops.Range.t_Range usize))
+      acc
+      (fun acc i ->
+          let acc:usize = acc in
+          let i:usize = i in
+          (acc +! i <: usize) +! sz 1 <: usize)
+  in
+  acc
 
 let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
   let acc:usize = sz 0 in
@@ -442,97 +529,6 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global
   in
   acc
 
-let composed_range (n: usize) : usize =
-  let acc:usize = sz 0 in
-  let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Chain.t_Chain
-              (Core.Ops.Range.t_Range usize) (Core.Ops.Range.t_Range usize))
-          #FStar.Tactics.Typeclasses.solve
-          (Core.Iter.Traits.Iterator.f_chain #(Core.Ops.Range.t_Range usize)
-              #FStar.Tactics.Typeclasses.solve
-              #(Core.Ops.Range.t_Range usize)
-              ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n }
-                <:
-                Core.Ops.Range.t_Range usize)
-              ({
-                  Core.Ops.Range.f_start = n +! sz 10 <: usize;
-                  Core.Ops.Range.f_end = n +! sz 50 <: usize
-                }
-                <:
-                Core.Ops.Range.t_Range usize)
-            <:
-            Core.Iter.Adapters.Chain.t_Chain (Core.Ops.Range.t_Range usize)
-              (Core.Ops.Range.t_Range usize))
-        <:
-        Core.Iter.Adapters.Chain.t_Chain (Core.Ops.Range.t_Range usize)
-          (Core.Ops.Range.t_Range usize))
-      acc
-      (fun acc i ->
-          let acc:usize = acc in
-          let i:usize = i in
-          (acc +! i <: usize) +! sz 1 <: usize)
-  in
-  acc
-
-let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
-  let acc:usize = sz 0 in
-  let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Enumerate.t_Enumerate
-            (Core.Slice.Iter.t_Chunks usize))
-          #FStar.Tactics.Typeclasses.solve
-          (Core.Iter.Traits.Iterator.f_enumerate #(Core.Slice.Iter.t_Chunks usize)
-              #FStar.Tactics.Typeclasses.solve
-              (Core.Slice.impl__chunks #usize
-                  (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global)
-                      #FStar.Tactics.Typeclasses.solve
-                      arr
-                    <:
-                    t_Slice usize)
-                  (sz 4)
-                <:
-                Core.Slice.Iter.t_Chunks usize)
-            <:
-            Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Chunks usize))
-        <:
-        Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Chunks usize))
-      acc
-      (fun acc temp_1_ ->
-          let acc:usize = acc in
-          let i, chunk:(usize & t_Slice usize) = temp_1_ in
-          Rust_primitives.Hax.Folds.fold_enumerated_slice chunk
-            (fun acc temp_1_ ->
-                let acc:usize = acc in
-                let _:usize = temp_1_ in
-                true)
-            acc
-            (fun acc temp_1_ ->
-                let acc:usize = acc in
-                let j, x:(usize & usize) = temp_1_ in
-                (i +! j <: usize) +! x <: usize)
-          <:
-          usize)
-  in
-  acc
-
-let f (_: Prims.unit) : (u8 & Prims.unit) =
-  let acc:u8 = 0uy in
-  Rust_primitives.Hax.Folds.fold_range 1uy
-    10uy
-    (fun acc temp_1_ ->
-        let acc:u8 = acc in
-        let _:u8 = temp_1_ in
-        true)
-    acc
-    (fun acc i ->
-        let acc:u8 = acc in
-        let i:u8 = i in
-        let acc:u8 = acc +! i in
-        let _:bool = bool_returning i in
-        acc),
-  ()
-  <:
-  (u8 & Prims.unit)
-
 let iterator (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
   let acc:usize = sz 0 in
   let acc:usize =
@@ -644,62 +640,66 @@ let pattern (arr: Alloc.Vec.t_Vec (usize & usize) Alloc.Alloc.t_Global) : usize
   in
   acc
 
-let range1 (_: Prims.unit) : usize =
-  let acc:usize = sz 0 in
-  let acc:usize =
-    Rust_primitives.Hax.Folds.fold_range (sz 0)
-      (sz 15)
-      (fun acc temp_1_ ->
-          let acc:usize = acc in
-          let _:usize = temp_1_ in
-          true)
-      acc
-      (fun acc i ->
-          let acc:usize = acc in
-          let i:usize = i in
-          acc +! i <: usize)
-  in
-  acc
-
-let range2 (n: usize) : usize =
-  let acc:usize = sz 0 in
-  let acc:usize =
-    Rust_primitives.Hax.Folds.fold_range (sz 0)
-      (n +! sz 10 <: usize)
-      (fun acc temp_1_ ->
-          let acc:usize = acc in
-          let _:usize = temp_1_ in
-          true)
-      acc
-      (fun acc i ->
-          let acc:usize = acc in
-          let i:usize = i in
-          (acc +! i <: usize) +! sz 1 <: usize)
-  in
-  acc
-
-let rev_range (n: usize) : usize =
+let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
   let acc:usize = sz 0 in
   let acc:usize =
-    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Rev.t_Rev
-            (Core.Ops.Range.t_Range usize))
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Enumerate.t_Enumerate
+            (Core.Slice.Iter.t_Chunks usize))
           #FStar.Tactics.Typeclasses.solve
-          (Core.Iter.Traits.Iterator.f_rev #(Core.Ops.Range.t_Range usize)
+          (Core.Iter.Traits.Iterator.f_enumerate #(Core.Slice.Iter.t_Chunks usize)
               #FStar.Tactics.Typeclasses.solve
-              ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n }
+              (Core.Slice.impl__chunks #usize
+                  (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global)
+                      #FStar.Tactics.Typeclasses.solve
+                      arr
+                    <:
+                    t_Slice usize)
+                  (sz 4)
                 <:
-                Core.Ops.Range.t_Range usize)
+                Core.Slice.Iter.t_Chunks usize)
             <:
-            Core.Iter.Adapters.Rev.t_Rev (Core.Ops.Range.t_Range usize))
+            Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Chunks usize))
         <:
-        Core.Iter.Adapters.Rev.t_Rev (Core.Ops.Range.t_Range usize))
+        Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Chunks usize))
       acc
-      (fun acc i ->
+      (fun acc temp_1_ ->
           let acc:usize = acc in
-          let i:usize = i in
-          (acc +! i <: usize) +! sz 1 <: usize)
+          let i, chunk:(usize & t_Slice usize) = temp_1_ in
+          Rust_primitives.Hax.Folds.fold_enumerated_slice chunk
+            (fun acc temp_1_ ->
+                let acc:usize = acc in
+                let _:usize = temp_1_ in
+                true)
+            acc
+            (fun acc temp_1_ ->
+                let acc:usize = acc in
+                let j, x:(usize & usize) = temp_1_ in
+                (i +! j <: usize) +! x <: usize)
+          <:
+          usize)
   in
   acc
+
+let bool_returning (x: u8) : bool = x <. 10uy
+
+let f (_: Prims.unit) : (u8 & Prims.unit) =
+  let acc:u8 = 0uy in
+  Rust_primitives.Hax.Folds.fold_range 1uy
+    10uy
+    (fun acc temp_1_ ->
+        let acc:u8 = acc in
+        let _:u8 = temp_1_ in
+        true)
+    acc
+    (fun acc i ->
+        let acc:u8 = acc in
+        let i:u8 = i in
+        let acc:u8 = acc +! i in
+        let _:bool = bool_returning i in
+        acc),
+  ()
+  <:
+  (u8 & Prims.unit)
 '''
 "Loops.Recognized_loops.fst" = '''
 module Loops.Recognized_loops
@@ -707,73 +707,73 @@ module Loops.Recognized_loops
 open Core
 open FStar.Mul
 
-let enumerated_chunked_slice (#v_T: Type0) (slice: t_Slice v_T) : (u64 & Prims.unit) =
+let range (_: Prims.unit) : (u64 & Prims.unit) =
   let count:u64 = 0uL in
-  Rust_primitives.Hax.Folds.fold_enumerated_chunked_slice (sz 3)
-    slice
+  Rust_primitives.Hax.Folds.fold_range 0uy
+    10uy
     (fun count i ->
         let count:u64 = count in
-        let i:usize = i in
-        i <= Core.Slice.impl__len #v_T slice <: usize)
+        let i:u8 = i in
+        i <=. 10uy <: bool)
     count
     (fun count i ->
         let count:u64 = count in
-        let i:(usize & t_Slice v_T) = i in
-        let count:u64 = count +! 3uL in
+        let i:u8 = i in
+        let count:u64 = count +! 1uL in
         count),
   ()
   <:
   (u64 & Prims.unit)
 
-let enumerated_slice (#v_T: Type0) (slice: t_Slice v_T) : (u64 & Prims.unit) =
+let range_step_by (_: Prims.unit) : (u64 & Prims.unit) =
   let count:u64 = 0uL in
-  Rust_primitives.Hax.Folds.fold_enumerated_slice slice
+  Rust_primitives.Hax.Folds.fold_range_step_by 0uy
+    10uy
+    (sz 2)
     (fun count i ->
         let count:u64 = count in
-        let i:usize = i in
-        i <=. sz 10 <: bool)
+        let i:u8 = i in
+        i <=. 10uy <: bool)
     count
     (fun count i ->
         let count:u64 = count in
-        let i:(usize & v_T) = i in
-        let count:u64 = count +! 2uL in
+        let i:u8 = i in
+        let count:u64 = count +! 1uL in
         count),
   ()
   <:
   (u64 & Prims.unit)
 
-let range (_: Prims.unit) : (u64 & Prims.unit) =
+let enumerated_slice (#v_T: Type0) (slice: t_Slice v_T) : (u64 & Prims.unit) =
   let count:u64 = 0uL in
-  Rust_primitives.Hax.Folds.fold_range 0uy
-    10uy
+  Rust_primitives.Hax.Folds.fold_enumerated_slice slice
     (fun count i ->
         let count:u64 = count in
-        let i:u8 = i in
-        i <=. 10uy <: bool)
+        let i:usize = i in
+        i <=. sz 10 <: bool)
     count
     (fun count i ->
         let count:u64 = count in
-        let i:u8 = i in
-        let count:u64 = count +! 1uL in
+        let i:(usize & v_T) = i in
+        let count:u64 = count +! 2uL in
         count),
   ()
   <:
   (u64 & Prims.unit)
 
-let range_step_by (_: Prims.unit) : (u64 & Prims.unit) =
+let enumerated_chunked_slice (#v_T: Type0) (slice: t_Slice v_T) : (u64 & Prims.unit) =
   let count:u64 = 0uL in
-  Rust_primitives.Hax.Folds.fold_range_step_by 0uy
-    10uy
-    (sz 2)
+  Rust_primitives.Hax.Folds.fold_enumerated_chunked_slice (sz 3)
+    slice
     (fun count i ->
         let count:u64 = count in
-        let i:u8 = i in
-        i <=. 10uy <: bool)
+        let i:usize = i in
+        i <= Core.Slice.impl__len #v_T slice <: usize)
     count
     (fun count i ->
         let count:u64 = count in
-        let i:u8 = i in
-        let count:u64 = count +! 1uL in
+        let i:(usize & t_Slice v_T) = i in
+        let count:u64 = count +! 3uL in
         count),
   ()
   <:
diff --git a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap
index fee5eaadb..f1ffe9f82 100644
--- a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap	
@@ -32,102 +32,8 @@ module Mut_ref_functionalization
 open Core
 open FStar.Mul
 
-type t_Bar = {
-  f_a:u8;
-  f_b:u8
-}
-
-type t_Foo = { f_field:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global }
-
-class t_FooTrait (v_Self: Type0) = {
-  f_z_pre:v_Self -> Type0;
-  f_z_post:v_Self -> v_Self -> Type0;
-  f_z:x0: v_Self -> Prims.Pure v_Self (f_z_pre x0) (fun result -> f_z_post x0 result)
-}
-
-[@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_FooTrait_for_Foo: t_FooTrait t_Foo =
-  {
-    f_z_pre = (fun (self: t_Foo) -> true);
-    f_z_post = (fun (self: t_Foo) (out: t_Foo) -> true);
-    f_z = fun (self: t_Foo) -> self
-  }
-
-type t_Pair (v_T: Type0) = {
-  f_a:v_T;
-  f_b:t_Foo
-}
-
 type t_S = { f_b:t_Array u8 (sz 5) }
 
-let impl__S__update (self: t_S) (x: u8) : t_S =
-  let self:t_S =
-    {
-      self with
-      f_b = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize self.f_b (sz 0) x
-    }
-    <:
-    t_S
-  in
-  self
-
-let array (x: t_Array u8 (sz 10)) : t_Array u8 (sz 10) =
-  let x:t_Array u8 (sz 10) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize x (sz 1) (x.[ sz 2 ] <: u8)
-  in
-  x
-
-let f (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new #u8 () in
-  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-    Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global vec 1uy
-  in
-  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-    Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global vec 2uy
-  in
-  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap #u8 vec (sz 0) (sz 1) in
-  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap #u8 vec (sz 0) (sz 1) in
-  vec
-
-let h (x: u8) : u8 =
-  let x:u8 = x +! 10uy in
-  x
-
-let i (bar: t_Bar) : (t_Bar & u8) =
-  let bar:t_Bar = { bar with f_b = bar.f_b +! bar.f_a } <: t_Bar in
-  let bar:t_Bar = { bar with f_a = h bar.f_a } <: t_Bar in
-  let hax_temp_output:u8 = bar.f_a +! bar.f_b in
-  bar, hax_temp_output <: (t_Bar & u8)
-
-let j (x: t_Bar) : (t_Bar & u8) =
-  let out:u8 = 123uy in
-  let tmp0, out1:(t_Bar & u8) = i x in
-  let x:t_Bar = tmp0 in
-  let hax_temp_output:u8 = out1 +! out in
-  x, hax_temp_output <: (t_Bar & u8)
-
-let k
-      (vec: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
-      (arg_1_wild3: u16)
-      (arg_1_wild: u8)
-      (arg_3_wild2: Prims.unit)
-    : (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & u16 & Prims.unit & u64) =
-  let arg_1_wild2:u8 = vec.[ sz 1 ] in
-  let arg_3_wild:u8 = vec.[ sz 2 ] in
-  let arg_1_wild1:u8 = vec.[ sz 3 ] in
-  let arg_3_wild1:u8 = vec.[ sz 4 ] in
-  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize vec
-      (sz 0)
-      ((((arg_1_wild +! arg_3_wild <: u8) +! arg_1_wild1 <: u8) +! arg_3_wild1 <: u8) +! arg_1_wild
-        <:
-        u8)
-  in
-  let hax_temp_output:u64 = 12345uL in
-  vec, arg_1_wild3, arg_3_wild2, hax_temp_output
-  <:
-  (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & u16 & Prims.unit & u64)
-
 let foo (lhs rhs: t_S) : t_S =
   let lhs:t_S =
     Rust_primitives.Hax.Folds.fold_range (sz 0)
@@ -155,56 +61,16 @@ let foo (lhs rhs: t_S) : t_S =
   in
   lhs
 
-let g (x: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
-    : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-  let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = x in
-  let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
-    Rust_primitives.Hax.Folds.fold_range 1uy
-      10uy
-      (fun x temp_1_ ->
-          let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = x in
-          let _:u8 = temp_1_ in
-          true)
-      x
-      (fun x i ->
-          let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = x in
-          let i:u8 = i in
-          {
-            x with
-            f_a
-            =
-            Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global x.f_a i
-            <:
-            Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global
-          }
-          <:
-          t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
-  in
-  let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
-    { x with f_a = Core.Slice.impl__swap #u8 x.f_a (sz 0) (sz 1) }
-    <:
-    t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
-  in
-  let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
+let impl__S__update (self: t_S) (x: u8) : t_S =
+  let self:t_S =
     {
-      x with
-      f_b = { x.f_b with f_field = Core.Slice.impl__swap #u8 x.f_b.f_field (sz 0) (sz 1) } <: t_Foo
+      self with
+      f_b = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize self.f_b (sz 0) x
     }
     <:
-    t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+    t_S
   in
-  x.f_a
-
-let build_vec (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-  Alloc.Slice.impl__into_vec #u8
-    #Alloc.Alloc.t_Global
-    (Rust_primitives.unsize (Rust_primitives.Hax.box_new (let list = [1uy; 2uy; 3uy] in
-              FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3);
-              Rust_primitives.Hax.array_of_list 3 list)
-          <:
-          Alloc.Boxed.t_Box (t_Array u8 (sz 3)) Alloc.Alloc.t_Global)
-      <:
-      Alloc.Boxed.t_Box (t_Slice u8) Alloc.Alloc.t_Global)
+  self
 
 let index_mutation (x: Core.Ops.Range.t_Range usize) (a: t_Slice u8) : Prims.unit =
   let v:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
@@ -250,6 +116,17 @@ let index_mutation_unsize (x: t_Array u8 (sz 12)) : u8 =
   in
   42uy
 
+let build_vec (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
+  Alloc.Slice.impl__into_vec #u8
+    #Alloc.Alloc.t_Global
+    (Rust_primitives.unsize (Rust_primitives.Hax.box_new (let list = [1uy; 2uy; 3uy] in
+              FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3);
+              Rust_primitives.Hax.array_of_list 3 list)
+          <:
+          Alloc.Boxed.t_Box (t_Array u8 (sz 3)) Alloc.Alloc.t_Global)
+      <:
+      Alloc.Boxed.t_Box (t_Slice u8) Alloc.Alloc.t_Global)
+
 let test_append (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
   let vec1:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new #u8 () in
   let vec2:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
@@ -277,4 +154,127 @@ let test_append (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
       (build_vec () <: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
   in
   vec1
+
+let f (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
+  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new #u8 () in
+  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
+    Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global vec 1uy
+  in
+  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
+    Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global vec 2uy
+  in
+  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap #u8 vec (sz 0) (sz 1) in
+  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap #u8 vec (sz 0) (sz 1) in
+  vec
+
+type t_Foo = { f_field:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global }
+
+type t_Pair (v_T: Type0) = {
+  f_a:v_T;
+  f_b:t_Foo
+}
+
+let g (x: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
+    : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
+  let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = x in
+  let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
+    Rust_primitives.Hax.Folds.fold_range 1uy
+      10uy
+      (fun x temp_1_ ->
+          let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = x in
+          let _:u8 = temp_1_ in
+          true)
+      x
+      (fun x i ->
+          let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = x in
+          let i:u8 = i in
+          {
+            x with
+            f_a
+            =
+            Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global x.f_a i
+            <:
+            Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global
+          }
+          <:
+          t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global))
+  in
+  let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
+    { x with f_a = Core.Slice.impl__swap #u8 x.f_a (sz 0) (sz 1) }
+    <:
+    t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+  in
+  let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) =
+    {
+      x with
+      f_b = { x.f_b with f_field = Core.Slice.impl__swap #u8 x.f_b.f_field (sz 0) (sz 1) } <: t_Foo
+    }
+    <:
+    t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+  in
+  x.f_a
+
+let h (x: u8) : u8 =
+  let x:u8 = x +! 10uy in
+  x
+
+type t_Bar = {
+  f_a:u8;
+  f_b:u8
+}
+
+let i (bar: t_Bar) : (t_Bar & u8) =
+  let bar:t_Bar = { bar with f_b = bar.f_b +! bar.f_a } <: t_Bar in
+  let bar:t_Bar = { bar with f_a = h bar.f_a } <: t_Bar in
+  let hax_temp_output:u8 = bar.f_a +! bar.f_b in
+  bar, hax_temp_output <: (t_Bar & u8)
+
+let j (x: t_Bar) : (t_Bar & u8) =
+  let out:u8 = 123uy in
+  let tmp0, out1:(t_Bar & u8) = i x in
+  let x:t_Bar = tmp0 in
+  let hax_temp_output:u8 = out1 +! out in
+  x, hax_temp_output <: (t_Bar & u8)
+
+let k
+      (vec: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+      (arg_1_wild3: u16)
+      (arg_1_wild: u8)
+      (arg_3_wild2: Prims.unit)
+    : (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & u16 & Prims.unit & u64) =
+  let arg_1_wild2:u8 = vec.[ sz 1 ] in
+  let arg_3_wild:u8 = vec.[ sz 2 ] in
+  let arg_1_wild1:u8 = vec.[ sz 3 ] in
+  let arg_3_wild1:u8 = vec.[ sz 4 ] in
+  let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
+    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize vec
+      (sz 0)
+      ((((arg_1_wild +! arg_3_wild <: u8) +! arg_1_wild1 <: u8) +! arg_3_wild1 <: u8) +! arg_1_wild
+        <:
+        u8)
+  in
+  let hax_temp_output:u64 = 12345uL in
+  vec, arg_1_wild3, arg_3_wild2, hax_temp_output
+  <:
+  (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & u16 & Prims.unit & u64)
+
+class t_FooTrait (v_Self: Type0) = {
+  f_z_pre:v_Self -> Type0;
+  f_z_post:v_Self -> v_Self -> Type0;
+  f_z:x0: v_Self -> Prims.Pure v_Self (f_z_pre x0) (fun result -> f_z_post x0 result)
+}
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl_FooTrait_for_Foo: t_FooTrait t_Foo =
+  {
+    f_z_pre = (fun (self: t_Foo) -> true);
+    f_z_post = (fun (self: t_Foo) (out: t_Foo) -> true);
+    f_z = fun (self: t_Foo) -> self
+  }
+
+let array (x: t_Array u8 (sz 10)) : t_Array u8 (sz 10) =
+  let x:t_Array u8 (sz 10) =
+    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize x (sz 1) (x.[ sz 2 ] <: u8)
+  in
+  x
 '''
diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap
index 01f4b474e..05c2da286 100644
--- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap	
@@ -94,41 +94,46 @@ module Naming
 open Core
 open FStar.Mul
 
-type t_Arity1 (v_T: Type0) = | Arity1 : v_T -> t_Arity1 v_T
-
-type t_B = | B : t_B
-
-let impl__B__f (self: t_B) : t_B = B <: t_B
-
-type t_C = { f_x:usize }
-
 type t_Foo =
   | Foo_A : t_Foo
   | Foo_B { f_x:usize }: t_Foo
 
-let impl__Foo__f (self: t_Foo) : t_Foo = Foo_A <: t_Foo
-
 type t_Foo2 =
   | Foo2_A : t_Foo2
   | Foo2_B { f_x:usize }: t_Foo2
 
-class t_FooTrait (v_Self: Type0) = { f_ASSOCIATED_CONSTANT:usize }
+type t_B = | B : t_B
+
+type t_C = { f_x:usize }
+
+type t_X = | X : t_X
+
+let mk_c (_: Prims.unit) : t_C =
+  let _:t_Foo = Foo_B ({ Naming.Foo.f_x = sz 3 }) <: t_Foo in
+  let _:t_X = X <: t_X in
+  { f_x = sz 3 } <: t_C
+
+let impl__Foo__f (self: t_Foo) : t_Foo = Foo_A <: t_Foo
+
+let impl__B__f (self: t_B) : t_B = B <: t_B
 
 type t_Foobar = { f_a:t_Foo }
 
-type t_StructA = { f_a:usize }
+let ff__g (_: Prims.unit) : Prims.unit = ()
 
-type t_StructB = {
-  f_a:usize;
-  f_b:usize
-}
+let ff__g__impl__g (self: t_B) : usize = sz 0
 
-type t_StructC = { f_a:usize }
+type t_f__g__impl__g__Foo =
+  | C_f__g__impl__g__Foo_A : t_f__g__impl__g__Foo
+  | C_f__g__impl__g__Foo_B { f_x:usize }: t_f__g__impl__g__Foo
 
-type t_StructD = {
-  f_a:usize;
-  f_b:usize
-}
+let ff__g__impl_1__g (self: t_Foo) : usize = sz 1
+
+let f (x: t_Foobar) : usize = ff__g__impl_1__g x.f_a
+
+let reserved_names (v_val v_noeq v_of: u8) : u8 = (v_val +! v_noeq <: u8) +! v_of
+
+type t_Arity1 (v_T: Type0) = | Arity1 : v_T -> t_Arity1 v_T
 
 class t_T1 (v_Self: Type0) = { __marker_trait_t_T1:Prims.unit }
 
@@ -149,16 +154,19 @@ class t_T3_e_for_a (v_Self: Type0) = { __marker_trait_t_T3_e_for_a:Prims.unit }
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_T3_e_e_for_a_for_Foo: t_T3_e_for_a t_Foo = { __marker_trait = () }
 
-type t_X = | X : t_X
+type t_StructA = { f_a:usize }
 
-let v_INHERENT_CONSTANT: usize = sz 3
+type t_StructB = {
+  f_a:usize;
+  f_b:usize
+}
 
-let constants
-      (#v_T: Type0)
-      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_FooTrait v_T)
-      (_: Prims.unit)
-    : usize =
-  (f_ASSOCIATED_CONSTANT #v_T #FStar.Tactics.Typeclasses.solve <: usize) +! v_INHERENT_CONSTANT
+type t_StructC = { f_a:usize }
+
+type t_StructD = {
+  f_a:usize;
+  f_b:usize
+}
 
 let construct_structs (a b: usize) : Prims.unit =
   let _:t_StructA = { f_a = a } <: t_StructA in
@@ -167,24 +175,16 @@ let construct_structs (a b: usize) : Prims.unit =
   let _:t_StructD = { f_a = a; f_b = b } <: t_StructD in
   ()
 
-let ff__g (_: Prims.unit) : Prims.unit = ()
-
-let ff__g__impl__g (self: t_B) : usize = sz 0
-
-type t_f__g__impl__g__Foo =
-  | C_f__g__impl__g__Foo_A : t_f__g__impl__g__Foo
-  | C_f__g__impl__g__Foo_B { f_x:usize }: t_f__g__impl__g__Foo
-
-let ff__g__impl_1__g (self: t_Foo) : usize = sz 1
-
-let f (x: t_Foobar) : usize = ff__g__impl_1__g x.f_a
+let v_INHERENT_CONSTANT: usize = sz 3
 
-let mk_c (_: Prims.unit) : t_C =
-  let _:t_Foo = Foo_B ({ Naming.Foo.f_x = sz 3 }) <: t_Foo in
-  let _:t_X = X <: t_X in
-  { f_x = sz 3 } <: t_C
+class t_FooTrait (v_Self: Type0) = { f_ASSOCIATED_CONSTANT:usize }
 
-let reserved_names (v_val v_noeq v_of: u8) : u8 = (v_val +! v_noeq <: u8) +! v_of
+let constants
+      (#v_T: Type0)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_FooTrait v_T)
+      (_: Prims.unit)
+    : usize =
+  (f_ASSOCIATED_CONSTANT #v_T #FStar.Tactics.Typeclasses.solve <: usize) +! v_INHERENT_CONSTANT
 
 /// From issue https://github.com/hacspec/hax/issues/839
 let string_shadows (v_string n: string) : Prims.unit = ()
diff --git a/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap b/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap
index f4b3cbfe0..470b72517 100644
--- a/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap	
@@ -42,6 +42,8 @@ Import RecordSetNotations.
 
 
 
+(* NotImplementedYet *)
+
 Inductive t_E : Type :=
 | E_A
 | E_B.
@@ -56,8 +58,6 @@ Definition t_E_cast_to_repr (x : t_E) : t_isize :=
     1
   end.
 
-(* NotImplementedYet *)
-
 Definition bar (x : t_E) : unit :=
   match x with
   | E_A
@@ -65,6 +65,17 @@ Definition bar (x : t_E) : unit :=
     tt
   end.
 
+Definition nested (x : t_Option ((t_i32))) : t_i32 :=
+  match x with
+  | Option_Some (1
+  | 2) =>
+    1
+  | Option_Some (x) =>
+    x
+  | Option_None =>
+    0
+  end.
+
 Definition deep (x : (t_i32*t_Option ((t_i32)))) : t_i32 :=
   match x with
   | (1
@@ -75,18 +86,6 @@ Definition deep (x : (t_i32*t_Option ((t_i32)))) : t_i32 :=
     x
   end.
 
-Definition deep_capture (x : t_Result (((t_i32*t_i32))) (((t_i32*t_i32)))) : t_i32 :=
-  match x with
-  | Result_Ok ((1
-  | 2,x))
-  | Result_Err ((3
-  | 4,x)) =>
-    x
-  | Result_Ok ((x,_))
-  | Result_Err ((x,_)) =>
-    x
-  end.
-
 Definition equivalent (x : (t_i32*t_Option ((t_i32)))) : t_i32 :=
   match x with
   | (1,Option_Some (3))
@@ -98,14 +97,15 @@ Definition equivalent (x : (t_i32*t_Option ((t_i32)))) : t_i32 :=
     x
   end.
 
-Definition nested (x : t_Option ((t_i32))) : t_i32 :=
+Definition deep_capture (x : t_Result (((t_i32*t_i32))) (((t_i32*t_i32)))) : t_i32 :=
   match x with
-  | Option_Some (1
-  | 2) =>
-    1
-  | Option_Some (x) =>
+  | Result_Ok ((1
+  | 2,x))
+  | Result_Err ((3
+  | 4,x)) =>
+    x
+  | Result_Ok ((x,_))
+  | Result_Err ((x,_)) =>
     x
-  | Option_None =>
-    0
   end.
 '''
diff --git a/test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap b/test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap
index 84708e9bd..24c0d8fb1 100644
--- a/test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap	
@@ -44,6 +44,12 @@ let t_E_cast_to_repr (x: t_E) : isize =
 
 let bar (x: t_E) : Prims.unit = match x <: t_E with | E_A  | E_B  -> () <: Prims.unit
 
+let nested (x: Core.Option.t_Option i32) : i32 =
+  match x <: Core.Option.t_Option i32 with
+  | Core.Option.Option_Some 1l | Core.Option.Option_Some 2l -> 1l
+  | Core.Option.Option_Some x -> x
+  | Core.Option.Option_None  -> 0l
+
 let deep (x: (i32 & Core.Option.t_Option i32)) : i32 =
   match x <: (i32 & Core.Option.t_Option i32) with
   | 1l, Core.Option.Option_Some 3l
@@ -52,14 +58,6 @@ let deep (x: (i32 & Core.Option.t_Option i32)) : i32 =
   | 2l, Core.Option.Option_Some 4l -> 0l
   | x, _ -> x
 
-let deep_capture (x: Core.Result.t_Result (i32 & i32) (i32 & i32)) : i32 =
-  match x <: Core.Result.t_Result (i32 & i32) (i32 & i32) with
-  | Core.Result.Result_Ok (1l, x)
-  | Core.Result.Result_Ok (2l, x)
-  | Core.Result.Result_Err (3l, x)
-  | Core.Result.Result_Err (4l, x) -> x
-  | Core.Result.Result_Ok (x, _) | Core.Result.Result_Err (x, _) -> x
-
 let equivalent (x: (i32 & Core.Option.t_Option i32)) : i32 =
   match x <: (i32 & Core.Option.t_Option i32) with
   | 1l, Core.Option.Option_Some 3l
@@ -68,9 +66,11 @@ let equivalent (x: (i32 & Core.Option.t_Option i32)) : i32 =
   | 2l, Core.Option.Option_Some 4l -> 0l
   | x, _ -> x
 
-let nested (x: Core.Option.t_Option i32) : i32 =
-  match x <: Core.Option.t_Option i32 with
-  | Core.Option.Option_Some 1l | Core.Option.Option_Some 2l -> 1l
-  | Core.Option.Option_Some x -> x
-  | Core.Option.Option_None  -> 0l
+let deep_capture (x: Core.Result.t_Result (i32 & i32) (i32 & i32)) : i32 =
+  match x <: Core.Result.t_Result (i32 & i32) (i32 & i32) with
+  | Core.Result.Result_Ok (1l, x)
+  | Core.Result.Result_Ok (2l, x)
+  | Core.Result.Result_Err (3l, x)
+  | Core.Result.Result_Err (4l, x) -> x
+  | Core.Result.Result_Ok (x, _) | Core.Result.Result_Err (x, _) -> x
 '''
diff --git a/test-harness/src/snapshots/toolchain__reordering into-coq.snap b/test-harness/src/snapshots/toolchain__reordering into-coq.snap
index 42cbf0bbf..9d1c84ae2 100644
--- a/test-harness/src/snapshots/toolchain__reordering into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__reordering into-coq.snap	
@@ -41,12 +41,23 @@ Import RecordSetNotations.
 
 
 
+(* NotImplementedYet *)
+
+Definition no_dependency_1_ (_ : unit) : unit :=
+  tt.
+
+Definition no_dependency_2_ (_ : unit) : unit :=
+  tt.
+
 Inductive t_Foo : Type :=
 | Foo_A
 | Foo_B.
 Arguments t_Foo:clear implicits.
 Arguments t_Foo.
 
+Definition f (_ : t_u32) : t_Foo :=
+  Foo_A.
+
 Record t_Bar : Type :=
   {
     0 : t_Foo;
@@ -57,6 +68,9 @@ Arguments Build_t_Bar.
 #[export] Instance settable_t_Bar : Settable _ :=
   settable! (@Build_t_Bar) <0>.
 
+Definition g (_ : unit) : t_Bar :=
+  Build_t_Bar (f (32)).
+
 Definition t_Foo_cast_to_repr (x : t_Foo) : t_isize :=
   match x with
   | Foo_A =>
@@ -68,18 +82,31 @@ Definition t_Foo_cast_to_repr (x : t_Foo) : t_isize :=
 (* NotImplementedYet *)
 
 (* NotImplementedYet *)
+'''
+"Reordering_Independent_cycles.v" = '''
+(* File automatically generated by Hacspec *)
+From Coq Require Import ZArith.
+Require Import List.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+Require Import Ascii.
+Require Import String.
+Require Import Coq.Floats.Floats.
+From RecordUpdate Require Import RecordSet.
+Import RecordSetNotations.
 
-Definition f (_ : t_u32) : t_Foo :=
-  Foo_A.
+Definition c (_ : unit) : unit :=
+  a (tt).
 
-Definition g (_ : unit) : t_Bar :=
-  Build_t_Bar (f (32)).
+Definition a (_ : unit) : unit :=
+  c (tt).
 
-Definition no_dependency_1_ (_ : unit) : unit :=
-  tt.
+Definition d (_ : unit) : unit :=
+  b (tt).
 
-Definition no_dependency_2_ (_ : unit) : unit :=
-  tt.
+Definition b (_ : unit) : unit :=
+  d (tt).
 '''
 "Reordering_Mut_rec.v" = '''
 (* File automatically generated by Hacspec *)
@@ -94,12 +121,12 @@ Require Import Coq.Floats.Floats.
 From RecordUpdate Require Import RecordSet.
 Import RecordSetNotations.
 
-Definition f (_ : unit) : unit :=
-  g (tt).
-
 Definition g (_ : unit) : unit :=
   f (tt).
 
+Definition f (_ : unit) : unit :=
+  g (tt).
+
 Definition ff_2_ (_ : unit) : unit :=
   f (tt).
 '''
diff --git a/test-harness/src/snapshots/toolchain__reordering into-fstar.snap b/test-harness/src/snapshots/toolchain__reordering into-fstar.snap
index d2d516b69..947e8487f 100644
--- a/test-harness/src/snapshots/toolchain__reordering into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__reordering into-fstar.snap	
@@ -26,15 +26,29 @@ exit = 0
 diagnostics = []
 
 [stdout.files]
+"Reordering.Independent_cycles.fst" = '''
+module Reordering.Independent_cycles
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let rec c (_: Prims.unit) : Prims.unit = a ()
+
+and a (_: Prims.unit) : Prims.unit = c ()
+
+let rec d (_: Prims.unit) : Prims.unit = b ()
+
+and b (_: Prims.unit) : Prims.unit = d ()
+'''
 "Reordering.Mut_rec.fst" = '''
 module Reordering.Mut_rec
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
 
-let rec f (_: Prims.unit) : Prims.unit = g ()
+let rec g (_: Prims.unit) : Prims.unit = f ()
 
-and g (_: Prims.unit) : Prims.unit = f ()
+and f (_: Prims.unit) : Prims.unit = g ()
 
 let ff_2_ (_: Prims.unit) : Prims.unit = f ()
 '''
@@ -44,22 +58,22 @@ module Reordering
 open Core
 open FStar.Mul
 
+let no_dependency_1_ (_: Prims.unit) : Prims.unit = ()
+
+let no_dependency_2_ (_: Prims.unit) : Prims.unit = ()
+
 type t_Foo =
   | Foo_A : t_Foo
   | Foo_B : t_Foo
 
+let f (_: u32) : t_Foo = Foo_A <: t_Foo
+
 type t_Bar = | Bar : t_Foo -> t_Bar
 
+let g (_: Prims.unit) : t_Bar = Bar (f 32ul) <: t_Bar
+
 let t_Foo_cast_to_repr (x: t_Foo) : isize =
   match x <: t_Foo with
   | Foo_A  -> isz 0
   | Foo_B  -> isz 1
-
-let f (_: u32) : t_Foo = Foo_A <: t_Foo
-
-let g (_: Prims.unit) : t_Bar = Bar (f 32ul) <: t_Bar
-
-let no_dependency_1_ (_: Prims.unit) : Prims.unit = ()
-
-let no_dependency_2_ (_: Prims.unit) : Prims.unit = ()
 '''
diff --git a/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap b/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap
index e0130182c..ff7d30d50 100644
--- a/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap	
+++ b/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap	
@@ -53,6 +53,18 @@ Import choice.Choice.Exports.
 
 Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.
 
+(*Not implemented yet? todo(item)*)
+
+Equations no_dependency_1_ {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  no_dependency_1_ _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Fail Next Obligation.
+
+Equations no_dependency_2_ {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  no_dependency_2_ _  :=
+    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Fail Next Obligation.
+
 Definition t_Foo : choice_type :=
   ('unit ∐ 'unit).
 Notation "'Foo_A_case'" := (inl tt) (at level 100).
@@ -66,6 +78,11 @@ Equations Foo_B {L : {fset Location}} {I : Interface} : both L I t_Foo :=
     solve_lift (ret_both (inr (tt : 'unit) : t_Foo)) : both L I t_Foo.
 Fail Next Obligation.
 
+Equations f {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 int32) : both L1 I1 t_Foo :=
+  f _  :=
+    Foo_A : both L1 I1 t_Foo.
+Fail Next Obligation.
+
 Definition t_Bar : choice_type :=
   (t_Foo).
 Equations 0 {L : {fset Location}} {I : Interface} (s : both L I t_Bar) : both L I t_Foo :=
@@ -80,6 +97,11 @@ Equations Build_t_Bar {L0 : {fset Location}} {I0 : Interface} {0 : both L0 I0 t_
 Fail Next Obligation.
 Notation "'Build_t_Bar' '[' x ']' '(' '0' ':=' y ')'" := (Build_t_Bar (0 := y)).
 
+Equations g {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 t_Bar :=
+  g _  :=
+    Bar (solve_lift (f (ret_both (32 : int32)))) : both L1 I1 t_Bar.
+Fail Next Obligation.
+
 Equations t_Foo_cast_to_repr {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 t_Foo) : both L1 I1 uint_size :=
   t_Foo_cast_to_repr x  :=
     matchb x with
@@ -93,25 +115,52 @@ Fail Next Obligation.
 (*Not implemented yet? todo(item)*)
 
 (*Not implemented yet? todo(item)*)
+'''
+"Reordering_Independent_cycles.v" = '''
+(* File automatically generated by Hacspec *)
+Set Warnings "-notation-overridden,-ambiguous-paths".
+From Crypt Require Import choice_type Package Prelude.
+Import PackageNotation.
+From extructures Require Import ord fset.
+From mathcomp Require Import word_ssrZ word.
+From Jasmin Require Import word.
 
-Equations f {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 int32) : both L1 I1 t_Foo :=
-  f _  :=
-    Foo_A : both L1 I1 t_Foo.
+From Coq Require Import ZArith.
+From Coq Require Import Strings.String.
+Import List.ListNotations.
+Open Scope list_scope.
+Open Scope Z_scope.
+Open Scope bool_scope.
+
+From Hacspec Require Import ChoiceEquality.
+From Hacspec Require Import LocationUtility.
+From Hacspec Require Import Hacspec_Lib_Comparable.
+From Hacspec Require Import Hacspec_Lib_Pre.
+From Hacspec Require Import Hacspec_Lib.
+
+Open Scope hacspec_scope.
+Import choice.Choice.Exports.
+
+Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.
+
+Equations c {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  c _  :=
+    solve_lift (a (ret_both (tt : 'unit))) : both L1 I1 'unit.
 Fail Next Obligation.
 
-Equations g {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 t_Bar :=
-  g _  :=
-    Bar (solve_lift (f (ret_both (32 : int32)))) : both L1 I1 t_Bar.
+Equations a {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  a _  :=
+    solve_lift (c (ret_both (tt : 'unit))) : both L1 I1 'unit.
 Fail Next Obligation.
 
-Equations no_dependency_1_ {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
-  no_dependency_1_ _  :=
-    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Equations d {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  d _  :=
+    solve_lift (b (ret_both (tt : 'unit))) : both L1 I1 'unit.
 Fail Next Obligation.
 
-Equations no_dependency_2_ {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
-  no_dependency_2_ _  :=
-    solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit.
+Equations b {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  b _  :=
+    solve_lift (d (ret_both (tt : 'unit))) : both L1 I1 'unit.
 Fail Next Obligation.
 '''
 "Reordering_Mut_rec.v" = '''
@@ -141,16 +190,16 @@ Import choice.Choice.Exports.
 
 Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.
 
-Equations f {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
-  f _  :=
-    solve_lift (g (ret_both (tt : 'unit))) : both L1 I1 'unit.
-Fail Next Obligation.
-
 Equations g {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
   g _  :=
     solve_lift (f (ret_both (tt : 'unit))) : both L1 I1 'unit.
 Fail Next Obligation.
 
+Equations f {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
+  f _  :=
+    solve_lift (g (ret_both (tt : 'unit))) : both L1 I1 'unit.
+Fail Next Obligation.
+
 Equations ff_2_ {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit :=
   ff_2_ _  :=
     solve_lift (f (ret_both (tt : 'unit))) : both L1 I1 'unit.
diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
index 14648c368..568e84317 100644
--- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap	
@@ -72,8 +72,8 @@ let test (x y: Core.Option.t_Option i32) : Core.Option.t_Option i32 =
       (fun i ->
           let i:i32 = i in
           match y <: Core.Option.t_Option i32 with
-          | Core.Option.Option_Some hoist1 ->
-            Core.Option.Option_Some (i +! hoist1 <: i32) <: Core.Option.t_Option i32
+          | Core.Option.Option_Some hoist38 ->
+            Core.Option.Option_Some (i +! hoist38 <: i32) <: Core.Option.t_Option i32
           | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option i32)
     <:
     Core.Option.t_Option (Core.Option.t_Option i32)
@@ -97,8 +97,8 @@ let v_fun (rng: i8) : (i8 & Core.Result.t_Result Prims.unit Prims.unit) =
   let tmp0, out:(i8 & Core.Result.t_Result Prims.unit Prims.unit) = other_fun rng in
   let rng:i8 = tmp0 in
   match out <: Core.Result.t_Result Prims.unit Prims.unit with
-  | Core.Result.Result_Ok hoist6 ->
-    rng, (Core.Result.Result_Ok hoist6 <: Core.Result.t_Result Prims.unit Prims.unit)
+  | Core.Result.Result_Ok hoist43 ->
+    rng, (Core.Result.Result_Ok hoist43 <: Core.Result.t_Result Prims.unit Prims.unit)
     <:
     (i8 & Core.Result.t_Result Prims.unit Prims.unit)
   | Core.Result.Result_Err err ->
@@ -112,150 +112,10 @@ module Side_effects
 open Core
 open FStar.Mul
 
-type t_A = | A : t_A
-
-type t_B = | B : t_B
-
-type t_Bar = {
-  f_a:bool;
-  f_b:(t_Array (bool & bool) (sz 6) & bool)
-}
-
-type t_Foo = {
-  f_x:bool;
-  f_y:(bool & Alloc.Vec.t_Vec t_Bar Alloc.Alloc.t_Global);
-  f_z:t_Array t_Bar (sz 6);
-  f_bar:t_Bar
-}
-
 /// Helper function
 let add3 (x y z: u32) : u32 =
   Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add x y <: u32) z
 
-/// Test assignation on non-trivial places
-let assign_non_trivial_lhs (foo: t_Foo) : t_Foo =
-  let foo:t_Foo = { foo with f_x = true } <: t_Foo in
-  let foo:t_Foo = { foo with f_bar = { foo.f_bar with f_a = true } <: t_Bar } <: t_Foo in
-  let foo:t_Foo =
-    {
-      foo with
-      f_bar
-      =
-      {
-        foo.f_bar with
-        f_b
-        =
-        {
-          foo.f_bar.f_b with
-          _1
-          =
-          Rust_primitives.Hax.Monomorphized_update_at.update_at_usize foo.f_bar.f_b._1
-            (sz 3)
-            ({ (foo.f_bar.f_b._1.[ sz 3 ] <: (bool & bool)) with _2 = true } <: (bool & bool))
-        }
-        <:
-        (t_Array (bool & bool) (sz 6) & bool)
-      }
-      <:
-      t_Bar
-    }
-    <:
-    t_Foo
-  in
-  let foo:t_Foo =
-    {
-      foo with
-      f_z
-      =
-      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize foo.f_z
-        (sz 3)
-        ({ (foo.f_z.[ sz 3 ] <: t_Bar) with f_a = true } <: t_Bar)
-    }
-    <:
-    t_Foo
-  in
-  let foo:t_Foo =
-    {
-      foo with
-      f_y
-      =
-      {
-        foo.f_y with
-        _2
-        =
-        Rust_primitives.Hax.Monomorphized_update_at.update_at_usize foo.f_y._2
-          (sz 3)
-          ({
-              (foo.f_y._2.[ sz 3 ] <: t_Bar) with
-              f_b
-              =
-              {
-                (foo.f_y._2.[ sz 3 ] <: t_Bar).f_b with
-                _1
-                =
-                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize (foo.f_y._2.[ sz 3 ]
-                    <:
-                    t_Bar)
-                    .f_b
-                    ._1
-                  (sz 5)
-                  ({
-                      ((foo.f_y._2.[ sz 3 ] <: t_Bar).f_b._1.[ sz 5 ] <: (bool & bool)) with
-                      _1 = true
-                    }
-                    <:
-                    (bool & bool))
-                <:
-                t_Array (bool & bool) (sz 6)
-              }
-              <:
-              (t_Array (bool & bool) (sz 6) & bool)
-            }
-            <:
-            t_Bar)
-      }
-      <:
-      (bool & Alloc.Vec.t_Vec t_Bar Alloc.Alloc.t_Global)
-    }
-    <:
-    t_Foo
-  in
-  foo
-
-/// Question mark without error coercion
-let direct_result_question_mark (y: Core.Result.t_Result Prims.unit u32)
-    : Core.Result.t_Result i8 u32 =
-  match y <: Core.Result.t_Result Prims.unit u32 with
-  | Core.Result.Result_Ok _ -> Core.Result.Result_Ok 0y <: Core.Result.t_Result i8 u32
-  | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result i8 u32
-
-/// Question mark with an error coercion
-let direct_result_question_mark_coercion (y: Core.Result.t_Result i8 u16)
-    : Core.Result.t_Result i8 u32 =
-  match y <: Core.Result.t_Result i8 u16 with
-  | Core.Result.Result_Ok hoist10 -> Core.Result.Result_Ok hoist10 <: Core.Result.t_Result i8 u32
-  | Core.Result.Result_Err err ->
-    Core.Result.Result_Err (Core.Convert.f_from #u32 #u16 #FStar.Tactics.Typeclasses.solve err)
-    <:
-    Core.Result.t_Result i8 u32
-
-/// Exercise early returns with control flow and loops
-let early_returns (x: u32) : u32 =
-  if x >. 3ul
-  then 0ul
-  else
-    if x >. 30ul
-    then
-      match true <: bool with
-      | true -> 34ul
-      | _ ->
-        let x, hoist14:(u32 & u32) = x, 3ul <: (u32 & u32) in
-        Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist14 <: u32) x
-    else
-      let x:u32 = x +! 9ul in
-      let x, hoist14:(u32 & u32) = x, x +! 1ul <: (u32 & u32) in
-      Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist14 <: u32) x
-
 /// Exercise local mutation with control flow and loops
 let local_mutation (x: u32) : u32 =
   let y:u32 = 0ul in
@@ -282,7 +142,7 @@ let local_mutation (x: u32) : u32 =
     in
     Core.Num.impl__u32__wrapping_add x y
   else
-    let (x, y), hoist24:((u32 & u32) & u32) =
+    let (x, y), hoist7:((u32 & u32) & u32) =
       match x <: u32 with
       | 12ul ->
         let y:u32 = Core.Num.impl__u32__wrapping_add x y in
@@ -294,47 +154,97 @@ let local_mutation (x: u32) : u32 =
         ((u32 & u32) & u32)
       | _ -> (x, y <: (u32 & u32)), 0ul <: ((u32 & u32) & u32)
     in
-    let x:u32 = hoist24 in
+    let x:u32 = hoist7 in
     Core.Num.impl__u32__wrapping_add x y
 
-/// Combine `?` and early return
-let monad_lifting (x: u8) : Core.Result.t_Result t_A t_B =
-  if x >. 123uy
+/// Exercise early returns with control flow and loops
+let early_returns (x: u32) : u32 =
+  if x >. 3ul
+  then 0ul
+  else
+    if x >. 30ul
+    then
+      match true <: bool with
+      | true -> 34ul
+      | _ ->
+        let x, hoist11:(u32 & u32) = x, 3ul <: (u32 & u32) in
+        Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist11 <: u32) x
+    else
+      let x:u32 = x +! 9ul in
+      let x, hoist11:(u32 & u32) = x, x +! 1ul <: (u32 & u32) in
+      Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist11 <: u32) x
+
+let simplifiable_return (c1 c2 c3: bool) : i32 =
+  let x:i32 = 0l in
+  if c1
   then
-    match Core.Result.Result_Err (B <: t_B) <: Core.Result.t_Result t_A t_B with
-    | Core.Result.Result_Ok hoist25 -> Core.Result.Result_Ok hoist25 <: Core.Result.t_Result t_A t_B
-    | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result t_A t_B
-  else Core.Result.Result_Ok (A <: t_A) <: Core.Result.t_Result t_A t_B
+    if c2
+    then
+      let x:i32 = x +! 10l in
+      if c3 then 1l else x +! 1l
+    else x +! 1l
+  else x
+
+let simplifiable_question_mark (c: bool) (x: Core.Option.t_Option i32) : Core.Option.t_Option i32 =
+  if c
+  then
+    match x <: Core.Option.t_Option i32 with
+    | Core.Option.Option_Some hoist16 ->
+      let a:i32 = hoist16 +! 10l in
+      let b:i32 = 20l in
+      Core.Option.Option_Some (a +! b) <: Core.Option.t_Option i32
+    | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option i32
+  else
+    let a:i32 = 0l in
+    let b:i32 = 20l in
+    Core.Option.Option_Some (a +! b) <: Core.Option.t_Option i32
+
+/// Question mark without error coercion
+let direct_result_question_mark (y: Core.Result.t_Result Prims.unit u32)
+    : Core.Result.t_Result i8 u32 =
+  match y <: Core.Result.t_Result Prims.unit u32 with
+  | Core.Result.Result_Ok _ -> Core.Result.Result_Ok 0y <: Core.Result.t_Result i8 u32
+  | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result i8 u32
+
+/// Question mark with an error coercion
+let direct_result_question_mark_coercion (y: Core.Result.t_Result i8 u16)
+    : Core.Result.t_Result i8 u32 =
+  match y <: Core.Result.t_Result i8 u16 with
+  | Core.Result.Result_Ok hoist17 -> Core.Result.Result_Ok hoist17 <: Core.Result.t_Result i8 u32
+  | Core.Result.Result_Err err ->
+    Core.Result.Result_Err (Core.Convert.f_from #u32 #u16 #FStar.Tactics.Typeclasses.solve err)
+    <:
+    Core.Result.t_Result i8 u32
 
 /// Test question mark on `Option`s with some control flow
 let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.Option.t_Option u8 =
   match x <: Core.Option.t_Option u8 with
-  | Core.Option.Option_Some hoist31 ->
-    if hoist31 >. 10uy
+  | Core.Option.Option_Some hoist21 ->
+    if hoist21 >. 10uy
     then
       match x <: Core.Option.t_Option u8 with
-      | Core.Option.Option_Some hoist33 ->
+      | Core.Option.Option_Some hoist23 ->
         (match
-            Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist33 3uy)
+            Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist23 3uy)
             <:
             Core.Option.t_Option u8
           with
-          | Core.Option.Option_Some hoist39 ->
-            (match hoist39 <: u8 with
+          | Core.Option.Option_Some hoist29 ->
+            (match hoist29 <: u8 with
               | 3uy ->
                 (match Core.Option.Option_None <: Core.Option.t_Option u8 with
                   | Core.Option.Option_Some some ->
                     let v:u8 = some in
                     (match x <: Core.Option.t_Option u8 with
-                      | Core.Option.Option_Some hoist40 ->
+                      | Core.Option.Option_Some hoist30 ->
                         (match y <: Core.Option.t_Option u8 with
-                          | Core.Option.Option_Some hoist41 ->
+                          | Core.Option.Option_Some hoist31 ->
                             Core.Option.Option_Some
                             (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
-                                    hoist40
+                                    hoist30
                                   <:
                                   u8)
-                                hoist41)
+                                hoist31)
                             <:
                             Core.Option.t_Option u8
                           | Core.Option.Option_None  ->
@@ -344,18 +254,18 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
                   | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option u8)
               | 4uy ->
                 (match z <: Core.Option.t_Option u64 with
-                  | Core.Option.Option_Some hoist28 ->
-                    let v:u8 = 4uy +! (if hoist28 >. 4uL <: bool then 0uy else 3uy) in
+                  | Core.Option.Option_Some hoist18 ->
+                    let v:u8 = 4uy +! (if hoist18 >. 4uL <: bool then 0uy else 3uy) in
                     (match x <: Core.Option.t_Option u8 with
-                      | Core.Option.Option_Some hoist40 ->
+                      | Core.Option.Option_Some hoist30 ->
                         (match y <: Core.Option.t_Option u8 with
-                          | Core.Option.Option_Some hoist41 ->
+                          | Core.Option.Option_Some hoist31 ->
                             Core.Option.Option_Some
                             (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
-                                    hoist40
+                                    hoist30
                                   <:
                                   u8)
-                                hoist41)
+                                hoist31)
                             <:
                             Core.Option.t_Option u8
                           | Core.Option.Option_None  ->
@@ -366,14 +276,14 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
               | _ ->
                 let v:u8 = 12uy in
                 match x <: Core.Option.t_Option u8 with
-                | Core.Option.Option_Some hoist40 ->
+                | Core.Option.Option_Some hoist30 ->
                   (match y <: Core.Option.t_Option u8 with
-                    | Core.Option.Option_Some hoist41 ->
+                    | Core.Option.Option_Some hoist31 ->
                       Core.Option.Option_Some
-                      (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v hoist40
+                      (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v hoist30
                             <:
                             u8)
-                          hoist41)
+                          hoist31)
                       <:
                       Core.Option.t_Option u8
                     | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option u8
@@ -383,30 +293,30 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
       | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option u8
     else
       (match x <: Core.Option.t_Option u8 with
-        | Core.Option.Option_Some hoist36 ->
+        | Core.Option.Option_Some hoist26 ->
           (match y <: Core.Option.t_Option u8 with
-            | Core.Option.Option_Some hoist35 ->
+            | Core.Option.Option_Some hoist25 ->
               (match
-                  Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist36 hoist35)
+                  Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist26 hoist25)
                   <:
                   Core.Option.t_Option u8
                 with
-                | Core.Option.Option_Some hoist39 ->
-                  (match hoist39 <: u8 with
+                | Core.Option.Option_Some hoist29 ->
+                  (match hoist29 <: u8 with
                     | 3uy ->
                       (match Core.Option.Option_None <: Core.Option.t_Option u8 with
                         | Core.Option.Option_Some some ->
                           let v:u8 = some in
                           (match x <: Core.Option.t_Option u8 with
-                            | Core.Option.Option_Some hoist40 ->
+                            | Core.Option.Option_Some hoist30 ->
                               (match y <: Core.Option.t_Option u8 with
-                                | Core.Option.Option_Some hoist41 ->
+                                | Core.Option.Option_Some hoist31 ->
                                   Core.Option.Option_Some
                                   (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
-                                          hoist40
+                                          hoist30
                                         <:
                                         u8)
-                                      hoist41)
+                                      hoist31)
                                   <:
                                   Core.Option.t_Option u8
                                 | Core.Option.Option_None  ->
@@ -417,18 +327,18 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
                           Core.Option.Option_None <: Core.Option.t_Option u8)
                     | 4uy ->
                       (match z <: Core.Option.t_Option u64 with
-                        | Core.Option.Option_Some hoist28 ->
-                          let v:u8 = 4uy +! (if hoist28 >. 4uL <: bool then 0uy else 3uy) in
+                        | Core.Option.Option_Some hoist18 ->
+                          let v:u8 = 4uy +! (if hoist18 >. 4uL <: bool then 0uy else 3uy) in
                           (match x <: Core.Option.t_Option u8 with
-                            | Core.Option.Option_Some hoist40 ->
+                            | Core.Option.Option_Some hoist30 ->
                               (match y <: Core.Option.t_Option u8 with
-                                | Core.Option.Option_Some hoist41 ->
+                                | Core.Option.Option_Some hoist31 ->
                                   Core.Option.Option_Some
                                   (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
-                                          hoist40
+                                          hoist30
                                         <:
                                         u8)
-                                      hoist41)
+                                      hoist31)
                                   <:
                                   Core.Option.t_Option u8
                                 | Core.Option.Option_None  ->
@@ -440,15 +350,15 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
                     | _ ->
                       let v:u8 = 12uy in
                       match x <: Core.Option.t_Option u8 with
-                      | Core.Option.Option_Some hoist40 ->
+                      | Core.Option.Option_Some hoist30 ->
                         (match y <: Core.Option.t_Option u8 with
-                          | Core.Option.Option_Some hoist41 ->
+                          | Core.Option.Option_Some hoist31 ->
                             Core.Option.Option_Some
                             (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
-                                    hoist40
+                                    hoist30
                                   <:
                                   u8)
-                                hoist41)
+                                hoist31)
                             <:
                             Core.Option.t_Option u8
                           | Core.Option.Option_None  ->
@@ -484,28 +394,118 @@ let question_mark (x: u32) : Core.Result.t_Result u32 u32 =
   else
     Core.Result.Result_Ok (Core.Num.impl__u32__wrapping_add 3ul x) <: Core.Result.t_Result u32 u32
 
-let simplifiable_question_mark (c: bool) (x: Core.Option.t_Option i32) : Core.Option.t_Option i32 =
-  if c
-  then
-    match x <: Core.Option.t_Option i32 with
-    | Core.Option.Option_Some hoist45 ->
-      let a:i32 = hoist45 +! 10l in
-      let b:i32 = 20l in
-      Core.Option.Option_Some (a +! b) <: Core.Option.t_Option i32
-    | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option i32
-  else
-    let a:i32 = 0l in
-    let b:i32 = 20l in
-    Core.Option.Option_Some (a +! b) <: Core.Option.t_Option i32
+type t_A = | A : t_A
 
-let simplifiable_return (c1 c2 c3: bool) : i32 =
-  let x:i32 = 0l in
-  if c1
+type t_B = | B : t_B
+
+/// Combine `?` and early return
+let monad_lifting (x: u8) : Core.Result.t_Result t_A t_B =
+  if x >. 123uy
   then
-    if c2
-    then
-      let x:i32 = x +! 10l in
-      if c3 then 1l else x +! 1l
-    else x +! 1l
-  else x
+    match Core.Result.Result_Err (B <: t_B) <: Core.Result.t_Result t_A t_B with
+    | Core.Result.Result_Ok hoist35 -> Core.Result.Result_Ok hoist35 <: Core.Result.t_Result t_A t_B
+    | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result t_A t_B
+  else Core.Result.Result_Ok (A <: t_A) <: Core.Result.t_Result t_A t_B
+
+type t_Bar = {
+  f_a:bool;
+  f_b:(t_Array (bool & bool) (sz 6) & bool)
+}
+
+type t_Foo = {
+  f_x:bool;
+  f_y:(bool & Alloc.Vec.t_Vec t_Bar Alloc.Alloc.t_Global);
+  f_z:t_Array t_Bar (sz 6);
+  f_bar:t_Bar
+}
+
+/// Test assignation on non-trivial places
+let assign_non_trivial_lhs (foo: t_Foo) : t_Foo =
+  let foo:t_Foo = { foo with f_x = true } <: t_Foo in
+  let foo:t_Foo = { foo with f_bar = { foo.f_bar with f_a = true } <: t_Bar } <: t_Foo in
+  let foo:t_Foo =
+    {
+      foo with
+      f_bar
+      =
+      {
+        foo.f_bar with
+        f_b
+        =
+        {
+          foo.f_bar.f_b with
+          _1
+          =
+          Rust_primitives.Hax.Monomorphized_update_at.update_at_usize foo.f_bar.f_b._1
+            (sz 3)
+            ({ (foo.f_bar.f_b._1.[ sz 3 ] <: (bool & bool)) with _2 = true } <: (bool & bool))
+        }
+        <:
+        (t_Array (bool & bool) (sz 6) & bool)
+      }
+      <:
+      t_Bar
+    }
+    <:
+    t_Foo
+  in
+  let foo:t_Foo =
+    {
+      foo with
+      f_z
+      =
+      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize foo.f_z
+        (sz 3)
+        ({ (foo.f_z.[ sz 3 ] <: t_Bar) with f_a = true } <: t_Bar)
+    }
+    <:
+    t_Foo
+  in
+  let foo:t_Foo =
+    {
+      foo with
+      f_y
+      =
+      {
+        foo.f_y with
+        _2
+        =
+        Rust_primitives.Hax.Monomorphized_update_at.update_at_usize foo.f_y._2
+          (sz 3)
+          ({
+              (foo.f_y._2.[ sz 3 ] <: t_Bar) with
+              f_b
+              =
+              {
+                (foo.f_y._2.[ sz 3 ] <: t_Bar).f_b with
+                _1
+                =
+                Rust_primitives.Hax.Monomorphized_update_at.update_at_usize (foo.f_y._2.[ sz 3 ]
+                    <:
+                    t_Bar)
+                    .f_b
+                    ._1
+                  (sz 5)
+                  ({
+                      ((foo.f_y._2.[ sz 3 ] <: t_Bar).f_b._1.[ sz 5 ] <: (bool & bool)) with
+                      _1 = true
+                    }
+                    <:
+                    (bool & bool))
+                <:
+                t_Array (bool & bool) (sz 6)
+              }
+              <:
+              (t_Array (bool & bool) (sz 6) & bool)
+            }
+            <:
+            t_Bar)
+      }
+      <:
+      (bool & Alloc.Vec.t_Vec t_Bar Alloc.Alloc.t_Global)
+    }
+    <:
+    t_Foo
+  in
+  foo
 '''
diff --git a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap
index a3aebbf34..766cd6165 100644
--- a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap	
+++ b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap	
@@ -54,6 +54,163 @@ Import choice.Choice.Exports.
 
 Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.
 
+(*Not implemented yet? todo(item)*)
+
+Equations add3 {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 int32) (y : both L2 I2 int32) (z : both L3 I3 int32) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32 :=
+  add3 x y z  :=
+    solve_lift (impl__u32__wrapping_add (impl__u32__wrapping_add x y) z) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32.
+Fail Next Obligation.
+
+Definition y_loc : Location :=
+  (int32;0%nat).
+Definition y_loc : Location :=
+  (int32;1%nat).
+Equations local_mutation {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both (L1 :|: fset [y_loc;y_loc]) I1 int32 :=
+  local_mutation x  :=
+    letb y loc(y_loc) := ret_both (0 : int32) in
+    letb _ := assign todo(term) in
+    letb hoist1 := x >.? (ret_both (3 : int32)) in
+    solve_lift (ifb hoist1
+    then letb _ := assign todo(term) in
+    letb y loc(y_loc) := x ./ (ret_both (2 : int32)) in
+    letb _ := assign todo(term) in
+    letb hoist2 := ret_both (0 : int32) in
+    letb hoist3 := Build_t_Range (f_start := hoist2) (f_end := ret_both (10 : int32)) in
+    letb hoist4 := f_into_iter hoist3 in
+    letb _ := foldi_both_list hoist4 (fun i =>
+      ssp (fun _ =>
+        assign todo(term) : (both (*0*)(L1:|:fset []) (I1) 'unit))) (ret_both (tt : 'unit)) in
+    impl__u32__wrapping_add x y
+    else letb hoist7 := matchb x with
+    | 12 =>
+      letb _ := assign todo(term) in
+      solve_lift (ret_both (3 : int32))
+    | 13 =>
+      letb hoist6 := x in
+      letb _ := assign todo(term) in
+      letb hoist5 := impl__u32__wrapping_add (ret_both (123 : int32)) x in
+      solve_lift (add3 hoist6 hoist5 x)
+    | _ =>
+      solve_lift (ret_both (0 : int32))
+    end in
+    letb _ := assign todo(term) in
+    impl__u32__wrapping_add x y) : both (L1 :|: fset [y_loc;y_loc]) I1 int32.
+Fail Next Obligation.
+
+Equations early_returns {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 int32 :=
+  early_returns x  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (3 : int32))
+    then letm[choice_typeMonad.result_bind_code int32] hoist8 := ControlFlow_Break (ret_both (0 : int32)) in
+    ControlFlow_Continue (never_to_any hoist8)
+    else () in
+    letb hoist9 := x >.? (ret_both (30 : int32)) in
+    letm[choice_typeMonad.result_bind_code int32] hoist11 := ifb hoist9
+    then matchb ret_both (true : 'bool) with
+    | true =>
+      letm[choice_typeMonad.result_bind_code int32] hoist10 := ControlFlow_Break (ret_both (34 : int32)) in
+      ControlFlow_Continue (solve_lift (never_to_any hoist10))
+    | _ =>
+      ControlFlow_Continue (solve_lift (ret_both (3 : int32)))
+    end
+    else ControlFlow_Continue (letb _ := assign todo(term) in
+    x .+ (ret_both (1 : int32))) in
+    letb hoist12 := impl__u32__wrapping_add (ret_both (123 : int32)) hoist11 in
+    letb hoist13 := impl__u32__wrapping_add hoist12 x in
+    letm[choice_typeMonad.result_bind_code int32] hoist14 := ControlFlow_Break hoist13 in
+    ControlFlow_Continue (never_to_any hoist14))) : both L1 I1 int32.
+Fail Next Obligation.
+
+Definition x_loc : Location :=
+  (int32;2%nat).
+Equations simplifiable_return {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (c1 : both L1 I1 'bool) (c2 : both L2 I2 'bool) (c3 : both L3 I3 'bool) : both (L1 :|: L2 :|: L3 :|: fset [x_loc]) (I1 :|: I2 :|: I3) int32 :=
+  simplifiable_return c1 c2 c3  :=
+    solve_lift (run (letb x loc(x_loc) := ret_both (0 : int32) in
+    letm[choice_typeMonad.result_bind_code int32] _ := ifb c1
+    then letm[choice_typeMonad.result_bind_code int32] _ := ifb c2
+    then letb _ := assign todo(term) in
+    ifb c3
+    then letm[choice_typeMonad.result_bind_code int32] hoist15 := ControlFlow_Break (ret_both (1 : int32)) in
+    ControlFlow_Continue (never_to_any hoist15)
+    else ()
+    else () in
+    ControlFlow_Continue (letb _ := assign todo(term) in
+    ret_both (tt : 'unit))
+    else () in
+    ControlFlow_Continue x)) : both (L1 :|: L2 :|: L3 :|: fset [x_loc]) (I1 :|: I2 :|: I3) int32.
+Fail Next Obligation.
+
+Equations simplifiable_question_mark {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (c : both L1 I1 'bool) (x : both L2 I2 (t_Option int32)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32) :=
+  simplifiable_question_mark c x  :=
+    solve_lift (run (letm[choice_typeMonad.option_bind_code] a := ifb c
+    then letm[choice_typeMonad.option_bind_code] hoist16 := x in
+    Option_Some (hoist16 .+ (ret_both (10 : int32)))
+    else Option_Some (ret_both (0 : int32)) in
+    Option_Some (letb b := ret_both (20 : int32) in
+    Option_Some (a .+ b)))) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32).
+Fail Next Obligation.
+
+Equations direct_result_question_mark {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result 'unit int32)) : both L1 I1 (t_Result int8 int32) :=
+  direct_result_question_mark y  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := y in
+    Result_Ok (Result_Ok (ret_both (0 : int8))))) : both L1 I1 (t_Result int8 int32).
+Fail Next Obligation.
+
+Equations direct_result_question_mark_coercion {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result int8 int16)) : both L1 I1 (t_Result int8 int32) :=
+  direct_result_question_mark_coercion y  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist17 := impl__map_err y f_from in
+    Result_Ok (Result_Ok hoist17))) : both L1 I1 (t_Result int8 int32).
+Fail Next Obligation.
+
+Equations options {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 (t_Option int8)) (y : both L2 I2 (t_Option int8)) (z : both L3 I3 (t_Option int64)) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8) :=
+  options x y z  :=
+    solve_lift (run (letm[choice_typeMonad.option_bind_code] hoist21 := x in
+    letb hoist22 := hoist21 >.? (ret_both (10 : int8)) in
+    letm[choice_typeMonad.option_bind_code] hoist28 := ifb hoist22
+    then letm[choice_typeMonad.option_bind_code] hoist23 := x in
+    Option_Some (letb hoist24 := impl__u8__wrapping_add hoist23 (ret_both (3 : int8)) in
+    Option_Some hoist24)
+    else letm[choice_typeMonad.option_bind_code] hoist26 := x in
+    letm[choice_typeMonad.option_bind_code] hoist25 := y in
+    Option_Some (letb hoist27 := impl__u8__wrapping_add hoist26 hoist25 in
+    Option_Some hoist27) in
+    letm[choice_typeMonad.option_bind_code] hoist29 := hoist28 in
+    letm[choice_typeMonad.option_bind_code] v := matchb hoist29 with
+    | 3 =>
+      Option_None
+    | 4 =>
+      letm[choice_typeMonad.option_bind_code] hoist18 := z in
+      Option_Some (letb hoist19 := hoist18 >.? (ret_both (4 : int64)) in
+      letb hoist20 := ifb hoist19
+      then ret_both (0 : int8)
+      else ret_both (3 : int8) in
+      solve_lift ((ret_both (4 : int8)) .+ hoist20))
+    | _ =>
+      Option_Some (solve_lift (ret_both (12 : int8)))
+    end in
+    letm[choice_typeMonad.option_bind_code] hoist30 := x in
+    letb hoist32 := impl__u8__wrapping_add v hoist30 in
+    letm[choice_typeMonad.option_bind_code] hoist31 := y in
+    Option_Some (letb hoist33 := impl__u8__wrapping_add hoist32 hoist31 in
+    Option_Some hoist33))) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8).
+Fail Next Obligation.
+
+Definition y_loc : Location :=
+  (int32;3%nat).
+Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both (L1 :|: fset [y_loc]) I1 (t_Result int32 int32) :=
+  question_mark x  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (40 : int32))
+    then letb y loc(y_loc) := ret_both (0 : int32) in
+    letb _ := assign todo(term) in
+    letb _ := assign todo(term) in
+    letb _ := assign todo(term) in
+    letb hoist34 := x >.? (ret_both (90 : int32)) in
+    ifb hoist34
+    then impl__map_err (Result_Err (ret_both (12 : int8))) f_from
+    else ()
+    else () in
+    Result_Ok (Result_Ok (impl__u32__wrapping_add (ret_both (3 : int32)) x)))) : both (L1 :|: fset [y_loc]) I1 (t_Result int32 int32).
+Fail Next Obligation.
+
 Definition t_A : choice_type :=
   'unit.
 Equations Build_t_A : both (fset []) (fset []) (t_A) :=
@@ -68,6 +225,16 @@ Equations Build_t_B : both (fset []) (fset []) (t_B) :=
     solve_lift (ret_both (tt (* Empty tuple *) : (t_B))) : both (fset []) (fset []) (t_B).
 Fail Next Obligation.
 
+Equations monad_lifting {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result t_A t_B) :=
+  monad_lifting x  :=
+    solve_lift (run (ifb x >.? (ret_both (123 : int8))
+    then letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist35 := ControlFlow_Continue (Result_Err B) in
+    letb hoist36 := Result_Ok hoist35 in
+    letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist37 := ControlFlow_Break hoist36 in
+    ControlFlow_Continue (never_to_any hoist37)
+    else ControlFlow_Continue (Result_Ok A))) : both L1 I1 (t_Result t_A t_B).
+Fail Next Obligation.
+
 Definition t_Bar : choice_type :=
   ('bool × nseq ('bool × 'bool) 6 × 'bool).
 Equations f_a {L : {fset Location}} {I : Interface} (s : both L I t_Bar) : both L I 'bool :=
@@ -124,19 +291,6 @@ Notation "'Build_t_Foo' '[' x ']' '(' 'f_y' ':=' y ')'" := (Build_t_Foo (f_x :=
 Notation "'Build_t_Foo' '[' x ']' '(' 'f_z' ':=' y ')'" := (Build_t_Foo (f_x := f_x x) (f_y := f_y x) (f_z := y) (f_bar := f_bar x)).
 Notation "'Build_t_Foo' '[' x ']' '(' 'f_bar' ':=' y ')'" := (Build_t_Foo (f_x := f_x x) (f_y := f_y x) (f_z := f_z x) (f_bar := y)).
 
-(*Not implemented yet? todo(item)*)
-
-(*Not implemented yet? todo(item)*)
-
-(*Not implemented yet? todo(item)*)
-
-(*Not implemented yet? todo(item)*)
-
-Equations add3 {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 int32) (y : both L2 I2 int32) (z : both L3 I3 int32) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32 :=
-  add3 x y z  :=
-    solve_lift (impl__u32__wrapping_add (impl__u32__wrapping_add x y) z) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32.
-Fail Next Obligation.
-
 Equations assign_non_trivial_lhs {L1 : {fset Location}} {I1 : Interface} (foo : both L1 I1 t_Foo) : both L1 I1 t_Foo :=
   assign_non_trivial_lhs foo  :=
     letb _ := assign todo(term) in
@@ -147,165 +301,11 @@ Equations assign_non_trivial_lhs {L1 : {fset Location}} {I1 : Interface} (foo :
     solve_lift foo : both L1 I1 t_Foo.
 Fail Next Obligation.
 
-Equations direct_result_question_mark {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result 'unit int32)) : both L1 I1 (t_Result int8 int32) :=
-  direct_result_question_mark y  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := y in
-    Result_Ok (Result_Ok (ret_both (0 : int8))))) : both L1 I1 (t_Result int8 int32).
-Fail Next Obligation.
-
-Equations direct_result_question_mark_coercion {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result int8 int16)) : both L1 I1 (t_Result int8 int32) :=
-  direct_result_question_mark_coercion y  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist12 := impl__map_err y f_from in
-    Result_Ok (Result_Ok hoist12))) : both L1 I1 (t_Result int8 int32).
-Fail Next Obligation.
-
-Equations early_returns {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 int32 :=
-  early_returns x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (3 : int32))
-    then letm[choice_typeMonad.result_bind_code int32] hoist13 := ControlFlow_Break (ret_both (0 : int32)) in
-    ControlFlow_Continue (never_to_any hoist13)
-    else () in
-    letb hoist14 := x >.? (ret_both (30 : int32)) in
-    letm[choice_typeMonad.result_bind_code int32] hoist16 := ifb hoist14
-    then matchb ret_both (true : 'bool) with
-    | true =>
-      letm[choice_typeMonad.result_bind_code int32] hoist15 := ControlFlow_Break (ret_both (34 : int32)) in
-      ControlFlow_Continue (solve_lift (never_to_any hoist15))
-    | _ =>
-      ControlFlow_Continue (solve_lift (ret_both (3 : int32)))
-    end
-    else ControlFlow_Continue (letb _ := assign todo(term) in
-    x .+ (ret_both (1 : int32))) in
-    letb hoist17 := impl__u32__wrapping_add (ret_both (123 : int32)) hoist16 in
-    letb hoist18 := impl__u32__wrapping_add hoist17 x in
-    letm[choice_typeMonad.result_bind_code int32] hoist19 := ControlFlow_Break hoist18 in
-    ControlFlow_Continue (never_to_any hoist19))) : both L1 I1 int32.
-Fail Next Obligation.
-
-Definition y_loc : Location :=
-  (int32;0%nat).
-Definition y_loc : Location :=
-  (int32;1%nat).
-Equations local_mutation {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both (L1 :|: fset [y_loc;y_loc]) I1 int32 :=
-  local_mutation x  :=
-    letb y loc(y_loc) := ret_both (0 : int32) in
-    letb _ := assign todo(term) in
-    letb hoist20 := x >.? (ret_both (3 : int32)) in
-    solve_lift (ifb hoist20
-    then letb _ := assign todo(term) in
-    letb y loc(y_loc) := x ./ (ret_both (2 : int32)) in
-    letb _ := assign todo(term) in
-    letb hoist21 := ret_both (0 : int32) in
-    letb hoist22 := Build_t_Range (f_start := hoist21) (f_end := ret_both (10 : int32)) in
-    letb hoist23 := f_into_iter hoist22 in
-    letb _ := foldi_both_list hoist23 (fun i =>
-      ssp (fun _ =>
-        assign todo(term) : (both (*0*)(L1:|:fset []) (I1) 'unit))) (ret_both (tt : 'unit)) in
-    impl__u32__wrapping_add x y
-    else letb hoist26 := matchb x with
-    | 12 =>
-      letb _ := assign todo(term) in
-      solve_lift (ret_both (3 : int32))
-    | 13 =>
-      letb hoist25 := x in
-      letb _ := assign todo(term) in
-      letb hoist24 := impl__u32__wrapping_add (ret_both (123 : int32)) x in
-      solve_lift (add3 hoist25 hoist24 x)
-    | _ =>
-      solve_lift (ret_both (0 : int32))
-    end in
-    letb _ := assign todo(term) in
-    impl__u32__wrapping_add x y) : both (L1 :|: fset [y_loc;y_loc]) I1 int32.
-Fail Next Obligation.
-
-Equations monad_lifting {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result t_A t_B) :=
-  monad_lifting x  :=
-    solve_lift (run (ifb x >.? (ret_both (123 : int8))
-    then letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist27 := ControlFlow_Continue (Result_Err B) in
-    letb hoist28 := Result_Ok hoist27 in
-    letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist29 := ControlFlow_Break hoist28 in
-    ControlFlow_Continue (never_to_any hoist29)
-    else ControlFlow_Continue (Result_Ok A))) : both L1 I1 (t_Result t_A t_B).
-Fail Next Obligation.
-
-Equations options {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 (t_Option int8)) (y : both L2 I2 (t_Option int8)) (z : both L3 I3 (t_Option int64)) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8) :=
-  options x y z  :=
-    solve_lift (run (letm[choice_typeMonad.option_bind_code] hoist33 := x in
-    letb hoist34 := hoist33 >.? (ret_both (10 : int8)) in
-    letm[choice_typeMonad.option_bind_code] hoist40 := ifb hoist34
-    then letm[choice_typeMonad.option_bind_code] hoist35 := x in
-    Option_Some (letb hoist36 := impl__u8__wrapping_add hoist35 (ret_both (3 : int8)) in
-    Option_Some hoist36)
-    else letm[choice_typeMonad.option_bind_code] hoist38 := x in
-    letm[choice_typeMonad.option_bind_code] hoist37 := y in
-    Option_Some (letb hoist39 := impl__u8__wrapping_add hoist38 hoist37 in
-    Option_Some hoist39) in
-    letm[choice_typeMonad.option_bind_code] hoist41 := hoist40 in
-    letm[choice_typeMonad.option_bind_code] v := matchb hoist41 with
-    | 3 =>
-      Option_None
-    | 4 =>
-      letm[choice_typeMonad.option_bind_code] hoist30 := z in
-      Option_Some (letb hoist31 := hoist30 >.? (ret_both (4 : int64)) in
-      letb hoist32 := ifb hoist31
-      then ret_both (0 : int8)
-      else ret_both (3 : int8) in
-      solve_lift ((ret_both (4 : int8)) .+ hoist32))
-    | _ =>
-      Option_Some (solve_lift (ret_both (12 : int8)))
-    end in
-    letm[choice_typeMonad.option_bind_code] hoist42 := x in
-    letb hoist44 := impl__u8__wrapping_add v hoist42 in
-    letm[choice_typeMonad.option_bind_code] hoist43 := y in
-    Option_Some (letb hoist45 := impl__u8__wrapping_add hoist44 hoist43 in
-    Option_Some hoist45))) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8).
-Fail Next Obligation.
-
-Definition y_loc : Location :=
-  (int32;2%nat).
-Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both (L1 :|: fset [y_loc]) I1 (t_Result int32 int32) :=
-  question_mark x  :=
-    solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (40 : int32))
-    then letb y loc(y_loc) := ret_both (0 : int32) in
-    letb _ := assign todo(term) in
-    letb _ := assign todo(term) in
-    letb _ := assign todo(term) in
-    letb hoist46 := x >.? (ret_both (90 : int32)) in
-    ifb hoist46
-    then impl__map_err (Result_Err (ret_both (12 : int8))) f_from
-    else ()
-    else () in
-    Result_Ok (Result_Ok (impl__u32__wrapping_add (ret_both (3 : int32)) x)))) : both (L1 :|: fset [y_loc]) I1 (t_Result int32 int32).
-Fail Next Obligation.
+(*Not implemented yet? todo(item)*)
 
-Equations simplifiable_question_mark {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (c : both L1 I1 'bool) (x : both L2 I2 (t_Option int32)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32) :=
-  simplifiable_question_mark c x  :=
-    solve_lift (run (letm[choice_typeMonad.option_bind_code] a := ifb c
-    then letm[choice_typeMonad.option_bind_code] hoist47 := x in
-    Option_Some (hoist47 .+ (ret_both (10 : int32)))
-    else Option_Some (ret_both (0 : int32)) in
-    Option_Some (letb b := ret_both (20 : int32) in
-    Option_Some (a .+ b)))) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32).
-Fail Next Obligation.
+(*Not implemented yet? todo(item)*)
 
-Definition x_loc : Location :=
-  (int32;3%nat).
-Equations simplifiable_return {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (c1 : both L1 I1 'bool) (c2 : both L2 I2 'bool) (c3 : both L3 I3 'bool) : both (L1 :|: L2 :|: L3 :|: fset [x_loc]) (I1 :|: I2 :|: I3) int32 :=
-  simplifiable_return c1 c2 c3  :=
-    solve_lift (run (letb x loc(x_loc) := ret_both (0 : int32) in
-    letm[choice_typeMonad.result_bind_code int32] _ := ifb c1
-    then letm[choice_typeMonad.result_bind_code int32] _ := ifb c2
-    then letb _ := assign todo(term) in
-    ifb c3
-    then letm[choice_typeMonad.result_bind_code int32] hoist48 := ControlFlow_Break (ret_both (1 : int32)) in
-    ControlFlow_Continue (never_to_any hoist48)
-    else ()
-    else () in
-    ControlFlow_Continue (letb _ := assign todo(term) in
-    ret_both (tt : 'unit))
-    else () in
-    ControlFlow_Continue x)) : both (L1 :|: L2 :|: L3 :|: fset [x_loc]) (I1 :|: I2 :|: I3) int32.
-Fail Next Obligation.
+(*Not implemented yet? todo(item)*)
 '''
 "Side_effects_Issue_1083_.v" = '''
 (* File automatically generated by Hacspec *)
@@ -382,12 +382,12 @@ Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.
 
 Equations test {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (x : both L1 I1 (t_Option int32)) (y : both L2 I2 (t_Option int32)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32) :=
   test x y  :=
-    solve_lift (run (letb hoist3 := fun i =>
-      letm[choice_typeMonad.option_bind_code] hoist1 := y in
-      Option_Some (letb hoist2 := i .+ hoist1 in
-      Option_Some hoist2) in
-    letb hoist4 := impl__map x hoist3 in
-    hoist4)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32).
+    solve_lift (run (letb hoist40 := fun i =>
+      letm[choice_typeMonad.option_bind_code] hoist38 := y in
+      Option_Some (letb hoist39 := i .+ hoist38 in
+      Option_Some hoist39) in
+    letb hoist41 := impl__map x hoist40 in
+    hoist41)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32).
 Fail Next Obligation.
 '''
 "Side_effects_Nested_return.v" = '''
@@ -427,21 +427,21 @@ Equations fun {L1 : {fset Location}} {I1 : Interface} (rng : both L1 I1 int8) :
   fun rng  :=
     solve_lift (run (letb '(tmp0,out) := other_fun rng in
     letb _ := assign todo(term) in
-    letb hoist6 := out in
-    letb hoist7 := f_branch hoist6 in
-    letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist8 := matchb hoist7 with
+    letb hoist43 := out in
+    letb hoist44 := f_branch hoist43 in
+    letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist45 := matchb hoist44 with
     | ControlFlow_Break_case residual =>
       letb residual := ret_both ((residual) : (t_Result t_Infallible 'unit)) in
-      letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist5 := ControlFlow_Break (prod_b (rng,f_from_residual residual)) in
-      ControlFlow_Continue (solve_lift (never_to_any hoist5))
+      letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist42 := ControlFlow_Break (prod_b (rng,f_from_residual residual)) in
+      ControlFlow_Continue (solve_lift (never_to_any hoist42))
     | ControlFlow_Continue_case val =>
       letb val := ret_both ((val) : ('unit)) in
       ControlFlow_Continue (solve_lift val)
     end in
-    letb hoist9 := Result_Ok hoist8 in
-    letb hoist10 := prod_b (rng,hoist9) in
-    letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist11 := ControlFlow_Break hoist10 in
-    ControlFlow_Continue (letb hax_temp_output := never_to_any hoist11 in
+    letb hoist46 := Result_Ok hoist45 in
+    letb hoist47 := prod_b (rng,hoist46) in
+    letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist48 := ControlFlow_Break hoist47 in
+    ControlFlow_Continue (letb hax_temp_output := never_to_any hoist48 in
     prod_b (rng,hax_temp_output)))) : both L1 I1 (int8 × t_Result 'unit 'unit).
 Fail Next Obligation.
 '''
diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
index 9e505d3a1..3ea441886 100644
--- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
@@ -79,33 +79,6 @@ module Traits.For_clauses.Issue_495_
 open Core
 open FStar.Mul
 
-let minimized_1_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
-    : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
-  Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter
-        (Core.Ops.Range.t_Range u8) (u8 -> bool))
-    #FStar.Tactics.Typeclasses.solve
-    #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
-    (Core.Iter.Traits.Iterator.f_filter #(Core.Ops.Range.t_Range u8)
-        #FStar.Tactics.Typeclasses.solve
-        ({ Core.Ops.Range.f_start = 0uy; Core.Ops.Range.f_end = 5uy } <: Core.Ops.Range.t_Range u8)
-        (fun temp_0_ ->
-            let _:u8 = temp_0_ in
-            true)
-      <:
-      Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool))
-
-let minimized_2_ (it: Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool))
-    : Prims.unit =
-  let (v__indices: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global):Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global
-  =
-    Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter
-          (Core.Ops.Range.t_Range u8) (u8 -> bool))
-      #FStar.Tactics.Typeclasses.solve
-      #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
-      it
-  in
-  ()
-
 let original_function_from_495_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) : Prims.unit =
   let (v__indices: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global):Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global
   =
@@ -139,6 +112,33 @@ let original_function_from_495_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
         Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool))
   in
   ()
+
+let minimized_1_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+    : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global =
+  Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter
+        (Core.Ops.Range.t_Range u8) (u8 -> bool))
+    #FStar.Tactics.Typeclasses.solve
+    #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+    (Core.Iter.Traits.Iterator.f_filter #(Core.Ops.Range.t_Range u8)
+        #FStar.Tactics.Typeclasses.solve
+        ({ Core.Ops.Range.f_start = 0uy; Core.Ops.Range.f_end = 5uy } <: Core.Ops.Range.t_Range u8)
+        (fun temp_0_ ->
+            let _:u8 = temp_0_ in
+            true)
+      <:
+      Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool))
+
+let minimized_2_ (it: Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool))
+    : Prims.unit =
+  let (v__indices: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global):Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global
+  =
+    Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter
+          (Core.Ops.Range.t_Range u8) (u8 -> bool))
+      #FStar.Tactics.Typeclasses.solve
+      #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
+      it
+  in
+  ()
 '''
 "Traits.For_clauses.fst" = '''
 module Traits.For_clauses
@@ -359,7 +359,7 @@ let impl (#v_TypeArg: Type0) (v_ConstArg: usize) : t_Trait Prims.unit v_TypeArg
       ()
   }
 
-let associated_function_caller
+let method_caller
       (#v_MethodTypeArg #v_TypeArg: Type0)
       (v_ConstArg v_MethodConstArg: usize)
       (#v_ImplTrait: Type0)
@@ -369,7 +369,7 @@ let associated_function_caller
       (value_Type: t_Type v_TypeArg v_ConstArg)
     : Prims.unit =
   let _:Prims.unit =
-    f_associated_function #v_ImplTrait
+    f_method #v_ImplTrait
       #v_TypeArg
       #v_ConstArg
       #FStar.Tactics.Typeclasses.solve
@@ -381,7 +381,7 @@ let associated_function_caller
   in
   ()
 
-let method_caller
+let associated_function_caller
       (#v_MethodTypeArg #v_TypeArg: Type0)
       (v_ConstArg v_MethodConstArg: usize)
       (#v_ImplTrait: Type0)
@@ -391,7 +391,7 @@ let method_caller
       (value_Type: t_Type v_TypeArg v_ConstArg)
     : Prims.unit =
   let _:Prims.unit =
-    f_method #v_ImplTrait
+    f_associated_function #v_ImplTrait
       #v_TypeArg
       #v_ConstArg
       #FStar.Tactics.Typeclasses.solve
@@ -508,14 +508,14 @@ module Traits.Unconstrainted_types_issue_677_
 open Core
 open FStar.Mul
 
-type t_Plus = | Plus : t_Plus
-
 class t_PolyOp (v_Self: Type0) = {
   f_op_pre:u32 -> u32 -> Type0;
   f_op_post:u32 -> u32 -> u32 -> Type0;
   f_op:x0: u32 -> x1: u32 -> Prims.Pure u32 (f_op_pre x0 x1) (fun result -> f_op_post x0 x1 result)
 }
 
+type t_Plus = | Plus : t_Plus
+
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl: t_PolyOp t_Plus =
   {
@@ -545,26 +545,6 @@ module Traits
 open Core
 open FStar.Mul
 
-class t_Bar (v_Self: Type0) = {
-  f_bar_pre:v_Self -> Type0;
-  f_bar_post:v_Self -> Prims.unit -> Type0;
-  f_bar:x0: v_Self -> Prims.Pure Prims.unit (f_bar_pre x0) (fun result -> f_bar_post x0 result)
-}
-
-let impl_2__method (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Bar v_T) (x: v_T)
-    : Prims.unit = f_bar #v_T #FStar.Tactics.Typeclasses.solve x
-
-type t_Error = | Error_Fail : t_Error
-
-let impl__Error__for_application_callback (_: Prims.unit) :  Prims.unit -> t_Error =
-  fun temp_0_ ->
-    let _:Prims.unit = temp_0_ in
-    Error_Fail <: t_Error
-
-let t_Error_cast_to_repr (x: t_Error) : isize = match x <: t_Error with | Error_Fail  -> isz 0
-
-type t_Struct = | Struct : t_Struct
-
 class t_SuperTrait (v_Self: Type0) = {
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_9529721400157967266:Core.Clone.t_Clone v_Self;
   f_function_of_super_trait_pre:v_Self -> Type0;
@@ -584,6 +564,17 @@ let impl_SuperTrait_for_i32: t_SuperTrait i32 =
     f_function_of_super_trait = fun (self: i32) -> cast (Core.Num.impl__i32__abs self <: i32) <: u32
   }
 
+type t_Struct = | Struct : t_Struct
+
+class t_Bar (v_Self: Type0) = {
+  f_bar_pre:v_Self -> Type0;
+  f_bar_post:v_Self -> Prims.unit -> Type0;
+  f_bar:x0: v_Self -> Prims.Pure Prims.unit (f_bar_pre x0) (fun result -> f_bar_post x0 result)
+}
+
+let impl_2__method (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Bar v_T) (x: v_T)
+    : Prims.unit = f_bar #v_T #FStar.Tactics.Typeclasses.solve x
+
 let closure_impl_expr
       (#v_I: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Iter.Traits.Iterator.t_Iterator v_I)
@@ -614,6 +605,15 @@ let closure_impl_expr_fngen
       <:
       Core.Iter.Adapters.Map.t_Map v_I v_F)
 
+type t_Error = | Error_Fail : t_Error
+
+let t_Error_cast_to_repr (x: t_Error) : isize = match x <: t_Error with | Error_Fail  -> isz 0
+
+let impl__Error__for_application_callback (_: Prims.unit) :  Prims.unit -> t_Error =
+  fun temp_0_ ->
+    let _:Prims.unit = temp_0_ in
+    Error_Fail <: t_Error
+
 let iter_option (#v_T: Type0) (x: Core.Option.t_Option v_T) : Core.Option.t_IntoIter v_T =
   Core.Iter.Traits.Collect.f_into_iter #(Core.Option.t_Option v_T)
     #FStar.Tactics.Typeclasses.solve
diff --git a/test-harness/src/snapshots/toolchain__unsafe into-fstar.snap b/test-harness/src/snapshots/toolchain__unsafe into-fstar.snap
index 4991e948c..5cc226a82 100644
--- a/test-harness/src/snapshots/toolchain__unsafe into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__unsafe into-fstar.snap	
@@ -38,13 +38,13 @@ type t_Impossible =
 let t_Impossible_cast_to_repr (x: t_Impossible) : Rust_primitives.Hax.t_Never =
   match x <: t_Impossible with
 
-let get_unchecked_example (slice: t_Slice u8)
-    : Prims.Pure u8
-      (requires (Core.Slice.impl__len #u8 slice <: usize) >. sz 10)
-      (fun _ -> Prims.l_True) = Core.Slice.impl__get_unchecked #u8 #usize slice (sz 6)
-
 let impossible (_: Prims.unit) : Prims.Pure t_Impossible (requires false) (fun _ -> Prims.l_True) =
   Rust_primitives.Hax.never_to_any (Core.Hint.unreachable_unchecked ()
       <:
       Rust_primitives.Hax.t_Never)
+
+let get_unchecked_example (slice: t_Slice u8)
+    : Prims.Pure u8
+      (requires (Core.Slice.impl__len #u8 slice <: usize) >. sz 10)
+      (fun _ -> Prims.l_True) = Core.Slice.impl__get_unchecked #u8 #usize slice (sz 6)
 '''
diff --git a/tests/reordering/src/lib.rs b/tests/reordering/src/lib.rs
index fb03140e2..25a3c0760 100644
--- a/tests/reordering/src/lib.rs
+++ b/tests/reordering/src/lib.rs
@@ -31,3 +31,18 @@ mod mut_rec {
         f()
     }
 }
+
+mod independent_cycles {
+    fn a() {
+        c()
+    }
+    fn b() {
+        d()
+    }
+    fn c() {
+        a()
+    }
+    fn d() {
+        b()
+    }
+}