Ghost Erasure produces wrong Go Code

[ArquintL]

The binary operation involving a function call in the following Gobra code is ghost erased to foo(n - 1) + 1 instead of foo(n - 1):

func foo(n int) (ghost res int) {
    if (n <= 0) {
        return 0
    } else {
        res = foo(n-1) + 1
    }
}

[jcp19]

Also, the following method in example infinite_list.gobra is incorrectly printed.

• Gobra code

requires infList(ptr)
requires n >= 0
pure func nth(ptr *node, n int) (r int) {
  return unfolding infList(ptr) in n == 0 ? ptr.value : nth(ptr.next, n-1)
}

• Translated code

func nth(ptr *node, n int) (r int) {
  return 
}

[jcp19]

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