From 59428b8f76e2c3300f445e05046bbc0174f84d78 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 15 Dec 2020 19:49:57 +0100 Subject: [PATCH] Fix SMTChecker tests on breaking --- .../array_members/push_as_lhs_and_rhs_bytes.sol | 4 ++-- .../array_members/push_as_lhs_bytes.sol | 10 +++++----- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_bytes.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_bytes.sol index b56761611..cbe09d4f0 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_bytes.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_bytes.sol @@ -9,8 +9,8 @@ contract C { assert(b[length - 1] == 0); assert(b[length - 1] == b[length - 2]); // Fails - assert(b[length - 1] == byte(uint8(1))); + assert(b[length - 1] == bytes1(uint8(1))); } } // ---- -// Warning 6328: (236-275): CHC: Assertion violation happens here.\nCounterexample:\nb = [0, 0]\n\n\n\nTransaction trace:\nconstructor()\nState: b = []\nf() +// Warning 6328: (236-277): CHC: Assertion violation happens here.\nCounterexample:\nb = [0, 0]\n\n\n\nTransaction trace:\nconstructor()\nState: b = []\nf() diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol index fc0dcb3fc..7b403f18e 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol @@ -5,18 +5,18 @@ contract C { function f() public { require(b.length == 0); - b.push() = byte(uint8(1)); - assert(b[0] == byte(uint8(1))); + b.push() = bytes1(uint8(1)); + assert(b[0] == bytes1(uint8(1))); } function g() public { - byte one = byte(uint8(1)); + bytes1 one = bytes1(uint8(1)); b.push() = one; assert(b[b.length - 1] == one); // Fails - assert(b[b.length - 1] == byte(uint8(100))); + assert(b[b.length - 1] == bytes1(uint8(100))); } } // ---- -// Warning 6328: (290-333): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\n\n\n\nTransaction trace:\nconstructor()\nState: b = []\ng() +// Warning 6328: (298-343): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\n\n\n\nTransaction trace:\nconstructor()\nState: b = []\ng()