[WIP] Updated smt tests

matheusaaguiar · matheusaaguiar · commit 4496590f9fc8 · 2025-07-21T10:31:58.000-03:00
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol
@@ -27,8 +27,6 @@ contract C {
 // SMTIgnoreCex: yes
 // SMTIgnoreOS: macos
 // ----
-// Warning 6328: (325-355): CHC: Assertion violation happens here.
+// Warning 6328: (325-355): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0x0\ndata = [0x52]\nb2 = [0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53, 0x53]\nb3 = []\nb4 = []\nx = 0\ny = 0\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSlice(0x0, [0x52])
 // Warning 6328: (578-608): CHC: Assertion violation happens here.
-// Warning 6328: (691-721): CHC: Assertion violation happens here.
-// Warning 6328: (959-989): CHC: Assertion violation happens here.
-// Warning 6328: (1079-1109): 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/abi/abi_encode_with_selector_array_slice_2.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol
@@ -29,6 +29,4 @@ contract C {
 // ----
 // Warning 6328: (326-356): CHC: Assertion violation happens here.
 // Warning 6328: (579-609): CHC: Assertion violation happens here.
-// Warning 6328: (692-722): CHC: Assertion violation happens here.
-// Warning 6328: (960-990): CHC: Assertion violation happens here.
-// Warning 6328: (1080-1110): 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/abi/abi_encode_with_selector_vs_sig.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_vs_sig.sol
@@ -12,4 +12,4 @@ contract C {
 // SMTIgnoreOS: macos
 // ----
 // Warning 6328: (330-360): CHC: Assertion violation might happen here.
-// Warning 4661: (330-360): BMC: Assertion violation happens here.
+// Warning 7812: (330-360): BMC: Assertion violation might happen here.
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol
@@ -24,11 +24,9 @@ contract C {
 }
 // ====
 // SMTEngine: chc
-// SMTIgnoreOS: macos
 // SMTIgnoreCex: yes
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (334-364): CHC: Assertion violation happens here.
 // Warning 6328: (588-618): CHC: Assertion violation happens here.
-// Warning 6328: (702-732): CHC: Assertion violation happens here.
-// Warning 6328: (971-1001): CHC: Assertion violation happens here.
-// Warning 6328: (1086-1116): 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/abi/abi_encode_with_sig_array_slice_2.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol
@@ -24,11 +24,9 @@ contract C {
 }
 // ====
 // SMTEngine: chc
-// SMTIgnoreOS: macos
 // SMTIgnoreCex: yes
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (335-365): CHC: Assertion violation happens here.
 // Warning 6328: (589-619): CHC: Assertion violation happens here.
-// Warning 6328: (703-733): CHC: Assertion violation happens here.
-// Warning 6328: (972-1002): CHC: Assertion violation happens here.
-// Warning 6328: (1087-1117): 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/bmc_coverage/compound_bitwise_or_uint_3.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/compound_bitwise_or_uint_3.sol
@@ -12,4 +12,4 @@ contract C {
 // SMTEngine: bmc
 // SMTShowUnproved: no
 // ----
-// Info 6002: BMC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Warning 2788: BMC: 1 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.
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_2.sol
@@ -50,5 +50,5 @@ contract C {
 // SMTIgnoreOS: macos
 // ----
 // Warning 6328: (434-455): CHC: Assertion violation happens here.
-// Warning 6328: (1270-1291): CHC: Assertion violation happens here.
+// Warning 6328: (1270-1291): CHC: Assertion violation might happen 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/external_calls/external_call_indirect_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_3.sol
@@ -42,5 +42,5 @@ contract C {
 // SMTExtCalls: trusted
 // SMTIgnoreOS: macos
 // ----
-// Warning 6328: (561-582): CHC: Assertion violation happens here.
+// Warning 6328: (561-582): CHC: Assertion violation might happen 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/external_calls/external_call_indirect_5.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_5.sol
@@ -47,5 +47,5 @@ contract C {
 // SMTEngine: chc
 // SMTExtCalls: trusted
 // ----
-// Warning 6328: (601-622): CHC: Assertion violation happens here.
+// Warning 6328: (601-622): CHC: Assertion violation might happen 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/array_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol
@@ -19,5 +19,5 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreCex: no
 // ----
-// Warning 6328: (242-256): CHC: Assertion violation happens here.\nCounterexample:\na = [[], [], [0, 0, 0, 0]]\ny = 0\n\nTransaction trace:\nC.constructor()\nState: a = [[], [], [0, 0, 0, 0]]\nC.f()
+// Warning 6328: (242-256): CHC: Assertion violation happens here.
 // Info 1391: CHC: 7 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol
@@ -13,5 +13,4 @@ contract C {
 // Warning 6368: (76-80): CHC: Out of bounds access might happen here.
 // Warning 6368: (115-119): CHC: Out of bounds access might happen here.
 // Warning 6368: (141-145): CHC: Out of bounds access might happen here.
-// Warning 6328: (134-151): CHC: Assertion violation might happen here.
-// Info 6002: BMC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// 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/operators/compound_bitwise_or_uint_3.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol
@@ -12,4 +12,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (125-140): CHC: Assertion violation might happen here.
-// Info 6002: BMC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Warning 7812: (125-140): BMC: Assertion violation might happen here.
