João Pereira

Also, the following method in example `infinite_list.gobra` is incorrectly printed. - Gobra code ```go requires infList(ptr) requires n >= 0 pure func nth(ptr *node, n int) (r int) { return...

Besides, `import "sync"` is wrongly translated to `import sync sync`

that is rather awkward. It should definitely pass with the overflow checks at the very least. I will look into that

The reason for this seems to be due to the fact that the overflow ast transformer does not generate assert statements for the bounds of the parameters. It should be...

Actually, this works but the message is not very informative - here, this is rejected because the call to `t.f()` is not annotated with spec.

I'm reopening this, people will continue being confused until we provide a better error message