Update smt tests

matheusaaguiar · matheusaaguiar · commit b48eeaa1a36d · 2025-09-02T23:23:15.000-03:00
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol
@@ -18,5 +18,6 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
+// Warning 9207: (175-186): transfer will be deprecated in the next breaking version.
 // Warning 6328: (280-314): CHC: Assertion violation happens here.
 // Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol
@@ -17,6 +17,7 @@ contract C {
 // SMTIgnoreCex: yes
 // SMTIgnoreOS: macos
 // ----
+// Warning 9207: (141-152): transfer will be deprecated in the next breaking version.
 // Warning 8656: (141-156): CHC: Insufficient funds happens here.
 // Warning 6328: (193-226): CHC: Assertion violation happens here.
 // Warning 6328: (245-279): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol b/test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol
@@ -18,4 +18,5 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 9207: (160-170): transfer will be deprecated in the next breaking version.
 // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol
@@ -19,5 +19,6 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
+// Warning 9207: (33-43): transfer will be deprecated in the next breaking version.
 // Warning 6328: (258-274): CHC: Assertion violation happens here.
 // Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol
@@ -22,5 +22,6 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
+// Warning 9207: (87-97): transfer will be deprecated in the next breaking version.
 // Warning 6328: (315-331): CHC: Assertion violation happens here.
 // Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/library_public_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/library_public_2.sol
@@ -20,6 +20,7 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
+// Warning 9207: (54-64): transfer will be deprecated in the next breaking version.
 // Warning 4588: (238-243): Assertion checker does not yet implement this type of function call.
 // Warning 8656: (54-67): CHC: Insufficient funds happens here.
 // Warning 6328: (282-298): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/transfer_1.sol b/test/libsolidity/smtCheckerTests/blockchain_state/transfer_1.sol
@@ -11,5 +11,6 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
+// Warning 9207: (96-106): transfer will be deprecated in the next breaking version.
 // Warning 6328: (166-201): CHC: Assertion violation happens here.
 // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/transfer_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/transfer_2.sol
@@ -11,4 +11,6 @@ contract C {
 // ====
 // SMTEngine: chc
 // ----
+// Warning 9207: (133-151): transfer will be deprecated in the next breaking version.
+// Warning 9207: (167-185): transfer will be deprecated in the next breaking version.
 // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/transfer_3.sol b/test/libsolidity/smtCheckerTests/blockchain_state/transfer_3.sol
@@ -8,4 +8,5 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 9207: (76-94): transfer will be deprecated in the next breaking version.
 // Warning 8656: (76-97): CHC: Insufficient funds happens here.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/transfer_4.sol b/test/libsolidity/smtCheckerTests/blockchain_state/transfer_4.sol
@@ -9,4 +9,5 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 9207: (101-119): transfer will be deprecated in the next breaking version.
 // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/funds.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/funds.sol
@@ -6,4 +6,5 @@ contract C {
 // ====
 // SMTEngine: bmc
 // ----
+// Warning 9207: (55-65): transfer will be deprecated in the next breaking version.
 // Warning 1236: (55-70): BMC: Insufficient funds happens here.
diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_addresses.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_addresses.sol
@@ -16,4 +16,5 @@ contract C {
 // SMTEngine: all
 // SMTExtCalls: trusted
 // ----
+// Warning 9170: (107-115): Comparison of variables of contract type will be deprecated in the next breaking version.Consider using an explicit cast to address type.
 // Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_untrusted_addresses.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_untrusted_addresses.sol
@@ -15,6 +15,7 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 9170: (107-115): Comparison of variables of contract type will be deprecated in the next breaking version.Consider using an explicit cast to address type.
 // Warning 8729: (70-77): Contract deployment is only supported in the trusted mode for external calls with the CHC engine.
 // Warning 8729: (88-95): Contract deployment is only supported in the trusted mode for external calls with the CHC engine.
 // Warning 6328: (100-116): CHC: Assertion violation happens here.\nCounterexample:\n\nd1 = 0\nd2 = 0\n\nTransaction trace:\nC.constructor()\nC.f()
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_1.sol
@@ -15,4 +15,5 @@ contract D {
 // ====
 // SMTEngine: all
 // ----
+// Warning 9511: (0-19): ABI coder v1 will be deprecated in the next breaking version.
 // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_2.sol
@@ -20,5 +20,6 @@ contract D {
 // SMTEngine: all
 // SMTIgnoreCex: no
 // ----
+// Warning 9511: (0-19): ABI coder v1 will be deprecated in the next breaking version.
 // Warning 6328: (267-281): CHC: Assertion violation happens here.\nCounterexample:\nitems = [{x: 42, y: 43}]\na = 42\nb = 43\n\nTransaction trace:\nD.constructor()\nState: items = []\nD.test()
 // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_3.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_3.sol
@@ -21,5 +21,6 @@ contract D {
 // ====
 // SMTEngine: all
 // ----
+// Warning 9511: (0-19): ABI coder v1 will be deprecated in the next breaking version.
 // Warning 6328: (322-336): CHC: Assertion violation happens here.
 // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/contract.sol b/test/libsolidity/smtCheckerTests/functions/getters/contract.sol
@@ -12,5 +12,6 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 9170: (97-103): Comparison of variables of contract type will be deprecated in the next breaking version.Consider using an explicit cast to address type.
 // Warning 6328: (123-158): CHC: Assertion violation happens here.
 // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/struct_4.sol b/test/libsolidity/smtCheckerTests/functions/getters/struct_4.sol
@@ -18,6 +18,7 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 9170: (206-214): Comparison of variables of contract type will be deprecated in the next breaking version.Consider using an explicit cast to address type.
 // Warning 2072: (146-183): Unused local variable.
 // Warning 8364: (187-193): Assertion checker does not yet implement type function () view external returns (contract D,function () external returns (uint256))
 // Warning 6328: (234-269): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_abstract.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_abstract.sol
@@ -5,3 +5,4 @@ abstract contract A {
 // ====
 // SMTEngine: all
 // ----
+// Warning 8429: (51-72): Virtual modifiers will be deprecated in the next breaking version.
diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_1.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_1.sol
@@ -20,5 +20,6 @@ contract B is A {
 // ====
 // SMTEngine: all
 // ----
+// Warning 8429: (64-93): Virtual modifiers will be deprecated in the next breaking version.
 // Warning 6328: (209-223): CHC: Assertion violation happens here.
 // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_2.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_2.sol
@@ -23,4 +23,6 @@ contract C is B {
 // ====
 // SMTEngine: all
 // ----
+// Warning 8429: (113-136): Virtual modifiers will be deprecated in the next breaking version.
+// Warning 8429: (159-213): Virtual modifiers will be deprecated in the next breaking version.
 // Warning 6328: (66-75): CHC: Assertion violation happens here.\nCounterexample:\ns = false\n\nTransaction trace:\nB.constructor()\nState: s = false\nA.f()
diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_3.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_3.sol
@@ -18,5 +18,7 @@ contract B is A {
 // ====
 // SMTEngine: all
 // ----
+// Warning 8429: (125-148): Virtual modifiers will be deprecated in the next breaking version.
+// Warning 8429: (171-238): Virtual modifiers will be deprecated in the next breaking version.
 // Warning 6328: (94-104): CHC: Assertion violation happens here.
 // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_4.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_4.sol
@@ -36,6 +36,10 @@ contract D is B,C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 8429: (262-294): Virtual modifiers will be deprecated in the next breaking version.
+// Warning 8429: (317-367): Virtual modifiers will be deprecated in the next breaking version.
+// Warning 8429: (390-440): Virtual modifiers will be deprecated in the next breaking version.
+// Warning 8429: (465-520): Virtual modifiers will be deprecated in the next breaking version.
 // Warning 6328: (160-174): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nB.constructor()\nState: x = 0\nA.f()
 // Warning 6328: (193-207): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nA.f()
 // Warning 6328: (226-240): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nD.constructor()\nState: x = 0\nA.f()
diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_virtual_static_call_1.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_virtual_static_call_1.sol
@@ -10,3 +10,4 @@ contract C is A {
 // ====
 // SMTEngine: all
 // ----
+// Warning 8429: (17-52): Virtual modifiers will be deprecated in the next breaking version.
diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_virtual_static_call_2.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_virtual_static_call_2.sol
@@ -20,5 +20,6 @@ contract C is A {
 // ====
 // SMTEngine: all
 // ----
+// Warning 8429: (27-122): Virtual modifiers will be deprecated in the next breaking version.
 // Warning 6328: (83-98): CHC: Assertion violation happens here.
 // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer.sol b/test/libsolidity/smtCheckerTests/types/address_transfer.sol
@@ -11,5 +11,6 @@ contract C
 // ====
 // SMTEngine: all
 // ----
+// Warning 9207: (98-108): transfer will be deprecated in the next breaking version.
 // Warning 8656: (98-113): CHC: Insufficient funds happens here.
 // Warning 6328: (162-186): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol b/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol
@@ -15,6 +15,8 @@ contract C
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
+// Warning 9207: (184-194): transfer will be deprecated in the next breaking version.
+// Warning 9207: (203-213): transfer will be deprecated in the next breaking version.
 // Warning 8656: (184-199): CHC: Insufficient funds happens here.
 // Warning 8656: (203-218): CHC: Insufficient funds happens here.
 // Warning 6328: (262-291): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer_3.sol b/test/libsolidity/smtCheckerTests/types/address_transfer_3.sol
@@ -13,4 +13,5 @@ contract C
 // ====
 // SMTEngine: all
 // ----
+// Warning 9207: (126-136): transfer will be deprecated in the next breaking version.
 // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol b/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol
@@ -12,6 +12,8 @@ contract C
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
+// Warning 9207: (101-111): transfer will be deprecated in the next breaking version.
+// Warning 9207: (120-130): transfer will be deprecated in the next breaking version.
 // Warning 8656: (101-116): CHC: Insufficient funds happens here.
 // Warning 8656: (120-136): CHC: Insufficient funds happens here.
 // Warning 6328: (180-204): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/contract.sol b/test/libsolidity/smtCheckerTests/types/contract.sol
@@ -8,4 +8,5 @@ contract C
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
+// Warning 9170: (58-64): Comparison of variables of contract type will be deprecated in the next breaking version.Consider using an explicit cast to address type.
 // Warning 6328: (51-65): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/contract_2.sol b/test/libsolidity/smtCheckerTests/types/contract_2.sol
@@ -13,4 +13,5 @@ contract C
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
+// Warning 9170: (83-89): Comparison of variables of contract type will be deprecated in the next breaking version.Consider using an explicit cast to address type.
 // Warning 6328: (76-90): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/contract_3.sol b/test/libsolidity/smtCheckerTests/types/contract_3.sol
@@ -9,4 +9,7 @@ contract C
 // ====
 // SMTEngine: all
 // ----
+// Warning 9170: (64-70): Comparison of variables of contract type will be deprecated in the next breaking version.Consider using an explicit cast to address type.
+// Warning 9170: (83-89): Comparison of variables of contract type will be deprecated in the next breaking version.Consider using an explicit cast to address type.
+// Warning 9170: (101-107): Comparison of variables of contract type will be deprecated in the next breaking version.Consider using an explicit cast to address type.
 // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/types/contract_address_conversion_2.sol b/test/libsolidity/smtCheckerTests/types/contract_address_conversion_2.sol
@@ -10,4 +10,5 @@ contract C
 // ====
 // SMTEngine: all
 // ----
+// Warning 9170: (121-127): Comparison of variables of contract type will be deprecated in the next breaking version.Consider using an explicit cast to address type.
 // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
