Nicolas Voirol

We can consider adding an `Unchecked` annotation when the `ADTSelector` is created in the AdtSpecialization phase otherwise: https://github.com/epfl-lara/stainless/blob/940261c8669beba76cff59fc05eea2ddfd4a6988/core/src/main/scala/stainless/extraction/oo/AdtSpecialization.scala#L73 The assertions will still be injected but they won't result in verification...

You can just add a let-binding to circumvent this.

Should we maybe add a new annotation which only ignores directly nested assertions/checks (instead of all checks within the annotated expression)?

Or rather, shouldn't we fix the `SizedADT` issue instead of introducing a bunch of extra hacks to work around it?

Can't we fix this by adding an untyped let-binding? Somethere where the let-binding type isn't checked but rather inferred. We can control this through a flag on the `ValDef` or...

I assume the lambdas are actually structurally different by the time they get to Inox in this example, something like `(x: T, y: T) => thiss.leq(x, y)` and `(x: T,...

> So, the example alone might just be a false precondition that (assuming we are sound) is not satisfiable? From the POV of Inox lambda equality semantics, yes, that's just...

That's weird, it almost looks like `variablesOf` is missing a free variable. Maybe if you add some debugging (with unique ids) under `instantiateExpr` I can try to understand what's going...

We don't need `--feeling-lucky` but using it with `--codegen` gives us the best regression suite we have for the codegen evaluator. @jad-hamza if you add some debugging around the assertion...

If someone adds some debugging lines around the offending assertion and pastes the output here I can try to guestimate what's going wrong.