Precondition on return value in modular arithmetic

[hajduakos]

In modular arithmetic we add range assumption preconditions for variables appearing in the postcondition. However, we should not do this for the return values because Boogie cannot access them in preconditions:

contract C {
    /// @notice postcondition x == 1
    function f() public pure returns (int x) {
        return 1;
    }
}

$ solc-verify.py Test.sol --arithmetic mod
Error while running verifier, details:
Parsing /tmp/tmp1ijaey2i/Test.sol.bpl
/tmp/tmp1ijaey2i/Test.sol.bpl(16,219): Error: undeclared identifier: x#4
/tmp/tmp1ijaey2i/Test.sol.bpl(16,228): Error: undeclared identifier: x#4
2 name resolution errors detected in /tmp/tmp1ijaey2i/Test.sol.bpl

I think we can just skip these preconditions and instead add them as assumes in the beginning of the function. Or it might even not be needed if return values are properly initialized to default value (see #116).

[hajduakos]

Fixed by f8adb1b