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

Disable assertion that gives non-deterministic results in in slice tests for SMTChecker

Browse Source
This commit is contained in:
Kamil Śliwak 2021-04-15 16:28:06 +02:00
parent 6941143613
commit 7b467a49d7
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.