============ after processor `global_invariant_instrumenter` ================

[variant verification]
pub fun Trafo::dummy_need_signer_use_in_move($t0|account: signer): address {
     var $t1: address
  0: assume WellFormed($t0)
  1: trace_local[account]($t0)
     # >> opaque call: $t1 := Signer::address_of($t0)
  2: nop
  3: assume Eq<address>($t1, Signer::spec_address_of($t0))
  4: assume WellFormed($t1)
     # << opaque call: $t1 := Signer::address_of($t0)
  5: nop
  6: trace_return[0]($t1)
  7: label L1
  8: return $t1
}


[variant verification]
pub fun Trafo::publish($t0|account: signer, $t1|x: u64) {
     var $t2: Trafo::R
     var $t3: num
  0: assume WellFormed($t0)
  1: assume WellFormed($t1)
  2: assume forall $rsc: ResourceDomain<Trafo::R>(): WellFormed($rsc)
  3: @0 := save_mem(Trafo::R)
  4: trace_local[account]($t0)
  5: trace_local[x]($t1)
  6: $t2 := pack Trafo::R($t1)
  7: move_to<Trafo::R>($t2, $t0) on_abort goto 13 with $t3
  8: label L1
     # VC: function does not abort under this condition at resource.move:14:7+26
  9: assert Not(exists[@0]<Trafo::R>(Trafo::addr$2[]($t0)))
     # VC: post-condition does not hold at resource.move:15:7+24
 10: assert exists<Trafo::R>(Trafo::addr$2($t0))
     # VC: post-condition does not hold at resource.move:16:7+31
 11: assert Eq<u64>(select Trafo::R.x(global<Trafo::R>(Trafo::addr$2($t0))), $t1)
 12: return ()
 13: label L2
     # VC: abort not covered by any of the `aborts_if` clauses at resource.move:12:3+175
 14: assert exists[@0]<Trafo::R>(Trafo::addr$2[]($t0))
 15: abort($t3)
}