solidity/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol

32 lines
599 B
Solidity
Raw Normal View History

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); // Disabled because of nondeterminism in Spacer
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);
}
}
// ====
2021-03-31 15:11:54 +00:00
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
2021-03-31 15:11:54 +00:00
// Warning 6328: (392-408): CHC: Assertion violation happens here.