diff options
| author | Leonardo Alt <leo@ethereum.org> | 2018-11-10 01:50:06 +0800 |
|---|---|---|
| committer | Leonardo Alt <leo@ethereum.org> | 2018-12-04 19:35:19 +0800 |
| commit | 8069bb61daa4009f73a7d629816bc63529af6455 (patch) | |
| tree | ef2b9a27257cc91aeb48b2f042dcd5a1d1c5924c /test/libsolidity/smtCheckerTests/loops/while_1.sol | |
| parent | e49f37be7f64d0306c2e63cea81eb98aa1bc85f1 (diff) | |
| download | dexon-solidity-8069bb61daa4009f73a7d629816bc63529af6455.tar dexon-solidity-8069bb61daa4009f73a7d629816bc63529af6455.tar.gz dexon-solidity-8069bb61daa4009f73a7d629816bc63529af6455.tar.bz2 dexon-solidity-8069bb61daa4009f73a7d629816bc63529af6455.tar.lz dexon-solidity-8069bb61daa4009f73a7d629816bc63529af6455.tar.xz dexon-solidity-8069bb61daa4009f73a7d629816bc63529af6455.tar.zst dexon-solidity-8069bb61daa4009f73a7d629816bc63529af6455.zip | |
[SMTChecker] Loops are unrolled once
Diffstat (limited to 'test/libsolidity/smtCheckerTests/loops/while_1.sol')
| -rw-r--r-- | test/libsolidity/smtCheckerTests/loops/while_1.sol | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/test/libsolidity/smtCheckerTests/loops/while_1.sol b/test/libsolidity/smtCheckerTests/loops/while_1.sol new file mode 100644 index 00000000..871ed929 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_1.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint x, bool b) public pure { + require(x < 100); + while (x < 10) { + if (b) + x = x + 1; + else + x = 0; + } + assert(x > 0); + } +} +// ---- +// Warning: (177-190): Assertion violation happens here |