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

[variant baseline]
fun Demo::f1($t0|addr: address) {
     var $t1: address
     var $t2: bool
     var $t3: u8
     var $t4: address
     var $t5: &mut Demo::S1<bool>
     var $t6: &mut u8
     var $t7: address
     var $t8: bool
     var $t9: u8
     var $t10: address
     var $t11: &mut Demo::S1<u64>
     var $t12: &mut u8
  0: $t1 := copy($t0)
  1: $t2 := exists<Demo::S1<bool>>($t1)
  2: if ($t2) goto 3 else goto 10
  3: label L0
  4: $t3 := 0
  5: $t4 := copy($t0)
  6: $t5 := borrow_global<Demo::S1<bool>>($t4)
  7: $t6 := borrow_field<Demo::S1<bool>>.v($t5)
  8: write_ref($t6, $t3)
  9: goto 10
 10: label L2
 11: $t7 := copy($t0)
 12: $t8 := exists<Demo::S1<u64>>($t7)
 13: if ($t8) goto 14 else goto 21
 14: label L3
 15: $t9 := 0
 16: $t10 := move($t0)
 17: $t11 := borrow_global<Demo::S1<u64>>($t10)
 18: $t12 := borrow_field<Demo::S1<u64>>.v($t11)
 19: write_ref($t12, $t9)
 20: goto 21
 21: label L5
 22: return ()
}

============ after pipeline `global_invariant_analysis` ================

[variant verification]
fun Demo::f1($t0|addr: address) {
     var $t1: bool
     var $t2: u8
     var $t3: &mut Demo::S1<bool>
     var $t4: num
     var $t5: &mut u8
     var $t6: bool
     var $t7: u8
     var $t8: &mut Demo::S1<u64>
     var $t9: &mut u8
  0: $t1 := exists<Demo::S1<bool>>($t0)
  1: if ($t1) goto 2 else goto 9
  2: label L0
  3: $t2 := 0
  4: $t3 := borrow_global<Demo::S1<bool>>($t0) on_abort goto 22 with $t4
  5: $t5 := borrow_field<Demo::S1<bool>>.v($t3)
  6: write_ref($t5, $t2)
  7: write_back[Reference($t3).v (u8)]($t5)
  8: write_back[Demo::S1<bool>@]($t3)
  9: label L2
 10: $t6 := exists<Demo::S1<u64>>($t0)
 11: if ($t6) goto 12 else goto 19
 12: label L3
 13: $t7 := 0
 14: $t8 := borrow_global<Demo::S1<u64>>($t0) on_abort goto 22 with $t4
 15: $t9 := borrow_field<Demo::S1<u64>>.v($t8)
 16: write_ref($t9, $t7)
 17: write_back[Reference($t8).v (u8)]($t9)
 18: write_back[Demo::S1<u64>@]($t8)
 19: label L5
 20: label L6
 21: return ()
 22: label L7
 23: abort($t4)
}


********* Result of global invariant instrumentation *********

Demo::f1: [
  entrypoint {
    assume @0 = [
      <> -> [
        <bool, #0>
        <u64, #1>
      ]
    ]
  }
  0: $t1 := exists<Demo::S1<bool>>($t0) {}
  8: write_back[Demo::S1<bool>@]($t3) {
    assert @0 = [
      <> -> [
        <bool, #0>
      ]
    ]
  }
  10: $t6 := exists<Demo::S1<u64>>($t0) {}
  18: write_back[Demo::S1<u64>@]($t8) {
    assert @0 = [
      <> -> [
        <u64, #1>
      ]
    ]
  }
  exitpoint {}
]

********* Global invariants by ID *********

@0 => invariant<T1, T2>
            (exists<S1<T1>>(@0x2) && exists<S2<T2>>(@0x2))
                ==> global<S1<T1>>(@0x2).v == 0;