From 201c6c68195b9dd72fa08c6f055aa7ff67fbabfe Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Thu, 5 May 2022 11:38:16 +0200 Subject: [PATCH] fix smt flaky test --- .../smtCheckerTests/operators/slice_default_end.sol | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/test/libsolidity/smtCheckerTests/operators/slice_default_end.sol b/test/libsolidity/smtCheckerTests/operators/slice_default_end.sol index 9c0db9007..c6f421a0c 100644 --- a/test/libsolidity/smtCheckerTests/operators/slice_default_end.sol +++ b/test/libsolidity/smtCheckerTests/operators/slice_default_end.sol @@ -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.