Skip to content

Commit 59a11f9

Browse files
Leo AltRuko97
Leo Alt
authored and
Ruko97
committed
update smt tests
1 parent c3309d7 commit 59a11f9

File tree

59 files changed

+95
-272
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

59 files changed

+95
-272
lines changed

‎test/libsolidity/SMTCheckerTest.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -38,10 +38,8 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E
3838
BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT \"show unproved\" choice."));
3939

4040
m_modelCheckerSettings.solvers = smtutil::SMTSolverChoice::None();
41-
auto const& choice = m_reader.stringSetting("SMTSolvers", "any");
42-
if (choice == "any")
43-
m_modelCheckerSettings.solvers = smtutil::SMTSolverChoice::All();
44-
else if (choice == "none")
41+
auto const& choice = m_reader.stringSetting("SMTSolvers", "z3");
42+
if (choice == "none")
4543
m_modelCheckerSettings.solvers = smtutil::SMTSolverChoice::None();
4644
else if (!m_modelCheckerSettings.solvers.setSolver(choice))
4745
BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT solver choice."));

‎test/libsolidity/smtCheckerTests/abi/abi_decode_simple.sol

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -21,14 +21,10 @@ contract C {
2121
// SMTEngine: all
2222
// SMTIgnoreCex: yes
2323
// ----
24-
// Warning 1218: (505-519): CHC: Error trying to invoke SMT solver.
25-
// Warning 1218: (538-552): CHC: Error trying to invoke SMT solver.
2624
// Warning 6328: (209-223): CHC: Assertion violation happens here.
2725
// Warning 6328: (260-274): CHC: Assertion violation happens here.
2826
// Warning 6328: (359-373): CHC: Assertion violation happens here.
2927
// Warning 6328: (392-406): CHC: Assertion violation happens here.
3028
// Warning 6328: (425-434): CHC: Assertion violation happens here.
31-
// Warning 6328: (505-519): CHC: Assertion violation might happen here.
32-
// Warning 6328: (538-552): CHC: Assertion violation might happen here.
33-
// Warning 4661: (505-519): BMC: Assertion violation happens here.
34-
// Warning 4661: (538-552): BMC: Assertion violation happens here.
29+
// Warning 6328: (505-519): CHC: Assertion violation happens here.
30+
// Warning 6328: (538-552): CHC: Assertion violation happens here.

‎test/libsolidity/smtCheckerTests/abi/abi_encode_packed_simple.sol

Lines changed: 4 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -23,15 +23,7 @@ contract C {
2323
// ====
2424
// SMTEngine: all
2525
// ----
26-
// Warning 1218: (322-352): CHC: Error trying to invoke SMT solver.
27-
// Warning 1218: (419-449): CHC: Error trying to invoke SMT solver.
28-
// Warning 1218: (528-558): CHC: Error trying to invoke SMT solver.
29-
// Warning 1218: (577-607): CHC: Error trying to invoke SMT solver.
30-
// Warning 6328: (322-352): CHC: Assertion violation might happen here.
31-
// Warning 6328: (419-449): CHC: Assertion violation might happen here.
32-
// Warning 6328: (528-558): CHC: Assertion violation might happen here.
33-
// Warning 6328: (577-607): CHC: Assertion violation might happen here.
34-
// Warning 4661: (322-352): BMC: Assertion violation happens here.
35-
// Warning 4661: (419-449): BMC: Assertion violation happens here.
36-
// Warning 4661: (528-558): BMC: Assertion violation happens here.
37-
// Warning 4661: (577-607): BMC: Assertion violation happens here.
26+
// Warning 6328: (322-352): CHC: Assertion violation happens here.\nCounterexample:\n\nt = false\nx = 0\ny = 0\nz = 0\nb4 = []\nb5 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedSimple(false, 0, 0, 0, a, b)
27+
// Warning 6328: (419-449): CHC: Assertion violation happens here.\nCounterexample:\n\nt = false\nx = 0\ny = 0\nz = 0\nb5 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedSimple(false, 0, 0, 0, a, b)
28+
// Warning 6328: (528-558): CHC: Assertion violation happens here.\nCounterexample:\n\nt = false\nx = 0\ny = 0\nz = 0\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedSimple(false, 0, 0, 0, a, b)
29+
// Warning 6328: (577-607): CHC: Assertion violation happens here.\nCounterexample:\n\nt = false\nx = 0\ny = 0\nz = 0\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedSimple(false, 0, 0, 0, a, b)

‎test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol

Lines changed: 5 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -22,18 +22,8 @@ contract C {
2222
// ====
2323
// SMTEngine: all
2424
// ----
25-
// Warning 1218: (226-256): CHC: Error trying to invoke SMT solver.
26-
// Warning 1218: (310-340): CHC: Error trying to invoke SMT solver.
27-
// Warning 1218: (483-513): CHC: Error trying to invoke SMT solver.
28-
// Warning 1218: (568-598): CHC: Error trying to invoke SMT solver.
29-
// Warning 1218: (654-684): CHC: Error trying to invoke SMT solver.
30-
// Warning 6328: (226-256): CHC: Assertion violation might happen here.
31-
// Warning 6328: (310-340): CHC: Assertion violation might happen here.
32-
// Warning 6328: (483-513): CHC: Assertion violation might happen here.
33-
// Warning 6328: (568-598): CHC: Assertion violation might happen here.
34-
// Warning 6328: (654-684): CHC: Assertion violation might happen here.
35-
// Warning 4661: (226-256): BMC: Assertion violation happens here.
36-
// Warning 4661: (310-340): BMC: Assertion violation happens here.
37-
// Warning 4661: (483-513): BMC: Assertion violation happens here.
38-
// Warning 4661: (568-598): BMC: Assertion violation happens here.
39-
// Warning 4661: (654-684): BMC: Assertion violation happens here.
25+
// Warning 6328: (226-256): CHC: Assertion violation happens here.\nCounterexample:\n\nb1 = [0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42]\nb3 = []\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
26+
// Warning 6328: (310-340): CHC: Assertion violation happens here.\nCounterexample:\n\nb2 = [0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72]\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
27+
// Warning 6328: (483-513): CHC: Assertion violation happens here.\nCounterexample:\n\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
28+
// Warning 6328: (568-598): CHC: Assertion violation happens here.\nCounterexample:\n\nb2 = [0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc]\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
29+
// Warning 6328: (654-684): CHC: Assertion violation happens here.\nCounterexample:\n\nb3 = [0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a]\nb6 = [0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117]\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()

‎test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal_no_unproved.sol

Lines changed: 5 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -23,14 +23,8 @@ contract C {
2323
// SMTEngine: all
2424
// SMTShowUnproved: no
2525
// ----
26-
// Warning 1218: (226-256): CHC: Error trying to invoke SMT solver.
27-
// Warning 1218: (310-340): CHC: Error trying to invoke SMT solver.
28-
// Warning 1218: (483-513): CHC: Error trying to invoke SMT solver.
29-
// Warning 1218: (568-598): CHC: Error trying to invoke SMT solver.
30-
// Warning 1218: (654-684): CHC: Error trying to invoke SMT solver.
31-
// Warning 5840: CHC: 5 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
32-
// Warning 4661: (226-256): BMC: Assertion violation happens here.
33-
// Warning 4661: (310-340): BMC: Assertion violation happens here.
34-
// Warning 4661: (483-513): BMC: Assertion violation happens here.
35-
// Warning 4661: (568-598): BMC: Assertion violation happens here.
36-
// Warning 4661: (654-684): BMC: Assertion violation happens here.
26+
// Warning 6328: (226-256): CHC: Assertion violation happens here.\nCounterexample:\n\nb1 = [0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42, 0x42]\nb3 = []\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
27+
// Warning 6328: (310-340): CHC: Assertion violation happens here.\nCounterexample:\n\nb2 = [0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72, 0x72]\nb4 = []\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
28+
// Warning 6328: (483-513): CHC: Assertion violation happens here.\nCounterexample:\n\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
29+
// Warning 6328: (568-598): CHC: Assertion violation happens here.\nCounterexample:\n\nb2 = [0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc, 0xcc]\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()
30+
// Warning 6328: (654-684): CHC: Assertion violation happens here.\nCounterexample:\n\nb3 = [0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a, 0x011a]\nb6 = [0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117, 0x0117]\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedStringLiteral()

‎test/libsolidity/smtCheckerTests/abi/abi_encode_simple.sol

Lines changed: 3 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -20,12 +20,6 @@ contract C {
2020
// ====
2121
// SMTEngine: all
2222
// ----
23-
// Warning 1218: (298-328): CHC: Error trying to invoke SMT solver.
24-
// Warning 1218: (389-419): CHC: Error trying to invoke SMT solver.
25-
// Warning 1218: (492-522): CHC: Error trying to invoke SMT solver.
26-
// Warning 6328: (298-328): CHC: Assertion violation might happen here.
27-
// Warning 6328: (389-419): CHC: Assertion violation might happen here.
28-
// Warning 6328: (492-522): CHC: Assertion violation might happen here.
29-
// Warning 4661: (298-328): BMC: Assertion violation happens here.
30-
// Warning 4661: (389-419): BMC: Assertion violation happens here.
31-
// Warning 4661: (492-522): BMC: Assertion violation happens here.
23+
// Warning 6328: (298-328): CHC: Assertion violation happens here.\nCounterexample:\n\nt = false\nx = 0\ny = 0\nz = 0\nb4 = []\nb5 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSimple(false, 0, 0, 0, a, b)
24+
// Warning 6328: (389-419): CHC: Assertion violation happens here.\nCounterexample:\n\nt = false\nx = 0\ny = 0\nz = 0\nb5 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSimple(false, 0, 0, 0, a, b)
25+
// Warning 6328: (492-522): CHC: Assertion violation happens here.\nCounterexample:\n\nt = false\nx = 0\ny = 0\nz = 0\nb1 = []\nb2 = []\nb5 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSimple(false, 0, 0, 0, a, b)

‎test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol

Lines changed: 4 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -19,15 +19,7 @@ contract C {
1919
// ====
2020
// SMTEngine: all
2121
// ----
22-
// Warning 1218: (208-238): CHC: Error trying to invoke SMT solver.
23-
// Warning 1218: (286-316): CHC: Error trying to invoke SMT solver.
24-
// Warning 1218: (453-483): CHC: Error trying to invoke SMT solver.
25-
// Warning 1218: (532-562): CHC: Error trying to invoke SMT solver.
26-
// Warning 6328: (208-238): CHC: Assertion violation might happen here.
27-
// Warning 6328: (286-316): CHC: Assertion violation might happen here.
28-
// Warning 6328: (453-483): CHC: Assertion violation might happen here.
29-
// Warning 6328: (532-562): CHC: Assertion violation might happen here.
30-
// Warning 4661: (208-238): BMC: Assertion violation happens here.
31-
// Warning 4661: (286-316): BMC: Assertion violation happens here.
32-
// Warning 4661: (453-483): BMC: Assertion violation happens here.
33-
// Warning 4661: (532-562): BMC: Assertion violation happens here.
22+
// Warning 6328: (208-238): CHC: Assertion violation happens here.\nCounterexample:\n\nb3 = []\nb4 = []\nb5 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral()
23+
// Warning 6328: (286-316): CHC: Assertion violation happens here.\nCounterexample:\n\nb2 = [0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d]\nb3 = [0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d, 0x6d]\nb4 = []\nb5 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral()
24+
// Warning 6328: (453-483): CHC: Assertion violation happens here.\nCounterexample:\n\nb5 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral()
25+
// Warning 6328: (532-562): CHC: Assertion violation happens here.\nCounterexample:\n\nb3 = [0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca, 0xca]\n\nTransaction trace:\nC.constructor()\nC.abiEncodeStringLiteral()

‎test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol

Lines changed: 1 addition & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -26,16 +26,7 @@ contract C {
2626
// SMTEngine: all
2727
// SMTIgnoreCex: yes
2828
// ----
29-
// Warning 1218: (578-608): CHC: Error trying to invoke SMT solver.
30-
// Warning 1218: (691-721): CHC: Error trying to invoke SMT solver.
31-
// Warning 1218: (959-989): CHC: Error trying to invoke SMT solver.
32-
// Warning 1218: (1079-1109): CHC: Error trying to invoke SMT solver.
3329
// Warning 6328: (325-355): CHC: Assertion violation happens here.
34-
// Warning 6328: (578-608): CHC: Assertion violation might happen here.
35-
// Warning 6328: (691-721): CHC: Assertion violation might happen here.
36-
// Warning 6328: (959-989): CHC: Assertion violation might happen here.
30+
// Warning 6328: (578-608): CHC: Assertion violation happens here.
3731
// Warning 6328: (1079-1109): CHC: Assertion violation might happen here.
38-
// Warning 4661: (578-608): BMC: Assertion violation happens here.
39-
// Warning 4661: (691-721): BMC: Assertion violation happens here.
40-
// Warning 4661: (959-989): BMC: Assertion violation happens here.
4132
// Warning 4661: (1079-1109): BMC: Assertion violation happens here.

‎test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol

Lines changed: 2 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -25,16 +25,7 @@ contract C {
2525
// ====
2626
// SMTEngine: all
2727
// ----
28-
// Warning 1218: (579-609): CHC: Error trying to invoke SMT solver.
29-
// Warning 1218: (692-722): CHC: Error trying to invoke SMT solver.
30-
// Warning 1218: (960-990): CHC: Error trying to invoke SMT solver.
31-
// Warning 1218: (1080-1110): CHC: Error trying to invoke SMT solver.
32-
// Warning 6328: (326-356): CHC: Assertion violation happens here.
33-
// Warning 6328: (579-609): CHC: Assertion violation might happen here.
34-
// Warning 6328: (692-722): CHC: Assertion violation might happen here.
35-
// Warning 6328: (960-990): CHC: Assertion violation might happen here.
28+
// Warning 6328: (326-356): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\ndata = [55]\nb2 = [0x32, 0x32, 0x32, 0x32, 0x32, 0x32, 0x32, 0x32, 0x32, 0x32, 0x32, 0x32, 0x32, 0x32, 0x32, 0x32, 0x32, 0x32, 0x32]\nb3 = []\nb4 = []\nx = 0\ny = 0\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSlice(0x0, [55])
29+
// Warning 6328: (579-609): CHC: Assertion violation happens here.
3630
// Warning 6328: (1080-1110): CHC: Assertion violation might happen here.
37-
// Warning 4661: (579-609): BMC: Assertion violation happens here.
38-
// Warning 4661: (692-722): BMC: Assertion violation happens here.
39-
// Warning 4661: (960-990): BMC: Assertion violation happens here.
4031
// Warning 4661: (1080-1110): BMC: Assertion violation happens here.

‎test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_simple.sol

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -26,9 +26,7 @@ contract C {
2626
// SMTIgnoreCex: yes
2727
// ----
2828
// Warning 5667: (100-115): Unused function parameter. Remove or comment out the variable name to silence this warning.
29-
// Warning 1218: (855-885): CHC: Error trying to invoke SMT solver.
3029
// Warning 6328: (571-601): CHC: Assertion violation happens here.
3130
// Warning 6328: (691-721): CHC: Assertion violation happens here.
3231
// Warning 6328: (740-770): CHC: Assertion violation happens here.
33-
// Warning 6328: (855-885): CHC: Assertion violation might happen here.
34-
// Warning 4661: (855-885): BMC: Assertion violation happens here.
32+
// Warning 6328: (855-885): CHC: Assertion violation happens here.

0 commit comments

Comments
 (0)