============ after processor `verification_analysis` ================

[variant baseline]
pub fun Trafo::opaque_caller($t0|addr: address) {
  0: trace_local[addr]($t0)
  1: Trafo::opaque_decr($t0)
  2: Trafo::opaque_decr($t0)
  3: return ()
}


[variant baseline]
pub fun Trafo::opaque_decr($t0|addr: address) {
     var $t1|r: &mut Trafo::R
     var $t2: &mut Trafo::R
     var $t3: u64
     var $t4: u64
     var $t5: u64
     var $t6: &mut u64
  0: trace_local[addr]($t0)
  1: $t2 := borrow_global<Trafo::R>($t0)
  2: trace_local[r]($t2)
  3: $t3 := get_field<Trafo::R>.x($t2)
  4: $t4 := 1
  5: $t5 := -($t3, $t4)
  6: $t6 := borrow_field<Trafo::R>.x($t2)
  7: write_ref($t6, $t5)
  8: write_back[Reference($t2)]($t6)
  9: write_back[Trafo::R]($t2)
 10: return ()
}