Non-termination in small programs

[jcp19]

The following was found by @HSMF

The following program causes Gobra to not terminate:

package main

func foo() {
        goto end
end:
}

Perhaps more surprising, Gobra does not terminate even if we pass the flag --noVerify, which indicates that this problem arises at some other step in our infrastructure.

[jcp19]

Another example:

requires x > 0.0
ensures  res > 0.0
func newton(x float32, y float32) (res float32) {
	return x/2 + y / 2 / x
}

[gottschali]

another one:

func main() {
	assert 1e2 > 0
}