mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
24 lines
599 B
Solidity
24 lines
599 B
Solidity
|
enum E {
|
||
|
|
READ,
|
||
|
|
WRITE
|
||
|
|
}
|
||
|
|
|
||
|
|
function allocate(bool b) pure returns (E) {
|
||
|
|
if (b) return E.READ;
|
||
|
|
return E.WRITE;
|
||
|
|
}
|
||
|
|
|
||
|
|
contract C {
|
||
|
|
function f() public pure {
|
||
|
|
E e1 = allocate(true);
|
||
|
|
assert(e1 == E.READ); // should hold
|
||
|
|
E e2 = allocate(false);
|
||
|
|
assert(e2 == E.READ); // should fail
|
||
|
|
assert(allocate(false) == E.WRITE); // should hold
|
||
|
|
}
|
||
|
|
}
|
||
|
|
// ====
|
||
|
|
// SMTEngine: all
|
||
|
|
// ----
|
||
|
|
// Warning 6328: (247-267): CHC: Assertion violation happens here.\nCounterexample:\n\ne1 = 0\ne2 = 1\n\nTransaction trace:\nC.constructor()\nC.f()\n allocate(true) -- internal call\n allocate(false) -- internal call
|