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

fix smt flaky test

Browse Source
This commit is contained in:
Leo Alt 2022-05-05 11:38:16 +02:00
parent 84c64edfee
commit 201c6c6819
1 changed files with 3 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
test/libsolidity/smtCheckerTests/operators/slice_default_end.sol
View File

@ -3,8 +3,9 @@ contract C {
require(b.length == 30);
require(b[10] == 0xff);
require(b[b.length - 1] == 0xaa);
assert(bytes(b[10:]).length == 20);
assert(bytes(b[10:])[0] == 0xff);
assert(bytes(b[10:]).length == 20); // should hold
// Disabled because of Spacer's nondeterminism.
//assert(bytes(b[10:])[0] == 0xff); // should hold
//assert(bytes(b[10:])[5] == 0xff); // Removed because of Spacer's nondeterminism
//assert(bytes(b[10:])[19] == 0xaa); // Removed because of Spacer nondeterminism
}
@ -12,5 +13,3 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (188-220): CHC: Assertion violation might happen here.
// Warning 4661: (188-220): BMC: Assertion violation happens here.