void A:mutate_arg (C a0, int a1) {
  guard = tt;
  ret(obj_level(a0)) = pc;
  ret(obj_level(this)) = obj_level(this);
  ret(a0.~>a0) = tt;
}
A A:mutate_args (A a0, C a1, int a2) {
  guard = tt;
  ret(level()) = pc ⊔ level(a0) ⊔ level(a1) ⊔ level(a2) ⊔ level(this) ⊔ obj_level(a0) ⊔ obj_level(a1) ⊔ obj_level(this);
  ret(obj_level()) = pc ⊔ level(a0) ⊔ level(a1) ⊔ level(a2) ⊔ level(this) ⊔ obj_level(a0) ⊔ obj_level(a1) ⊔ obj_level(this) ⊔ (if ret(~a0) then obj_level(a0) else ⊥) ⊔ (if ret(~this) then obj_level(this) else ⊥);
  ret(obj_level(a0)) = pc ⊔ level(a0) ⊔ level(a1) ⊔ level(a2) ⊔ level(this) ⊔ obj_level(a0) ⊔ obj_level(a1) ⊔ obj_level(this);
  ret(obj_level(a1)) = pc ⊔ level(a0) ⊔ level(a1) ⊔ level(a2) ⊔ level(this) ⊔ obj_level(a0) ⊔ obj_level(a1) ⊔ obj_level(this);
  ret(obj_level(this)) = obj_level(this);
  ret(~a0) = tt;
  ret(~this) = tt;
  ret(a1.~>a1) = tt;
}