solidity/test/libsolidity/smtCheckerTests/file_level/easy.sol
2021-04-19 19:23:18 +02:00

18 lines
557 B
Solidity

function add(uint a, uint b) pure returns (uint) {
return a + b;
}
contract C {
function f(uint x) internal pure returns (uint) {
return add(x, 2);
}
function g() public pure {
assert(f(7) == 9); // should hold
assert(f(8) == 9); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (222-239): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f(7) -- internal call\n add(7, 2) -- internal call\n C.f(8) -- internal call\n add(8, 2) -- internal call