rjraya

Could you please display the trees that you obtain before and after measure inference?

@romac I did not solve chain processor as measures during my internship, so the solution that is in master is not really mine and I don't really follow what it...

Do you know in which processor did the measure inference succeed previously? @yannbolllger

@yannbolliger if you debug with the option --debug=termination you should see for each function who "cleared" the function termination problem, something like "Cleared by Relation Processor". A processor is the...

This occurred for instance in: frontends/benchmarks/verification/valid/Count.scala Note that 2. still gives an error, as attached. [stainless-stack-trace.txt](https://github.com/epfl-lara/stainless/files/6457478/stainless-stack-trace.txt)

Just added a `getType` call in both parameters of `instantiation`: ``` protected def unapplyAccessor(unapplied: Expr, id: Identifier, up: UnapplyPattern)(implicit s: Symbols): Expr = { val fd = s.lookupFunction(id) .filter(_.params.size ==...

Complete trace of unapplyAccessor: [error.txt](https://github.com/epfl-lara/stainless/files/6457855/error.txt)

It seems like the culprit is rather: `unapplyAccessorResultType` who was missing 3 getTypes and `unapplyAccessor` who was missing one. Indeed, generalizing Inox's methods to support dependent types seems like most...