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

[variant baseline]
public fun Test::test_borrow_imm<#0>(): u64 {
     var $t0|r: &Test::R<#0>
     var $t1: address
     var $t2: &Test::R<#0>
     var $t3: &Test::R<#0>
     var $t4: &u64
     var $t5: u64
  0: $t1 := 0x1
  1: $t2 := borrow_global<Test::R<#0>>($t1)
  2: $t0 := $t2
  3: $t3 := move($t0)
  4: $t4 := borrow_field<Test::R<#0>>.x($t3)
  5: $t5 := read_ref($t4)
  6: return $t5
}


[variant baseline]
public fun Test::test_borrow_mut<#0>(): u64 {
     var $t0|r: &mut Test::R<#0>
     var $t1: address
     var $t2: &mut Test::R<#0>
     var $t3: u64
     var $t4: &mut Test::R<#0>
     var $t5: &mut Test::S
     var $t6: &mut u64
     var $t7: u64
     var $t8: &mut Test::R<#0>
     var $t9: &mut u64
     var $t10: &mut Test::R<#0>
     var $t11: &u64
     var $t12: u64
  0: $t1 := 0x1
  1: $t2 := borrow_global<Test::R<#0>>($t1)
  2: $t0 := $t2
  3: $t3 := 2
  4: $t4 := copy($t0)
  5: $t5 := borrow_field<Test::R<#0>>.s($t4)
  6: $t6 := borrow_field<Test::S>.y($t5)
  7: write_ref($t6, $t3)
  8: $t7 := 3
  9: $t8 := copy($t0)
 10: $t9 := borrow_field<Test::R<#0>>.x($t8)
 11: write_ref($t9, $t7)
 12: $t10 := move($t0)
 13: $t11 := borrow_field<Test::R<#0>>.x($t10)
 14: $t12 := read_ref($t11)
 15: return $t12
}


[variant baseline]
public fun Test::test_borrow_mut_local(): Test::R<u64> {
     var $t0|d: Test::R<u64>
     var $t1|r: &mut Test::R<u64>
     var $t2: u64
     var $t3: u64
     var $t4: Test::S
     var $t5: u64
     var $t6: Test::R<u64>
     var $t7: &mut Test::R<u64>
     var $t8: u64
     var $t9: &mut Test::R<u64>
     var $t10: &mut Test::S
     var $t11: &mut u64
     var $t12: u64
     var $t13: &mut Test::R<u64>
     var $t14: &mut u64
     var $t15: Test::R<u64>
  0: $t2 := 2
  1: $t3 := 1
  2: $t4 := pack Test::S($t3)
  3: $t5 := 0
  4: $t6 := pack Test::R<u64>($t2, $t4, $t5)
  5: $t0 := $t6
  6: $t7 := borrow_local($t0)
  7: $t1 := $t7
  8: $t8 := 2
  9: $t9 := copy($t1)
 10: $t10 := borrow_field<Test::R<u64>>.s($t9)
 11: $t11 := borrow_field<Test::S>.y($t10)
 12: write_ref($t11, $t8)
 13: $t12 := 3
 14: $t13 := move($t1)
 15: $t14 := borrow_field<Test::R<u64>>.x($t13)
 16: write_ref($t14, $t12)
 17: $t15 := move($t0)
 18: return $t15
}

============ after pipeline `data_invariant_instrumentation` ================

[variant verification]
public fun Test::test_borrow_imm<#0>(): u64 {
     var $t0|r: Test::R<#0>
     var $t1: address
     var $t2: Test::R<#0>
     var $t3: num
     var $t4: u64
  0: assume forall $rsc: ResourceDomain<Test::R<#0>>(): And(WellFormed($rsc), And(Gt(select Test::R.x($rsc), select Test::S.y(select Test::R.s($rsc))), Gt(select Test::S.y(select Test::R.s($rsc)), 0)))
  1: $t1 := 0x1
  2: $t2 := get_global<Test::R<#0>>($t1) on_abort goto 6 with $t3
  3: $t4 := get_field<Test::R<#0>>.x($t2)
  4: label L1
  5: return $t4
  6: label L2
  7: abort($t3)
}


