[SMTChecker] Add buggy short circuit test

This commit is contained in:
Leonardo Alt 2019-03-21 18:47:14 +01:00
parent 8c388592be
commit 2ae778bf0a

View File

@ -0,0 +1,20 @@
pragma experimental SMTChecker;
contract c {
uint x;
function f() internal returns (uint) {
x = x + 1;
return x;
}
function g() public {
x = 0;
assert((f() > 0) || (f() > 0));
// This assertion should NOT fail.
// It currently does because the SMTChecker does not
// handle short-circuiting properly and inlines f() twice.
assert(x == 1);
}
}
// ----
// Warning: (101-106): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (344-358): Assertion violation happens here