solidity/test/cmdlineTests/model_checker_timeout_bmc/input.sol
2020-11-06 13:35:07 +00:00

12 lines
275 B
Solidity

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
function f(uint x, uint y, uint k) public pure {
require(k > 0);
require(x % k == 0);
require(y % k == 0);
uint r = mulmod(x, y, k);
assert(r % k == 0);
}
}