mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
31 lines
842 B
Solidity
31 lines
842 B
Solidity
pragma experimental SMTChecker;
|
|
contract A {
|
|
int x;
|
|
int y;
|
|
function a() public {
|
|
require(A.x < 100);
|
|
A.y = A.x++;
|
|
assert(A.y == A.x - 1);
|
|
// Fails
|
|
assert(A.y == 0);
|
|
A.y = ++A.x;
|
|
assert(A.y == A.x);
|
|
delete A.x;
|
|
assert(A.x == 0);
|
|
A.y = A.x--;
|
|
assert(A.y == A.x + 1);
|
|
assert(A.y == 0);
|
|
A.y = --A.x;
|
|
assert(A.y == A.x);
|
|
A.x += 10;
|
|
// Fails
|
|
assert(A.y == 0);
|
|
assert(A.y + 10 == A.x);
|
|
A.x -= 10;
|
|
assert(A.y == A.x);
|
|
}
|
|
}
|
|
// ----
|
|
// Warning 6328: (160-176): CHC: Assertion violation happens here.\nCounterexample:\nx = (- 1), y = (- 2)\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, y = 0\na()\nState: x = (- 2), y = (- 2)\na()
|
|
// Warning 6328: (373-389): CHC: Assertion violation happens here.\nCounterexample:\nx = 8, y = (- 2)\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, y = 0\na()
|