[variant verification]
public fun Test::test_borrow_mut<#0>(): u64 {
     var $t0|r: &mut Test::R<#0>
     var $t1: address
     var $t2: &mut Test::R<#0>
     var $t3: num
     var $t4: u64
     var $t5: &mut Test::S
     var $t6: &mut u64
     var $t7: u64
     var $t8: &mut u64
     var $t9: u64
  0: assume forall $rsc: ResourceDomain<Test::R<#0>>(): And(WellFormed($rsc), And(Gt(select Test::R.x($rsc), select Test::S.y(select Test::R.s($rsc))), Gt(select Test::S.y(select Test::R.s($rsc)), 0)))
  1: $t1 := 0x1
  2: $t2 := borrow_global<Test::R<#0>>($t1) on_abort goto 19 with $t3
  3: $t4 := 2
  4: $t5 := borrow_field<Test::R<#0>>.s($t2)
  5: $t6 := borrow_field<Test::S>.y($t5)
  6: write_ref($t6, $t4)
  7: write_back[Reference($t5).y (u64)]($t6)
  8: write_back[Reference($t2).s (Test::S)]($t5)
  9: $t7 := 3
 10: $t8 := borrow_field<Test::R<#0>>.x($t2)
 11: write_ref($t8, $t7)
 12: write_back[Reference($t2).x (u64)]($t8)
 13: $t9 := get_field<Test::R<#0>>.x($t2)
     # data invariant at tests/data_invariant_instrumentation/borrow.move:13:9+18
     # VC: data invariant does not hold at tests/data_invariant_instrumentation/borrow.move:13:9+18
 14: assert Gt(select Test::R.x($t2), select Test::S.y(select Test::R.s($t2)))
     # data invariant at tests/data_invariant_instrumentation/borrow.move:17:9+16
     # VC: data invariant does not hold at tests/data_invariant_instrumentation/borrow.move:17:9+16
 15: assert Gt(select Test::S.y(select Test::R.s($t2)), 0)
 16: write_back[Test::R<#0>@]($t2)
 17: label L1
 18: return $t9
 19: label L2
 20: abort($t3)
}


[variant verification]
public fun Test::test_borrow_mut_local(): Test::R<u64> {
     var $t0|d: Test::R<u64>
     var $t1|r: &mut Test::R<u64>
     var $t2: u64
     var $t3: u64
     var $t4: Test::S
     var $t5: u64
     var $t6: &mut Test::R<u64>
     var $t7: u64
     var $t8: &mut Test::S
     var $t9: &mut u64
     var $t10: u64
     var $t11: &mut u64
     var $t12: Test::R<u64>
  0: $t2 := 2
  1: $t3 := 1
  2: $t4 := pack Test::S($t3)
     # data invariant at tests/data_invariant_instrumentation/borrow.move:17:9+16
     # VC: data invariant does not hold at tests/data_invariant_instrumentation/borrow.move:17:9+16
  3: assert Gt(select Test::S.y($t4), 0)
  4: $t5 := 0
  5: $t0 := pack Test::R<u64>($t2, $t4, $t5)
     # data invariant at tests/data_invariant_instrumentation/borrow.move:13:9+18
     # VC: data invariant does not hold at tests/data_invariant_instrumentation/borrow.move:13:9+18
  6: assert Gt(select Test::R.x($t0), select Test::S.y(select Test::R.s($t0)))
  7: $t6 := borrow_local($t0)
  8: $t7 := 2
  9: $t8 := borrow_field<Test::R<u64>>.s($t6)
 10: $t9 := borrow_field<Test::S>.y($t8)
 11: write_ref($t9, $t7)
 12: write_back[Reference($t8).y (u64)]($t9)
 13: write_back[Reference($t6).s (Test::S)]($t8)
 14: $t10 := 3
 15: $t11 := borrow_field<Test::R<u64>>.x($t6)
 16: write_ref($t11, $t10)
 17: write_back[Reference($t6).x (u64)]($t11)
     # data invariant at tests/data_invariant_instrumentation/borrow.move:13:9+18
     # VC: data invariant does not hold at tests/data_invariant_instrumentation/borrow.move:13:9+18
 18: assert Gt(select Test::R.x($t6), select Test::S.y(select Test::R.s($t6)))
     # data invariant at tests/data_invariant_instrumentation/borrow.move:17:9+16
     # VC: data invariant does not hold at tests/data_invariant_instrumentation/borrow.move:17:9+16
 19: assert Gt(select Test::S.y(select Test::R.s($t6)), 0)
 20: write_back[LocalRoot($t0)@]($t6)
 21: trace_local[d]($t0)
 22: $t12 := move($t0)
 23: label L1
 24: return $t12
}