Stack overflow from Boogie

[atoiz]

Stack overflow error by Boogie when verifying this code:

field f: Ref
field g: Ref

method multi_nested_6_0(x: Ref) {
	inhale acc(x.f, 1/1000000)
	inhale acc(x.g, 1/1000000)
	inhale acc(x.g.f, 1/1000000)
	inhale acc(x.g.g, 1/1000000)
	inhale acc(x.f.f, 1/1000000)
	inhale acc(x.f.g, 1/1000000)
	inhale x.g.f == x.f.g
	inhale acc(x.g.g.f, 1/1000000)
	inhale acc(x.g.g.g, 1/1000000)
	inhale acc(x.f.g.f, 1/1000000)
	inhale acc(x.f.g.g, 1/1000000)
	inhale acc(x.f.f.f, 1/1000000)
	inhale acc(x.f.f.g, 1/1000000)
	inhale x.g.g.f == x.f.g.g
	inhale x.f.g.f == x.f.f.g
	inhale acc(x.g.g.g.f, 1/1000000)
	inhale acc(x.g.g.g.g, 1/1000000)
	inhale acc(x.f.g.g.f, 1/1000000)
	inhale acc(x.f.g.g.g, 1/1000000)
	inhale acc(x.f.f.g.f, 1/1000000)
	inhale acc(x.f.f.g.g, 1/1000000)
	inhale acc(x.f.f.f.f, 1/1000000)
	inhale acc(x.f.f.f.g, 1/1000000)
	inhale x.g.g.g.f == x.f.g.g.g
	inhale x.f.g.g.f == x.f.f.g.g
	inhale x.f.f.g.f == x.f.f.f.g
	inhale acc(x.g.g.g.g.f, 1/1000000)
	inhale acc(x.g.g.g.g.g, 1/1000000)
	inhale acc(x.f.g.g.g.f, 1/1000000)
	inhale acc(x.f.g.g.g.g, 1/1000000)
	inhale acc(x.f.f.g.g.f, 1/1000000)
	inhale acc(x.f.f.g.g.g, 1/1000000)
	inhale acc(x.f.f.f.g.f, 1/1000000)
	inhale acc(x.f.f.f.g.g, 1/1000000)
	inhale acc(x.f.f.f.f.f, 1/1000000)
	inhale acc(x.f.f.f.f.g, 1/1000000)
	inhale x.g.g.g.g.f == x.f.g.g.g.g
	inhale x.f.g.g.g.f == x.f.f.g.g.g
	inhale x.f.f.g.g.f == x.f.f.f.g.g
	inhale x.f.f.f.g.f == x.f.f.f.f.g
	inhale acc(x.g.g.g.g.g.f, 1/1000000)
	inhale acc(x.g.g.g.g.g.g, 1/1000000)
	inhale acc(x.f.g.g.g.g.f, 1/1000000)
	inhale acc(x.f.g.g.g.g.g, 1/1000000)
	inhale acc(x.f.f.g.g.g.f, 1/1000000)
	inhale acc(x.f.f.g.g.g.g, 1/1000000)
	inhale acc(x.f.f.f.g.g.f, 1/1000000)
	inhale acc(x.f.f.f.g.g.g, 1/1000000)
	inhale acc(x.f.f.f.f.g.f, 1/1000000)
	inhale acc(x.f.f.f.f.g.g, 1/1000000)
	inhale acc(x.f.f.f.f.f.f, 1/1000000)
	inhale acc(x.f.f.f.f.f.g, 1/1000000)
	inhale x.g.g.g.g.g.f == x.f.g.g.g.g.g
	inhale x.f.g.g.g.g.f == x.f.f.g.g.g.g
	inhale x.f.f.g.g.g.f == x.f.f.f.g.g.g
	inhale x.f.f.f.g.g.f == x.f.f.f.f.g.g
	inhale x.f.f.f.f.g.f == x.f.f.f.f.f.g
}

The received error message is:
An internal error occurred. Found an unparsable output from Boogie: Stack overflow. (<no position>)

The Viper code is generated by this Python script:

import random, sys

denom = 1000000
def multi_nested(layers, tests, file):
    file.write('field f: Ref\n')
    file.write('field g: Ref\n')
    file.write('\n')
    file.write(f'method multi_nested_{layers}_{tests}(x: Ref) {{\n')
    for depth in range(layers):
        for f in range(depth + 1):
            g = depth - f
            file.write(f'\tinhale acc(x{'.f' * f}{'.g' * g}.f, 1/{denom})\n')
            file.write(f'\tinhale acc(x{'.f' * f}{'.g' * g}.g, 1/{denom})\n')

        for f in range(1, depth + 1):
            g = depth + 1 - f
            file.write(f'\tinhale x{'.f' * (f - 1)}{'.g' * g}.f == x{'.f' * f}{'.g' * (g - 1)}.g\n')

    for _ in range(tests):
        suffixes = [random.choice(['f', 'g']) for _ in range(layers)]
        random.shuffle(suffixes)
        lhs = 'x' + ''.join('.' + s for s in suffixes)
        random.shuffle(suffixes)
        rhs = 'x' + ''.join('.' + s for s in suffixes)
        file.write(f'\tassert {lhs} == {rhs}\n')
    file.write('}\n')

multi_nested(6, 0, sys.stdout)