Postcondition violation is reported on wrong line.

[marcoeilers]

Originally reported by: Vytautas Astrauskas (Bitbucket: vakaras, GitHub: vakaras)

---

For the following code:

#!python

from py2viper_contracts.contracts import *
from typing import Tuple


def test(a: int, b: int) -> Tuple[int, int]:
    Ensures(
        #:: UnexpectedOutput(postcondition.violated:assertion.false, /py2viper/issue/26/)
        ((True and
        True) and
        True) and
        #:: ExpectedOutput(postcondition.violated:assertion.false)
        #:: MissingOutput(postcondition.violated:assertion.false, /py2viper/issue/26/)
        (Result()[0] == a and
        Result()[1] == b)
        )
    return b, a

the postcondition violation is reported on line 8 while it should be reported on line 11.

---

• Bitbucket: https://bitbucket.org/viperproject/py2viper-translation/issue/26