Merge pull request #9068 from ethereum/smt_fix_state_var_init_call

[SMTChecker] Relax assertion about callstack
This commit is contained in:
Leonardo
2020-06-02 15:53:14 +02:00
committed by GitHub
2 changed files with 13 additions and 2 deletions
@@ -0,0 +1,12 @@
pragma experimental SMTChecker;
contract c {
uint x;
function f() internal returns (uint) {
x = x + 1;
}
bool b = (f() > 0) || (f() > 0);
}
// ----
// Warning: (100-105): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (100-105): Underflow (resulting value less than 0) happens here
// Warning: (100-105): Overflow (resulting value larger than 2**256 - 1) happens here