Nicolas Voirol

> The two builds might have been killed due to memory or time usage, can we increase the limits? Yeah, it should be possible. The memory limit is hard-coded in...

Shouldn't we be using Scala's `eq` and `ne` for reference equality?

Agreed about the different notions of equality, although I would stay away from user-defined equality for now since it's a significant project. A simple preliminary solution would be to only...

Hmm, this is quite strange. It seems like all the function params are incorrectly transformed inside the body. I don't think the `dropRefinements` function is the problem. In order to...

Ah, the information I need is indeed inside the missing types. Maybe you can call `variablesOf` on the transformed `fullBody` and print the free variables (with unique ids)? That might...

You can either 1. add support for dependent types in the `instantiation` method, or 2. erase them with `getType` inside [unapplyAccessor](https://github.com/epfl-lara/stainless/blob/43aa5c786ca5b969e442e8078b1c38fa3dae3a41/core/src/main/scala/stainless/ast/Expressions.scala#L164). The first option will give better support for dependent...

The stack trace by itself isn't very useful, please show us your code changes at least.

Hmm, that should remove all refinement types, so they are probably not the issue here. Maybe add some print statements to debug what's going on.

Well those two types certainly look unifiable to me. The only issue I can think of is an id mismatch for the `Option` type, but I don't know where it...

I went back and looked at all your traces: I don't see any indication that instantiation is failing in `unapplyAccessor`. I would expect to see an exception with message `"Unapply...