undeclared identifier: __verifier_idx_uint error with --arithmetic mod option

[nelaturuk]

pragma solidity >=0.5.0;

/// @notice invariant __verifier_sum_uint(items[__verifier_idx_uint]) >= total
contract C {
    uint total;
    uint[] items;

    function add(uint item) public {
        items.push(item);
        total += item;
    }
}

Command: solc-verify.py test.sol --arithmetic mod

[hajduakos]

Hi @nelaturuk,

Can you try /// @notice invariant __verifier_sum_uint(items) >= total? If the array contains integers __verifier_idx_uint is not needed. It is only required if your array/mapping contains structs, and you want to pick some field of the struct, see example.

[nelaturuk]

That works. Thank you.