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 index fad743744..b231ee7ce 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol @@ -28,6 +28,8 @@ contract C { // ---- // Warning 6328: (334-364): CHC: Assertion violation happens here. // Warning 6328: (588-618): CHC: Assertion violation happens here. +// Warning 6328: (971-1001): CHC: Assertion violation might happen here. // Warning 6328: (1086-1116): 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. +// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Warning 4661: (971-1001): BMC: Assertion violation happens here. // Warning 4661: (1086-1116): BMC: Assertion violation happens here. 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 index 41e71ee5b..163caaa73 100644 --- 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 @@ -28,6 +28,8 @@ contract C { // ---- // Warning 6328: (335-365): CHC: Assertion violation happens here. // Warning 6328: (589-619): CHC: Assertion violation happens here. +// Warning 6328: (972-1002): CHC: Assertion violation might happen here. // Warning 6328: (1087-1117): 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. +// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Warning 4661: (972-1002): BMC: Assertion violation happens here. // Warning 4661: (1087-1117): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol index 5df0b9995..71a0eacde 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol @@ -16,8 +16,7 @@ contract C { // SMTEngine: all // SMTIgnoreCex: yes // ---- -// Warning 6328: (193-226): CHC: Assertion violation might happen here. +// Warning 6328: (193-226): CHC: Assertion violation happens here. // Warning 6328: (245-279): CHC: Assertion violation happens here. // Warning 6328: (298-332): CHC: Assertion violation happens here. // Warning 1236: (141-156): BMC: Insufficient funds happens here. -// Warning 4661: (193-226): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol index eb0a0c049..6a0f9de7b 100644 --- a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol @@ -21,8 +21,10 @@ contract C { // SMTIgnoreOS: macos // ---- // Warning 4984: (47-50): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. -// Warning 6328: (215-233): CHC: Assertion violation might happen here. +// Warning 6328: (167-185): CHC: Assertion violation might happen here. +// Warning 6328: (267-285): CHC: Assertion violation might happen here. // Warning 6328: (304-322): 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. +// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. // Warning 2661: (47-50): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. -// Warning 4661: (215-233): BMC: Assertion violation happens here. +// Warning 4661: (167-185): BMC: Assertion violation happens here. +// Warning 4661: (267-285): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_trusted.sol index 1c557f7a6..b5cd7bf78 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_trusted.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_trusted.sol @@ -32,5 +32,5 @@ contract C { // SMTEngine: chc // SMTExtCalls: trusted // ---- -// Warning 6328: (355-381): CHC: Assertion violation might happen here. // Warning 6328: (385-399): 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/external_calls/external_safe.sol b/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol index 593aba289..fd45ef2d7 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol @@ -18,4 +18,6 @@ contract C { // SMTEngine: all // SMTIgnoreOS: macos // ---- -// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Warning 6328: (167-181): 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. +// Warning 4661: (167-181): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/imports/duplicated_errors_1.sol b/test/libsolidity/smtCheckerTests/imports/duplicated_errors_1.sol index a98ba962a..63bc8f79f 100644 --- a/test/libsolidity/smtCheckerTests/imports/duplicated_errors_1.sol +++ b/test/libsolidity/smtCheckerTests/imports/duplicated_errors_1.sol @@ -14,13 +14,7 @@ contract C is B { } // ==== // SMTEngine: all -// SMTSolvers: smtlib2 +// SMTSolvers: z3 // ---- -// Warning 6328: (b.sol:62-75): CHC: Assertion violation might happen here. -// Warning 3996: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled. -// Warning 7812: (b.sol:62-75): BMC: Assertion violation might happen here. -// Warning 8084: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled. -// Warning 6328: (c.sol:68-81): CHC: Assertion violation might happen here. -// Warning 3996: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled. -// Warning 7812: (c.sol:68-81): BMC: Assertion violation might happen here. -// Warning 8084: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled. +// Warning 6328: (b.sol:62-75): CHC: Assertion violation happens here. +// Warning 6328: (c.sol:68-81): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol b/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol index d18f605f7..32c9780d1 100644 --- a/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol +++ b/test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol @@ -23,6 +23,4 @@ contract C { // SMTIgnoreCex: yes // SMTIgnoreOS: macos // ---- -// Warning 6328: (335-354): CHC: Assertion violation might happen here. -// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. -// Warning 4661: (335-354): BMC: 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/types/array_mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol index 5ac20c96f..fce586987 100644 --- a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol +++ b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol @@ -45,4 +45,5 @@ contract C // Warning 6368: (850-866): CHC: Out of bounds access happens here. // Warning 6368: (850-869): CHC: Out of bounds access happens here. // Warning 6328: (936-956): 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. +// Warning 6368: (1029-1043): CHC: Out of bounds access might happen 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/types/fixed_bytes_access_3.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol index bb4ef0342..d89f020ae 100644 --- a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol +++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol @@ -32,5 +32,6 @@ contract C { // SMTEngine: all // SMTIgnoreOS: macos // ---- +// Warning 6368: (374-381): CHC: Out of bounds access might happen here. // Warning 6368: (456-462): CHC: Out of bounds access happens here. -// Info 1391: CHC: 13 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Info 1391: CHC: 12 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/struct/array_struct_array_struct_storage_safe.sol b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_storage_safe.sol index b2f7b9825..7b3ff5115 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_storage_safe.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_storage_safe.sol @@ -53,4 +53,55 @@ contract C { // ==== // SMTEngine: all // ---- -// Info 1391: CHC: 51 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Warning 6368: (212-217): CHC: Out of bounds access might happen here. +// Warning 6368: (234-239): CHC: Out of bounds access might happen here. +// Warning 6328: (227-247): CHC: Assertion violation might happen here. +// Warning 6368: (251-256): CHC: Out of bounds access might happen here. +// Warning 6368: (275-280): CHC: Out of bounds access might happen here. +// Warning 6328: (268-290): CHC: Assertion violation might happen here. +// Warning 6368: (294-299): CHC: Out of bounds access might happen here. +// Warning 6368: (312-317): CHC: Out of bounds access might happen here. +// Warning 6368: (330-335): CHC: Out of bounds access might happen here. +// Warning 6368: (348-353): CHC: Out of bounds access might happen here. +// Warning 6368: (348-358): CHC: Out of bounds access might happen here. +// Warning 6368: (373-378): CHC: Out of bounds access might happen here. +// Warning 6368: (373-383): CHC: Out of bounds access might happen here. +// Warning 6328: (366-389): CHC: Assertion violation might happen here. +// Warning 6368: (393-398): CHC: Out of bounds access might happen here. +// Warning 6368: (412-417): CHC: Out of bounds access might happen here. +// Warning 6368: (431-436): CHC: Out of bounds access might happen here. +// Warning 6368: (450-455): CHC: Out of bounds access might happen here. +// Warning 6368: (469-474): CHC: Out of bounds access might happen here. +// Warning 6368: (488-493): CHC: Out of bounds access might happen here. +// Warning 6368: (488-499): CHC: Out of bounds access might happen here. +// Warning 6368: (516-521): CHC: Out of bounds access might happen here. +// Warning 6368: (516-527): CHC: Out of bounds access might happen here. +// Warning 6328: (509-535): CHC: Assertion violation might happen here. +// Warning 6368: (539-544): CHC: Out of bounds access might happen here. +// Warning 6368: (558-563): CHC: Out of bounds access might happen here. +// Warning 6368: (577-582): CHC: Out of bounds access might happen here. +// Warning 6368: (596-601): CHC: Out of bounds access might happen here. +// Warning 6368: (615-620): CHC: Out of bounds access might happen here. +// Warning 6368: (634-639): CHC: Out of bounds access might happen here. +// Warning 6368: (634-645): CHC: Out of bounds access might happen here. +// Warning 6368: (658-663): CHC: Out of bounds access might happen here. +// Warning 6368: (658-669): CHC: Out of bounds access might happen here. +// Warning 6368: (682-687): CHC: Out of bounds access might happen here. +// Warning 6368: (682-693): CHC: Out of bounds access might happen here. +// Warning 6368: (706-711): CHC: Out of bounds access might happen here. +// Warning 6368: (706-717): CHC: Out of bounds access might happen here. +// Warning 6368: (730-735): CHC: Out of bounds access might happen here. +// Warning 6368: (730-741): CHC: Out of bounds access might happen here. +// Warning 6368: (754-759): CHC: Out of bounds access might happen here. +// Warning 6368: (754-765): CHC: Out of bounds access might happen here. +// Warning 6368: (778-783): CHC: Out of bounds access might happen here. +// Warning 6368: (778-789): CHC: Out of bounds access might happen here. +// Warning 6368: (778-794): CHC: Out of bounds access might happen here. +// Warning 6368: (809-814): CHC: Out of bounds access might happen here. +// Warning 6368: (809-820): CHC: Out of bounds access might happen here. +// Warning 6368: (809-825): CHC: Out of bounds access might happen here. +// Warning 6328: (802-831): CHC: Assertion violation might happen here. +// Warning 2529: (835-843): CHC: Empty array "pop" might happen here. +// Warning 2529: (847-855): CHC: Empty array "pop" might happen here. +// Warning 2529: (859-867): CHC: Empty array "pop" might happen here. +// Info 6002: BMC: 5 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/struct_array_branches_2d.sol b/test/libsolidity/smtCheckerTests/types/struct_array_branches_2d.sol index 0d45aee14..7f7e06a06 100644 --- a/test/libsolidity/smtCheckerTests/types/struct_array_branches_2d.sol +++ b/test/libsolidity/smtCheckerTests/types/struct_array_branches_2d.sol @@ -17,5 +17,4 @@ contract C // SMTEngine: all // SMTIgnoreOS: macos // ---- -// Warning 6368: (216-225): CHC: Out of bounds access might happen here. -// Info 1391: CHC: 9 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Info 1391: CHC: 10 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/type_minmax.sol b/test/libsolidity/smtCheckerTests/types/type_minmax.sol index da9bb1b6d..ea0cf0591 100644 --- a/test/libsolidity/smtCheckerTests/types/type_minmax.sol +++ b/test/libsolidity/smtCheckerTests/types/type_minmax.sol @@ -82,4 +82,18 @@ contract C { // SMTEngine: all // ---- // Warning 6328: (178-207): CHC: Assertion violation happens here. -// Info 1391: CHC: 24 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Warning 6328: (872-900): CHC: Assertion violation might happen here. +// Warning 6328: (942-970): CHC: Assertion violation might happen here. +// Warning 6328: (1015-1045): CHC: Assertion violation might happen here. +// Warning 6328: (1125-1147): CHC: Assertion violation might happen here. +// Warning 6328: (1192-1215): CHC: Assertion violation might happen here. +// Warning 6328: (1260-1283): CHC: Assertion violation might happen here. +// Warning 6328: (1328-1351): CHC: Assertion violation might happen here. +// Warning 6328: (1399-1423): CHC: Assertion violation might happen here. +// Warning 6328: (1503-1530): CHC: Assertion violation might happen here. +// Warning 6328: (1575-1604): CHC: Assertion violation might happen here. +// Warning 6328: (1649-1678): CHC: Assertion violation might happen here. +// Warning 6328: (1723-1752): CHC: Assertion violation might happen here. +// Warning 6328: (1800-1831): CHC: Assertion violation might happen here. +// Info 1391: CHC: 11 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Info 6002: BMC: 13 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.