cerc-io/solidity
16
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

Merge pull request #12984 from ethereum/fix_smt

Browse Source 
fix smt flaky test
This commit is contained in:
Leo 2022-05-05 14:26:27 +02:00 committed by GitHub
commit 2c49ae7a9d
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
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.length == 30);
require(b[10] == 0xff); require(b[10] == 0xff);
require(b[b.length - 1] == 0xaa); require(b[b.length - 1] == 0xaa);
assert(bytes(b[10:]).length == 20); assert(bytes(b[10:]).length == 20); // should hold
assert(bytes(b[10:])[0] == 0xff); // 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:])[5] == 0xff); // Removed because of Spacer's nondeterminism
//assert(bytes(b[10:])[19] == 0xaa); // Removed because of Spacer nondeterminism //assert(bytes(b[10:])[19] == 0xaa); // Removed because of Spacer nondeterminism
} }
@ -12,5 +13,3 @@ contract C {
// ==== // ====
// SMTEngine: all // SMTEngine: all
// ---- // ----
// Warning 6328: (188-220): CHC: Assertion violation might happen here.
// Warning 4661: (188-220): BMC: Assertion violation happens here.