Report of INVALID for missing measure

[SimonGuilloud]

[Warning ] src/Resolution.scala:72:7: Could not infer measure for function negationNormalForm
             def negationNormalForm(f: Formula): Formula = {
...

[Warning ]  - Result for 'measure missing' VC for negationNormalForm @72:7:
[Warning ] false
[Warning ] src/Resolution.scala:72:7:  => INVALID
             def negationNormalForm(f: Formula): Formula = {
                 ^
[Warning ] Found counter-example:
[Warning ]   (Empty model)

def negationNormalForm(f: Formula): Formula = {
    f match
      case Predicate(name, children) => Predicate(name, children)
      case And(l, r) => And(negationNormalForm(l), negationNormalForm(r))
      case Or(l, r) => Or(negationNormalForm(l), negationNormalForm(r))
      case Implies(left, right) => Or(negationNormalForm(Neg(left)), negationNormalForm(right)) // not(left) or right
      case Neg(And(l, r)) => Or(negationNormalForm(Neg(negationNormalForm(l))), negationNormalForm(Neg(negationNormalForm(r))))
      case Neg(Or(l, r)) => And(negationNormalForm(Neg(l)), negationNormalForm(Neg(r)))
      case Neg(Implies(l, r)) => And(negationNormalForm(l), negationNormalForm(Neg(r)))
      case Neg(Forall(variable, inner)) => Exists(variable, negationNormalForm(Neg(inner)))
      case Neg(Exists(variable, inner)) => Forall(variable, negationNormalForm(Neg(inner)))
      case Neg(Predicate(name, children)) => Neg(Predicate(name, children))
      case Neg(Neg(f)) => negationNormalForm(f)
      case Forall(variable, inner) => Forall(variable, negationNormalForm(inner))
      case Exists(variable, inner) => Exists(variable, negationNormalForm(inner))

  }.ensuring(res =>
    res.isNNF
  )

The measure is non-trivial (pair on "number of non-Neg nodes", then "number of Neg nodes" for example) so it is expected that stainless does not find it, but I believe the function is terminating nonetheless, so it probably shouldn't report invalid.