PrimitiveSize functions should not be generated when termination checking is off?

[drganam]

Stainless seems to generate size functions even when they are not needed:

Input:

sealed abstract class Exp
case class Num(param0: BigInt) extends Exp
case class Plus(param0: Exp, param1: Exp) extends Exp
case class Minus(param0: Exp, param1: Exp) extends Exp

def eval(exp: Exp): BigInt = exp match
  case Num(a) => a
  case Plus(a, b) => eval(a) + eval(b)
  case Minus(a, b) => eval(a) - eval(b)

Output trees (when running with --infer-measures=no --check-measures=no): eval$1, @synthetic ExpPrimitiveSize$0, @synthetic ObjectPrimitiveSize$0, @synthetic BigIntAbs$0