Closed zhao-nan closed 3 years ago
When a quantifier is preceeded by another term, or when it is in parentheses, a parser error is thrown.
pragma solidity ^0.5.0; contract ExistTest { bool[] arr; /// @notice postcondition exists (uint u) (0 <= u && u < arr.length && arr[u]) == result function test() public view returns (bool result) { bool res = false; /// @notice invariant exists (uint j) (0 <= j && j < i && arr[j]) == res for (uint i = 0; i < arr.length; i += 1) { if (arr[i]) {res = true;} } return res; } }
When the equality in the postcondition is flipped ...
/// @notice postcondition result == exists (uint u) (0 <= u && u < arr.length && arr[u])
... or when the quantifier term is in parentheses ...
/// @notice postcondition (exists (uint u) (0 <= u && u < arr.length && arr[u])) == result
... a parser error happens:
Annotation:1:24: solc-verify error: Expected ',' but got identifier result == exists (uint u) (0 <= u && u < arr.length && arr[u])
Duplicate of #170
Description
When a quantifier is preceeded by another term, or when it is in parentheses, a parser error is thrown.
Steps to Reproduce
When the equality in the postcondition is flipped ...
... or when the quantifier term is in parentheses ...
... a parser error happens: