cerc-io/solidity
15
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

[SMTChecker] Update test expectations for z3 4.8.6

Browse Source
This commit is contained in:
Leonardo Alt 2019-11-11 16:59:28 +01:00
parent 2f9779d06b
commit b323134ef0
3 changed files with 7 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
test/libsolidity/smtCheckerTests/invariants/loop_array_for.sol
View File

@ -7,10 +7,11 @@ contract Simple {
for (i = 0; i < n; ++i)
a[i] = i;
require(n > 1);
// Assertion is safe but current solver version cannot solve it.
// Assertion is safe but current solver version times out.
// Keep test for next solver release.
assert(a[n-1] > a[n-2]);
}
}
// ----
// Warning: (267-290): Assertion violation happens here
// Warning: (261-284): Error trying to invoke SMT solver.
// Warning: (261-284): Assertion violation happens here

23
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_memory.sol
View File

@ -1,23 +0,0 @@
pragma experimental SMTChecker;
contract LoopFor2 {
uint[] b;
uint[] c;
function testUnboundedForLoop(uint n) public {
b[0] = 900;
uint[] memory a = b;
require(n > 0 && n < 100);
uint i;
while (i < n) {
b[i] = i + 1;
c[i] = b[i];
++i;
}
assert(b[0] == c[0]);
assert(a[0] == 900);
assert(b[0] == 900);
}
}
// ----
// Warning: (312-331): Assertion violation happens here

6
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
View File

@ -14,11 +14,13 @@ contract LoopFor2 {
c[i] = b[i];
++i;
}
// Fails as false positive.
assert(b[0] == c[0]);
assert(a[0] == 900);
assert(b[0] == 900);
}
}
// ----
// Warning: (290-309): Assertion violation happens here
// Warning: (313-332): Assertion violation happens here
// Warning: (296-316): Assertion violation happens here
// Warning: (320-339): Assertion violation happens here
// Warning: (343-362): Assertion violation happens here