int A:nice1 (C a0, C a1, int a2) {
  guard = tt;
  ret(level()) = ⊥;
  ret(obj_level(a0)) = obj_level(a0);
  ret(obj_level(a1)) = obj_level(a1);
  ret(obj_level(this)) = obj_level(this);
  ret(a0.~>a0) = a0.~>a0;
  ret(a0.~>a1) = a0.~>a1;
  ret(a1.~>a0) = a1.~>a0;
  ret(a1.~>a1) = a1.~>a1;
}
int A:nice2 (C a0, C a1, int a2) {
  guard = tt;
  ret(level()) = level(a0) ⊔ level(a1) ⊔ level(a2) ⊔ level(this) ⊔ obj_level(a0) ⊔ obj_level(a1) ⊔ obj_level(this);
  ret(obj_level(a0)) = obj_level(a0);
  ret(obj_level(a1)) = obj_level(a1);
  ret(obj_level(this)) = obj_level(this);
  ret(a0.~>a0) = a0.~>a0;
  ret(a0.~>a1) = a0.~>a1;
  ret(a1.~>a0) = a1.~>a0;
  ret(a1.~>a1) = a1.~>a1;
}
C A:nice_allocC (C a0, C a1, int a2) {
  guard = tt;
  ret(level()) = ⊥;
  ret(obj_level()) = (if ret(~a0) then obj_level(a0) else ⊥) ⊔ (if ret(~a1) then obj_level(a1) else ⊥) ⊔ (if ret(a0.~>) then obj_level(a0) else ⊥) ⊔ (if ret(a1.~>) then obj_level(a1) else ⊥);
  ret(obj_level(a0)) = obj_level(a0);
  ret(obj_level(a1)) = obj_level(a1);
  ret(obj_level(this)) = obj_level(this);
  ret(~a0) = ff;
  ret(~a1) = ff;
  ret(.~>a0) = tt;
  ret(.~>a1) = tt;
  ret(a0.~>) = ff;
  ret(a0.~>a0) = a0.~>a0;
  ret(a0.~>a1) = a0.~>a1;
  ret(a1.~>) = ff;
  ret(a1.~>a0) = a1.~>a0;
  ret(a1.~>a1) = a1.~>a1;
}
void A:nice_log (C a0, int a1) {
  guard = pc ⊑ ⊥ ∧ level(a0) ⊔ level(a1) ⊔ level(this) ⊔ obj_level(a0) ⊔ obj_level(this) ⊑ ⊥;
  ret(obj_level(a0)) = obj_level(a0);
  ret(obj_level(this)) = obj_level(this);
  ret(a0.~>a0) = a0.~>a0;
}