diff --git a/third_party/move/move-compiler-v2/src/lib.rs b/third_party/move/move-compiler-v2/src/lib.rs
index 56f2e5a1b4d67..cdae728718bb8 100644
--- a/third_party/move/move-compiler-v2/src/lib.rs
+++ b/third_party/move/move-compiler-v2/src/lib.rs
@@ -162,7 +162,6 @@ pub fn run_move_compiler_for_analysis(
     options.whole_program = true; // will set `treat_everything_as_target`
     options = options.set_experiment(Experiment::SPEC_REWRITE, true);
     options = options.set_experiment(Experiment::ATTACH_COMPILED_MODULE, true);
-    options = options.set_experiment(Experiment::CFG_SIMPLIFICATION, false);
     let (env, _units) = run_move_compiler(error_writer, options)?;
     // Reset for subsequent analysis
     env.treat_everything_as_target(false);
diff --git a/third_party/move/move-model/bytecode/ast-generator-tests/tests/abort_example.exp b/third_party/move/move-model/bytecode/ast-generator-tests/tests/abort_example.exp
index 4d886eb3fa03d..bf73e7d811621 100644
--- a/third_party/move/move-model/bytecode/ast-generator-tests/tests/abort_example.exp
+++ b/third_party/move/move-model/bytecode/ast-generator-tests/tests/abort_example.exp
@@ -18,13 +18,13 @@ public fun m::f($t0|length: u64): u64 {
      var $t5: bool
      var $t6: u64
      var $t7: u64
-     var $t8: u64
-     var $t9: bool
+     var $t8: bool
+     var $t9: u64
      var $t10: u64
      var $t11: u64
-     var $t12: u64
+     var $t12: bool
      var $t13: u64
-     var $t14: bool
+     var $t14: u64
      var $t15: u64
      var $t16: u64
      var $t17: u64
@@ -32,44 +32,36 @@ public fun m::f($t0|length: u64): u64 {
   0: $t3 := copy($t0)
   1: $t4 := 0
   2: $t5 := >($t3, $t4)
-  3: if ($t5) goto 4 else goto 6
+  3: if ($t5) goto 4 else goto 30
   4: label L1
-  5: goto 9
-  6: label L0
-  7: $t6 := 1
-  8: abort($t6)
-  9: label L2
- 10: $t7 := copy($t0)
- 11: $t8 := 100
- 12: $t9 := <($t7, $t8)
- 13: if ($t9) goto 14 else goto 16
- 14: label L4
- 15: goto 19
- 16: label L3
- 17: $t10 := 2
- 18: abort($t10)
- 19: label L5
- 20: $t11 := 0
- 21: $t1 := $t11
- 22: goto 23
- 23: label L10
- 24: $t12 := copy($t1)
- 25: $t13 := copy($t0)
- 26: $t14 := <($t12, $t13)
- 27: if ($t14) goto 28 else goto 34
- 28: label L7
- 29: $t15 := move($t1)
- 30: $t16 := 1
- 31: $t17 := +($t15, $t16)
- 32: $t1 := $t17
- 33: goto 36
- 34: label L6
- 35: goto 38
- 36: label L8
- 37: goto 23
- 38: label L9
- 39: $t18 := move($t1)
- 40: return $t18
+  5: $t6 := copy($t0)
+  6: $t7 := 100
+  7: $t8 := <($t6, $t7)
+  8: if ($t8) goto 9 else goto 27
+  9: label L3
+ 10: $t9 := 0
+ 11: $t1 := $t9
+ 12: goto 13
+ 13: label L6
+ 14: $t10 := copy($t1)
+ 15: $t11 := copy($t0)
+ 16: $t12 := <($t10, $t11)
+ 17: if ($t12) goto 18 else goto 24
+ 18: label L5
+ 19: $t13 := move($t1)
+ 20: $t14 := 1
+ 21: $t15 := +($t13, $t14)
+ 22: $t1 := $t15
+ 23: goto 13
+ 24: label L4
+ 25: $t16 := move($t1)
+ 26: return $t16
+ 27: label L2
+ 28: $t17 := 2
+ 29: abort($t17)
+ 30: label L0
+ 31: $t18 := 1
+ 32: abort($t18)
 }
 
 --- Raw Generated AST
@@ -78,32 +70,32 @@ _t4: u64 = 0;
 _t5: bool = Gt(_t3, _t4);
 loop {
   if (_t5) break;
-  _t6: u64 = 1;
-  Abort(_t6)
+  _t18: u64 = 1;
+  Abort(_t18)
 };
-_t7: u64 = length;
-_t8: u64 = 100;
-_t9: bool = Lt(_t7, _t8);
+_t6: u64 = length;
+_t7: u64 = 100;
+_t8: bool = Lt(_t6, _t7);
 loop {
-  if (_t9) break;
-  _t10: u64 = 2;
-  Abort(_t10)
+  if (_t8) break;
+  _t17: u64 = 2;
+  Abort(_t17)
 };
-_t11: u64 = 0;
-_t1: u64 = _t11;
+_t9: u64 = 0;
+_t1: u64 = _t9;
 loop {
-  _t12: u64 = _t1;
-  _t13: u64 = length;
-  _t14: bool = Lt(_t12, _t13);
-  if (Not(_t14)) break;
-  _t15: u64 = _t1;
-  _t16: u64 = 1;
-  _t17: u64 = Add(_t15, _t16);
-  _t1: u64 = _t17;
+  _t10: u64 = _t1;
+  _t11: u64 = length;
+  _t12: bool = Lt(_t10, _t11);
+  if (Not(_t12)) break;
+  _t13: u64 = _t1;
+  _t14: u64 = 1;
+  _t15: u64 = Add(_t13, _t14);
+  _t1: u64 = _t15;
   continue
 };
-_t18: u64 = _t1;
-return _t18
+_t16: u64 = _t1;
+return _t16
 
 --- Assign-Transformed Generated AST
 loop {
diff --git a/third_party/move/move-model/bytecode/ast-generator-tests/tests/bit_vector_loop_example.exp b/third_party/move/move-model/bytecode/ast-generator-tests/tests/bit_vector_loop_example.exp
index 49fee5291b0c8..732f4d6f359fb 100644
--- a/third_party/move/move-model/bytecode/ast-generator-tests/tests/bit_vector_loop_example.exp
+++ b/third_party/move/move-model/bytecode/ast-generator-tests/tests/bit_vector_loop_example.exp
@@ -18,12 +18,12 @@ public fun m::is_index_set($t0|self: &0x1::m::BitVector, $t1|bit_index: u64): bo
      var $t9: u64
      var $t10: bool
      var $t11: &0x1::m::BitVector
-     var $t12: u64
-     var $t13: &0x1::m::BitVector
-     var $t14: &vector<bool>
-     var $t15: u64
-     var $t16: &bool
-     var $t17: bool
+     var $t12: &vector<bool>
+     var $t13: u64
+     var $t14: &bool
+     var $t15: bool
+     var $t16: &0x1::m::BitVector
+     var $t17: u64
   0: $t4 := copy($t1)
   1: $t2 := $t4
   2: $t5 := copy($t0)
@@ -33,21 +33,19 @@ public fun m::is_index_set($t0|self: &0x1::m::BitVector, $t1|bit_index: u64): bo
   6: $t8 := move($t2)
   7: $t9 := move($t3)
   8: $t10 := <($t8, $t9)
-  9: if ($t10) goto 10 else goto 12
+  9: if ($t10) goto 10 else goto 17
  10: label L1
- 11: goto 17
- 12: label L0
- 13: $t11 := move($t0)
- 14: drop($t11)
- 15: $t12 := 131072
- 16: abort($t12)
- 17: label L2
- 18: $t13 := move($t0)
- 19: $t14 := borrow_field<0x1::m::BitVector>.bit_field($t13)
- 20: $t15 := move($t1)
- 21: $t16 := vector::borrow<bool>($t14, $t15)
- 22: $t17 := read_ref($t16)
- 23: return $t17
+ 11: $t11 := move($t0)
+ 12: $t12 := borrow_field<0x1::m::BitVector>.bit_field($t11)
+ 13: $t13 := move($t1)
+ 14: $t14 := vector::borrow<bool>($t12, $t13)
+ 15: $t15 := read_ref($t14)
+ 16: return $t15
+ 17: label L0
+ 18: $t16 := move($t0)
+ 19: drop($t16)
+ 20: $t17 := 131072
+ 21: abort($t17)
 }
 
 --- Raw Generated AST
@@ -62,16 +60,16 @@ _t9: u64 = _t3;
 _t10: bool = Lt(_t8, _t9);
 loop {
   if (_t10) break;
-  _t11: &BitVector = self;
-  _t12: u64 = 131072;
-  Abort(_t12)
+  _t16: &BitVector = self;
+  _t17: u64 = 131072;
+  Abort(_t17)
 };
-_t13: &BitVector = self;
-_t14: &vector<bool> = select m::BitVector.bit_field(_t13);
-_t15: u64 = bit_index;
-_t16: &bool = vector::borrow<bool>(_t14, _t15);
-_t17: bool = Deref(_t16);
-return _t17
+_t11: &BitVector = self;
+_t12: &vector<bool> = select m::BitVector.bit_field(_t11);
+_t13: u64 = bit_index;
+_t14: &bool = vector::borrow<bool>(_t12, _t13);
+_t15: bool = Deref(_t14);
+return _t15
 
 --- Assign-Transformed Generated AST
 loop {
@@ -110,13 +108,13 @@ public fun m::set($t0|self: &mut 0x1::m::BitVector, $t1|bit_index: u64) {
      var $t10: u64
      var $t11: bool
      var $t12: &mut 0x1::m::BitVector
-     var $t13: u64
-     var $t14: &mut 0x1::m::BitVector
-     var $t15: &mut vector<bool>
-     var $t16: u64
+     var $t13: &mut vector<bool>
+     var $t14: u64
+     var $t15: &mut bool
+     var $t16: bool
      var $t17: &mut bool
-     var $t18: bool
-     var $t19: &mut bool
+     var $t18: &mut 0x1::m::BitVector
+     var $t19: u64
   0: $t5 := copy($t1)
   1: $t2 := $t5
   2: $t6 := copy($t0)
@@ -126,24 +124,22 @@ public fun m::set($t0|self: &mut 0x1::m::BitVector, $t1|bit_index: u64) {
   6: $t9 := move($t2)
   7: $t10 := move($t3)
   8: $t11 := <($t9, $t10)
-  9: if ($t11) goto 10 else goto 12
+  9: if ($t11) goto 10 else goto 20
  10: label L1
- 11: goto 17
- 12: label L0
- 13: $t12 := move($t0)
- 14: drop($t12)
- 15: $t13 := 131072
- 16: abort($t13)
- 17: label L2
- 18: $t14 := move($t0)
- 19: $t15 := borrow_field<0x1::m::BitVector>.bit_field($t14)
- 20: $t16 := move($t1)
- 21: $t17 := vector::borrow_mut<bool>($t15, $t16)
- 22: $t4 := $t17
- 23: $t18 := true
- 24: $t19 := move($t4)
- 25: write_ref($t19, $t18)
- 26: return ()
+ 11: $t12 := move($t0)
+ 12: $t13 := borrow_field<0x1::m::BitVector>.bit_field($t12)
+ 13: $t14 := move($t1)
+ 14: $t15 := vector::borrow_mut<bool>($t13, $t14)
+ 15: $t4 := $t15
+ 16: $t16 := true
+ 17: $t17 := move($t4)
+ 18: write_ref($t17, $t16)
+ 19: return ()
+ 20: label L0
+ 21: $t18 := move($t0)
+ 22: drop($t18)
+ 23: $t19 := 131072
+ 24: abort($t19)
 }
 
 --- Raw Generated AST
@@ -158,18 +154,18 @@ _t10: u64 = _t3;
 _t11: bool = Lt(_t9, _t10);
 loop {
   if (_t11) break;
-  _t12: &mut BitVector = self;
-  _t13: u64 = 131072;
-  Abort(_t13)
+  _t18: &mut BitVector = self;
+  _t19: u64 = 131072;
+  Abort(_t19)
 };
-_t14: &mut BitVector = self;
-_t15: &mut vector<bool> = select m::BitVector.bit_field(_t14);
-_t16: u64 = bit_index;
-_t17: &mut bool = vector::borrow_mut<bool>(_t15, _t16);
-_t4: &mut bool = _t17;
-_t18: bool = true;
-_t19: &mut bool = _t4;
-_t19 = _t18;
+_t12: &mut BitVector = self;
+_t13: &mut vector<bool> = select m::BitVector.bit_field(_t12);
+_t14: u64 = bit_index;
+_t15: &mut bool = vector::borrow_mut<bool>(_t13, _t14);
+_t4: &mut bool = _t15;
+_t16: bool = true;
+_t17: &mut bool = _t4;
+_t17 = _t16;
 return Tuple()
 
 --- Assign-Transformed Generated AST
@@ -267,10 +263,10 @@ public fun m::shift_left($t0|self: &mut 0x1::m::BitVector, $t1|amount: u64) {
      var $t48: u64
      var $t49: u64
      var $t50: u64
-     var $t51: &mut 0x1::m::BitVector
+     var $t51: u64
      var $t52: u64
      var $t53: u64
-     var $t54: u64
+     var $t54: &mut 0x1::m::BitVector
      var $t55: u64
      var $t56: &mut 0x1::m::BitVector
      var $t57: &u64
@@ -296,7 +292,7 @@ public fun m::shift_left($t0|self: &mut 0x1::m::BitVector, $t1|amount: u64) {
   4: $t10 := copy($t1)
   5: $t11 := move($t2)
   6: $t12 := >=($t10, $t11)
-  7: if ($t12) goto 8 else goto 47
+  7: if ($t12) goto 8 else goto 45
   8: label L1
   9: $t13 := move($t0)
  10: $t14 := borrow_field<0x1::m::BitVector>.bit_field($t13)
@@ -304,7 +300,7 @@ public fun m::shift_left($t0|self: &mut 0x1::m::BitVector, $t1|amount: u64) {
  12: $t15 := 0
  13: $t2 := $t15
  14: goto 15
- 15: label L6
+ 15: label L4
  16: $t16 := copy($t2)
  17: $t4 := $t16
  18: $t17 := copy($t3)
@@ -327,96 +323,86 @@ public fun m::shift_left($t0|self: &mut 0x1::m::BitVector, $t1|amount: u64) {
  35: $t29 := 1
  36: $t30 := +($t28, $t29)
  37: $t2 := $t30
- 38: goto 43
+ 38: goto 15
  39: label L2
  40: $t31 := move($t3)
  41: drop($t31)
- 42: goto 45
- 43: label L4
- 44: goto 15
- 45: label L5
- 46: goto 126
- 47: label L0
- 48: $t32 := copy($t1)
- 49: $t2 := $t32
- 50: goto 51
- 51: label L15
- 52: $t33 := copy($t0)
- 53: $t34 := borrow_field<0x1::m::BitVector>.length($t33)
- 54: $t35 := read_ref($t34)
- 55: $t4 := $t35
- 56: $t36 := copy($t2)
- 57: $t37 := move($t4)
- 58: $t38 := <($t36, $t37)
- 59: if ($t38) goto 60 else goto 90
- 60: label L9
- 61: $t39 := copy($t0)
- 62: $t40 := freeze_ref($t39)
- 63: $t41 := copy($t2)
- 64: $t42 := m::is_index_set($t40, $t41)
- 65: if ($t42) goto 66 else goto 75
- 66: label L11
- 67: $t43 := copy($t2)
- 68: $t44 := copy($t1)
- 69: $t45 := -($t43, $t44)
- 70: $t4 := $t45
- 71: $t46 := copy($t0)
- 72: $t47 := move($t4)
- 73: m::set($t46, $t47)
- 74: goto 84
- 75: label L10
- 76: $t48 := copy($t2)
- 77: $t49 := copy($t1)
- 78: $t50 := -($t48, $t49)
- 79: $t4 := $t50
- 80: $t51 := copy($t0)
- 81: $t52 := move($t4)
- 82: m::unset($t51, $t52)
- 83: goto 84
- 84: label L12
- 85: $t53 := move($t2)
- 86: $t54 := 1
- 87: $t55 := +($t53, $t54)
- 88: $t2 := $t55
- 89: goto 92
- 90: label L8
- 91: goto 94
- 92: label L13
- 93: goto 51
- 94: label L14
- 95: $t56 := copy($t0)
- 96: $t57 := borrow_field<0x1::m::BitVector>.length($t56)
- 97: $t58 := read_ref($t57)
- 98: $t59 := move($t1)
- 99: $t60 := -($t58, $t59)
-100: $t2 := $t60
-101: goto 102
-102: label L19
-103: $t61 := copy($t0)
-104: $t62 := borrow_field<0x1::m::BitVector>.length($t61)
-105: $t63 := read_ref($t62)
-106: $t1 := $t63
-107: $t64 := copy($t2)
-108: $t65 := move($t1)
-109: $t66 := <($t64, $t65)
-110: if ($t66) goto 111 else goto 120
-111: label L17
-112: $t67 := copy($t0)
-113: $t68 := copy($t2)
-114: m::unset($t67, $t68)
-115: $t69 := move($t2)
-116: $t70 := 1
-117: $t71 := +($t69, $t70)
-118: $t2 := $t71
-119: goto 124
-120: label L16
-121: $t72 := move($t0)
-122: drop($t72)
-123: goto 126
-124: label L18
-125: goto 102
-126: label L7
-127: return ()
+ 42: goto 43
+ 43: label L14
+ 44: return ()
+ 45: label L0
+ 46: $t32 := copy($t1)
+ 47: $t2 := $t32
+ 48: goto 49
+ 49: label L9
+ 50: $t33 := copy($t0)
+ 51: $t34 := borrow_field<0x1::m::BitVector>.length($t33)
+ 52: $t35 := read_ref($t34)
+ 53: $t4 := $t35
+ 54: $t36 := copy($t2)
+ 55: $t37 := move($t4)
+ 56: $t38 := <($t36, $t37)
+ 57: if ($t38) goto 58 else goto 88
+ 58: label L6
+ 59: $t39 := copy($t0)
+ 60: $t40 := freeze_ref($t39)
+ 61: $t41 := copy($t2)
+ 62: $t42 := m::is_index_set($t40, $t41)
+ 63: if ($t42) goto 64 else goto 79
+ 64: label L8
+ 65: $t43 := copy($t2)
+ 66: $t44 := copy($t1)
+ 67: $t45 := -($t43, $t44)
+ 68: $t4 := $t45
+ 69: $t46 := copy($t0)
+ 70: $t47 := move($t4)
+ 71: m::set($t46, $t47)
+ 72: goto 73
+ 73: label L10
+ 74: $t48 := move($t2)
+ 75: $t49 := 1
+ 76: $t50 := +($t48, $t49)
+ 77: $t2 := $t50
+ 78: goto 49
+ 79: label L7
+ 80: $t51 := copy($t2)
+ 81: $t52 := copy($t1)
+ 82: $t53 := -($t51, $t52)
+ 83: $t4 := $t53
+ 84: $t54 := copy($t0)
+ 85: $t55 := move($t4)
+ 86: m::unset($t54, $t55)
+ 87: goto 73
+ 88: label L5
+ 89: $t56 := copy($t0)
+ 90: $t57 := borrow_field<0x1::m::BitVector>.length($t56)
+ 91: $t58 := read_ref($t57)
+ 92: $t59 := move($t1)
+ 93: $t60 := -($t58, $t59)
+ 94: $t2 := $t60
+ 95: goto 96
+ 96: label L13
+ 97: $t61 := copy($t0)
+ 98: $t62 := borrow_field<0x1::m::BitVector>.length($t61)
+ 99: $t63 := read_ref($t62)
+100: $t1 := $t63
+101: $t64 := copy($t2)
+102: $t65 := move($t1)
+103: $t66 := <($t64, $t65)
+104: if ($t66) goto 105 else goto 114
+105: label L12
+106: $t67 := copy($t0)
+107: $t68 := copy($t2)
+108: m::unset($t67, $t68)
+109: $t69 := move($t2)
+110: $t70 := 1
+111: $t71 := +($t69, $t70)
+112: $t2 := $t71
+113: goto 96
+114: label L11
+115: $t72 := move($t0)
+116: drop($t72)
+117: goto 43
 }
 
 --- Raw Generated AST
@@ -495,19 +481,19 @@ loop {
         m::set(_t46, _t47);
         break[1]
       };
-      _t48: u64 = _t2;
-      _t49: u64 = amount;
-      _t50: u64 = Sub(_t48, _t49);
-      _t4: u64 = _t50;
-      _t51: &mut BitVector = self;
-      _t52: u64 = _t4;
-      m::unset(_t51, _t52);
+      _t51: u64 = _t2;
+      _t52: u64 = amount;
+      _t53: u64 = Sub(_t51, _t52);
+      _t4: u64 = _t53;
+      _t54: &mut BitVector = self;
+      _t55: u64 = _t4;
+      m::unset(_t54, _t55);
       break
     };
-    _t53: u64 = _t2;
-    _t54: u64 = 1;
-    _t55: u64 = Add(_t53, _t54);
-    _t2: u64 = _t55;
+    _t48: u64 = _t2;
+    _t49: u64 = 1;
+    _t50: u64 = Add(_t48, _t49);
+    _t2: u64 = _t50;
     continue
   };
   _t56: &mut BitVector = self;
@@ -706,13 +692,13 @@ public fun m::unset($t0|self: &mut 0x1::m::BitVector, $t1|bit_index: u64) {
      var $t10: u64
      var $t11: bool
      var $t12: &mut 0x1::m::BitVector
-     var $t13: u64
-     var $t14: &mut 0x1::m::BitVector
-     var $t15: &mut vector<bool>
-     var $t16: u64
+     var $t13: &mut vector<bool>
+     var $t14: u64
+     var $t15: &mut bool
+     var $t16: bool
      var $t17: &mut bool
-     var $t18: bool
-     var $t19: &mut bool
+     var $t18: &mut 0x1::m::BitVector
+     var $t19: u64
   0: $t5 := copy($t1)
   1: $t2 := $t5
   2: $t6 := copy($t0)
@@ -722,24 +708,22 @@ public fun m::unset($t0|self: &mut 0x1::m::BitVector, $t1|bit_index: u64) {
   6: $t9 := move($t2)
   7: $t10 := move($t3)
   8: $t11 := <($t9, $t10)
-  9: if ($t11) goto 10 else goto 12
+  9: if ($t11) goto 10 else goto 20
  10: label L1
- 11: goto 17
- 12: label L0
- 13: $t12 := move($t0)
- 14: drop($t12)
- 15: $t13 := 131072
- 16: abort($t13)
- 17: label L2
- 18: $t14 := move($t0)
- 19: $t15 := borrow_field<0x1::m::BitVector>.bit_field($t14)
- 20: $t16 := move($t1)
- 21: $t17 := vector::borrow_mut<bool>($t15, $t16)
- 22: $t4 := $t17
- 23: $t18 := false
- 24: $t19 := move($t4)
- 25: write_ref($t19, $t18)
- 26: return ()
+ 11: $t12 := move($t0)
+ 12: $t13 := borrow_field<0x1::m::BitVector>.bit_field($t12)
+ 13: $t14 := move($t1)
+ 14: $t15 := vector::borrow_mut<bool>($t13, $t14)
+ 15: $t4 := $t15
+ 16: $t16 := false
+ 17: $t17 := move($t4)
+ 18: write_ref($t17, $t16)
+ 19: return ()
+ 20: label L0
+ 21: $t18 := move($t0)
+ 22: drop($t18)
+ 23: $t19 := 131072
+ 24: abort($t19)
 }
 
 --- Raw Generated AST
@@ -754,18 +738,18 @@ _t10: u64 = _t3;
 _t11: bool = Lt(_t9, _t10);
 loop {
   if (_t11) break;
-  _t12: &mut BitVector = self;
-  _t13: u64 = 131072;
-  Abort(_t13)
+  _t18: &mut BitVector = self;
+  _t19: u64 = 131072;
+  Abort(_t19)
 };
-_t14: &mut BitVector = self;
-_t15: &mut vector<bool> = select m::BitVector.bit_field(_t14);
-_t16: u64 = bit_index;
-_t17: &mut bool = vector::borrow_mut<bool>(_t15, _t16);
-_t4: &mut bool = _t17;
-_t18: bool = false;
-_t19: &mut bool = _t4;
-_t19 = _t18;
+_t12: &mut BitVector = self;
+_t13: &mut vector<bool> = select m::BitVector.bit_field(_t12);
+_t14: u64 = bit_index;
+_t15: &mut bool = vector::borrow_mut<bool>(_t13, _t14);
+_t4: &mut bool = _t15;
+_t16: bool = false;
+_t17: &mut bool = _t4;
+_t17 = _t16;
 return Tuple()
 
 --- Assign-Transformed Generated AST
diff --git a/third_party/move/move-model/bytecode/ast-generator-tests/tests/conditionals.exp b/third_party/move/move-model/bytecode/ast-generator-tests/tests/conditionals.exp
index 9c19f2c204116..be960ad6afff7 100644
--- a/third_party/move/move-model/bytecode/ast-generator-tests/tests/conditionals.exp
+++ b/third_party/move/move-model/bytecode/ast-generator-tests/tests/conditionals.exp
@@ -20,11 +20,11 @@ fun m::if_1($t0|c: bool): u8 {
   1: $t1 := $t2
   2: $t3 := move($t0)
   3: if ($t3) goto 4 else goto 8
-  4: label L1
+  4: label L0
   5: $t4 := 1
   6: $t1 := $t4
   7: goto 8
-  8: label L0
+  8: label L2
   9: $t5 := move($t1)
  10: return $t5
 }
@@ -79,18 +79,18 @@ fun m::if_else_1($t0|c: bool): u8 {
      var $t4: u8
      var $t5: u8
   0: $t2 := move($t0)
-  1: if ($t2) goto 2 else goto 6
+  1: if ($t2) goto 2 else goto 9
   2: label L1
   3: $t3 := 1
   4: $t1 := $t3
-  5: goto 10
-  6: label L0
-  7: $t4 := 2
-  8: $t1 := $t4
-  9: goto 10
- 10: label L2
- 11: $t5 := move($t1)
- 12: return $t5
+  5: goto 6
+  6: label L2
+  7: $t4 := move($t1)
+  8: return $t4
+  9: label L0
+ 10: $t5 := 2
+ 11: $t1 := $t5
+ 12: goto 6
 }
 
 --- Raw Generated AST
@@ -102,12 +102,12 @@ loop {
     _t1: u8 = _t3;
     break[1]
   };
-  _t4: u8 = 2;
-  _t1: u8 = _t4;
+  _t5: u8 = 2;
+  _t1: u8 = _t5;
   break
 };
-_t5: u8 = _t1;
-return _t5
+_t4: u8 = _t1;
+return _t4
 
 --- Assign-Transformed Generated AST
 loop {
@@ -165,27 +165,25 @@ fun m::if_else_2($t0|c: bool, $t1|d: bool): u8 {
      var $t7: u8
      var $t8: u8
   0: $t3 := move($t0)
-  1: if ($t3) goto 2 else goto 15
+  1: if ($t3) goto 2 else goto 16
   2: label L1
   3: $t4 := move($t1)
-  4: if ($t4) goto 5 else goto 9
+  4: if ($t4) goto 5 else goto 12
   5: label L3
   6: $t5 := 1
   7: $t2 := $t5
-  8: goto 13
-  9: label L2
- 10: $t6 := 2
- 11: $t2 := $t6
- 12: goto 13
- 13: label L4
- 14: goto 19
- 15: label L0
- 16: $t7 := 3
- 17: $t2 := $t7
- 18: goto 19
- 19: label L5
- 20: $t8 := move($t2)
- 21: return $t8
+  8: goto 9
+  9: label L4
+ 10: $t6 := move($t2)
+ 11: return $t6
+ 12: label L2
+ 13: $t7 := 2
+ 14: $t2 := $t7
+ 15: goto 9
+ 16: label L0
+ 17: $t8 := 3
+ 18: $t2 := $t8
+ 19: goto 9
 }
 
 --- Raw Generated AST
@@ -193,8 +191,8 @@ _t3: bool = c;
 loop {
   loop {
     if (_t3) break;
-    _t7: u8 = 3;
-    _t2: u8 = _t7;
+    _t8: u8 = 3;
+    _t2: u8 = _t8;
     break[1]
   };
   _t4: bool = d;
@@ -204,12 +202,12 @@ loop {
     _t2: u8 = _t5;
     break[1]
   };
-  _t6: u8 = 2;
-  _t2: u8 = _t6;
+  _t7: u8 = 2;
+  _t2: u8 = _t7;
   break
 };
-_t8: u8 = _t2;
-return _t8
+_t6: u8 = _t2;
+return _t6
 
 --- Assign-Transformed Generated AST
 loop {
@@ -266,36 +264,37 @@ fun if_else_3(c: bool): u64 {
 --- Stackless Bytecode
 fun m::if_else_3($t0|c: bool): u64 {
      var $t1|r: u64
-     var $t2: bool
-     var $t3: u64
+     var $t2|return: u64 [unused]
+     var $t3: bool
      var $t4: u64
      var $t5: u64
-  0: $t2 := move($t0)
-  1: if ($t2) goto 2 else goto 6
+     var $t6: u64
+  0: $t3 := move($t0)
+  1: if ($t3) goto 2 else goto 9
   2: label L1
-  3: $t3 := 1
-  4: $t1 := $t3
-  5: goto 10
-  6: label L0
-  7: $t4 := 2
-  8: $t1 := $t4
-  9: goto 10
- 10: label L2
- 11: $t5 := move($t1)
- 12: return $t5
+  3: $t4 := 1
+  4: $t1 := $t4
+  5: goto 6
+  6: label L2
+  7: $t5 := move($t1)
+  8: return $t5
+  9: label L0
+ 10: $t6 := 2
+ 11: $t1 := $t6
+ 12: goto 6
 }
 
 --- Raw Generated AST
-_t2: bool = c;
+_t3: bool = c;
 loop {
   loop {
-    if (Not(_t2)) break;
-    _t3: u64 = 1;
-    _t1: u64 = _t3;
+    if (Not(_t3)) break;
+    _t4: u64 = 1;
+    _t1: u64 = _t4;
     break[1]
   };
-  _t4: u64 = 2;
-  _t1: u64 = _t4;
+  _t6: u64 = 2;
+  _t1: u64 = _t6;
   break
 };
 _t5: u64 = _t1;
@@ -350,30 +349,30 @@ fun m::if_else_if($t0|c: bool, $t1|d: bool): u8 {
      var $t2|return: u8
      var $t3: bool
      var $t4: u8
-     var $t5: bool
-     var $t6: u8
+     var $t5: u8
+     var $t6: bool
      var $t7: u8
      var $t8: u8
   0: $t3 := move($t0)
-  1: if ($t3) goto 2 else goto 6
+  1: if ($t3) goto 2 else goto 9
   2: label L1
   3: $t4 := 1
   4: $t2 := $t4
-  5: goto 17
-  6: label L0
-  7: $t5 := move($t1)
-  8: if ($t5) goto 9 else goto 13
-  9: label L4
- 10: $t6 := 2
- 11: $t2 := $t6
- 12: goto 17
- 13: label L3
- 14: $t7 := 3
- 15: $t2 := $t7
- 16: goto 17
- 17: label L2
- 18: $t8 := move($t2)
- 19: return $t8
+  5: goto 6
+  6: label L4
+  7: $t5 := move($t2)
+  8: return $t5
+  9: label L0
+ 10: $t6 := move($t1)
+ 11: if ($t6) goto 12 else goto 16
+ 12: label L3
+ 13: $t7 := 2
+ 14: $t2 := $t7
+ 15: goto 6
+ 16: label L2
+ 17: $t8 := 3
+ 18: $t2 := $t8
+ 19: goto 6
 }
 
 --- Raw Generated AST
@@ -385,19 +384,19 @@ loop {
     _t2: u8 = _t4;
     break[1]
   };
-  _t5: bool = d;
+  _t6: bool = d;
   loop {
-    if (Not(_t5)) break;
-    _t6: u8 = 2;
-    _t2: u8 = _t6;
+    if (Not(_t6)) break;
+    _t7: u8 = 2;
+    _t2: u8 = _t7;
     break[1]
   };
-  _t7: u8 = 3;
-  _t2: u8 = _t7;
+  _t8: u8 = 3;
+  _t2: u8 = _t8;
   break
 };
-_t8: u8 = _t2;
-return _t8
+_t5: u8 = _t2;
+return _t5
 
 --- Assign-Transformed Generated AST
 loop {
@@ -483,22 +482,22 @@ fun m::if_else_with_shared_exp($t0|x: u64): u64 {
   8: $t9 := copy($t0)
   9: $t10 := 0
  10: $t11 := >($t9, $t10)
- 11: if ($t11) goto 12 else goto 18
+ 11: if ($t11) goto 12 else goto 21
  12: label L1
  13: $t12 := move($t0)
  14: $t13 := 1
  15: $t14 := +($t12, $t13)
  16: $t1 := $t14
- 17: goto 24
- 18: label L0
- 19: $t15 := move($t0)
- 20: $t16 := 1
- 21: $t17 := -($t15, $t16)
- 22: $t1 := $t17
- 23: goto 24
- 24: label L2
- 25: $t18 := move($t1)
- 26: return $t18
+ 17: goto 18
+ 18: label L2
+ 19: $t15 := move($t1)
+ 20: return $t15
+ 21: label L0
+ 22: $t16 := move($t0)
+ 23: $t17 := 1
+ 24: $t18 := -($t16, $t17)
+ 25: $t1 := $t18
+ 26: goto 18
 }
 
 --- Raw Generated AST
@@ -522,14 +521,14 @@ loop {
     _t1: u64 = _t14;
     break[1]
   };
-  _t15: u64 = x;
-  _t16: u64 = 1;
-  _t17: u64 = Sub(_t15, _t16);
-  _t1: u64 = _t17;
+  _t16: u64 = x;
+  _t17: u64 = 1;
+  _t18: u64 = Sub(_t16, _t17);
+  _t1: u64 = _t18;
   break
 };
-_t18: u64 = _t1;
-return _t18
+_t15: u64 = _t1;
+return _t15
 
 --- Assign-Transformed Generated AST
 x: u64 = Add(x, x);
diff --git a/third_party/move/move-model/bytecode/ast-generator-tests/tests/loops.exp b/third_party/move/move-model/bytecode/ast-generator-tests/tests/loops.exp
index 41922169af241..77603ad0468e7 100644
--- a/third_party/move/move-model/bytecode/ast-generator-tests/tests/loops.exp
+++ b/third_party/move/move-model/bytecode/ast-generator-tests/tests/loops.exp
@@ -54,14 +54,10 @@ fun m::loop_1($t0|c: u64): u64 {
  20: $t15 := %($t13, $t14)
  21: $t16 := 1
  22: $t17 := ==($t15, $t16)
- 23: if ($t17) goto 24 else goto 26
- 24: label L4
- 25: goto 28
- 26: label L3
- 27: goto 0
- 28: label L5
- 29: $t18 := move($t0)
- 30: return $t18
+ 23: if ($t17) goto 24 else goto 0
+ 24: label L3
+ 25: $t18 := move($t0)
+ 26: return $t18
 }
 
 --- Raw Generated AST
@@ -156,31 +152,27 @@ fun m::nested_loop($t0|x: u64): u64 {
   1: $t2 := copy($t0)
   2: $t3 := 0
   3: $t4 := >($t2, $t3)
-  4: if ($t4) goto 5 else goto 24
+  4: if ($t4) goto 5 else goto 22
   5: label L1
   6: $t5 := copy($t0)
   7: $t6 := 10
   8: $t7 := >($t5, $t6)
   9: if ($t7) goto 10 else goto 16
- 10: label L3
+ 10: label L2
  11: $t8 := move($t0)
  12: $t9 := 1
  13: $t10 := -($t8, $t9)
  14: $t0 := $t10
- 15: goto 18
- 16: label L2
- 17: goto 18
- 18: label L4
- 19: $t11 := move($t0)
- 20: $t12 := 1
- 21: $t13 := -($t11, $t12)
- 22: $t0 := $t13
- 23: goto 0
- 24: label L0
- 25: goto 26
- 26: label L6
- 27: $t14 := move($t0)
- 28: return $t14
+ 15: goto 16
+ 16: label L4
+ 17: $t11 := move($t0)
+ 18: $t12 := 1
+ 19: $t13 := -($t11, $t12)
+ 20: $t0 := $t13
+ 21: goto 0
+ 22: label L0
+ 23: $t14 := move($t0)
+ 24: return $t14
 }
 
 --- Raw Generated AST
@@ -256,7 +248,7 @@ fun m::while_1($t0|c: u64) {
      var $t5: u64
      var $t6: u64
      var $t7: u64
-  0: label L4
+  0: label L2
   1: $t2 := copy($t0)
   2: $t3 := 0
   3: $t4 := >($t2, $t3)
@@ -266,13 +258,9 @@ fun m::while_1($t0|c: u64) {
   7: $t6 := 1
   8: $t7 := -($t5, $t6)
   9: $t0 := $t7
- 10: goto 13
+ 10: goto 0
  11: label L0
- 12: goto 15
- 13: label L2
- 14: goto 0
- 15: label L3
- 16: return ()
+ 12: return ()
 }
 
 --- Raw Generated AST
@@ -341,33 +329,27 @@ fun m::while_2($t0|c: u64): u64 {
      var $t11: u64
      var $t12: u64
      var $t13: u64
-  0: label L6
+  0: label L4
   1: $t2 := copy($t0)
   2: $t3 := 0
   3: $t4 := >($t2, $t3)
-  4: if ($t4) goto 5 else goto 18
+  4: if ($t4) goto 5 else goto 16
   5: label L1
   6: $t5 := copy($t0)
   7: $t6 := 10
   8: $t7 := >=($t5, $t6)
-  9: if ($t7) goto 10 else goto 16
- 10: label L3
+  9: if ($t7) goto 10 else goto 0
+ 10: label L2
  11: $t8 := move($t0)
  12: $t9 := 10
  13: $t10 := -($t8, $t9)
  14: $t0 := $t10
- 15: goto 16
- 16: label L2
- 17: goto 20
- 18: label L0
- 19: goto 22
- 20: label L4
- 21: goto 0
- 22: label L5
- 23: $t11 := move($t0)
- 24: $t12 := 1
- 25: $t13 := +($t11, $t12)
- 26: return $t13
+ 15: goto 0
+ 16: label L0
+ 17: $t11 := move($t0)
+ 18: $t12 := 1
+ 19: $t13 := +($t11, $t12)
+ 20: return $t13
 }
 
 --- Raw Generated AST
@@ -445,39 +427,33 @@ fun m::while_3($t0|c: u64): u64 {
      var $t12: u64
      var $t13: u64
      var $t14: u64
-  0: label L8
+  0: label L5
   1: $t2 := copy($t0)
   2: $t3 := 0
   3: $t4 := >($t2, $t3)
-  4: if ($t4) goto 5 else goto 26
+  4: if ($t4) goto 5 else goto 24
   5: label L1
-  6: $t5 := copy($t0)
-  7: $t6 := 10
-  8: $t7 := >($t5, $t6)
-  9: if ($t7) goto 10 else goto 16
- 10: label L3
- 11: $t8 := move($t0)
- 12: $t9 := 10
- 13: $t10 := -($t8, $t9)
- 14: $t0 := $t10
- 15: goto 18
- 16: label L2
- 17: goto 20
- 18: label L4
- 19: goto 5
- 20: label L5
- 21: $t11 := move($t0)
- 22: $t12 := 1
- 23: $t13 := -($t11, $t12)
- 24: $t0 := $t13
- 25: goto 28
- 26: label L0
- 27: goto 30
- 28: label L6
- 29: goto 0
- 30: label L7
- 31: $t14 := move($t0)
- 32: return $t14
+  6: goto 7
+  7: label L2
+  8: $t5 := copy($t0)
+  9: $t6 := 10
+ 10: $t7 := >($t5, $t6)
+ 11: if ($t7) goto 12 else goto 18
+ 12: label L4
+ 13: $t8 := move($t0)
+ 14: $t9 := 10
+ 15: $t10 := -($t8, $t9)
+ 16: $t0 := $t10
+ 17: goto 7
+ 18: label L3
+ 19: $t11 := move($t0)
+ 20: $t12 := 1
+ 21: $t13 := -($t11, $t12)
+ 22: $t0 := $t13
+ 23: goto 0
+ 24: label L0
+ 25: $t14 := move($t0)
+ 26: return $t14
 }
 
 --- Raw Generated AST
diff --git a/third_party/move/move-model/bytecode/ast-generator-tests/tests/match.exp b/third_party/move/move-model/bytecode/ast-generator-tests/tests/match.exp
index f2f4c5f070e1f..0b545627c8eeb 100644
--- a/third_party/move/move-model/bytecode/ast-generator-tests/tests/match.exp
+++ b/third_party/move/move-model/bytecode/ast-generator-tests/tests/match.exp
@@ -16,41 +16,41 @@ fun m::id($t0|self: &0x815::m::Entity): u64 {
      var $t4: &0x815::m::Entity
      var $t5: &u64
      var $t6: u64
-     var $t7: &0x815::m::Entity
-     var $t8: bool
-     var $t9: &0x815::m::Entity
-     var $t10: &u64
-     var $t11: u64
-     var $t12: &0x815::m::Entity
-     var $t13: u64
+     var $t7: u64
+     var $t8: &0x815::m::Entity
+     var $t9: bool
+     var $t10: &0x815::m::Entity
+     var $t11: &u64
+     var $t12: u64
+     var $t13: &0x815::m::Entity
      var $t14: u64
   0: $t2 := copy($t0)
   1: $t3 := test_variant 0x815::m::Entity::Person($t2)
-  2: if ($t3) goto 3 else goto 9
+  2: if ($t3) goto 3 else goto 12
   3: label L1
   4: $t4 := move($t0)
   5: $t5 := borrow_variant_field<0x815::m::Entity::Person>.id($t4)
   6: $t6 := read_ref($t5)
   7: $t1 := $t6
-  8: goto 24
-  9: label L0
- 10: $t7 := copy($t0)
- 11: $t8 := test_variant 0x815::m::Entity::Institution($t7)
- 12: if ($t8) goto 13 else goto 19
- 13: label L4
- 14: $t9 := move($t0)
- 15: $t10 := borrow_variant_field<0x815::m::Entity::Institution>.id($t9)
- 16: $t11 := read_ref($t10)
- 17: $t1 := $t11
- 18: goto 24
- 19: label L3
- 20: $t12 := move($t0)
- 21: drop($t12)
- 22: $t13 := 14566554180833181697
- 23: abort($t13)
- 24: label L2
- 25: $t14 := move($t1)
- 26: return $t14
+  8: goto 9
+  9: label L4
+ 10: $t7 := move($t1)
+ 11: return $t7
+ 12: label L0
+ 13: $t8 := copy($t0)
+ 14: $t9 := test_variant 0x815::m::Entity::Institution($t8)
+ 15: if ($t9) goto 16 else goto 22
+ 16: label L3
+ 17: $t10 := move($t0)
+ 18: $t11 := borrow_variant_field<0x815::m::Entity::Institution>.id($t10)
+ 19: $t12 := read_ref($t11)
+ 20: $t1 := $t12
+ 21: goto 9
+ 22: label L2
+ 23: $t13 := move($t0)
+ 24: drop($t13)
+ 25: $t14 := 14566554180833181697
+ 26: abort($t14)
 }
 
 --- Raw Generated AST
@@ -65,22 +65,22 @@ loop {
     _t1: u64 = _t6;
     break[1]
   };
-  _t7: &Entity = self;
-  _t8: bool = test_variants m::Entity::Institution(_t7);
+  _t8: &Entity = self;
+  _t9: bool = test_variants m::Entity::Institution(_t8);
   loop {
-    if (_t8) break;
-    _t12: &Entity = self;
-    _t13: u64 = 14566554180833181697;
-    Abort(_t13)
+    if (_t9) break;
+    _t13: &Entity = self;
+    _t14: u64 = 14566554180833181697;
+    Abort(_t14)
   };
-  _t9: &Entity = self;
-  _t10: &u64 = select_variants m::Entity.Institution.id(_t9);
-  _t11: u64 = Deref(_t10);
-  _t1: u64 = _t11;
+  _t10: &Entity = self;
+  _t11: &u64 = select_variants m::Entity.Institution.id(_t10);
+  _t12: u64 = Deref(_t11);
+  _t1: u64 = _t12;
   break
 };
-_t14: u64 = _t1;
-return _t14
+_t7: u64 = _t1;
+return _t7
 
 --- Assign-Transformed Generated AST
 loop {
@@ -133,61 +133,61 @@ fun id2(self: Entity): u64 {
 --- Stackless Bytecode
 fun m::id2($t0|self: 0x815::m::Entity): u64 {
      var $t1|$t2: &0x815::m::Entity
-     var $t2|$t5: u64
+     var $t2|id: u64
      var $t3: &0x815::m::Entity
      var $t4: &0x815::m::Entity
      var $t5: bool
      var $t6: &0x815::m::Entity
-     var $t7: &u64
-     var $t8: u64
+     var $t7: bool
+     var $t8: 0x815::m::Entity
      var $t9: u64
-     var $t10: bool
-     var $t11: &0x815::m::Entity
-     var $t12: 0x815::m::Entity
-     var $t13: u64
-     var $t14: &0x815::m::Entity
-     var $t15: bool
-     var $t16: 0x815::m::Entity
-     var $t17: u64
-     var $t18: u64
-     var $t19: u64
+     var $t10: u64
+     var $t11: u64
+     var $t12: u64
+     var $t13: &0x815::m::Entity
+     var $t14: &u64
+     var $t15: u64
+     var $t16: u64
+     var $t17: bool
+     var $t18: &0x815::m::Entity
+     var $t19: 0x815::m::Entity
      var $t20: u64
   0: $t3 := borrow_local($t0)
   1: $t1 := $t3
   2: $t4 := copy($t1)
   3: $t5 := test_variant 0x815::m::Entity::Person($t4)
-  4: if ($t5) goto 5 else goto 19
-  5: label L0
-  6: $t6 := copy($t1)
-  7: $t7 := borrow_variant_field<0x815::m::Entity::Person>.id($t6)
-  8: $t8 := read_ref($t7)
-  9: $t9 := 0
- 10: $t10 := >($t8, $t9)
- 11: if ($t10) goto 12 else goto 19
- 12: label L3
- 13: $t11 := move($t1)
- 14: drop($t11)
- 15: $t12 := move($t0)
- 16: $t13 := unpack_variant 0x815::m::Entity::Person($t12)
- 17: $t2 := $t13
- 18: goto 33
- 19: label L2
- 20: $t14 := move($t1)
- 21: $t15 := test_variant 0x815::m::Entity::Institution($t14)
- 22: if ($t15) goto 23 else goto 29
- 23: label L7
- 24: $t16 := move($t0)
- 25: ($t17, $t18) := unpack_variant 0x815::m::Entity::Institution($t16)
- 26: drop($t18)
- 27: $t2 := $t17
- 28: goto 33
+  4: if ($t5) goto 22 else goto 5
+  5: label L2
+  6: $t6 := move($t1)
+  7: $t7 := test_variant 0x815::m::Entity::Institution($t6)
+  8: if ($t7) goto 9 else goto 18
+  9: label L4
+ 10: $t8 := move($t0)
+ 11: ($t9, $t10) := unpack_variant 0x815::m::Entity::Institution($t8)
+ 12: drop($t10)
+ 13: $t2 := $t9
+ 14: goto 15
+ 15: label L5
+ 16: $t11 := move($t2)
+ 17: return $t11
+ 18: label L3
+ 19: $t12 := 0
+ 20: $t2 := $t12
+ 21: goto 15
+ 22: label L0
+ 23: $t13 := copy($t1)
+ 24: $t14 := borrow_variant_field<0x815::m::Entity::Person>.id($t13)
+ 25: $t15 := read_ref($t14)
+ 26: $t16 := 0
+ 27: $t17 := >($t15, $t16)
+ 28: if ($t17) goto 29 else goto 5
  29: label L6
- 30: $t19 := 0
- 31: $t2 := $t19
- 32: goto 33
- 33: label L5
- 34: $t20 := move($t2)
- 35: return $t20
+ 30: $t18 := move($t1)
+ 31: drop($t18)
+ 32: $t19 := move($t0)
+ 33: $t20 := unpack_variant 0x815::m::Entity::Person($t19)
+ 34: $t2 := $t20
+ 35: goto 15
 }
 
 --- Raw Generated AST
@@ -198,33 +198,33 @@ _t5: bool = test_variants m::Entity::Person(_t4);
 loop {
   loop {
     if (Not(_t5)) break;
-    _t6: &Entity = _t1;
-    _t7: &u64 = select_variants m::Entity.Person.id(_t6);
-    _t8: u64 = Deref(_t7);
-    _t9: u64 = 0;
-    _t10: bool = Gt(_t8, _t9);
-    if (Not(_t10)) break;
-    _t11: &Entity = _t1;
-    _t12: Entity = self;
-    m::Entity::Person{ id: _t13 } = _t12;
-    _t2: u64 = _t13;
+    _t13: &Entity = _t1;
+    _t14: &u64 = select_variants m::Entity.Person.id(_t13);
+    _t15: u64 = Deref(_t14);
+    _t16: u64 = 0;
+    _t17: bool = Gt(_t15, _t16);
+    if (Not(_t17)) break;
+    _t18: &Entity = _t1;
+    _t19: Entity = self;
+    m::Entity::Person{ id: _t20 } = _t19;
+    _t2: u64 = _t20;
     break[1]
   };
-  _t14: &Entity = _t1;
-  _t15: bool = test_variants m::Entity::Institution(_t14);
+  _t6: &Entity = _t1;
+  _t7: bool = test_variants m::Entity::Institution(_t6);
   loop {
-    if (Not(_t15)) break;
-    _t16: Entity = self;
-    m::Entity::Institution{ id: _t17, admin: _t18 } = _t16;
-    _t2: u64 = _t17;
+    if (Not(_t7)) break;
+    _t8: Entity = self;
+    m::Entity::Institution{ id: _t9, admin: _t10 } = _t8;
+    _t2: u64 = _t9;
     break[1]
   };
-  _t19: u64 = 0;
-  _t2: u64 = _t19;
+  _t12: u64 = 0;
+  _t2: u64 = _t12;
   break
 };
-_t20: u64 = _t2;
-return _t20
+_t11: u64 = _t2;
+return _t11
 
 --- Assign-Transformed Generated AST
 _t1: &Entity = Borrow(Immutable)(self);
@@ -232,14 +232,14 @@ loop {
   loop {
     if (Not(test_variants m::Entity::Person(_t1))) break;
     if (Not(Gt(Deref(select_variants m::Entity.Person.id(_t1)), 0))) break;
-    m::Entity::Person{ id: _t13 } = self;
-    _t2: u64 = _t13;
+    m::Entity::Person{ id: _t20 } = self;
+    _t2: u64 = _t20;
     break[1]
   };
   loop {
     if (Not(test_variants m::Entity::Institution(_t1))) break;
-    m::Entity::Institution{ id: _t17, admin: _t18 } = self;
-    _t2: u64 = _t17;
+    m::Entity::Institution{ id: _t9, admin: _t10 } = self;
+    _t2: u64 = _t9;
     break[1]
   };
   _t2: u64 = 0;
@@ -250,12 +250,12 @@ return _t2
 --- If-Transformed Generated AST
 _t1: &Entity = Borrow(Immutable)(self);
 if And(test_variants m::Entity::Person(_t1), Gt(Deref(select_variants m::Entity.Person.id(_t1)), 0)) {
-  m::Entity::Person{ id: _t13 } = self;
-  _t2: u64 = _t13
+  m::Entity::Person{ id: _t20 } = self;
+  _t2: u64 = _t20
 } else {
   if test_variants m::Entity::Institution(_t1) {
-    m::Entity::Institution{ id: _t17, admin: _t18 } = self;
-    _t2: u64 = _t17
+    m::Entity::Institution{ id: _t9, admin: _t10 } = self;
+    _t2: u64 = _t9
   } else {
     _t2: u64 = 0
   }
@@ -264,23 +264,23 @@ return _t2
 
 --- Var-Bound Generated AST
 {
-  let _t18: u64;
+  let _t10: u64;
   {
-    let _t17: u64;
+    let _t9: u64;
     {
       let _t2: u64;
       {
-        let _t13: u64;
+        let _t20: u64;
         {
           let _t1: &Entity;
           _t1: &Entity = Borrow(Immutable)(self);
           if And(test_variants m::Entity::Person(_t1), Gt(Deref(select_variants m::Entity.Person.id(_t1)), 0)) {
-            m::Entity::Person{ id: _t13 } = self;
-            _t2: u64 = _t13
+            m::Entity::Person{ id: _t20 } = self;
+            _t2: u64 = _t20
           } else {
             if test_variants m::Entity::Institution(_t1) {
-              m::Entity::Institution{ id: _t17, admin: _t18 } = self;
-              _t2: u64 = _t17
+              m::Entity::Institution{ id: _t9, admin: _t10 } = self;
+              _t2: u64 = _t9
             } else {
               _t2: u64 = 0
             }
@@ -312,18 +312,18 @@ module 0x815::m {
         _t1
     }
     fun id2(self: Entity): u64 {
-        let _t18;
-        let _t17;
+        let _t10;
+        let _t9;
         let _t2;
-        let _t13;
+        let _t20;
         let _t1;
         _t1 = &self;
         if ((_t1 is Person) && *&_t1.id > 0) {
-            Entity::Person{id: _t13} = self;
-            _t2 = _t13
+            Entity::Person{id: _t20} = self;
+            _t2 = _t20
         } else if (_t1 is Institution) {
-            Entity::Institution{id: _t17,admin: _t18} = self;
-            _t2 = _t17
+            Entity::Institution{id: _t9,admin: _t10} = self;
+            _t2 = _t9
         } else _t2 = 0;
         _t2
     }
diff --git a/third_party/move/move-model/bytecode/src/fat_loop.rs b/third_party/move/move-model/bytecode/src/fat_loop.rs
index 224baa7e8bca3..0aee1dcc78654 100644
--- a/third_party/move/move-model/bytecode/src/fat_loop.rs
+++ b/third_party/move/move-model/bytecode/src/fat_loop.rs
@@ -450,7 +450,8 @@ impl FatLoopBuilder {
         cfg: &StacklessControlFlowGraph,
         sub_loops: &[NaturalLoop<BlockId>],
     ) -> Vec<Vec<Bytecode>> {
-        sub_loops
+        let mut id_label_map = BTreeMap::new();
+        let blocks: Vec<(BlockId, Vec<Bytecode>)> = sub_loops
             .iter()
             .flat_map(|l| l.loop_body.iter())
             .map(|block_id| match cfg.content(*block_id) {
@@ -458,12 +459,47 @@ impl FatLoopBuilder {
                     panic!("A loop body should never contain a dummy block")
                 },
                 BlockContent::Basic { lower, upper } => {
+                    if let Some(lbl) = code[*lower as usize].get_label_inner_opt() {
+                        id_label_map.insert(*block_id, lbl);
+                    }
                     let block: Vec<_> = (*lower..=*upper)
                         .map(|i| code.get(i as usize).unwrap().clone())
                         .collect();
-                    block
+                    (*block_id, block)
                 },
             })
-            .collect()
+            .collect();
+        let mut results = vec![];
+        for (i, (block_id, block)) in blocks.iter().enumerate() {
+            // if this block is a fallthough block, we need to remove it by inserting a jump to the correct block
+            // because the fatloop algorithm doesn't support fallthrough
+            if cfg.successors(*block_id).len() == 1 && !block[block.len() - 1].is_branching() {
+                let successor_id = cfg.successors(*block_id).first().unwrap();
+                let successor_label_opt = id_label_map.get(successor_id);
+                if successor_label_opt.is_some()
+                    && i != blocks.len() - 1
+                    && !blocks.get(i + 1).unwrap().1.is_empty()
+                {
+                    if let Some(lbl) = blocks.get(i + 1).unwrap().1[0].get_label_inner_opt() {
+                        let successor_label = *successor_label_opt.unwrap();
+                        if lbl != successor_label {
+                            let mut new_block = block.clone();
+                            // Inserted bc is used for jumping to its successor so
+                            // we just use the attr_id of its previous bc
+                            new_block.push(Bytecode::Jump(
+                                block[block.len() - 1].get_attr_id(),
+                                Label::new(successor_label as usize),
+                            ));
+                            results.push(new_block);
+                            continue;
+                        }
+                    }
+                }
+                results.push(block.clone());
+            } else {
+                results.push(block.clone());
+            }
+        }
+        results
     }
 }
diff --git a/third_party/move/move-model/bytecode/src/stackless_bytecode.rs b/third_party/move/move-model/bytecode/src/stackless_bytecode.rs
index 0fc475a821a39..e7720423b267f 100644
--- a/third_party/move/move-model/bytecode/src/stackless_bytecode.rs
+++ b/third_party/move/move-model/bytecode/src/stackless_bytecode.rs
@@ -541,6 +541,13 @@ impl Bytecode {
         self.is_possibly_branching() || self.is_always_branching()
     }
 
+    pub fn get_label_inner_opt(&self) -> Option<u16> {
+        match self {
+            Bytecode::Label(_, l) => Some(l.0),
+            _ => None,
+        }
+    }
+
     /// Returns true if the bytecode is spec-only.
     pub fn is_spec_only(&self) -> bool {
         use Bytecode::*;
diff --git a/third_party/move/move-prover/tests/sources/functional/aborts_if.v2_exp b/third_party/move/move-prover/tests/sources/functional/aborts_if.v2_exp
index 58e49d00fd5d7..8179a66a39bdf 100644
--- a/third_party/move/move-prover/tests/sources/functional/aborts_if.v2_exp
+++ b/third_party/move/move-prover/tests/sources/functional/aborts_if.v2_exp
@@ -102,7 +102,7 @@ error: abort not covered by any of the `aborts_if` clauses
     ┌─ tests/sources/functional/aborts_if.move:139:5
     │
 137 │           if (x == 2 || x == 3) abort 1;
-    │                         ------ abort happened here with code 0x1
+    │           ----------------------------- abort happened here with code 0x1
 138 │       }
 139 │ ╭     spec abort_at_2_or_3_total_incorrect {
 140 │ │         // Counter check that we get an error message without the pragma.
@@ -114,6 +114,8 @@ error: abort not covered by any of the `aborts_if` clauses
     =     at tests/sources/functional/aborts_if.move:136: abort_at_2_or_3_total_incorrect
     =         x = <redacted>
     =     at tests/sources/functional/aborts_if.move:137: abort_at_2_or_3_total_incorrect
+    =     at tests/sources/functional/aborts_if.move:136: abort_at_2_or_3_total_incorrect
+    =     at tests/sources/functional/aborts_if.move:137: abort_at_2_or_3_total_incorrect
     =         <redacted> = <redacted>
     =     at tests/sources/functional/aborts_if.move:137: abort_at_2_or_3_total_incorrect
     =         ABORTED
@@ -127,16 +129,17 @@ error: function does not abort under this condition
     =     at tests/sources/functional/aborts_if.move:145: abort_at_2_or_3_spec_incorrect
     =         x = <redacted>
     =     at tests/sources/functional/aborts_if.move:146: abort_at_2_or_3_spec_incorrect
+    =     at tests/sources/functional/aborts_if.move:145: abort_at_2_or_3_spec_incorrect
+    =     at tests/sources/functional/aborts_if.move:146: abort_at_2_or_3_spec_incorrect
     =         <redacted> = <redacted>
     =     at tests/sources/functional/aborts_if.move:146: abort_at_2_or_3_spec_incorrect
-    =     at tests/sources/functional/aborts_if.move:147: abort_at_2_or_3_spec_incorrect
     =     at tests/sources/functional/aborts_if.move:151: abort_at_2_or_3_spec_incorrect (spec)
 
 error: abort not covered by any of the `aborts_if` clauses
     ┌─ tests/sources/functional/aborts_if.move:157:5
     │
 155 │           if (x == 2 || x == 3) abort 1;
-    │                         ------ abort happened here with code 0x1
+    │           ----------------------------- abort happened here with code 0x1
 156 │       }
 157 │ ╭     spec abort_at_2_or_3_strict_incorrect {
 158 │ │         // When the strict mode is enabled, no aborts_if clause means aborts_if false.
@@ -147,6 +150,8 @@ error: abort not covered by any of the `aborts_if` clauses
     =     at tests/sources/functional/aborts_if.move:154: abort_at_2_or_3_strict_incorrect
     =         x = <redacted>
     =     at tests/sources/functional/aborts_if.move:155: abort_at_2_or_3_strict_incorrect
+    =     at tests/sources/functional/aborts_if.move:154: abort_at_2_or_3_strict_incorrect
+    =     at tests/sources/functional/aborts_if.move:155: abort_at_2_or_3_strict_incorrect
     =         <redacted> = <redacted>
     =     at tests/sources/functional/aborts_if.move:155: abort_at_2_or_3_strict_incorrect
     =         ABORTED
diff --git a/third_party/move/move-prover/tests/sources/functional/bug_15044.move b/third_party/move/move-prover/tests/sources/functional/bug_15044.move
new file mode 100644
index 0000000000000..c493e679451b1
--- /dev/null
+++ b/third_party/move/move-prover/tests/sources/functional/bug_15044.move
@@ -0,0 +1,52 @@
+module 0x42::comparator {
+    use std::vector;
+
+    const EQUAL: u8 = 0;
+    const SMALLER: u8 = 1;
+    const GREATER: u8 = 2;
+
+    struct Result has drop {
+        inner: u8,
+    }
+
+    spec compare_u8_vector(left: vector<u8>, right: vector<u8>): Result {
+        pragma unroll = 5;
+
+        let left_length = len(left);
+        let right_length = len(right);
+
+        ensures (result.inner == EQUAL) ==> (
+            (left_length == right_length) &&
+                (forall i: u64 where i < left_length: left[i] == right[i])
+        );
+    }
+
+    // Performs a comparison of two vector<u8>s or byte vectors
+    public fun compare_u8_vector(left: vector<u8>, right: vector<u8>): Result {
+        let left_length = vector::length(&left);
+        let right_length = vector::length(&right);
+
+        let idx = 0;
+
+        while (idx < left_length && idx < right_length) {
+            let left_byte = *vector::borrow(&left, idx);
+            let right_byte = *vector::borrow(&right, idx);
+
+            if (left_byte < right_byte) {
+                return Result { inner: SMALLER }
+            } else if (left_byte > right_byte) {
+                return Result { inner: GREATER }
+            };
+            idx = idx + 1;
+        };
+
+        if (left_length < right_length) {
+            Result { inner: SMALLER }
+        } else if (left_length > right_length) {
+            Result { inner: GREATER }
+        } else {
+            Result { inner: EQUAL }
+        }
+    }
+
+}
diff --git a/third_party/move/move-prover/tests/sources/functional/bv_aborts.v2_exp b/third_party/move/move-prover/tests/sources/functional/bv_aborts.v2_exp
index bcdb810526eb5..2d106370311c2 100644
--- a/third_party/move/move-prover/tests/sources/functional/bv_aborts.v2_exp
+++ b/third_party/move/move-prover/tests/sources/functional/bv_aborts.v2_exp
@@ -8,22 +8,24 @@ error: function does not abort under this condition
    =     at tests/sources/functional/bv_aborts.move:11: assert_with_spec
    =         x = <redacted>
    =     at tests/sources/functional/bv_aborts.move:12: assert_with_spec
-   =     at tests/sources/functional/bv_aborts.move:13: assert_with_spec
    =     at tests/sources/functional/bv_aborts.move:16: assert_with_spec (spec)
 
 error: abort not covered by any of the `aborts_if` clauses
    ┌─ tests/sources/functional/bv_aborts.move:14:5
    │
-12 │           assert!(x > 815);
-   │           ------ abort happened here
-13 │       }
-14 │ ╭     spec assert_with_spec  {
-15 │ │         // This will fail
-16 │ │         aborts_if x > 815 with std::error::internal(0) | (0xCA26CBD9BE << 24);
-17 │ │     }
-   │ ╰─────^
+11 │         fun assert_with_spec(x: u64) {
+   │   ╭──────────────────────────────────'
+12 │   │         assert!(x > 815);
+13 │   │     }
+   │   ╰─────' abort happened here
+14 │ ╭       spec assert_with_spec  {
+15 │ │           // This will fail
+16 │ │           aborts_if x > 815 with std::error::internal(0) | (0xCA26CBD9BE << 24);
+17 │ │       }
+   │ ╰───────^
    │
    =     at tests/sources/functional/bv_aborts.move:11: assert_with_spec
    =         x = <redacted>
    =     at tests/sources/functional/bv_aborts.move:12: assert_with_spec
+   =     at tests/sources/functional/bv_aborts.move:11: assert_with_spec
    =         ABORTED
diff --git a/third_party/move/move-prover/tests/sources/functional/choice.v2_exp b/third_party/move/move-prover/tests/sources/functional/choice.v2_exp
index 2928962906277..a5d5c96f98fbe 100644
--- a/third_party/move/move-prover/tests/sources/functional/choice.v2_exp
+++ b/third_party/move/move-prover/tests/sources/functional/choice.v2_exp
@@ -11,7 +11,6 @@ error: post-condition does not hold
    =         return = <redacted>
    =     at tests/sources/functional/choice.move:17: simple_incorrect
    =         result = <redacted>
-   =     at tests/sources/functional/choice.move:18: simple_incorrect
    =     at tests/sources/functional/choice.move:22: simple_incorrect (spec)
    =         `TRACE(choose x: u64 where x >= 4 && x <= 5)` = <redacted>
 
diff --git a/third_party/move/move-prover/tests/sources/functional/emits.v2_exp b/third_party/move/move-prover/tests/sources/functional/emits.v2_exp
index fc5f3c931bad3..2387c17c66674 100644
--- a/third_party/move/move-prover/tests/sources/functional/emits.v2_exp
+++ b/third_party/move/move-prover/tests/sources/functional/emits.v2_exp
@@ -76,8 +76,8 @@ error: function does not emit the expected event
     =         x = <redacted>
     =         handle = <redacted>
     =     at tests/sources/functional/emits.move:106: conditional_wrong_condition_incorrect
+    =     at tests/sources/functional/emits.move:107: conditional_wrong_condition_incorrect
     =         handle = <redacted>
-    =     at tests/sources/functional/emits.move:109: conditional_wrong_condition_incorrect
     =     at tests/sources/functional/emits.move:111: conditional_wrong_condition_incorrect (spec)
 
 error: function does not emit the expected event
@@ -90,8 +90,8 @@ error: function does not emit the expected event
     =         x = <redacted>
     =         handle = <redacted>
     =     at tests/sources/functional/emits.move:115: conditional_missing_condition_incorrect
+    =     at tests/sources/functional/emits.move:116: conditional_missing_condition_incorrect
     =         handle = <redacted>
-    =     at tests/sources/functional/emits.move:118: conditional_missing_condition_incorrect
     =     at tests/sources/functional/emits.move:120: conditional_missing_condition_incorrect (spec)
 
 error: function does not emit the expected event
@@ -110,7 +110,6 @@ error: function does not emit the expected event
     =     at tests/sources/functional/emits.move:152: conditional_multiple_incorrect
     =     at tests/sources/functional/emits.move:149: conditional_multiple_incorrect
     =         handle = <redacted>
-    =     at tests/sources/functional/emits.move:155: conditional_multiple_incorrect
     =     at tests/sources/functional/emits.move:157: conditional_multiple_incorrect (spec)
     =     at tests/sources/functional/emits.move:158: conditional_multiple_incorrect (spec)
     =     at tests/sources/functional/emits.move:159: conditional_multiple_incorrect (spec)
@@ -131,7 +130,6 @@ error: function does not emit the expected event
     =     at tests/sources/functional/emits.move:182: conditional_multiple_same_incorrect
     =     at tests/sources/functional/emits.move:179: conditional_multiple_same_incorrect
     =         handle = <redacted>
-    =     at tests/sources/functional/emits.move:185: conditional_multiple_same_incorrect
     =     at tests/sources/functional/emits.move:187: conditional_multiple_same_incorrect (spec)
     =     at tests/sources/functional/emits.move:188: conditional_multiple_same_incorrect (spec)
     =     at tests/sources/functional/emits.move:189: conditional_multiple_same_incorrect (spec)
diff --git a/third_party/move/move-prover/tests/sources/functional/enum_abort.v2_exp b/third_party/move/move-prover/tests/sources/functional/enum_abort.v2_exp
index ae88dbefbd545..e913c0054b4b3 100644
--- a/third_party/move/move-prover/tests/sources/functional/enum_abort.v2_exp
+++ b/third_party/move/move-prover/tests/sources/functional/enum_abort.v2_exp
@@ -103,6 +103,7 @@ error: abort not covered by any of the `aborts_if` clauses
     =         <redacted> = <redacted>
     =     at tests/sources/functional/enum_abort.move:122: test_match_abort
     =         _z = <redacted>
+    =     at tests/sources/functional/enum_abort.move:123: test_match_abort
     =     at tests/sources/functional/enum_abort.move:122: test_match_abort
     =         <redacted> = <redacted>
     =     at tests/sources/functional/enum_abort.move:122: test_match_abort
diff --git a/third_party/move/move-prover/tests/sources/functional/global_invariants.v2_exp b/third_party/move/move-prover/tests/sources/functional/global_invariants.v2_exp
index 6d7b62ce06171..30735438b7dc4 100644
--- a/third_party/move/move-prover/tests/sources/functional/global_invariants.v2_exp
+++ b/third_party/move/move-prover/tests/sources/functional/global_invariants.v2_exp
@@ -27,7 +27,6 @@ error: global memory invariant does not hold
    =     at ../move-stdlib/sources/signer.move:13: address_of
    =         result = <redacted>
    =     at ../move-stdlib/sources/signer.move:14: address_of
-   =     at tests/sources/functional/global_invariants.move:55: remove_S_invalid
    =     at tests/sources/functional/global_invariants.move:56: remove_S_invalid
    =     at ../move-stdlib/sources/signer.move:12: address_of
    =         s = <redacted>
@@ -50,7 +49,6 @@ error: global memory invariant does not hold
    =     at ../move-stdlib/sources/signer.move:13: address_of
    =         result = <redacted>
    =     at ../move-stdlib/sources/signer.move:14: address_of
-   =     at tests/sources/functional/global_invariants.move:64: remove_R_invalid
    =     at tests/sources/functional/global_invariants.move:65: remove_R_invalid
    =     at ../move-stdlib/sources/signer.move:12: address_of
    =         s = <redacted>
diff --git a/third_party/move/move-prover/tests/sources/functional/is_txn_signer.v2_exp b/third_party/move/move-prover/tests/sources/functional/is_txn_signer.v2_exp
index 10e0b83097ae0..9d2fee976c7e8 100644
--- a/third_party/move/move-prover/tests/sources/functional/is_txn_signer.v2_exp
+++ b/third_party/move/move-prover/tests/sources/functional/is_txn_signer.v2_exp
@@ -31,7 +31,6 @@ error: unknown assertion failed
    =     at ../move-stdlib/sources/signer.move:13: address_of
    =         result = <redacted>
    =     at ../move-stdlib/sources/signer.move:14: address_of
-   =     at tests/sources/functional/is_txn_signer.move:30: f4_incorrect
    =     at tests/sources/functional/is_txn_signer.move:31: f4_incorrect
 
 error: precondition does not hold at this call
diff --git a/third_party/move/move-prover/tests/sources/functional/loop_unroll.v2_exp b/third_party/move/move-prover/tests/sources/functional/loop_unroll.v2_exp
index 0cbe6434c9e40..c561bd90334e9 100644
--- a/third_party/move/move-prover/tests/sources/functional/loop_unroll.v2_exp
+++ b/third_party/move/move-prover/tests/sources/functional/loop_unroll.v2_exp
@@ -24,8 +24,6 @@ error: abort not covered by any of the `aborts_if` clauses
     =     at tests/sources/functional/loop_unroll.move:97: t6_failure
     =         <redacted> = <redacted>
     =     at tests/sources/functional/loop_unroll.move:97: t6_failure
-    =     at tests/sources/functional/loop_unroll.move:95: t6_failure
-    =     at tests/sources/functional/loop_unroll.move:90: t6_failure
     =     at tests/sources/functional/loop_unroll.move:92: t6_failure
     =     at tests/sources/functional/loop_unroll.move:94: t6_failure
     =     at tests/sources/functional/loop_unroll.move:90: t6_failure
@@ -34,8 +32,6 @@ error: abort not covered by any of the `aborts_if` clauses
     =         i = <redacted>
     =     at tests/sources/functional/loop_unroll.move:97: t6_failure
     =         <redacted> = <redacted>
-    =     at tests/sources/functional/loop_unroll.move:95: t6_failure
-    =     at tests/sources/functional/loop_unroll.move:90: t6_failure
     =     at tests/sources/functional/loop_unroll.move:91: t6_failure
     =     at tests/sources/functional/loop_unroll.move:92: t6_failure
     =     at tests/sources/functional/loop_unroll.move:94: t6_failure
@@ -45,8 +41,6 @@ error: abort not covered by any of the `aborts_if` clauses
     =         i = <redacted>
     =     at tests/sources/functional/loop_unroll.move:97: t6_failure
     =         <redacted> = <redacted>
-    =     at tests/sources/functional/loop_unroll.move:95: t6_failure
-    =     at tests/sources/functional/loop_unroll.move:90: t6_failure
     =     at tests/sources/functional/loop_unroll.move:91: t6_failure
     =     at tests/sources/functional/loop_unroll.move:92: t6_failure
     =     at tests/sources/functional/loop_unroll.move:94: t6_failure
@@ -56,8 +50,6 @@ error: abort not covered by any of the `aborts_if` clauses
     =         i = <redacted>
     =     at tests/sources/functional/loop_unroll.move:97: t6_failure
     =         <redacted> = <redacted>
-    =     at tests/sources/functional/loop_unroll.move:95: t6_failure
-    =     at tests/sources/functional/loop_unroll.move:90: t6_failure
     =     at tests/sources/functional/loop_unroll.move:91: t6_failure
     =     at tests/sources/functional/loop_unroll.move:92: t6_failure
     =     at tests/sources/functional/loop_unroll.move:94: t6_failure
diff --git a/third_party/move/move-prover/tests/sources/functional/loops.v2_exp b/third_party/move/move-prover/tests/sources/functional/loops.v2_exp
index 20030b26d9475..72bdc9792f620 100644
--- a/third_party/move/move-prover/tests/sources/functional/loops.v2_exp
+++ b/third_party/move/move-prover/tests/sources/functional/loops.v2_exp
@@ -61,7 +61,6 @@ error: induction case of the loop invariant does not hold
     =     at tests/sources/functional/loops.move:122: nested_loop_outer_invariant_incorrect
     =     enter loop, variable(s) y havocked and reassigned
     =         y = <redacted>
-    =     at tests/sources/functional/loops.move:123: nested_loop_outer_invariant_incorrect
     =     at tests/sources/functional/loops.move:128: nested_loop_outer_invariant_incorrect
     =     at tests/sources/functional/loops.move:131: nested_loop_outer_invariant_incorrect
     =         <redacted> = <redacted>
@@ -89,7 +88,6 @@ error: induction case of the loop invariant does not hold
     =     at tests/sources/functional/loops.move:150: nested_loop_inner_invariant_incorrect
     =         <redacted> = <redacted>
     =         y = <redacted>
-    =     at tests/sources/functional/loops.move:143: nested_loop_inner_invariant_incorrect
     =     at tests/sources/functional/loops.move:145: nested_loop_inner_invariant_incorrect
 
 error: induction case of the loop invariant does not hold
@@ -149,7 +147,6 @@ error: induction case of the loop invariant does not hold
     =     at tests/sources/functional/loops.move:227: loop_invariant_induction_invalid
     =         <redacted> = <redacted>
     =         x = <redacted>
-    =     at tests/sources/functional/loops.move:226: loop_invariant_induction_invalid
     =     at tests/sources/functional/loops.move:221: loop_invariant_induction_invalid
     =     at tests/sources/functional/loops.move:223: loop_invariant_induction_invalid
 
diff --git a/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp b/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp
index 294a93f8a4f5a..d6f72efdfd3a5 100644
--- a/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp
+++ b/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp
@@ -38,10 +38,10 @@ error: induction case of the loop invariant does not hold
    =     enter loop, variable(s) x, y havocked and reassigned
    =         x = <redacted>
    =         y = <redacted>
-   =     at tests/sources/functional/loops_with_memory_ops.move:75: nested_loop2
    =     at tests/sources/functional/loops_with_memory_ops.move:80: nested_loop2
    =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
    =         a = <redacted>
+   =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
    =         b = <redacted>
    =     at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2
    =         <redacted> = <redacted>
@@ -96,14 +96,13 @@ error: unknown assertion failed
    =     enter loop, variable(s) x, y havocked and reassigned
    =         x = <redacted>
    =         y = <redacted>
-   =     at tests/sources/functional/loops_with_memory_ops.move:75: nested_loop2
    =     at tests/sources/functional/loops_with_memory_ops.move:80: nested_loop2
    =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
-   =         b = <redacted>
+   =         a = <redacted>
    =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
+   =         b = <redacted>
    =     at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2
    =         <redacted> = <redacted>
    =         i = <redacted>
    =     at tests/sources/functional/loops_with_memory_ops.move:86: nested_loop2
-   =     at tests/sources/functional/loops_with_memory_ops.move:87: nested_loop2
    =     at tests/sources/functional/loops_with_memory_ops.move:93: nested_loop2
diff --git a/third_party/move/move-prover/tests/sources/functional/macro_verification.v2_exp b/third_party/move/move-prover/tests/sources/functional/macro_verification.v2_exp
index d78843e68141f..782a513256905 100644
--- a/third_party/move/move-prover/tests/sources/functional/macro_verification.v2_exp
+++ b/third_party/move/move-prover/tests/sources/functional/macro_verification.v2_exp
@@ -80,7 +80,6 @@ error: post-condition does not hold
    =         `invariant sum == spec_sum(v, i);` = <redacted>
    =     at tests/sources/functional/macro_verification.move:43: reduce
    =         <redacted> = <redacted>
-   =     at tests/sources/functional/macro_verification.move:43: reduce
    =     at tests/sources/functional/macro_verification.move:52: reduce
    =         <redacted> = <redacted>
    =     at tests/sources/functional/macro_verification.move:40: reduce
@@ -132,7 +131,6 @@ error: post-condition does not hold
    =     at tests/sources/functional/macro_verification.move:50: reduce
    =     at tests/sources/functional/macro_verification.move:43: reduce
    =         <redacted> = <redacted>
-   =     at tests/sources/functional/macro_verification.move:43: reduce
    =     at tests/sources/functional/macro_verification.move:52: reduce
    =         <redacted> = <redacted>
    =     at tests/sources/functional/macro_verification.move:40: reduce
diff --git a/third_party/move/move-prover/tests/sources/functional/script_incorrect.v2_exp b/third_party/move/move-prover/tests/sources/functional/script_incorrect.v2_exp
index 924116a65e5f2..8334205070254 100644
--- a/third_party/move/move-prover/tests/sources/functional/script_incorrect.v2_exp
+++ b/third_party/move/move-prover/tests/sources/functional/script_incorrect.v2_exp
@@ -24,7 +24,6 @@ error: abort not covered by any of the `aborts_if` clauses
    =     at ../move-stdlib/sources/signer.move:13: address_of
    =         result = <redacted>
    =     at ../move-stdlib/sources/signer.move:14: address_of
-   =     at tests/sources/functional/script_provider.move:9: register
    =     at tests/sources/functional/script_provider.move:10: register
    =         <redacted> = <redacted>
    =     at tests/sources/functional/script_provider.move:10: register
diff --git a/third_party/move/tools/move-decompiler/tests/fixed_point32.exp b/third_party/move/tools/move-decompiler/tests/fixed_point32.exp
index d23d905418232..f88e3a6e3ab55 100644
--- a/third_party/move/tools/move-decompiler/tests/fixed_point32.exp
+++ b/third_party/move/tools/move-decompiler/tests/fixed_point32.exp
@@ -13,17 +13,16 @@ module 0x1::fixed_point32 {
         *&(&self).value >> 32u8
     }
     public fun create_from_rational(numerator: u64, denominator: u64): FixedPoint32 {
-        let _t5;
+        let _t6;
+        let _t4;
         let _t3;
-        let _t2;
-        _t2 = (numerator as u128) << 64u8;
         _t3 = (denominator as u128) << 32u8;
         if (!(_t3 != 0u128)) abort 65537;
-        _t2 = _t2 / _t3;
-        if (_t2 != 0u128) _t5 = true else _t5 = numerator == 0;
-        if (!_t5) abort 131077;
-        if (!(_t2 <= 18446744073709551615u128)) abort 131077;
-        FixedPoint32{value: _t2 as u64}
+        _t4 = ((numerator as u128) << 64u8) / _t3;
+        if (_t4 != 0u128) _t6 = true else _t6 = numerator == 0;
+        if (!_t6) abort 131077;
+        if (!(_t4 <= 18446744073709551615u128)) abort 131077;
+        FixedPoint32{value: _t4 as u64}
     }
     public fun create_from_raw_value(value: u64): FixedPoint32 {
         FixedPoint32{value: value}
diff --git a/third_party/move/tools/move-decompiler/tests/option.exp b/third_party/move/tools/move-decompiler/tests/option.exp
index 63ad169dc1dcd..a1c20a0c2ad05 100644
--- a/third_party/move/tools/move-decompiler/tests/option.exp
+++ b/third_party/move/tools/move-decompiler/tests/option.exp
@@ -33,20 +33,20 @@ module 0x1::option {
         _t3
     }
     public fun destroy_none<Element>(self: Option<Element>) {
-        let _t5;
+        let _t4;
         if (!is_none<Element>(&self)) abort 262144;
-        Option<Element>{vec: _t5} = self;
-        vector::destroy_empty<Element>(_t5);
+        Option<Element>{vec: _t4} = self;
+        vector::destroy_empty<Element>(_t4);
     }
     public fun is_none<Element>(self: &Option<Element>): bool {
         vector::is_empty<Element>(&self.vec)
     }
     public fun destroy_some<Element>(self: Option<Element>): Element {
         let _t1;
-        let _t6;
+        let _t5;
         if (!is_some<Element>(&self)) abort 262145;
-        Option<Element>{vec: _t6} = self;
-        _t1 = _t6;
+        Option<Element>{vec: _t5} = self;
+        _t1 = _t5;
         vector::destroy_empty<Element>(_t1);
         vector::pop_back<Element>(&mut _t1)
     }
diff --git a/third_party/move/tools/move-decompiler/tests/simple_map.exp b/third_party/move/tools/move-decompiler/tests/simple_map.exp
index 43ed9bea7d2aa..056957264c034 100644
--- a/third_party/move/tools/move-decompiler/tests/simple_map.exp
+++ b/third_party/move/tools/move-decompiler/tests/simple_map.exp
@@ -40,13 +40,13 @@ module 0x1::simple_map {
         option::none<u64>()
     }
     public fun remove<Key: store, Value: store>(self: &mut SimpleMap<Key, Value>, key: &Key): (Key, Value) {
-        let _t20;
-        let _t19;
+        let _t17;
+        let _t16;
         let _t2;
         _t2 = find<Key,Value>(/*freeze*/self, key);
         if (!option::is_some<u64>(&_t2)) abort error::invalid_argument(2);
-        Element<Key,Value>{key: _t19,value: _t20} = vector::swap_remove<Element<Key, Value>>(&mut self.data, option::extract<u64>(&mut _t2));
-        (_t19, _t20)
+        Element<Key,Value>{key: _t16,value: _t17} = vector::swap_remove<Element<Key, Value>>(&mut self.data, option::extract<u64>(&mut _t2));
+        (_t16, _t17)
     }
     public fun add<Key: store, Value: store>(self: &mut SimpleMap<Key, Value>, key: Key, value: Value) {
         if (!option::is_none<u64>(&find<Key,Value>(/*freeze*/self, &key))) abort error::invalid_argument(1);
diff --git a/third_party/move/tools/move-decompiler/tests/string.exp b/third_party/move/tools/move-decompiler/tests/string.exp
index 00de95bdbb469..6df58cc3c6ebb 100644
--- a/third_party/move/tools/move-decompiler/tests/string.exp
+++ b/third_party/move/tools/move-decompiler/tests/string.exp
@@ -34,13 +34,15 @@ module 0x1::string {
     }
     native fun internal_is_char_boundary(v: &vector<u8>, i: u64): bool;
     public fun sub_string(self: &String, i: u64, j: u64): String {
+        let _t7;
+        let _t6;
         let _t5;
         let _t3;
         _t3 = &self.bytes;
         if (j <= vector::length<u8>(_t3)) _t5 = i <= j else _t5 = false;
-        if (_t5) _t5 = internal_is_char_boundary(_t3, i) else _t5 = false;
-        if (_t5) _t5 = internal_is_char_boundary(_t3, j) else _t5 = false;
-        if (!_t5) abort 2;
+        if (_t5) _t6 = internal_is_char_boundary(_t3, i) else _t6 = false;
+        if (_t6) _t7 = internal_is_char_boundary(_t3, j) else _t7 = false;
+        if (!_t7) abort 2;
         String{bytes: internal_sub_string(_t3, i, j)}
     }
     public fun is_empty(self: &String): bool {