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

28 lines
631 B
Solidity
Raw Normal View History

pragma experimental SMTChecker;
abstract contract D {
function d() public virtual ;
}
contract C {
bool a;
uint x;
D d;
function g() public returns (uint) {
x = 2;
d.d();
return x;
}
2020-09-29 18:54:26 +00:00
function f() public {
x = 1;
2020-09-29 18:54:26 +00:00
uint y = g();
assert(x == 2 || x == 1);
}
function h() public {
x = 3;
}
}
// ----
2020-09-29 18:54:26 +00:00
// Warning 2072: (282-288): Unused local variable.
// Warning 6328: (304-328): CHC: Assertion violation happens here.\nCounterexample:\na = false, x = 3, d = 0\n\n\n\nTransaction trace:\nconstructor()\nState: a = false, x = 0, d = 0\nf()