pragma solidity >=0.5.0;
contract A {
function f(uint x, uint y, uint m) public returns (uint r) {
r = addmod(x, y, m);
}
}
Currently gives
$ solc-verify.py issue.sol --solver cvc4 --output .
Error while running verifier, details:
Parsing ./issue.sol.bpl
./issue.sol.bpl(20,1): Error: call to undeclared procedure: addmod#25
1 name resolution errors detected in ./issue.sol.bpl
From documentation addmod(uint x, uint y, uint k) returns (uint): compute (x + y) % k where the addition is performed with arbitrary precision and does not wrap around at 2**256. Assert that k != 0 starting from version 0.5.0.
Currently gives
From documentation
addmod(uint x, uint y, uint k) returns (uint): compute (x + y) % k where the addition is performed with arbitrary precision and does not wrap around at 2**256. Assert that k != 0 starting from version 0.5.0.