cerc-io/solidity
10
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 #11262 from ethereum/disable-smt-assertion-in-slices-3

Browse Source 
Disable assertion that gives non-deterministic results in slice tests for SMTChecker
This commit is contained in:
Đorđe Mijović 2021-04-16 09:34:25 +02:00 committed by GitHub
commit da87eea309
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 2 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
test/libsolidity/smtCheckerTests/operators/slices_3.sol
View File

@ -5,7 +5,8 @@ function f(int[] calldata b, uint256 start, uint256 end) public returns (int) {
uint len = end - start; uint len = end - start;
assert(len == s.length); assert(len == s.length);
for (uint i = 0; i < len; i++) { for (uint i = 0; i < len; i++) {
assert(b[start:end][i] == s[i]); // Removed because of Spacer nondeterminism.
//assert(b[start:end][i] == s[i]);
} }
return s[0]; return s[0];
} }
@ -13,5 +14,3 @@ function f(int[] calldata b, uint256 start, uint256 end) public returns (int) {
// ==== // ====
// SMTEngine: all // SMTEngine: all
// ---- // ----
// Warning 6328: (226-257): CHC: Assertion violation might happen here.
// Warning 4661: (226-257): BMC: Assertion violation happens here.