============ initial translation from Move ================

[variant baseline]
fun Counter::call_increment1($t0|s: &mut Counter::S) {
     var $t1: &mut Counter::S
     var $t2: &mut u64
  0: $t1 := move($t0)
  1: $t2 := borrow_field<Counter::S>.f($t1)
  2: Counter::increment1($t2)
  3: return ()
}


[variant baseline]
fun Counter::call_increment2($t0|a: address) {
     var $t1: address
     var $t2: &mut Counter::S
  0: $t1 := move($t0)
  1: $t2 := borrow_global<Counter::S>($t1)
  2: Counter::increment2($t2)
  3: return ()
}


[variant baseline]
fun Counter::increment1($t0|i: &mut u64) {
     var $t1: &mut u64
     var $t2: u64
     var $t3: u64
     var $t4: u64
     var $t5: &mut u64
  0: $t1 := copy($t0)
  1: $t2 := read_ref($t1)
  2: $t3 := 1
  3: $t4 := +($t2, $t3)
  4: $t5 := move($t0)
  5: write_ref($t5, $t4)
  6: return ()
}


[variant baseline]
fun Counter::increment2($t0|s: &mut Counter::S) {
     var $t1: &mut Counter::S
     var $t2: &mut u64
     var $t3: u64
     var $t4: u64
     var $t5: u64
     var $t6: &mut Counter::S
     var $t7: &mut u64
  0: $t1 := copy($t0)
  1: $t2 := borrow_field<Counter::S>.f($t1)
  2: $t3 := read_ref($t2)
  3: $t4 := 1
  4: $t5 := +($t3, $t4)
  5: $t6 := move($t0)
  6: $t7 := borrow_field<Counter::S>.f($t6)
  7: write_ref($t7, $t5)
  8: return ()
}

============ after pipeline `read_write_set` ================

[variant baseline]
fun Counter::call_increment1($t0|s: &mut Counter::S) {
     var $t1: &mut Counter::S
     var $t2: &mut u64
     # Accesses:
     # Formal(0): Read
     # Formal(0)/f: ReadWrite
     #
     # Locals:
     #
  0: $t1 := move($t0)
  1: $t2 := borrow_field<Counter::S>.f($t1)
  2: Counter::increment1($t2)
  3: return ()
}


[variant baseline]
fun Counter::call_increment2($t0|a: address) {
     var $t1: address
     var $t2: &mut Counter::S
     # Accesses:
     # Formal(0): Read
     # Formal(0)/0x1::Counter::S: Read
     # Formal(0)/0x1::Counter::S/f: ReadWrite
     #
     # Locals:
     #
  0: $t1 := move($t0)
  1: $t2 := borrow_global<Counter::S>($t1)
  2: Counter::increment2($t2)
  3: return ()
}


[variant baseline]
fun Counter::increment1($t0|i: &mut u64) {
     var $t1: &mut u64
     var $t2: u64
     var $t3: u64
     var $t4: u64
     var $t5: &mut u64
     # Accesses:
     # Formal(0): ReadWrite
     #
     # Locals:
     #
  0: $t1 := copy($t0)
  1: $t2 := read_ref($t1)
  2: $t3 := 1
  3: $t4 := +($t2, $t3)
  4: $t5 := move($t0)
  5: write_ref($t5, $t4)
  6: return ()
}


[variant baseline]
fun Counter::increment2($t0|s: &mut Counter::S) {
     var $t1: &mut Counter::S
     var $t2: &mut u64
     var $t3: u64
     var $t4: u64
     var $t5: u64
     var $t6: &mut Counter::S
     var $t7: &mut u64
     # Accesses:
     # Formal(0): Read
     # Formal(0)/f: ReadWrite
     #
     # Locals:
     #
  0: $t1 := copy($t0)
  1: $t2 := borrow_field<Counter::S>.f($t1)
  2: $t3 := read_ref($t2)
  3: $t4 := 1
  4: $t5 := +($t3, $t4)
  5: $t6 := move($t0)
  6: $t7 := borrow_field<Counter::S>.f($t6)
  7: write_ref($t7, $t5)
  8: return ()
}