From 50be39fc2111114c6862aeb234c0ea0365dfd935 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Thu, 10 Dec 2020 14:06:34 +0100 Subject: [PATCH] Add and update tests --- .../output.json | 4 +- .../output.json | 236 ++--- .../output.json | 834 +++++++++--------- .../smtCheckerTests/abi/abi_decode_array.sol | 67 ++ .../smtCheckerTests/abi/abi_decode_simple.sol | 30 + .../abi/abi_encode_array_slice.sol | 31 + .../abi/abi_encode_array_slice_2.sol | 31 + .../smtCheckerTests/abi/abi_encode_hash.sol | 9 + .../abi/abi_encode_packed_array_slice.sol | 36 + .../abi/abi_encode_packed_array_slice_2.sol | 37 + .../abi/abi_encode_packed_hash.sol | 16 + .../abi/abi_encode_packed_simple.sol | 34 + .../abi/abi_encode_packed_string_literal.sol | 38 + .../smtCheckerTests/abi/abi_encode_simple.sol | 30 + .../abi/abi_encode_string_literal.sol | 32 + .../abi_encode_with_selector_array_slice.sol | 37 + ...abi_encode_with_selector_array_slice_2.sol | 37 + .../abi/abi_encode_with_selector_hash.sol | 20 + .../abi/abi_encode_with_selector_simple.sol | 32 + ...bi_encode_with_selector_string_literal.sol | 36 + .../abi/abi_encode_with_selector_vs_sig.sol | 12 + .../abi/abi_encode_with_sig_array_slice.sol | 37 + .../abi/abi_encode_with_sig_array_slice_2.sol | 37 + .../abi/abi_encode_with_sig_hash.sol | 20 + .../abi/abi_encode_with_sig_simple.sol | 34 + .../abi_encode_with_sig_string_literal.sol | 36 + .../push_storage_ref_unsafe_aliasing.sol | 2 +- .../push_storage_ref_unsafe_length.sol | 4 +- .../blockchain_state/transfer.sol | 2 +- .../smtCheckerTests/complex/MerkleProof.sol | 4 - .../complex/slither/external_function.sol | 8 +- ...or_state_variable_init_chain_alternate.sol | 2 +- .../branches_with_return/constructors.sol | 2 +- .../crypto_functions_compare_hashes.sol | 8 +- .../crypto/crypto_functions_not_same.sol | 2 +- .../external_calls/external_inc.sol | 4 +- .../functions/abi_encode_functions.sol | 4 - .../functions/constructor_hierarchy_4.sol | 2 +- .../constructor_hierarchy_diamond_2.sol | 6 +- .../constructor_hierarchy_diamond_3.sol | 8 +- .../functions/constructor_state_value.sol | 2 +- .../constructor_state_value_inherited.sol | 2 +- .../constructor_state_value_parameter.sol | 4 +- .../getters/nested_arrays_mappings_4.sol | 2 +- .../getters/nested_arrays_mappings_5.sol | 4 +- ...chy_base_calls_inheritance_specifier_1.sol | 2 +- ...chy_base_calls_inheritance_specifier_2.sol | 6 +- ...erarchy_base_calls_with_side_effects_5.sol | 4 +- ...or_loop_array_assignment_memory_memory.sol | 9 +- ..._loop_array_assignment_storage_storage.sol | 10 +- ...le_loop_array_assignment_memory_memory.sol | 9 +- .../loops/while_nested_break_fail.sol | 2 +- .../operators/compound_sub_array_index.sol | 4 +- .../operators/compound_sub_mapping.sol | 4 +- .../smtCheckerTests/operators/slice.sol | 3 +- .../operators/unary_add_array.sol | 2 +- .../operators/unary_sub_mapping.sol | 4 +- .../overflow/overflow_mul_cex_with_array.sol | 2 +- .../overflow/signed_div_overflow.sol | 2 +- .../special/abi_decode_memory_v2.sol | 2 - .../abi_decode_memory_v2_value_types.sol | 16 +- .../special/abi_decode_simple.sol | 30 +- .../special/abi_encode_slice.sol | 2 - .../special/tx_data_gasleft_changes.sol | 6 +- .../smtCheckerTests/types/address_call.sol | 10 +- .../types/address_delegatecall.sol | 10 +- .../types/address_staticcall.sol | 2 +- .../types/address_transfer_2.sol | 2 +- .../types/array_aliasing_storage_2.sol | 2 +- .../types/array_aliasing_storage_4.sol | 6 +- .../types/array_aliasing_storage_5.sol | 2 +- .../smtCheckerTests/types/array_branch_1d.sol | 2 +- .../types/array_dynamic_parameter_1_fail.sol | 2 +- .../types/array_mapping_aliasing_1.sol | 2 +- .../types/array_static_aliasing_storage_5.sol | 4 +- .../types/array_static_mapping_aliasing_1.sol | 2 +- .../types/array_static_mapping_aliasing_2.sol | 2 +- .../smtCheckerTests/types/bytes_2_fail.sol | 2 +- .../smtCheckerTests/types/contract.sol | 4 +- .../smtCheckerTests/types/contract_2.sol | 4 +- .../types/fixed_bytes_access_2.sol | 2 +- .../types/mapping_aliasing_2.sol | 6 +- .../types/mapping_as_parameter_1.sol | 2 +- .../types/string_literal_comparison_2.sol | 2 +- .../struct/struct_state_var_array_pop_2.sol | 6 +- .../types/tuple_assignment_array_empty.sol | 4 +- .../types/tuple_extra_parens_7.sol | 2 + 87 files changed, 1434 insertions(+), 642 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_decode_array.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_decode_simple.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice_2.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_hash.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice_2.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_packed_hash.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_packed_simple.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_simple.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_simple.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_vs_sig.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_hash.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_simple.sol create mode 100644 test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_string_literal.sol diff --git a/test/cmdlineTests/standard_model_checker_engine_bmc/output.json b/test/cmdlineTests/standard_model_checker_engine_bmc/output.json index 663136f69..9f008693e 100644 --- a/test/cmdlineTests/standard_model_checker_engine_bmc/output.json +++ b/test/cmdlineTests/standard_model_checker_engine_bmc/output.json @@ -1,4 +1,4 @@ -{"auxiliaryInputRequested":{"smtlib2queries":{"0x238aade411d63d50406236089e28f3770d51f95888222fdb838f930911e0f763":"(set-option :produce-models true) +{"auxiliaryInputRequested":{"smtlib2queries":{"0x88f5b0fdb94a459ff6e3f6ee6fd482520d1d0ddeb45b14acd5060b6ecfe818dd":"(set-option :produce-models true) (set-logic ALL) (declare-fun |error_0| () Int) (declare-fun |this_0| () Int) @@ -10,6 +10,8 @@ (declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) (declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) (declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) (declare-fun |x_4_0| () Int) (declare-fun |expr_8_0| () Int) (declare-fun |expr_9_0| () Int) diff --git a/test/cmdlineTests/standard_model_checker_timeout_all/output.json b/test/cmdlineTests/standard_model_checker_timeout_all/output.json index 3b063aa59..ff9ed6e9c 100644 --- a/test/cmdlineTests/standard_model_checker_timeout_all/output.json +++ b/test/cmdlineTests/standard_model_checker_timeout_all/output.json @@ -1,57 +1,4 @@ -{"auxiliaryInputRequested":{"smtlib2queries":{"0x0d6f843ef6990bfad1918be96d1aad42b5d7ca87a171d0ac34009e0d4b6e8e03":"(set-option :produce-models true) -(set-option :timeout 1000) -(set-logic ALL) -(declare-fun |error_0| () Int) -(declare-fun |this_0| () Int) -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-fun |state_0| () |state_type|) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-fun |tx_0| () |tx_type|) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-fun |crypto_0| () |crypto_type|) -(declare-fun |x_4_0| () Int) -(declare-fun |y_6_0| () Int) -(declare-fun |k_8_0| () Int) -(declare-fun |r_34_0| () Int) -(declare-fun |expr_12_0| () Int) -(declare-fun |expr_13_0| () Int) -(declare-fun |expr_14_1| () Bool) -(declare-fun |expr_18_0| () Int) -(declare-fun |expr_19_0| () Int) -(declare-fun |d_div_mod_15_0| () Int) -(declare-fun |r_div_mod_15_0| () Int) -(declare-fun |expr_20_1| () Int) -(declare-fun |expr_21_0| () Int) -(declare-fun |expr_22_1| () Bool) - -(assert (and (and (and true true) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) expr_22_1)) -(check-sat) -","0x3091365cefd5a713eea87735305ab53c75303343ebf74b77d3578ae0b73c64a2":"(set-option :produce-models true) -(set-option :timeout 1000) -(set-logic ALL) -(declare-fun |error_0| () Int) -(declare-fun |this_0| () Int) -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-fun |state_0| () |state_type|) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-fun |tx_0| () |tx_type|) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-fun |crypto_0| () |crypto_type|) -(declare-fun |x_4_0| () Int) -(declare-fun |y_6_0| () Int) -(declare-fun |k_8_0| () Int) -(declare-fun |r_34_0| () Int) -(declare-fun |expr_12_0| () Int) -(declare-fun |expr_13_0| () Int) -(declare-fun |expr_14_1| () Bool) - -(assert (and (and (and true true) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) (not expr_14_1))) -(check-sat) -","0x6b268fc2d87ebda3f3b3b93c8d0b2b5374fd3bd33387113b9ee138a85c142dae":"(set-option :produce-models true) +{"auxiliaryInputRequested":{"smtlib2queries":{"0x17eb7e6c3c9675e486088d4f0c4091012e0d7d510a5b9c0d2912b9c57e5456d5":"(set-option :produce-models true) (set-option :timeout 1000) (set-logic ALL) (declare-fun |error_0| () Int) @@ -64,6 +11,8 @@ (declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) (declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) (declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) (declare-fun |x_4_0| () Int) (declare-fun |y_6_0| () Int) (declare-fun |k_8_0| () Int) @@ -86,62 +35,9 @@ (declare-fun |expr_29_0| () Int) (declare-fun |expr_30_1| () Bool) -(assert (and (and (and true true) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_16_0)) (and (and (<= 0 r_div_mod_16_0) (or (= expr_27_0 0) (< r_div_mod_16_0 expr_27_0))) (and (= (+ (* d_div_mod_16_0 expr_27_0) r_div_mod_16_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) expr_30_1)) +(assert (and (and (and true true) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_16_0)) (and (and (<= 0 r_div_mod_16_0) (or (= expr_27_0 0) (< r_div_mod_16_0 expr_27_0))) (and (= (+ (* d_div_mod_16_0 expr_27_0) r_div_mod_16_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) (not expr_30_1))) (check-sat) -","0xa81ce8317a79fc74d85d9edfe56caf9b0274a7da4556bfb418652051e0bfa679":"(set-option :produce-models true) -(set-option :timeout 1000) -(set-logic ALL) -(declare-fun |error_0| () Int) -(declare-fun |this_0| () Int) -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-fun |state_0| () |state_type|) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-fun |tx_0| () |tx_type|) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-fun |crypto_0| () |crypto_type|) -(declare-fun |x_4_0| () Int) -(declare-fun |y_6_0| () Int) -(declare-fun |k_8_0| () Int) -(declare-fun |r_34_0| () Int) -(declare-fun |expr_12_0| () Int) -(declare-fun |expr_13_0| () Int) -(declare-fun |expr_14_1| () Bool) - -(assert (and (and (and true true) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) expr_14_1)) -(check-sat) -","0xaec7aba847ba235b585e4c7e6ec8d8eee964e76bd40a02e00af3354acede95d8":"(set-option :produce-models true) -(set-option :timeout 1000) -(set-logic ALL) -(declare-fun |error_0| () Int) -(declare-fun |this_0| () Int) -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-fun |state_0| () |state_type|) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-fun |tx_0| () |tx_type|) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-fun |crypto_0| () |crypto_type|) -(declare-fun |x_4_0| () Int) -(declare-fun |y_6_0| () Int) -(declare-fun |k_8_0| () Int) -(declare-fun |r_34_0| () Int) -(declare-fun |expr_12_0| () Int) -(declare-fun |expr_13_0| () Int) -(declare-fun |expr_14_1| () Bool) -(declare-fun |expr_18_0| () Int) -(declare-fun |expr_19_0| () Int) -(declare-fun |d_div_mod_15_0| () Int) -(declare-fun |r_div_mod_15_0| () Int) -(declare-fun |expr_20_1| () Int) -(declare-fun |expr_21_0| () Int) -(declare-fun |expr_22_1| () Bool) - -(assert (and (and (and true true) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) (not expr_22_1))) -(check-sat) -","0xe6aad7b5a7ba681908e47e11921c93815f9a4cdd90ef82dd79a60fcac94492c9":"(set-option :produce-models true) +","0x2b53b933e67842c0d550b4a25069debb0949a378a0c560f021c914b93615b1fc":"(set-option :produce-models true) (set-option :timeout 1000) (set-logic ALL) (declare-fun |error_0| () Int) @@ -154,6 +50,8 @@ (declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) (declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) (declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) (declare-fun |x_4_0| () Int) (declare-fun |y_6_0| () Int) (declare-fun |k_8_0| () Int) @@ -203,7 +101,7 @@ (assert (= |EVALEXPR_3| r_34_1)) (check-sat) (get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| )) -","0xf877f10b1dc480ae2403c9376947f543da579bf3aff7dfaa2f946e300b81d305":"(set-option :produce-models true) +","0x47c361f3e8e669764e26b1b1498b9455e7c589547ab5b90e5efdd82b14dfbd3a":"(set-option :produce-models true) (set-option :timeout 1000) (set-logic ALL) (declare-fun |error_0| () Int) @@ -216,6 +114,90 @@ (declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) (declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) (declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |x_4_0| () Int) +(declare-fun |y_6_0| () Int) +(declare-fun |k_8_0| () Int) +(declare-fun |r_34_0| () Int) +(declare-fun |expr_12_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_1| () Bool) +(declare-fun |expr_18_0| () Int) +(declare-fun |expr_19_0| () Int) +(declare-fun |d_div_mod_15_0| () Int) +(declare-fun |r_div_mod_15_0| () Int) +(declare-fun |expr_20_1| () Int) +(declare-fun |expr_21_0| () Int) +(declare-fun |expr_22_1| () Bool) + +(assert (and (and (and true true) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) (not expr_22_1))) +(check-sat) +","0xcb2117c40da91e8a86270886eca9e12cf9524141e96a95d18711d0c97f974086":"(set-option :produce-models true) +(set-option :timeout 1000) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |x_4_0| () Int) +(declare-fun |y_6_0| () Int) +(declare-fun |k_8_0| () Int) +(declare-fun |r_34_0| () Int) +(declare-fun |expr_12_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_1| () Bool) + +(assert (and (and (and true true) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) (not expr_14_1))) +(check-sat) +","0xcc5b317723ba883782a53eb35e82063ffcd1eee56de51d63c6c2971413b03d3a":"(set-option :produce-models true) +(set-option :timeout 1000) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |x_4_0| () Int) +(declare-fun |y_6_0| () Int) +(declare-fun |k_8_0| () Int) +(declare-fun |r_34_0| () Int) +(declare-fun |expr_12_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_1| () Bool) + +(assert (and (and (and true true) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) expr_14_1)) +(check-sat) +","0xdee28d62f23c1f8b40466ff649c947e3e5793e66b2049a92d0de96208e441565":"(set-option :produce-models true) +(set-option :timeout 1000) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) (declare-fun |x_4_0| () Int) (declare-fun |y_6_0| () Int) (declare-fun |k_8_0| () Int) @@ -238,7 +220,39 @@ (declare-fun |expr_29_0| () Int) (declare-fun |expr_30_1| () Bool) -(assert (and (and (and true true) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_16_0)) (and (and (<= 0 r_div_mod_16_0) (or (= expr_27_0 0) (< r_div_mod_16_0 expr_27_0))) (and (= (+ (* d_div_mod_16_0 expr_27_0) r_div_mod_16_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) (not expr_30_1))) +(assert (and (and (and true true) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_16_0)) (and (and (<= 0 r_div_mod_16_0) (or (= expr_27_0 0) (< r_div_mod_16_0 expr_27_0))) (and (= (+ (* d_div_mod_16_0 expr_27_0) r_div_mod_16_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) expr_30_1)) +(check-sat) +","0xf4cd8362dc82ca7448e9c27bbf7b391942d5110c7b29a1dba6a4e8037a7f68cf":"(set-option :produce-models true) +(set-option :timeout 1000) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |x_4_0| () Int) +(declare-fun |y_6_0| () Int) +(declare-fun |k_8_0| () Int) +(declare-fun |r_34_0| () Int) +(declare-fun |expr_12_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_1| () Bool) +(declare-fun |expr_18_0| () Int) +(declare-fun |expr_19_0| () Int) +(declare-fun |d_div_mod_15_0| () Int) +(declare-fun |r_div_mod_15_0| () Int) +(declare-fun |expr_20_1| () Int) +(declare-fun |expr_21_0| () Int) +(declare-fun |expr_22_1| () Bool) + +(assert (and (and (and true true) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_15_0)) (and (and (<= 0 r_div_mod_15_0) (or (= expr_19_0 0) (< r_div_mod_15_0 expr_19_0))) (and (= (+ (* d_div_mod_15_0 expr_19_0) r_div_mod_15_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) expr_22_1)) (check-sat) "}},"errors":[{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation might happen here. --> A:6:85: diff --git a/test/cmdlineTests/standard_model_checker_timeout_bmc/output.json b/test/cmdlineTests/standard_model_checker_timeout_bmc/output.json index 8b6f289b9..b1d3704e4 100644 --- a/test/cmdlineTests/standard_model_checker_timeout_bmc/output.json +++ b/test/cmdlineTests/standard_model_checker_timeout_bmc/output.json @@ -1,185 +1,4 @@ -{"auxiliaryInputRequested":{"smtlib2queries":{"0x0e2ec6d70e3de7ac14f07c9bbb08f9436e3b832ae8456d340e4d4a8b8712c7f5":"(set-option :produce-models true) -(set-option :timeout 1000) -(set-logic ALL) -(declare-fun |error_0| () Int) -(declare-fun |this_0| () Int) -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-fun |state_0| () |state_type|) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-fun |tx_0| () |tx_type|) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-fun |crypto_0| () |crypto_type|) -(declare-fun |x_4_0| () Int) -(declare-fun |y_6_0| () Int) -(declare-fun |k_8_0| () Int) -(declare-fun |r_34_0| () Int) -(declare-fun |expr_12_0| () Int) -(declare-fun |expr_13_0| () Int) -(declare-fun |expr_14_1| () Bool) -(declare-fun |expr_18_0| () Int) -(declare-fun |expr_19_0| () Int) -(declare-fun |d_div_mod_0_0| () Int) -(declare-fun |r_div_mod_0_0| () Int) -(declare-fun |expr_20_1| () Int) -(declare-fun |expr_21_0| () Int) -(declare-fun |expr_22_1| () Bool) -(declare-fun |expr_26_0| () Int) -(declare-fun |expr_27_0| () Int) -(declare-fun |d_div_mod_1_0| () Int) -(declare-fun |r_div_mod_1_0| () Int) -(declare-fun |expr_28_1| () Int) -(declare-fun |expr_29_0| () Int) -(declare-fun |expr_30_1| () Bool) -(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int) -(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int) -(declare-fun |expr_36_0| () Int) -(declare-fun |expr_37_0| () Int) -(declare-fun |expr_38_0| () Int) -(declare-fun |d_div_mod_2_0| () Int) -(declare-fun |r_div_mod_2_0| () Int) -(declare-fun |expr_39_1| () Int) -(declare-fun |r_34_1| () Int) -(declare-fun |expr_42_0| () Int) -(declare-fun |expr_43_0| () Int) -(declare-fun |d_div_mod_3_0| () Int) -(declare-fun |r_div_mod_3_0| () Int) -(declare-fun |expr_44_1| () Int) -(declare-fun |expr_45_0| () Int) -(declare-fun |expr_46_1| () Bool) - -(assert (and (and (and true true) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))))))))))) (= expr_27_0 0))) -(declare-const |EVALEXPR_0| Int) -(assert (= |EVALEXPR_0| x_4_0)) -(declare-const |EVALEXPR_1| Int) -(assert (= |EVALEXPR_1| y_6_0)) -(declare-const |EVALEXPR_2| Int) -(assert (= |EVALEXPR_2| k_8_0)) -(declare-const |EVALEXPR_3| Int) -(assert (= |EVALEXPR_3| r_34_0)) -(declare-const |EVALEXPR_4| Int) -(assert (= |EVALEXPR_4| expr_27_0)) -(check-sat) -(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| )) -","0x3091365cefd5a713eea87735305ab53c75303343ebf74b77d3578ae0b73c64a2":"(set-option :produce-models true) -(set-option :timeout 1000) -(set-logic ALL) -(declare-fun |error_0| () Int) -(declare-fun |this_0| () Int) -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-fun |state_0| () |state_type|) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-fun |tx_0| () |tx_type|) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-fun |crypto_0| () |crypto_type|) -(declare-fun |x_4_0| () Int) -(declare-fun |y_6_0| () Int) -(declare-fun |k_8_0| () Int) -(declare-fun |r_34_0| () Int) -(declare-fun |expr_12_0| () Int) -(declare-fun |expr_13_0| () Int) -(declare-fun |expr_14_1| () Bool) - -(assert (and (and (and true true) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) (not expr_14_1))) -(check-sat) -","0x46c0f34a4da6b31138e9238be92256a3c472a5a24c88371ef680f78e0c520cb6":"(set-option :produce-models true) -(set-option :timeout 1000) -(set-logic ALL) -(declare-fun |error_0| () Int) -(declare-fun |this_0| () Int) -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-fun |state_0| () |state_type|) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-fun |tx_0| () |tx_type|) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-fun |crypto_0| () |crypto_type|) -(declare-fun |x_4_0| () Int) -(declare-fun |y_6_0| () Int) -(declare-fun |k_8_0| () Int) -(declare-fun |r_34_0| () Int) -(declare-fun |expr_12_0| () Int) -(declare-fun |expr_13_0| () Int) -(declare-fun |expr_14_1| () Bool) -(declare-fun |expr_18_0| () Int) -(declare-fun |expr_19_0| () Int) -(declare-fun |d_div_mod_0_0| () Int) -(declare-fun |r_div_mod_0_0| () Int) -(declare-fun |expr_20_1| () Int) -(declare-fun |expr_21_0| () Int) -(declare-fun |expr_22_1| () Bool) -(declare-fun |expr_26_0| () Int) -(declare-fun |expr_27_0| () Int) -(declare-fun |d_div_mod_1_0| () Int) -(declare-fun |r_div_mod_1_0| () Int) -(declare-fun |expr_28_1| () Int) -(declare-fun |expr_29_0| () Int) -(declare-fun |expr_30_1| () Bool) -(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int) -(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int) -(declare-fun |expr_36_0| () Int) -(declare-fun |expr_37_0| () Int) -(declare-fun |expr_38_0| () Int) -(declare-fun |d_div_mod_2_0| () Int) -(declare-fun |r_div_mod_2_0| () Int) -(declare-fun |expr_39_1| () Int) -(declare-fun |r_34_1| () Int) -(declare-fun |expr_42_0| () Int) -(declare-fun |expr_43_0| () Int) -(declare-fun |d_div_mod_3_0| () Int) -(declare-fun |r_div_mod_3_0| () Int) -(declare-fun |expr_44_1| () Int) -(declare-fun |expr_45_0| () Int) -(declare-fun |expr_46_1| () Bool) - -(assert (and (and (and true true) (and (= expr_38_0 k_8_0) (and (= expr_37_0 y_6_0) (and (= expr_36_0 x_4_0) (and true (and (implies (and true true) expr_30_1) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))))))))))))))))))))) (= expr_38_0 0))) -(declare-const |EVALEXPR_0| Int) -(assert (= |EVALEXPR_0| x_4_0)) -(declare-const |EVALEXPR_1| Int) -(assert (= |EVALEXPR_1| y_6_0)) -(declare-const |EVALEXPR_2| Int) -(assert (= |EVALEXPR_2| k_8_0)) -(declare-const |EVALEXPR_3| Int) -(assert (= |EVALEXPR_3| r_34_0)) -(declare-const |EVALEXPR_4| Int) -(assert (= |EVALEXPR_4| expr_38_0)) -(check-sat) -(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| )) -","0x6378f27de46d517b5bafe774eab66c12cb656dbd031cb5e710f07b1bfd6c5f79":"(set-option :produce-models true) -(set-option :timeout 1000) -(set-logic ALL) -(declare-fun |error_0| () Int) -(declare-fun |this_0| () Int) -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-fun |state_0| () |state_type|) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-fun |tx_0| () |tx_type|) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-fun |crypto_0| () |crypto_type|) -(declare-fun |x_4_0| () Int) -(declare-fun |y_6_0| () Int) -(declare-fun |k_8_0| () Int) -(declare-fun |r_34_0| () Int) -(declare-fun |expr_12_0| () Int) -(declare-fun |expr_13_0| () Int) -(declare-fun |expr_14_1| () Bool) -(declare-fun |expr_18_0| () Int) -(declare-fun |expr_19_0| () Int) -(declare-fun |d_div_mod_0_0| () Int) -(declare-fun |r_div_mod_0_0| () Int) -(declare-fun |expr_20_1| () Int) -(declare-fun |expr_21_0| () Int) -(declare-fun |expr_22_1| () Bool) - -(assert (and (and (and true true) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) (not expr_22_1))) -(check-sat) -","0x7db419e89d4bb9fbaa4bda7fd522223a515177ff577a6d381e7f2b7f4612582b":"(set-option :produce-models true) +{"auxiliaryInputRequested":{"smtlib2queries":{"0x0017aa24ac5e0f5ac607f58201176163a5609823b2487aec1cdb16e925cfb577":"(set-option :produce-models true) (set-option :timeout 1000) (set-logic ALL) (declare-fun |error_0| () Int) @@ -192,6 +11,8 @@ (declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) (declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) (declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) (declare-fun |x_4_0| () Int) (declare-fun |y_6_0| () Int) (declare-fun |k_8_0| () Int) @@ -209,230 +30,7 @@ (assert (and (and (and true true) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) expr_22_1)) (check-sat) -","0x7de8eaf2518b47eec1afadbebacdfa7d93a1878e0f1b6eef91b8a80f1246937e":"(set-option :produce-models true) -(set-option :timeout 1000) -(set-logic ALL) -(declare-fun |error_0| () Int) -(declare-fun |this_0| () Int) -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-fun |state_0| () |state_type|) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-fun |tx_0| () |tx_type|) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-fun |crypto_0| () |crypto_type|) -(declare-fun |x_4_0| () Int) -(declare-fun |y_6_0| () Int) -(declare-fun |k_8_0| () Int) -(declare-fun |r_34_0| () Int) -(declare-fun |expr_12_0| () Int) -(declare-fun |expr_13_0| () Int) -(declare-fun |expr_14_1| () Bool) -(declare-fun |expr_18_0| () Int) -(declare-fun |expr_19_0| () Int) -(declare-fun |d_div_mod_0_0| () Int) -(declare-fun |r_div_mod_0_0| () Int) -(declare-fun |expr_20_1| () Int) -(declare-fun |expr_21_0| () Int) -(declare-fun |expr_22_1| () Bool) -(declare-fun |expr_26_0| () Int) -(declare-fun |expr_27_0| () Int) -(declare-fun |d_div_mod_1_0| () Int) -(declare-fun |r_div_mod_1_0| () Int) -(declare-fun |expr_28_1| () Int) -(declare-fun |expr_29_0| () Int) -(declare-fun |expr_30_1| () Bool) - -(assert (and (and (and true true) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) (not expr_30_1))) -(check-sat) -","0x8c4f3faef8ad4a2fe9935f16ec93e2df20f5a3831be51c13afe060774658141c":"(set-option :produce-models true) -(set-option :timeout 1000) -(set-logic ALL) -(declare-fun |error_0| () Int) -(declare-fun |this_0| () Int) -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-fun |state_0| () |state_type|) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-fun |tx_0| () |tx_type|) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-fun |crypto_0| () |crypto_type|) -(declare-fun |x_4_0| () Int) -(declare-fun |y_6_0| () Int) -(declare-fun |k_8_0| () Int) -(declare-fun |r_34_0| () Int) -(declare-fun |expr_12_0| () Int) -(declare-fun |expr_13_0| () Int) -(declare-fun |expr_14_1| () Bool) -(declare-fun |expr_18_0| () Int) -(declare-fun |expr_19_0| () Int) -(declare-fun |d_div_mod_0_0| () Int) -(declare-fun |r_div_mod_0_0| () Int) -(declare-fun |expr_20_1| () Int) -(declare-fun |expr_21_0| () Int) -(declare-fun |expr_22_1| () Bool) -(declare-fun |expr_26_0| () Int) -(declare-fun |expr_27_0| () Int) -(declare-fun |d_div_mod_1_0| () Int) -(declare-fun |r_div_mod_1_0| () Int) -(declare-fun |expr_28_1| () Int) -(declare-fun |expr_29_0| () Int) -(declare-fun |expr_30_1| () Bool) - -(assert (and (and (and true true) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) expr_30_1)) -(check-sat) -","0xa4666c5d197afd69bd82af703fb694c1d3cdd8926ab480fc42e69231134d9265":"(set-option :produce-models true) -(set-option :timeout 1000) -(set-logic ALL) -(declare-fun |error_0| () Int) -(declare-fun |this_0| () Int) -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-fun |state_0| () |state_type|) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-fun |tx_0| () |tx_type|) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-fun |crypto_0| () |crypto_type|) -(declare-fun |x_4_0| () Int) -(declare-fun |y_6_0| () Int) -(declare-fun |k_8_0| () Int) -(declare-fun |r_34_0| () Int) -(declare-fun |expr_12_0| () Int) -(declare-fun |expr_13_0| () Int) -(declare-fun |expr_14_1| () Bool) -(declare-fun |expr_18_0| () Int) -(declare-fun |expr_19_0| () Int) -(declare-fun |d_div_mod_0_0| () Int) -(declare-fun |r_div_mod_0_0| () Int) -(declare-fun |expr_20_1| () Int) -(declare-fun |expr_21_0| () Int) -(declare-fun |expr_22_1| () Bool) -(declare-fun |expr_26_0| () Int) -(declare-fun |expr_27_0| () Int) -(declare-fun |d_div_mod_1_0| () Int) -(declare-fun |r_div_mod_1_0| () Int) -(declare-fun |expr_28_1| () Int) -(declare-fun |expr_29_0| () Int) -(declare-fun |expr_30_1| () Bool) -(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int) -(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int) -(declare-fun |expr_36_0| () Int) -(declare-fun |expr_37_0| () Int) -(declare-fun |expr_38_0| () Int) -(declare-fun |d_div_mod_2_0| () Int) -(declare-fun |r_div_mod_2_0| () Int) -(declare-fun |expr_39_1| () Int) -(declare-fun |r_34_1| () Int) -(declare-fun |expr_42_0| () Int) -(declare-fun |expr_43_0| () Int) -(declare-fun |d_div_mod_3_0| () Int) -(declare-fun |r_div_mod_3_0| () Int) -(declare-fun |expr_44_1| () Int) -(declare-fun |expr_45_0| () Int) -(declare-fun |expr_46_1| () Bool) - -(assert (and (and (and true true) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))) (= expr_19_0 0))) -(declare-const |EVALEXPR_0| Int) -(assert (= |EVALEXPR_0| x_4_0)) -(declare-const |EVALEXPR_1| Int) -(assert (= |EVALEXPR_1| y_6_0)) -(declare-const |EVALEXPR_2| Int) -(assert (= |EVALEXPR_2| k_8_0)) -(declare-const |EVALEXPR_3| Int) -(assert (= |EVALEXPR_3| r_34_0)) -(declare-const |EVALEXPR_4| Int) -(assert (= |EVALEXPR_4| expr_19_0)) -(check-sat) -(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| )) -","0xa81ce8317a79fc74d85d9edfe56caf9b0274a7da4556bfb418652051e0bfa679":"(set-option :produce-models true) -(set-option :timeout 1000) -(set-logic ALL) -(declare-fun |error_0| () Int) -(declare-fun |this_0| () Int) -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-fun |state_0| () |state_type|) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-fun |tx_0| () |tx_type|) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-fun |crypto_0| () |crypto_type|) -(declare-fun |x_4_0| () Int) -(declare-fun |y_6_0| () Int) -(declare-fun |k_8_0| () Int) -(declare-fun |r_34_0| () Int) -(declare-fun |expr_12_0| () Int) -(declare-fun |expr_13_0| () Int) -(declare-fun |expr_14_1| () Bool) - -(assert (and (and (and true true) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) expr_14_1)) -(check-sat) -","0xa96a68b7853fcc0a10dd525c3ff838e3bfac425b104c44b240623f7a35aee6f1":"(set-option :produce-models true) -(set-option :timeout 1000) -(set-logic ALL) -(declare-fun |error_0| () Int) -(declare-fun |this_0| () Int) -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-fun |state_0| () |state_type|) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-fun |tx_0| () |tx_type|) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-fun |crypto_0| () |crypto_type|) -(declare-fun |x_4_0| () Int) -(declare-fun |y_6_0| () Int) -(declare-fun |k_8_0| () Int) -(declare-fun |r_34_0| () Int) -(declare-fun |expr_12_0| () Int) -(declare-fun |expr_13_0| () Int) -(declare-fun |expr_14_1| () Bool) -(declare-fun |expr_18_0| () Int) -(declare-fun |expr_19_0| () Int) -(declare-fun |d_div_mod_0_0| () Int) -(declare-fun |r_div_mod_0_0| () Int) -(declare-fun |expr_20_1| () Int) -(declare-fun |expr_21_0| () Int) -(declare-fun |expr_22_1| () Bool) -(declare-fun |expr_26_0| () Int) -(declare-fun |expr_27_0| () Int) -(declare-fun |d_div_mod_1_0| () Int) -(declare-fun |r_div_mod_1_0| () Int) -(declare-fun |expr_28_1| () Int) -(declare-fun |expr_29_0| () Int) -(declare-fun |expr_30_1| () Bool) -(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int) -(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int) -(declare-fun |expr_36_0| () Int) -(declare-fun |expr_37_0| () Int) -(declare-fun |expr_38_0| () Int) -(declare-fun |d_div_mod_2_0| () Int) -(declare-fun |r_div_mod_2_0| () Int) -(declare-fun |expr_39_1| () Int) -(declare-fun |r_34_1| () Int) -(declare-fun |expr_42_0| () Int) -(declare-fun |expr_43_0| () Int) -(declare-fun |d_div_mod_3_0| () Int) -(declare-fun |r_div_mod_3_0| () Int) -(declare-fun |expr_44_1| () Int) -(declare-fun |expr_45_0| () Int) -(declare-fun |expr_46_1| () Bool) - -(assert (and (and (and true true) (and (= expr_46_1 (= expr_44_1 expr_45_0)) (and (= expr_45_0 0) (and (= expr_44_1 (ite (= expr_43_0 0) 0 r_div_mod_3_0)) (and (and (<= 0 r_div_mod_3_0) (or (= expr_43_0 0) (< r_div_mod_3_0 expr_43_0))) (and (= (+ (* d_div_mod_3_0 expr_43_0) r_div_mod_3_0) expr_42_0) (and (= expr_43_0 k_8_0) (and (= expr_42_0 r_34_1) (and (ite (and true true) (= r_34_1 expr_39_1) (= r_34_1 r_34_0)) (and (= expr_39_1 (ite (= expr_38_0 0) 0 r_div_mod_2_0)) (and (and (<= 0 r_div_mod_2_0) (or (= expr_38_0 0) (< r_div_mod_2_0 expr_38_0))) (and (= (+ (* d_div_mod_2_0 expr_38_0) r_div_mod_2_0) (* expr_36_0 expr_37_0)) (and (= expr_38_0 k_8_0) (and (= expr_37_0 y_6_0) (and (= expr_36_0 x_4_0) (and true (and (implies (and true true) expr_30_1) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))))))))))))))))))) (not expr_46_1))) -(declare-const |EVALEXPR_0| Int) -(assert (= |EVALEXPR_0| x_4_0)) -(declare-const |EVALEXPR_1| Int) -(assert (= |EVALEXPR_1| y_6_0)) -(declare-const |EVALEXPR_2| Int) -(assert (= |EVALEXPR_2| k_8_0)) -(declare-const |EVALEXPR_3| Int) -(assert (= |EVALEXPR_3| r_34_1)) -(check-sat) -(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| )) -","0xcc1de975d2f5e9b3e4ff9b4f46c8248513ac3b755b60f8a630a46d12b4b11f9a":"(set-option :produce-models true) +","0x01adbdf930a8c2d705ee70e5e78e29c29dac476aa100fcb798f868f51b26204f":"(set-option :produce-models true) (set-option :timeout 1000) (set-logic ALL) (declare-fun |error_0| () Int) @@ -445,6 +43,8 @@ (declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) (declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) (declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) (declare-fun |x_4_0| () Int) (declare-fun |y_6_0| () Int) (declare-fun |k_8_0| () Int) @@ -496,6 +96,428 @@ (assert (= |EVALEXPR_4| expr_43_0)) (check-sat) (get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| )) +","0x0240b78036d9401081928b0678ac1093bc5f539b272727c2f666f50cbc42f152":"(set-option :produce-models true) +(set-option :timeout 1000) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |x_4_0| () Int) +(declare-fun |y_6_0| () Int) +(declare-fun |k_8_0| () Int) +(declare-fun |r_34_0| () Int) +(declare-fun |expr_12_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_1| () Bool) +(declare-fun |expr_18_0| () Int) +(declare-fun |expr_19_0| () Int) +(declare-fun |d_div_mod_0_0| () Int) +(declare-fun |r_div_mod_0_0| () Int) +(declare-fun |expr_20_1| () Int) +(declare-fun |expr_21_0| () Int) +(declare-fun |expr_22_1| () Bool) +(declare-fun |expr_26_0| () Int) +(declare-fun |expr_27_0| () Int) +(declare-fun |d_div_mod_1_0| () Int) +(declare-fun |r_div_mod_1_0| () Int) +(declare-fun |expr_28_1| () Int) +(declare-fun |expr_29_0| () Int) +(declare-fun |expr_30_1| () Bool) +(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int) +(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int) +(declare-fun |expr_36_0| () Int) +(declare-fun |expr_37_0| () Int) +(declare-fun |expr_38_0| () Int) +(declare-fun |d_div_mod_2_0| () Int) +(declare-fun |r_div_mod_2_0| () Int) +(declare-fun |expr_39_1| () Int) +(declare-fun |r_34_1| () Int) +(declare-fun |expr_42_0| () Int) +(declare-fun |expr_43_0| () Int) +(declare-fun |d_div_mod_3_0| () Int) +(declare-fun |r_div_mod_3_0| () Int) +(declare-fun |expr_44_1| () Int) +(declare-fun |expr_45_0| () Int) +(declare-fun |expr_46_1| () Bool) + +(assert (and (and (and true true) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))) (= expr_19_0 0))) +(declare-const |EVALEXPR_0| Int) +(assert (= |EVALEXPR_0| x_4_0)) +(declare-const |EVALEXPR_1| Int) +(assert (= |EVALEXPR_1| y_6_0)) +(declare-const |EVALEXPR_2| Int) +(assert (= |EVALEXPR_2| k_8_0)) +(declare-const |EVALEXPR_3| Int) +(assert (= |EVALEXPR_3| r_34_0)) +(declare-const |EVALEXPR_4| Int) +(assert (= |EVALEXPR_4| expr_19_0)) +(check-sat) +(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| )) +","0x330edc0eeae79b3a01e99e82b2ee2b82fb55bb3a293e5bdf000b21347c367bf5":"(set-option :produce-models true) +(set-option :timeout 1000) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |x_4_0| () Int) +(declare-fun |y_6_0| () Int) +(declare-fun |k_8_0| () Int) +(declare-fun |r_34_0| () Int) +(declare-fun |expr_12_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_1| () Bool) +(declare-fun |expr_18_0| () Int) +(declare-fun |expr_19_0| () Int) +(declare-fun |d_div_mod_0_0| () Int) +(declare-fun |r_div_mod_0_0| () Int) +(declare-fun |expr_20_1| () Int) +(declare-fun |expr_21_0| () Int) +(declare-fun |expr_22_1| () Bool) +(declare-fun |expr_26_0| () Int) +(declare-fun |expr_27_0| () Int) +(declare-fun |d_div_mod_1_0| () Int) +(declare-fun |r_div_mod_1_0| () Int) +(declare-fun |expr_28_1| () Int) +(declare-fun |expr_29_0| () Int) +(declare-fun |expr_30_1| () Bool) + +(assert (and (and (and true true) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) (not expr_30_1))) +(check-sat) +","0x65adca9cfdac21d489384711fb7cecea5c811b2d9ea3115e661640f5c4f6b653":"(set-option :produce-models true) +(set-option :timeout 1000) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |x_4_0| () Int) +(declare-fun |y_6_0| () Int) +(declare-fun |k_8_0| () Int) +(declare-fun |r_34_0| () Int) +(declare-fun |expr_12_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_1| () Bool) +(declare-fun |expr_18_0| () Int) +(declare-fun |expr_19_0| () Int) +(declare-fun |d_div_mod_0_0| () Int) +(declare-fun |r_div_mod_0_0| () Int) +(declare-fun |expr_20_1| () Int) +(declare-fun |expr_21_0| () Int) +(declare-fun |expr_22_1| () Bool) +(declare-fun |expr_26_0| () Int) +(declare-fun |expr_27_0| () Int) +(declare-fun |d_div_mod_1_0| () Int) +(declare-fun |r_div_mod_1_0| () Int) +(declare-fun |expr_28_1| () Int) +(declare-fun |expr_29_0| () Int) +(declare-fun |expr_30_1| () Bool) +(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int) +(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int) +(declare-fun |expr_36_0| () Int) +(declare-fun |expr_37_0| () Int) +(declare-fun |expr_38_0| () Int) +(declare-fun |d_div_mod_2_0| () Int) +(declare-fun |r_div_mod_2_0| () Int) +(declare-fun |expr_39_1| () Int) +(declare-fun |r_34_1| () Int) +(declare-fun |expr_42_0| () Int) +(declare-fun |expr_43_0| () Int) +(declare-fun |d_div_mod_3_0| () Int) +(declare-fun |r_div_mod_3_0| () Int) +(declare-fun |expr_44_1| () Int) +(declare-fun |expr_45_0| () Int) +(declare-fun |expr_46_1| () Bool) + +(assert (and (and (and true true) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))))))))))) (= expr_27_0 0))) +(declare-const |EVALEXPR_0| Int) +(assert (= |EVALEXPR_0| x_4_0)) +(declare-const |EVALEXPR_1| Int) +(assert (= |EVALEXPR_1| y_6_0)) +(declare-const |EVALEXPR_2| Int) +(assert (= |EVALEXPR_2| k_8_0)) +(declare-const |EVALEXPR_3| Int) +(assert (= |EVALEXPR_3| r_34_0)) +(declare-const |EVALEXPR_4| Int) +(assert (= |EVALEXPR_4| expr_27_0)) +(check-sat) +(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| )) +","0x6615bd1d9fcf33421097f19e3ad0fb38bcd1d1191aa6ae4f0689699322e0c0d9":"(set-option :produce-models true) +(set-option :timeout 1000) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |x_4_0| () Int) +(declare-fun |y_6_0| () Int) +(declare-fun |k_8_0| () Int) +(declare-fun |r_34_0| () Int) +(declare-fun |expr_12_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_1| () Bool) +(declare-fun |expr_18_0| () Int) +(declare-fun |expr_19_0| () Int) +(declare-fun |d_div_mod_0_0| () Int) +(declare-fun |r_div_mod_0_0| () Int) +(declare-fun |expr_20_1| () Int) +(declare-fun |expr_21_0| () Int) +(declare-fun |expr_22_1| () Bool) +(declare-fun |expr_26_0| () Int) +(declare-fun |expr_27_0| () Int) +(declare-fun |d_div_mod_1_0| () Int) +(declare-fun |r_div_mod_1_0| () Int) +(declare-fun |expr_28_1| () Int) +(declare-fun |expr_29_0| () Int) +(declare-fun |expr_30_1| () Bool) + +(assert (and (and (and true true) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))) expr_30_1)) +(check-sat) +","0x7f31c70550c1d2f3c45a8c0e8468fe1477b68f37f97127d10746210f1fe97f96":"(set-option :produce-models true) +(set-option :timeout 1000) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |x_4_0| () Int) +(declare-fun |y_6_0| () Int) +(declare-fun |k_8_0| () Int) +(declare-fun |r_34_0| () Int) +(declare-fun |expr_12_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_1| () Bool) +(declare-fun |expr_18_0| () Int) +(declare-fun |expr_19_0| () Int) +(declare-fun |d_div_mod_0_0| () Int) +(declare-fun |r_div_mod_0_0| () Int) +(declare-fun |expr_20_1| () Int) +(declare-fun |expr_21_0| () Int) +(declare-fun |expr_22_1| () Bool) +(declare-fun |expr_26_0| () Int) +(declare-fun |expr_27_0| () Int) +(declare-fun |d_div_mod_1_0| () Int) +(declare-fun |r_div_mod_1_0| () Int) +(declare-fun |expr_28_1| () Int) +(declare-fun |expr_29_0| () Int) +(declare-fun |expr_30_1| () Bool) +(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int) +(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int) +(declare-fun |expr_36_0| () Int) +(declare-fun |expr_37_0| () Int) +(declare-fun |expr_38_0| () Int) +(declare-fun |d_div_mod_2_0| () Int) +(declare-fun |r_div_mod_2_0| () Int) +(declare-fun |expr_39_1| () Int) +(declare-fun |r_34_1| () Int) +(declare-fun |expr_42_0| () Int) +(declare-fun |expr_43_0| () Int) +(declare-fun |d_div_mod_3_0| () Int) +(declare-fun |r_div_mod_3_0| () Int) +(declare-fun |expr_44_1| () Int) +(declare-fun |expr_45_0| () Int) +(declare-fun |expr_46_1| () Bool) + +(assert (and (and (and true true) (and (= expr_46_1 (= expr_44_1 expr_45_0)) (and (= expr_45_0 0) (and (= expr_44_1 (ite (= expr_43_0 0) 0 r_div_mod_3_0)) (and (and (<= 0 r_div_mod_3_0) (or (= expr_43_0 0) (< r_div_mod_3_0 expr_43_0))) (and (= (+ (* d_div_mod_3_0 expr_43_0) r_div_mod_3_0) expr_42_0) (and (= expr_43_0 k_8_0) (and (= expr_42_0 r_34_1) (and (ite (and true true) (= r_34_1 expr_39_1) (= r_34_1 r_34_0)) (and (= expr_39_1 (ite (= expr_38_0 0) 0 r_div_mod_2_0)) (and (and (<= 0 r_div_mod_2_0) (or (= expr_38_0 0) (< r_div_mod_2_0 expr_38_0))) (and (= (+ (* d_div_mod_2_0 expr_38_0) r_div_mod_2_0) (* expr_36_0 expr_37_0)) (and (= expr_38_0 k_8_0) (and (= expr_37_0 y_6_0) (and (= expr_36_0 x_4_0) (and true (and (implies (and true true) expr_30_1) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))))))))))))))))))))))))))) (not expr_46_1))) +(declare-const |EVALEXPR_0| Int) +(assert (= |EVALEXPR_0| x_4_0)) +(declare-const |EVALEXPR_1| Int) +(assert (= |EVALEXPR_1| y_6_0)) +(declare-const |EVALEXPR_2| Int) +(assert (= |EVALEXPR_2| k_8_0)) +(declare-const |EVALEXPR_3| Int) +(assert (= |EVALEXPR_3| r_34_1)) +(check-sat) +(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| )) +","0x9bd658c40e2e05920cb7023c6bae797f58090029e71d5c679c9b55d2f016307e":"(set-option :produce-models true) +(set-option :timeout 1000) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |x_4_0| () Int) +(declare-fun |y_6_0| () Int) +(declare-fun |k_8_0| () Int) +(declare-fun |r_34_0| () Int) +(declare-fun |expr_12_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_1| () Bool) +(declare-fun |expr_18_0| () Int) +(declare-fun |expr_19_0| () Int) +(declare-fun |d_div_mod_0_0| () Int) +(declare-fun |r_div_mod_0_0| () Int) +(declare-fun |expr_20_1| () Int) +(declare-fun |expr_21_0| () Int) +(declare-fun |expr_22_1| () Bool) +(declare-fun |expr_26_0| () Int) +(declare-fun |expr_27_0| () Int) +(declare-fun |d_div_mod_1_0| () Int) +(declare-fun |r_div_mod_1_0| () Int) +(declare-fun |expr_28_1| () Int) +(declare-fun |expr_29_0| () Int) +(declare-fun |expr_30_1| () Bool) +(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_0| (Int Int Int ) Int) +(declare-fun |t_function_mulmod_pure$_t_uint256_$_t_uint256_$_t_uint256_$returns$_t_uint256_$_abstract_0| () Int) +(declare-fun |expr_36_0| () Int) +(declare-fun |expr_37_0| () Int) +(declare-fun |expr_38_0| () Int) +(declare-fun |d_div_mod_2_0| () Int) +(declare-fun |r_div_mod_2_0| () Int) +(declare-fun |expr_39_1| () Int) +(declare-fun |r_34_1| () Int) +(declare-fun |expr_42_0| () Int) +(declare-fun |expr_43_0| () Int) +(declare-fun |d_div_mod_3_0| () Int) +(declare-fun |r_div_mod_3_0| () Int) +(declare-fun |expr_44_1| () Int) +(declare-fun |expr_45_0| () Int) +(declare-fun |expr_46_1| () Bool) + +(assert (and (and (and true true) (and (= expr_38_0 k_8_0) (and (= expr_37_0 y_6_0) (and (= expr_36_0 x_4_0) (and true (and (implies (and true true) expr_30_1) (and (= expr_30_1 (= expr_28_1 expr_29_0)) (and (= expr_29_0 0) (and (= expr_28_1 (ite (= expr_27_0 0) 0 r_div_mod_1_0)) (and (and (<= 0 r_div_mod_1_0) (or (= expr_27_0 0) (< r_div_mod_1_0 expr_27_0))) (and (= (+ (* d_div_mod_1_0 expr_27_0) r_div_mod_1_0) expr_26_0) (and (= expr_27_0 k_8_0) (and (= expr_26_0 y_6_0) (and (implies (and true true) expr_22_1) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true))))))))))))))))))))))))))))) (= expr_38_0 0))) +(declare-const |EVALEXPR_0| Int) +(assert (= |EVALEXPR_0| x_4_0)) +(declare-const |EVALEXPR_1| Int) +(assert (= |EVALEXPR_1| y_6_0)) +(declare-const |EVALEXPR_2| Int) +(assert (= |EVALEXPR_2| k_8_0)) +(declare-const |EVALEXPR_3| Int) +(assert (= |EVALEXPR_3| r_34_0)) +(declare-const |EVALEXPR_4| Int) +(assert (= |EVALEXPR_4| expr_38_0)) +(check-sat) +(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| )) +","0xc47149a0c48b40420cedfb8f77dc50e53fdad2f202344393df79022cd0b2105c":"(set-option :produce-models true) +(set-option :timeout 1000) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |x_4_0| () Int) +(declare-fun |y_6_0| () Int) +(declare-fun |k_8_0| () Int) +(declare-fun |r_34_0| () Int) +(declare-fun |expr_12_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_1| () Bool) +(declare-fun |expr_18_0| () Int) +(declare-fun |expr_19_0| () Int) +(declare-fun |d_div_mod_0_0| () Int) +(declare-fun |r_div_mod_0_0| () Int) +(declare-fun |expr_20_1| () Int) +(declare-fun |expr_21_0| () Int) +(declare-fun |expr_22_1| () Bool) + +(assert (and (and (and true true) (and (= expr_22_1 (= expr_20_1 expr_21_0)) (and (= expr_21_0 0) (and (= expr_20_1 (ite (= expr_19_0 0) 0 r_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_19_0 0) (< r_div_mod_0_0 expr_19_0))) (and (= (+ (* d_div_mod_0_0 expr_19_0) r_div_mod_0_0) expr_18_0) (and (= expr_19_0 k_8_0) (and (= expr_18_0 x_4_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))))))))))) (not expr_22_1))) +(check-sat) +","0xcb2117c40da91e8a86270886eca9e12cf9524141e96a95d18711d0c97f974086":"(set-option :produce-models true) +(set-option :timeout 1000) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |x_4_0| () Int) +(declare-fun |y_6_0| () Int) +(declare-fun |k_8_0| () Int) +(declare-fun |r_34_0| () Int) +(declare-fun |expr_12_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_1| () Bool) + +(assert (and (and (and true true) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) (not expr_14_1))) +(check-sat) +","0xcc5b317723ba883782a53eb35e82063ffcd1eee56de51d63c6c2971413b03d3a":"(set-option :produce-models true) +(set-option :timeout 1000) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-fun |crypto_0| () |crypto_type|) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |abi_0| () |abi_type|) +(declare-fun |x_4_0| () Int) +(declare-fun |y_6_0| () Int) +(declare-fun |k_8_0| () Int) +(declare-fun |r_34_0| () Int) +(declare-fun |expr_12_0| () Int) +(declare-fun |expr_13_0| () Int) +(declare-fun |expr_14_1| () Bool) + +(assert (and (and (and true true) (and (= expr_14_1 (> expr_12_0 expr_13_0)) (and (= expr_13_0 0) (and (= expr_12_0 k_8_0) (and (and (>= k_8_0 0) (<= k_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= y_6_0 0) (<= y_6_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (= r_34_0 0) true)))))))) expr_14_1)) +(check-sat) "}},"errors":[{"component":"general","errorCode":"7812","formattedMessage":"Warning: BMC: Assertion violation might happen here. --> A:6:85: | diff --git a/test/libsolidity/smtCheckerTests/abi/abi_decode_array.sol b/test/libsolidity/smtCheckerTests/abi/abi_decode_array.sol new file mode 100644 index 000000000..dd0470ce0 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_decode_array.sol @@ -0,0 +1,67 @@ +pragma experimental SMTChecker; +pragma abicoder v2; + +contract C { + function abiDecodeArray(bytes memory b1, bytes memory b2) public pure { + (uint[] memory a, uint[] memory b) = abi.decode(b1, (uint[], uint[])); + assert(a.length == b.length); // should fail + + (uint[] memory c, uint[] memory d) = abi.decode(b1, (uint[], uint[])); + assert(a.length == c.length); + assert(a.length == d.length); // should fail + assert(b.length == d.length); + assert(b.length == c.length); // should fail + + (uint[] memory e, uint[] memory f, uint[] memory g) = abi.decode(b1, (uint[], uint[], uint[])); + assert(e.length == a.length); // should fail + assert(f.length == b.length); // should fail + assert(e.length == g.length); // should fail + + (uint[][] memory h, uint[][][] memory i, uint j) = abi.decode(b1, (uint[][], uint[][][], uint)); + assert(h[j].length == i[j][j].length); // should fail + + (uint[] memory k, uint[] memory l) = abi.decode(b2, (uint[], uint[])); + assert(k.length == a.length); // should fail + assert(k.length == l.length); // should fail + assert(l.length == b.length); // should fail + } +} +// ---- +// Warning 8364: (194-200): Assertion checker does not yet implement type type(uint256[] memory) +// Warning 8364: (202-208): Assertion checker does not yet implement type type(uint256[] memory) +// Warning 8364: (315-321): Assertion checker does not yet implement type type(uint256[] memory) +// Warning 8364: (323-329): Assertion checker does not yet implement type type(uint256[] memory) +// Warning 8364: (564-570): Assertion checker does not yet implement type type(uint256[] memory) +// Warning 8364: (572-578): Assertion checker does not yet implement type type(uint256[] memory) +// Warning 8364: (580-586): Assertion checker does not yet implement type type(uint256[] memory) +// Warning 8364: (801-807): Assertion checker does not yet implement type type(uint256[] memory) +// Warning 8364: (801-809): Assertion checker does not yet implement type type(uint256[] memory[] memory) +// Warning 8364: (811-817): Assertion checker does not yet implement type type(uint256[] memory) +// Warning 8364: (811-819): Assertion checker does not yet implement type type(uint256[] memory[] memory) +// Warning 8364: (811-821): Assertion checker does not yet implement type type(uint256[] memory[] memory[] memory) +// Warning 8364: (943-949): Assertion checker does not yet implement type type(uint256[] memory) +// Warning 8364: (951-957): Assertion checker does not yet implement type type(uint256[] memory) +// Warning 6328: (214-242): CHC: Assertion violation happens here. +// Warning 6328: (367-395): CHC: Assertion violation happens here. +// Warning 6328: (446-474): CHC: Assertion violation happens here. +// Warning 6328: (592-620): CHC: Assertion violation happens here. +// Warning 6328: (639-667): CHC: Assertion violation happens here. +// Warning 6328: (686-714): CHC: Assertion violation happens here. +// Warning 6328: (833-870): CHC: Assertion violation happens here. +// Warning 6328: (963-991): CHC: Assertion violation happens here. +// Warning 6328: (1010-1038): CHC: Assertion violation happens here. +// Warning 6328: (1057-1085): CHC: Assertion violation happens here. +// Warning 8364: (194-200): Assertion checker does not yet implement type type(uint256[] memory) +// Warning 8364: (202-208): Assertion checker does not yet implement type type(uint256[] memory) +// Warning 8364: (315-321): Assertion checker does not yet implement type type(uint256[] memory) +// Warning 8364: (323-329): Assertion checker does not yet implement type type(uint256[] memory) +// Warning 8364: (564-570): Assertion checker does not yet implement type type(uint256[] memory) +// Warning 8364: (572-578): Assertion checker does not yet implement type type(uint256[] memory) +// Warning 8364: (580-586): Assertion checker does not yet implement type type(uint256[] memory) +// Warning 8364: (801-807): Assertion checker does not yet implement type type(uint256[] memory) +// Warning 8364: (801-809): Assertion checker does not yet implement type type(uint256[] memory[] memory) +// Warning 8364: (811-817): Assertion checker does not yet implement type type(uint256[] memory) +// Warning 8364: (811-819): Assertion checker does not yet implement type type(uint256[] memory[] memory) +// Warning 8364: (811-821): Assertion checker does not yet implement type type(uint256[] memory[] memory[] memory) +// Warning 8364: (943-949): Assertion checker does not yet implement type type(uint256[] memory) +// Warning 8364: (951-957): Assertion checker does not yet implement type type(uint256[] memory) diff --git a/test/libsolidity/smtCheckerTests/abi/abi_decode_simple.sol b/test/libsolidity/smtCheckerTests/abi/abi_decode_simple.sol new file mode 100644 index 000000000..8c4b8d678 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_decode_simple.sol @@ -0,0 +1,30 @@ +pragma experimental SMTChecker; +contract C { + function abiDecodeSimple(bytes memory b1, bytes memory b2) public pure { + (uint x, uint y) = abi.decode(b1, (uint, uint)); + (uint z, uint w) = abi.decode(b1, (uint, uint)); + assert(x == z); + assert(x == y); // should fail + assert(y == w); + assert(z == w); // should fail + + (uint a, uint b, bool c) = abi.decode(b1, (uint, uint, bool)); + assert(a == x); // should fail + assert(b == y); // should fail + assert(c); // should fail + + (uint k, uint l) = abi.decode(b2, (uint, uint)); + assert(k == x); // should fail + assert(l == y); // should fail + } +} +// ==== +// SMTIgnoreCex: yes +// ---- +// Warning 6328: (241-255): CHC: Assertion violation happens here. +// Warning 6328: (292-306): CHC: Assertion violation happens here. +// Warning 6328: (391-405): CHC: Assertion violation happens here. +// Warning 6328: (424-438): CHC: Assertion violation happens here. +// Warning 6328: (457-466): CHC: Assertion violation happens here. +// Warning 6328: (537-551): CHC: Assertion violation happens here. +// Warning 6328: (570-584): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice.sol new file mode 100644 index 000000000..6318e55c2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice.sol @@ -0,0 +1,31 @@ +pragma experimental SMTChecker; +contract C { + function abiEncodeSlice(bytes calldata data) external pure { + bytes memory b1 = abi.encode(data); + bytes memory b2 = abi.encode(data[0:]); + // should hold but the engine cannot infer that data is fully equals data[0:] because each index is assigned separately + assert(b1.length == b2.length); // fails for now + + // Disabled because of Spacer nondeterminism + //bytes memory b3 = abi.encode(data[:data.length]); + // should hold but the engine cannot infer that data is fully equals data[:data.length] because each index is assigned separately + //assert(b1.length == b3.length); // fails for now + + bytes memory b4 = abi.encode(data[5:10]); + assert(b1.length == b4.length); // should fail + + uint x = 5; + uint y = 10; + bytes memory b5 = abi.encode(data[x:y]); + // should hold but the engine cannot infer that data[5:10] is fully equals data[x:y] because each index is assigned separately + assert(b1.length == b5.length); // fails for now + } +} +// ---- +// Warning 6328: (311-341): CHC: Assertion violation happens here. +// Warning 1218: (694-724): CHC: Error trying to invoke SMT solver. +// Warning 6328: (694-724): CHC: Assertion violation might happen here. +// Warning 1218: (945-975): CHC: Error trying to invoke SMT solver. +// Warning 6328: (945-975): CHC: Assertion violation might happen here. +// Warning 4661: (694-724): BMC: Assertion violation happens here. +// Warning 4661: (945-975): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice_2.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice_2.sol new file mode 100644 index 000000000..351721d2a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice_2.sol @@ -0,0 +1,31 @@ +pragma experimental SMTChecker; +contract C { + function abiEncodeSlice(uint[] calldata data) external pure { + bytes memory b1 = abi.encode(data); + bytes memory b2 = abi.encode(data[0:]); + // should hold but the engine cannot infer that data is fully equals data[0:] because each index is assigned separately + assert(b1.length == b2.length); // fails for now + + bytes memory b3 = abi.encode(data[:data.length]); + // should hold but the engine cannot infer that data is fully equals data[:data.length] because each index is assigned separately + assert(b1.length == b3.length); // fails for now + + bytes memory b4 = abi.encode(data[5:10]); + assert(b1.length == b4.length); // should fail + + uint x = 5; + uint y = 10; + bytes memory b5 = abi.encode(data[x:y]); + // should hold but the engine cannot infer that data[5:10] is fully equals data[x:y] because each index is assigned separately + assert(b1.length == b5.length); // fails for now + } +} +// ---- +// Warning 6328: (312-342): CHC: Assertion violation happens here. +// Warning 6328: (548-578): CHC: Assertion violation happens here. +// Warning 1218: (644-674): CHC: Error trying to invoke SMT solver. +// Warning 6328: (644-674): CHC: Assertion violation might happen here. +// Warning 1218: (895-925): CHC: Error trying to invoke SMT solver. +// Warning 6328: (895-925): CHC: Assertion violation might happen here. +// Warning 4661: (644-674): BMC: Assertion violation happens here. +// Warning 4661: (895-925): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_hash.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_hash.sol new file mode 100644 index 000000000..dd4762fe2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_hash.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; +contract C { + function abiEncodeHash(uint a, uint b) public pure { + require(a == b); + bytes memory b1 = abi.encode(a, a, a, a); + bytes memory b2 = abi.encode(b, a, b, a); + assert(keccak256(b1) == keccak256(b2)); + } +} diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice.sol new file mode 100644 index 000000000..3538f9130 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice.sol @@ -0,0 +1,36 @@ +pragma experimental SMTChecker; +contract C { + function abiencodePackedSlice(bytes calldata data) external pure { + bytes memory b1 = abi.encodePacked(data); + bytes memory b2 = abi.encodePacked(data[0:]); + // should hold but the engine cannot infer that data is fully equals data[0:] because each index is assigned separately + // Disabled because of Spacer nondeterminism + //assert(b1.length == b2.length); // fails for now + + // Disabled because of Spacer nondeterminism + //bytes memory b3 = abi.encodePacked(data[:data.length]); + // should hold but the engine cannot infer that data is fully equals data[:data.length] because each index is assigned separately + //assert(b1.length == b3.length); // fails for now + + bytes memory b4 = abi.encodePacked(data[5:10]); + // Disabled because of Spacer nondeterminism + //assert(b1.length == b4.length); // should fail + + uint x = 5; + uint y = 10; + bytes memory b5 = abi.encodePacked(data[x:y]); + // should hold but the engine cannot infer that data[5:10] is fully equals data[x:y] because each index is assigned separately + assert(b1.length == b5.length); // fails for now + + bytes memory b6 = abi.encode(data[5:10]); + // Disabled because of Spacer nondeterminism + //assert(b4.length == b6.length); // should fail + } +} +// ==== +// SMTIgnoreCex: yes +// ---- +// Warning 2072: (159-174): Unused local variable. +// Warning 2072: (723-738): Unused local variable. +// Warning 2072: (1131-1146): Unused local variable. +// Warning 6328: (1079-1109): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice_2.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice_2.sol new file mode 100644 index 000000000..f39576cba --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice_2.sol @@ -0,0 +1,37 @@ +pragma experimental SMTChecker; +contract C { + function abiencodePackedSlice(uint[] calldata data) external pure { + bytes memory b1 = abi.encodePacked(data); + bytes memory b2 = abi.encodePacked(data[0:]); + // should hold but the engine cannot infer that data is fully equals data[0:] because each index is assigned separately + assert(b1.length == b2.length); // fails for now + + // Disabled because of Spacer nondeterminism + //bytes memory b3 = abi.encodePacked(data[:data.length]); + // should hold but the engine cannot infer that data is fully equals data[:data.length] because each index is assigned separately + //assert(b1.length == b3.length); // fails for now + + bytes memory b4 = abi.encodePacked(data[5:10]); + assert(b1.length == b4.length); // should fail + + uint x = 5; + uint y = 10; + bytes memory b5 = abi.encodePacked(data[x:y]); + // should hold but the engine cannot infer that data[5:10] is fully equals data[x:y] because each index is assigned separately + assert(b1.length == b5.length); // fails for now + + bytes memory b6 = abi.encode(data[5:10]); + assert(b4.length == b6.length); // should fail + } +} +// ---- +// Warning 6328: (330-360): CHC: Assertion violation happens here. +// Warning 1218: (725-755): CHC: Error trying to invoke SMT solver. +// Warning 6328: (725-755): CHC: Assertion violation might happen here. +// Warning 1218: (982-1012): CHC: Error trying to invoke SMT solver. +// Warning 6328: (982-1012): CHC: Assertion violation might happen here. +// Warning 1218: (1078-1108): CHC: Error trying to invoke SMT solver. +// Warning 6328: (1078-1108): CHC: Assertion violation might happen here. +// Warning 4661: (725-755): BMC: Assertion violation happens here. +// Warning 4661: (982-1012): BMC: Assertion violation happens here. +// Warning 4661: (1078-1108): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_hash.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_hash.sol new file mode 100644 index 000000000..5682e4a04 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_hash.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; +contract C { + function abiencodePackedHash(uint a, uint b) public pure { + require(a == b); + bytes memory b1 = abi.encodePacked(a, a, a, a); + bytes memory b2 = abi.encodePacked(b, a, b, a); + assert(keccak256(b1) == keccak256(b2)); + + bytes memory b3 = abi.encode(a, a, a, a); + assert(keccak256(b1) == keccak256(b3)); // should fail + } +} +// ---- +// Warning 1218: (313-351): CHC: Error trying to invoke SMT solver. +// Warning 6328: (313-351): CHC: Assertion violation might happen here. +// Warning 4661: (313-351): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_simple.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_simple.sol new file mode 100644 index 000000000..caa8c8042 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_simple.sol @@ -0,0 +1,34 @@ +pragma experimental SMTChecker; +contract C { + function abiencodePackedSimple(bool t, uint x, uint y, uint z, uint[] memory a, uint[] memory b) public pure { + require(x == y); + bytes memory b1 = abi.encodePacked(x, z, a); + bytes memory b2 = abi.encodePacked(y, z, a); + assert(b1.length == b2.length); + + bytes memory b3 = abi.encodePacked(y, z, b); + assert(b1.length == b3.length); // should fail + + bytes memory b4 = abi.encodePacked(t, z, a); + assert(b1.length == b4.length); // should fail + + bytes memory b5 = abi.encodePacked(y, y, y, y, a, a, a); + assert(b1.length != b5.length); // should fail + assert(b1.length == b5.length); // should fail + + bytes memory b6 = abi.encode(x, z, a); + assert(b1.length == b6.length); // should fail + } +} +// ---- +// Warning 6328: (354-384): CHC: Assertion violation happens here. +// Warning 1218: (451-481): CHC: Error trying to invoke SMT solver. +// Warning 6328: (451-481): CHC: Assertion violation might happen here. +// Warning 1218: (560-590): CHC: Error trying to invoke SMT solver. +// Warning 6328: (560-590): CHC: Assertion violation might happen here. +// Warning 1218: (609-639): CHC: Error trying to invoke SMT solver. +// Warning 6328: (609-639): CHC: Assertion violation might happen here. +// Warning 6328: (700-730): CHC: Assertion violation happens here. +// Warning 4661: (451-481): BMC: Assertion violation happens here. +// Warning 4661: (560-590): BMC: Assertion violation happens here. +// Warning 4661: (609-639): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol new file mode 100644 index 000000000..ea0648a91 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol @@ -0,0 +1,38 @@ +pragma experimental SMTChecker; +contract C { + function abiencodePackedStringLiteral() public pure { + bytes memory b1 = abi.encodePacked(""); + bytes memory b2 = abi.encodePacked(""); + // should hold, but currently fails due to string literal abstraction + assert(b1.length == b2.length); + + bytes memory b3 = abi.encodePacked(bytes("")); + assert(b1.length == b3.length); // should fail + + bytes memory b4 = abi.encodePacked(bytes24("")); + // should hold, but currently fails due to string literal abstraction + assert(b1.length == b4.length); + + bytes memory b5 = abi.encodePacked(string("")); + assert(b1.length == b5.length); // should fail + + bytes memory b6 = abi.encode(""); + assert(b1.length == b6.length); // should fail + } +} +// ---- +// Warning 1218: (258-288): CHC: Error trying to invoke SMT solver. +// Warning 6328: (258-288): CHC: Assertion violation might happen here. +// Warning 1218: (342-372): CHC: Error trying to invoke SMT solver. +// Warning 6328: (342-372): CHC: Assertion violation might happen here. +// Warning 1218: (515-545): CHC: Error trying to invoke SMT solver. +// Warning 6328: (515-545): CHC: Assertion violation might happen here. +// Warning 1218: (600-630): CHC: Error trying to invoke SMT solver. +// Warning 6328: (600-630): CHC: Assertion violation might happen here. +// Warning 1218: (686-716): CHC: Error trying to invoke SMT solver. +// Warning 6328: (686-716): CHC: Assertion violation might happen here. +// Warning 4661: (258-288): BMC: Assertion violation happens here. +// Warning 4661: (342-372): BMC: Assertion violation happens here. +// Warning 4661: (515-545): BMC: Assertion violation happens here. +// Warning 4661: (600-630): BMC: Assertion violation happens here. +// Warning 4661: (686-716): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_simple.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_simple.sol new file mode 100644 index 000000000..3ba9238bb --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_simple.sol @@ -0,0 +1,30 @@ +pragma experimental SMTChecker; +contract C { + function abiEncodeSimple(bool t, uint x, uint y, uint z, uint[] memory a, uint[] memory b) public pure { + require(x == y); + bytes memory b1 = abi.encode(x, z, a); + bytes memory b2 = abi.encode(y, z, a); + assert(b1.length == b2.length); + + bytes memory b3 = abi.encode(y, z, b); + assert(b1.length == b3.length); // should fail + + bytes memory b4 = abi.encode(t, z, a); + assert(b1.length == b4.length); // should fail + + bytes memory b5 = abi.encode(y, y, y, y, a, a, a); + assert(b1.length != b5.length); // should fail + assert(b1.length == b5.length); // should fail + } +} +// ---- +// Warning 1218: (330-360): CHC: Error trying to invoke SMT solver. +// Warning 6328: (330-360): CHC: Assertion violation might happen here. +// Warning 1218: (421-451): CHC: Error trying to invoke SMT solver. +// Warning 6328: (421-451): CHC: Assertion violation might happen here. +// Warning 1218: (524-554): CHC: Error trying to invoke SMT solver. +// Warning 6328: (524-554): CHC: Assertion violation might happen here. +// Warning 6328: (573-603): CHC: Assertion violation happens here. +// Warning 4661: (330-360): BMC: Assertion violation happens here. +// Warning 4661: (421-451): BMC: Assertion violation happens here. +// Warning 4661: (524-554): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol new file mode 100644 index 000000000..fadc9f48d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol @@ -0,0 +1,32 @@ +pragma experimental SMTChecker; +contract C { + function abiEncodeStringLiteral() public pure { + bytes memory b1 = abi.encode(""); + bytes memory b2 = abi.encode(""); + // should hold, but currently fails due to string literal abstraction + assert(b1.length == b2.length); + + bytes memory b3 = abi.encode(bytes("")); + assert(b1.length == b3.length); // should fail + + bytes memory b4 = abi.encode(bytes24("")); + // should hold, but currently fails due to string literal abstraction + assert(b1.length == b4.length); + + bytes memory b5 = abi.encode(string("")); + assert(b1.length == b5.length); // should fail + } +} +// ---- +// Warning 1218: (240-270): CHC: Error trying to invoke SMT solver. +// Warning 6328: (240-270): CHC: Assertion violation might happen here. +// Warning 1218: (318-348): CHC: Error trying to invoke SMT solver. +// Warning 6328: (318-348): CHC: Assertion violation might happen here. +// Warning 1218: (485-515): CHC: Error trying to invoke SMT solver. +// Warning 6328: (485-515): CHC: Assertion violation might happen here. +// Warning 1218: (564-594): CHC: Error trying to invoke SMT solver. +// Warning 6328: (564-594): CHC: Assertion violation might happen here. +// Warning 4661: (240-270): BMC: Assertion violation happens here. +// Warning 4661: (318-348): BMC: Assertion violation happens here. +// Warning 4661: (485-515): BMC: Assertion violation happens here. +// Warning 4661: (564-594): BMC: Assertion violation happens here. 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 new file mode 100644 index 000000000..fd713f1c6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol @@ -0,0 +1,37 @@ +pragma experimental SMTChecker; +contract C { + function abiEncodeSlice(bytes4 sel, bytes calldata data) external pure { + bytes memory b1 = abi.encodeWithSelector(sel, data); + bytes memory b2 = abi.encodeWithSelector(sel, data[0:]); + // should hold but the engine cannot infer that data is fully equals data[0:] because each index is assigned separately + assert(b1.length == b2.length); // fails for now + + bytes memory b3 = abi.encodeWithSelector(sel, data[:data.length]); + // should hold but the engine cannot infer that data is fully equals data[:data.length] because each index is assigned separately + assert(b1.length == b3.length); // fails for now + + bytes memory b4 = abi.encodeWithSelector(sel, data[5:10]); + assert(b1.length == b4.length); // should fail + + uint x = 5; + uint y = 10; + bytes memory b5 = abi.encodeWithSelector(sel, data[x:y]); + // should hold but the engine cannot infer that data[5:10] is fully equals data[x:y] because each index is assigned separately + assert(b1.length == b5.length); // fails for now + + bytes memory b6 = abi.encodeWithSelector(0xcafecafe, data[5:10]); + assert(b4.length == b6.length); // should fail + } +} +// ---- +// Warning 6328: (357-387): CHC: Assertion violation happens here. +// Warning 6328: (610-640): CHC: Assertion violation happens here. +// Warning 1218: (723-753): CHC: Error trying to invoke SMT solver. +// Warning 6328: (723-753): CHC: Assertion violation might happen here. +// Warning 1218: (991-1021): CHC: Error trying to invoke SMT solver. +// Warning 6328: (991-1021): CHC: Assertion violation might happen here. +// Warning 1218: (1111-1141): CHC: Error trying to invoke SMT solver. +// Warning 6328: (1111-1141): CHC: Assertion violation might happen here. +// Warning 4661: (723-753): BMC: Assertion violation happens here. +// Warning 4661: (991-1021): BMC: Assertion violation happens here. +// Warning 4661: (1111-1141): BMC: Assertion violation happens here. 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 new file mode 100644 index 000000000..3418df5a4 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol @@ -0,0 +1,37 @@ +pragma experimental SMTChecker; +contract C { + function abiEncodeSlice(bytes4 sel, uint[] calldata data) external pure { + bytes memory b1 = abi.encodeWithSelector(sel, data); + bytes memory b2 = abi.encodeWithSelector(sel, data[0:]); + // should hold but the engine cannot infer that data is fully equals data[0:] because each index is assigned separately + assert(b1.length == b2.length); // fails for now + + bytes memory b3 = abi.encodeWithSelector(sel, data[:data.length]); + // should hold but the engine cannot infer that data is fully equals data[:data.length] because each index is assigned separately + assert(b1.length == b3.length); // fails for now + + bytes memory b4 = abi.encodeWithSelector(sel, data[5:10]); + assert(b1.length == b4.length); // should fail + + uint x = 5; + uint y = 10; + bytes memory b5 = abi.encodeWithSelector(sel, data[x:y]); + // should hold but the engine cannot infer that data[5:10] is fully equals data[x:y] because each index is assigned separately + assert(b1.length == b5.length); // fails for now + + bytes memory b6 = abi.encodeWithSelector(0xcafecafe, data[5:10]); + assert(b4.length == b6.length); // should fail + } +} +// ---- +// Warning 6328: (358-388): CHC: Assertion violation happens here. +// Warning 6328: (611-641): CHC: Assertion violation happens here. +// Warning 1218: (724-754): CHC: Error trying to invoke SMT solver. +// Warning 6328: (724-754): CHC: Assertion violation might happen here. +// Warning 1218: (992-1022): CHC: Error trying to invoke SMT solver. +// Warning 6328: (992-1022): CHC: Assertion violation might happen here. +// Warning 1218: (1112-1142): CHC: Error trying to invoke SMT solver. +// Warning 6328: (1112-1142): CHC: Assertion violation might happen here. +// Warning 4661: (724-754): BMC: Assertion violation happens here. +// Warning 4661: (992-1022): BMC: Assertion violation happens here. +// Warning 4661: (1112-1142): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol new file mode 100644 index 000000000..c3d311fbc --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol @@ -0,0 +1,20 @@ +pragma experimental SMTChecker; +contract C { + function abiEncodeHash(bytes4 sel, uint a, uint b) public pure { + require(a == b); + bytes memory b1 = abi.encodeWithSelector(sel, a, a, a, a); + bytes memory b2 = abi.encodeWithSelector(sel, b, a, b, a); + assert(keccak256(b1) == keccak256(b2)); + + bytes memory b3 = abi.encodeWithSelector(0xcafecafe, a, a, a, a); + assert(keccak256(b1) == keccak256(b3)); // should fail + assert(keccak256(b1) != keccak256(b3)); // should fail + } +} +// ---- +// Warning 1218: (365-403): CHC: Error trying to invoke SMT solver. +// Warning 6328: (365-403): CHC: Assertion violation might happen here. +// Warning 1218: (422-460): CHC: Error trying to invoke SMT solver. +// Warning 6328: (422-460): CHC: Assertion violation might happen here. +// Warning 4661: (365-403): BMC: Assertion violation happens here. +// Warning 4661: (422-460): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_simple.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_simple.sol new file mode 100644 index 000000000..26696eb51 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_simple.sol @@ -0,0 +1,32 @@ +pragma experimental SMTChecker; +contract C { + function abiEncodeSimple(bytes4 sel, bool t, uint x, uint y, uint z, uint[] memory a, uint[] memory b) public pure { + require(x == y); + // Disabled because of Spacer nondeterminism + bytes memory b1 = abi.encodeWithSelector(sel, x, z, a); + //bytes memory b2 = abi.encodeWithSelector(sel, y, z, a); + //assert(b1.length == b2.length); + + // Disabled because of Spacer nondeterminism + //bytes memory b3 = abi.encodeWithSelector(sel, y, z, b); + //assert(b1.length == b3.length); // should fail + + bytes memory b4 = abi.encodeWithSelector(sel, t, z, a); + assert(b1.length == b4.length); // should fail + + bytes memory b5 = abi.encodeWithSelector(sel, y, y, y, y, a, a, a); + assert(b1.length != b5.length); // should fail + assert(b1.length == b5.length); // should fail + + bytes memory b6 = abi.encodeWithSelector(0xcafecafe, x, z, a); + assert(b1.length == b6.length); // should fail + } +} +// ---- +// Warning 5667: (132-147): Unused function parameter. Remove or comment out the variable name to silence this warning. +// Warning 6328: (603-633): CHC: Assertion violation happens here. +// Warning 6328: (723-753): CHC: Assertion violation happens here. +// Warning 6328: (772-802): CHC: Assertion violation happens here. +// Warning 1218: (887-917): CHC: Error trying to invoke SMT solver. +// Warning 6328: (887-917): CHC: Assertion violation might happen here. +// Warning 4661: (887-917): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal.sol new file mode 100644 index 000000000..79c875bc1 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal.sol @@ -0,0 +1,36 @@ +pragma experimental SMTChecker; +contract C { + function abiEncodeStringLiteral(bytes4 sel) public pure { + bytes memory b1 = abi.encodeWithSelector(sel, ""); + bytes memory b2 = abi.encodeWithSelector(sel, ""); + // should hold, but currently fails due to string literal abstraction + assert(b1.length == b2.length); + + bytes memory b3 = abi.encodeWithSelector(sel, bytes("")); + assert(b1.length == b3.length); // should fail + + bytes memory b4 = abi.encodeWithSelector(sel, bytes24("")); + // should hold, but currently fails due to string literal abstraction + assert(b1.length == b4.length); + + bytes memory b5 = abi.encodeWithSelector(sel, string("")); + assert(b1.length == b5.length); // should fail + + bytes memory b6 = abi.encodeWithSelector(0xcafecafe, bytes24("")); + assert(b4.length == b6.length); // should fail + } +} +// ---- +// Warning 6328: (284-314): CHC: Assertion violation happens here. +// Warning 1218: (379-409): CHC: Error trying to invoke SMT solver. +// Warning 6328: (379-409): CHC: Assertion violation might happen here. +// Warning 1218: (563-593): CHC: Error trying to invoke SMT solver. +// Warning 6328: (563-593): CHC: Assertion violation might happen here. +// Warning 1218: (659-689): CHC: Error trying to invoke SMT solver. +// Warning 6328: (659-689): CHC: Assertion violation might happen here. +// Warning 1218: (778-808): CHC: Error trying to invoke SMT solver. +// Warning 6328: (778-808): CHC: Assertion violation might happen here. +// Warning 4661: (379-409): BMC: Assertion violation happens here. +// Warning 4661: (563-593): BMC: Assertion violation happens here. +// Warning 4661: (659-689): BMC: Assertion violation happens here. +// Warning 4661: (778-808): BMC: Assertion violation happens here. 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 new file mode 100644 index 000000000..c76ab68e6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_vs_sig.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; +contract C { + function f(string memory sig, uint x, uint[] memory a) public pure { + bytes memory b1 = abi.encodeWithSignature(sig, x, a); + bytes memory b2 = abi.encodeWithSelector(bytes4(keccak256(bytes(sig))), x, a); + // should hold but we do not evaluate keccak256 in an interpreted way + assert(b1.length == b2.length); + } +} +// ---- +// Warning 6328: (326-356): CHC: Assertion violation might happen here. +// Warning 7812: (326-356): 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 new file mode 100644 index 000000000..a108d6f69 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol @@ -0,0 +1,37 @@ +pragma experimental SMTChecker; +contract C { + function abiEncodeSlice(string memory sig, bytes calldata data) external pure { + bytes memory b1 = abi.encodeWithSignature(sig, data); + bytes memory b2 = abi.encodeWithSignature(sig, data[0:]); + // should hold but the engine cannot infer that data is fully equals data[0:] because each index is assigned separately + assert(b1.length == b2.length); // fails for now + + bytes memory b3 = abi.encodeWithSignature(sig, data[:data.length]); + // should hold but the engine cannot infer that data is fully equals data[:data.length] because each index is assigned separately + assert(b1.length == b3.length); // fails for now + + bytes memory b4 = abi.encodeWithSignature(sig, data[5:10]); + assert(b1.length == b4.length); // should fail + + uint x = 5; + uint y = 10; + bytes memory b5 = abi.encodeWithSignature(sig, data[x:y]); + // should hold but the engine cannot infer that data[5:10] is fully equals data[x:y] because each index is assigned separately + assert(b1.length == b5.length); // fails for now + + bytes memory b6 = abi.encodeWithSelector("f()", data[5:10]); + assert(b4.length == b6.length); // should fail + } +} +// ---- +// Warning 6328: (366-396): CHC: Assertion violation happens here. +// Warning 6328: (620-650): CHC: Assertion violation happens here. +// Warning 1218: (734-764): CHC: Error trying to invoke SMT solver. +// Warning 6328: (734-764): CHC: Assertion violation might happen here. +// Warning 1218: (1003-1033): CHC: Error trying to invoke SMT solver. +// Warning 6328: (1003-1033): CHC: Assertion violation might happen here. +// Warning 1218: (1118-1148): CHC: Error trying to invoke SMT solver. +// Warning 6328: (1118-1148): CHC: Assertion violation might happen here. +// Warning 4661: (734-764): BMC: Assertion violation happens here. +// Warning 4661: (1003-1033): BMC: Assertion violation happens here. +// Warning 4661: (1118-1148): 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 new file mode 100644 index 000000000..053d08d6d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol @@ -0,0 +1,37 @@ +pragma experimental SMTChecker; +contract C { + function abiEncodeSlice(string memory sig, uint[] calldata data) external pure { + bytes memory b1 = abi.encodeWithSignature(sig, data); + bytes memory b2 = abi.encodeWithSignature(sig, data[0:]); + // should hold but the engine cannot infer that data is fully equals data[0:] because each index is assigned separately + assert(b1.length == b2.length); // fails for now + + bytes memory b3 = abi.encodeWithSignature(sig, data[:data.length]); + // should hold but the engine cannot infer that data is fully equals data[:data.length] because each index is assigned separately + assert(b1.length == b3.length); // fails for now + + bytes memory b4 = abi.encodeWithSignature(sig, data[5:10]); + assert(b1.length == b4.length); // should fail + + uint x = 5; + uint y = 10; + bytes memory b5 = abi.encodeWithSignature(sig, data[x:y]); + // should hold but the engine cannot infer that data[5:10] is fully equals data[x:y] because each index is assigned separately + assert(b1.length == b5.length); // fails for now + + bytes memory b6 = abi.encodeWithSelector("f()", data[5:10]); + assert(b4.length == b6.length); // should fail + } +} +// ---- +// Warning 6328: (367-397): CHC: Assertion violation happens here. +// Warning 6328: (621-651): CHC: Assertion violation happens here. +// Warning 1218: (735-765): CHC: Error trying to invoke SMT solver. +// Warning 6328: (735-765): CHC: Assertion violation might happen here. +// Warning 1218: (1004-1034): CHC: Error trying to invoke SMT solver. +// Warning 6328: (1004-1034): CHC: Assertion violation might happen here. +// Warning 1218: (1119-1149): CHC: Error trying to invoke SMT solver. +// Warning 6328: (1119-1149): CHC: Assertion violation might happen here. +// Warning 4661: (735-765): BMC: Assertion violation happens here. +// Warning 4661: (1004-1034): BMC: Assertion violation happens here. +// Warning 4661: (1119-1149): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_hash.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_hash.sol new file mode 100644 index 000000000..fc499921b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_hash.sol @@ -0,0 +1,20 @@ +pragma experimental SMTChecker; +contract C { + function abiEncodeHash(string memory sig, uint a, uint b) public pure { + require(a == b); + bytes memory b1 = abi.encodeWithSignature(sig, a, a, a, a); + bytes memory b2 = abi.encodeWithSignature(sig, b, a, b, a); + assert(keccak256(b1) == keccak256(b2)); + + bytes memory b3 = abi.encodeWithSelector("f()", a, a, a, a); + assert(keccak256(b1) == keccak256(b3)); // should fail + assert(keccak256(b1) != keccak256(b3)); // should fail + } +} +// ---- +// Warning 1218: (369-407): CHC: Error trying to invoke SMT solver. +// Warning 6328: (369-407): CHC: Assertion violation might happen here. +// Warning 1218: (426-464): CHC: Error trying to invoke SMT solver. +// Warning 6328: (426-464): CHC: Assertion violation might happen here. +// Warning 4661: (369-407): BMC: Assertion violation happens here. +// Warning 4661: (426-464): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_simple.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_simple.sol new file mode 100644 index 000000000..9b3b7d185 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_simple.sol @@ -0,0 +1,34 @@ +pragma experimental SMTChecker; +contract C { + function abiEncodeSimple(string memory sig, bool t, uint x, uint y, uint z, uint[] memory a, uint[] memory b) public pure { + require(x == y); + bytes memory b1 = abi.encodeWithSignature(sig, x, z, a); + bytes memory b2 = abi.encodeWithSignature(sig, y, z, a); + assert(b1.length == b2.length); + + bytes memory b3 = abi.encodeWithSignature(sig, y, z, b); + assert(b1.length == b3.length); // should fail + + bytes memory b4 = abi.encodeWithSignature(sig, t, z, a); + assert(b1.length == b4.length); // should fail + + bytes memory b5 = abi.encodeWithSignature(sig, y, y, y, y, a, a, a); + assert(b1.length != b5.length); // should fail + assert(b1.length == b5.length); // should fail + + bytes memory b6 = abi.encodeWithSignature("f()", x, z, a); + assert(b1.length == b6.length); // should fail + } +} +// ---- +// Warning 6328: (403-433): CHC: Assertion violation happens here. +// Warning 6328: (512-542): CHC: Assertion violation happens here. +// Warning 1218: (633-663): CHC: Error trying to invoke SMT solver. +// Warning 6328: (633-663): CHC: Assertion violation might happen here. +// Warning 1218: (682-712): CHC: Error trying to invoke SMT solver. +// Warning 6328: (682-712): CHC: Assertion violation might happen here. +// Warning 1218: (793-823): CHC: Error trying to invoke SMT solver. +// Warning 6328: (793-823): CHC: Assertion violation might happen here. +// Warning 4661: (633-663): BMC: Assertion violation happens here. +// Warning 4661: (682-712): BMC: Assertion violation happens here. +// Warning 4661: (793-823): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_string_literal.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_string_literal.sol new file mode 100644 index 000000000..e586e6fba --- /dev/null +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_string_literal.sol @@ -0,0 +1,36 @@ +pragma experimental SMTChecker; +contract C { + function abiEncodeStringLiteral(string memory sig) public pure { + bytes memory b1 = abi.encodeWithSignature(sig, ""); + bytes memory b2 = abi.encodeWithSignature(sig, ""); + // should hold, but currently fails due to string literal abstraction + assert(b1.length == b2.length); + + bytes memory b3 = abi.encodeWithSignature(sig, bytes("")); + assert(b1.length == b3.length); // should fail + + bytes memory b4 = abi.encodeWithSignature(sig, bytes24("")); + // should hold, but currently fails due to string literal abstraction + assert(b1.length == b4.length); + + bytes memory b5 = abi.encodeWithSignature(sig, string("")); + assert(b1.length == b5.length); // should fail + + bytes memory b6 = abi.encodeWithSelector("f()", bytes24("")); + assert(b4.length == b6.length); // should fail + } +} +// ---- +// Warning 6328: (293-323): CHC: Assertion violation happens here. +// Warning 1218: (389-419): CHC: Error trying to invoke SMT solver. +// Warning 6328: (389-419): CHC: Assertion violation might happen here. +// Warning 1218: (574-604): CHC: Error trying to invoke SMT solver. +// Warning 6328: (574-604): CHC: Assertion violation might happen here. +// Warning 1218: (671-701): CHC: Error trying to invoke SMT solver. +// Warning 6328: (671-701): CHC: Assertion violation might happen here. +// Warning 1218: (785-815): CHC: Error trying to invoke SMT solver. +// Warning 6328: (785-815): CHC: Assertion violation might happen here. +// Warning 4661: (389-419): BMC: Assertion violation happens here. +// Warning 4661: (574-604): BMC: Assertion violation happens here. +// Warning 4661: (671-701): BMC: Assertion violation happens here. +// Warning 4661: (785-815): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol index 0b2955154..477c5a4c6 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol @@ -12,4 +12,4 @@ contract C { } } // ---- -// Warning 6328: (167-188): CHC: Assertion violation happens here.\nCounterexample:\na = [[17, 12, 12, 12, 12], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15]]\n\n\n\nTransaction trace:\nconstructor()\nState: a = []\nf() +// Warning 6328: (167-188): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nState: a = []\nf() diff --git a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol index 5fff9d312..2b8bf69f4 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol @@ -19,5 +19,5 @@ contract C { } } // ---- -// Warning 6328: (193-217): CHC: Assertion violation happens here.\nCounterexample:\na = [[12, 12, 12, 12, 12, 12, 12, 6, 12, 8, 12, 10, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15], [15, 15]], c = [], d = []\n\n\n\nTransaction trace:\nconstructor()\nState: a = [], c = [], d = []\nf() -// Warning 6328: (309-333): CHC: Assertion violation happens here.\nCounterexample:\na = [[24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 23, 24, 24, 24, 24, 24, 24, 16, 24, 24, 19, 24, 21, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27], [27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27]], c = [[[3, 15, 15, 15, 15, 15], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36], [36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36, 36]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]], [[42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42], [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]]], d = []\n\n\n\nTransaction trace:\nconstructor()\nState: a = [], c = [], d = []\nf() +// Warning 6328: (193-217): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nState: a = [], c = [], d = []\nf() +// Warning 6328: (309-333): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol b/test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol index 3f8296d46..e5df8eb8a 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol @@ -10,4 +10,4 @@ contract C { } } // ---- -// Warning 6328: (199-234): CHC: Assertion violation happens here.\nCounterexample:\n\na = 2437\n\n\nTransaction trace:\nconstructor()\nf(2437) +// Warning 6328: (199-234): CHC: Assertion violation happens here.\nCounterexample:\n\na = 21238\n\n\nTransaction trace:\nconstructor()\nf(21238) diff --git a/test/libsolidity/smtCheckerTests/complex/MerkleProof.sol b/test/libsolidity/smtCheckerTests/complex/MerkleProof.sol index 187bf87f7..0e18796a1 100644 --- a/test/libsolidity/smtCheckerTests/complex/MerkleProof.sol +++ b/test/libsolidity/smtCheckerTests/complex/MerkleProof.sol @@ -34,7 +34,3 @@ library MerkleProof { } // ---- -// Warning 4588: (988-1032): Assertion checker does not yet implement this type of function call. -// Warning 4588: (1175-1219): Assertion checker does not yet implement this type of function call. -// Warning 4588: (988-1032): Assertion checker does not yet implement this type of function call. -// Warning 4588: (1175-1219): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol b/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol index 69da6b331..bf7345c75 100644 --- a/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol +++ b/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol @@ -83,6 +83,10 @@ contract InternalCall { // Warning 2018: (1144-1206): Function state mutability can be restricted to pure // Warning 2018: (1212-1274): Function state mutability can be restricted to pure // Warning 2018: (1280-1342): Function state mutability can be restricted to pure -// Warning 4588: (771-814): Assertion checker does not yet implement this type of function call. -// Warning 4588: (771-814): Assertion checker does not yet implement this type of function call. +// Warning 4588: (714-749): Assertion checker does not yet implement this type of function call. +// Warning 4588: (760-815): Assertion checker does not yet implement this type of function call. +// Warning 4588: (887-919): Assertion checker does not yet implement this type of function call. +// Warning 4588: (714-749): Assertion checker does not yet implement this type of function call. +// Warning 4588: (760-815): Assertion checker does not yet implement this type of function call. +// Warning 4588: (887-919): Assertion checker does not yet implement this type of function call. // Warning 5729: (1403-1408): BMC does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init_chain_alternate.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init_chain_alternate.sol index f82b7de23..0cd03a113 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init_chain_alternate.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init_chain_alternate.sol @@ -25,4 +25,4 @@ contract D is C { } } // ---- -// Warning 6328: (319-333): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\na = 0\n\n\nTransaction trace:\nconstructor(0) +// Warning 6328: (319-333): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\na = 1\n\n\nTransaction trace:\nconstructor(1) diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructors.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructors.sol index 2a014ecc7..05595cbde 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructors.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructors.sol @@ -26,6 +26,6 @@ contract C is B { } // ---- // Warning 5740: (152-157): Unreachable code. -// Warning 6328: (310-324): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 1\n\n\nTransaction trace:\nconstructor(1) +// Warning 6328: (310-324): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\na = 0\n\n\nTransaction trace:\nconstructor(0) // Warning 6328: (343-357): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 1\n\n\nTransaction trace:\nconstructor(1) // Warning 6328: (376-390): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\na = 0\n\n\nTransaction trace:\nconstructor(0) diff --git a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_compare_hashes.sol b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_compare_hashes.sol index 6e2534e20..86570e811 100644 --- a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_compare_hashes.sol +++ b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_compare_hashes.sol @@ -10,7 +10,9 @@ contract C { assert(r == k); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (183-197): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [7, 7]\n\n\nTransaction trace:\nconstructor()\nf([7, 7]) -// Warning 6328: (201-215): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [9, 9]\n\n\nTransaction trace:\nconstructor()\nf([9, 9]) -// Warning 6328: (219-233): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [7, 7]\n\n\nTransaction trace:\nconstructor()\nf([7, 7]) +// Warning 6328: (183-197): CHC: Assertion violation happens here. +// Warning 6328: (201-215): CHC: Assertion violation happens here. +// Warning 6328: (219-233): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_not_same.sol b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_not_same.sol index 13537a23d..54a0bdd35 100644 --- a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_not_same.sol +++ b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_not_same.sol @@ -11,4 +11,4 @@ contract C { } } // ---- -// Warning 6328: (229-243): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7]\n\n\nTransaction trace:\nconstructor()\nf([7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7]) +// Warning 6328: (229-243): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf(data) diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol b/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol index deab0cc9a..3448f1221 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol @@ -17,7 +17,9 @@ contract C { assert(x < 10); } } +// ==== +// SMTIgnoreCex: yes // ---- // Warning 4984: (146-149): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. -// Warning 6328: (189-203): CHC: Assertion violation happens here.\nCounterexample:\nx = 10, d = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, d = 0\ninc()\nState: x = 1, d = 0\ninc()\nState: x = 2, d = 0\nf() +// Warning 6328: (189-203): CHC: Assertion violation happens here. // Warning 2661: (146-149): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol b/test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol index 3c7fc141e..1f4eb6d6f 100644 --- a/test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol +++ b/test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol @@ -5,7 +5,3 @@ contract C { } } // ---- -// Warning 4588: (162-176): Assertion checker does not yet implement this type of function call. -// Warning 4588: (178-203): Assertion checker does not yet implement this type of function call. -// Warning 4588: (162-176): Assertion checker does not yet implement this type of function call. -// Warning 4588: (178-203): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol index 2af4d4669..60e987ad5 100644 --- a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol @@ -18,6 +18,6 @@ contract A is B { } } // ---- -// Warning 4984: (230-235): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 4984: (230-235): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639935) // Warning 4984: (207-212): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639935) // Warning 4984: (198-203): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639935) diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_2.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_2.sol index 1b02db694..b5e63ec55 100644 --- a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_2.sol +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_2.sol @@ -24,7 +24,9 @@ contract A is B2, B1 { assert(a == x + 1); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 4984: (200-205): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639934\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639934) +// Warning 4984: (200-205): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 4984: (314-319): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. -// Warning 6328: (302-320): CHC: Assertion violation happens here.\nCounterexample:\na = 0\nx = 0\n\n\nTransaction trace:\nconstructor(0) +// Warning 6328: (302-320): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol index c8412f96d..f0bfc37cc 100644 --- a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol @@ -26,8 +26,10 @@ contract A is B2, B1 { assert(b1 != b2); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 4984: (160-165): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nb1 = 0, a = 115792089237316195423570985008687907853269984665640564039457584007913129639935\nx = 1\n\n\nTransaction trace:\nconstructor(1) -// Warning 4984: (241-246): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nb2 = 0, a = 1\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639935) -// Warning 4984: (225-230): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nb2 = 0, a = 0\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639934\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639934) +// Warning 4984: (160-165): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 4984: (241-246): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 4984: (225-230): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 6328: (334-350): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol b/test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol index 8c6ee5517..0c8108559 100644 --- a/test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol +++ b/test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol @@ -13,4 +13,4 @@ contract C { } } // ---- -// Warning 6328: (145-159): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 11\n\n\nTransaction trace:\nconstructor()\nState: x = 10\nf(11) +// Warning 6328: (145-159): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 9\n\n\nTransaction trace:\nconstructor()\nState: x = 10\nf(9) diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_state_value_inherited.sol b/test/libsolidity/smtCheckerTests/functions/constructor_state_value_inherited.sol index 100183012..1c5b62abc 100644 --- a/test/libsolidity/smtCheckerTests/functions/constructor_state_value_inherited.sol +++ b/test/libsolidity/smtCheckerTests/functions/constructor_state_value_inherited.sol @@ -15,4 +15,4 @@ contract C is B { } } // ---- -// Warning 6328: (165-179): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 9\n\n\nTransaction trace:\nconstructor()\nState: x = 10\nf(9) +// Warning 6328: (165-179): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 11\n\n\nTransaction trace:\nconstructor()\nState: x = 10\nf(11) diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol b/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol index faee3d0cf..24f04987e 100644 --- a/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol +++ b/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol @@ -13,5 +13,5 @@ contract C { } } // ---- -// Warning 6328: (162-176): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\ny = 0\n\n\nTransaction trace:\nconstructor(1, 0)\nState: x = 1\nf(0) -// Warning 4984: (115-120): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 5\na = 1\nb = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor(1, 115792089237316195423570985008687907853269984665640564039457584007913129639935) +// Warning 6328: (162-176): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 1\n\n\nTransaction trace:\nconstructor(0, 0)\nState: x = 0\nf(1) +// Warning 4984: (115-120): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 5\na = 115792089237316195423570985008687907853269984665640564039457584007913129639935\nb = 1\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639935, 1) diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol index 2dc53b7e5..97344ab23 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol @@ -17,4 +17,4 @@ contract C { } } // ---- -// Warning 6328: (293-307): CHC: Assertion violation happens here. +// Warning 6328: (293-307): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf() diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_5.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_5.sol index 5fbc0ceb8..5ff431452 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_5.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_5.sol @@ -20,5 +20,7 @@ contract C { assert(y == 1); // should fail } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (387-401): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf() +// Warning 6328: (387-401): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_1.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_1.sol index 274129c73..593ee6c4e 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_1.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_1.sol @@ -32,5 +32,5 @@ contract C is Z(5) { } } // ---- -// Warning 4984: (325-332): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 1\nz = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639935) +// Warning 4984: (325-332): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 6328: (400-413): CHC: Assertion violation happens here.\nCounterexample:\nx = 6\n\n\n\nTransaction trace:\nconstructor() diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_2.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_2.sol index adf4f0d23..6471eaa1b 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_2.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_2.sol @@ -32,7 +32,9 @@ contract C is Z(5) { assert(x > 90); // should fail } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 4984: (143-149): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 9\nb = 115792089237316195423570985008687907853269984665640564039457584007913129639927\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639927) +// Warning 4984: (143-149): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 4984: (333-340): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. -// Warning 6328: (409-423): CHC: Assertion violation happens here.\nCounterexample:\nx = 15\n\n\n\nTransaction trace:\nconstructor() +// Warning 6328: (409-423): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_5.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_5.sol index bf885f0c7..df19a2b17 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_5.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_5.sol @@ -34,6 +34,8 @@ contract C is Z, B { assert(x == k); // should fail } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 4984: (138-145): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 1\nb = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639935) +// Warning 4984: (138-145): CHC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 6328: (456-470): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol index cab6a677d..6e1c2d9c7 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol @@ -11,14 +11,15 @@ contract LoopFor2 { } // Removed because current Spacer seg faults in cex generation. //assert(b[0] == c[0]); - assert(a[0] == 900); - assert(b[0] == 900); + // Removed because current Spacer seg faults in cex generation. + //assert(a[0] == 900); + // Removed because current Spacer seg faults in cex generation. + //assert(b[0] == 900); } } // ==== // SMTIgnoreCex: yes // ---- +// Warning 2072: (156-171): Unused local variable. // Warning 4984: (252-257): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 4984: (232-238): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. -// Warning 6328: (373-392): CHC: Assertion violation happens here. -// Warning 6328: (396-415): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol index 9937ae040..88ce49dee 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol @@ -4,6 +4,9 @@ contract LoopFor2 { uint[] b; uint[] c; + // Disabled because of Spancer nondeterminism in the overflow queries + // which can't be disabled separately. + /* function testUnboundedForLoop(uint n) public { b[0] = 900; uint[] storage a = b; @@ -17,9 +20,8 @@ contract LoopFor2 { assert(a[0] == 900); assert(b[0] == 900); } + */ } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 4984: (237-242): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. -// Warning 4984: (217-223): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. -// Warning 6328: (341-360): CHC: Assertion violation happens here.\nCounterexample:\nb = [], c = []\nn = 1\n\n\nTransaction trace:\nconstructor()\nState: b = [], c = []\ntestUnboundedForLoop(1) -// Warning 6328: (364-383): CHC: Assertion violation happens here.\nCounterexample:\nb = [], c = []\nn = 1\n\n\nTransaction trace:\nconstructor()\nState: b = [], c = []\ntestUnboundedForLoop(1) diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol index 3ea615a2a..5caa00893 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol @@ -13,15 +13,16 @@ contract LoopFor2 { } // Removed because current Spacer seg faults in cex generation. //assert(b[0] == c[0]); - assert(a[0] == 900); - assert(b[0] == 900); + // Removed because current Spacer seg faults in cex generation. + //assert(a[0] == 900); + // Removed because current Spacer seg faults in cex generation. + //assert(b[0] == 900); } } // ==== // SMTIgnoreCex: yes // SMTSolvers: z3 // ---- +// Warning 2072: (156-171): Unused local variable. // Warning 4984: (244-249): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 4984: (270-273): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. -// Warning 6328: (373-392): CHC: Assertion violation happens here. -// Warning 6328: (396-415): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/loops/while_nested_break_fail.sol b/test/libsolidity/smtCheckerTests/loops/while_nested_break_fail.sol index bba71e3f1..59a0a7ee9 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_nested_break_fail.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_nested_break_fail.sol @@ -30,4 +30,4 @@ contract C } // ---- // Warning 6328: (329-344): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 10\nb = false\nc = true\n\n\nTransaction trace:\nconstructor()\nf(0, 9, false, true) -// Warning 6328: (380-395): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 15\ny = 20\nb = false\nc = false\n\n\nTransaction trace:\nconstructor()\nf(0, 0, false, false) +// Warning 6328: (380-395): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 15\ny = 0\nb = true\nc = false\n\n\nTransaction trace:\nconstructor()\nf(9, 0, true, false) diff --git a/test/libsolidity/smtCheckerTests/operators/compound_sub_array_index.sol b/test/libsolidity/smtCheckerTests/operators/compound_sub_array_index.sol index 30e43b2e8..98f0c1fca 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_sub_array_index.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_sub_array_index.sol @@ -11,5 +11,7 @@ contract C assert(array[p] < 90); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (191-212): CHC: Assertion violation happens here.\nCounterexample:\narray = []\nx = 90\np = 0\n\n\nTransaction trace:\nconstructor()\nState: array = []\nf(90, 0) +// Warning 6328: (191-212): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_sub_mapping.sol b/test/libsolidity/smtCheckerTests/operators/compound_sub_mapping.sol index 1ab625eac..2196afce2 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_sub_mapping.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_sub_mapping.sol @@ -11,5 +11,7 @@ contract C assert(map[p] < 90); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (197-216): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 99\np = 0\n\n\nTransaction trace:\nconstructor()\nf(99, 0) +// Warning 6328: (197-216): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/slice.sol b/test/libsolidity/smtCheckerTests/operators/slice.sol index 08af575de..0e52e75a1 100644 --- a/test/libsolidity/smtCheckerTests/operators/slice.sol +++ b/test/libsolidity/smtCheckerTests/operators/slice.sol @@ -4,7 +4,8 @@ contract C { function f(bytes calldata b) external pure { require(b[10] == 0xff); assert(bytes(b[10:20]).length == 10); - assert(bytes(b[10:20])[0] == 0xff); + // Disabled because of Spacer nondeterminism + //assert(bytes(b[10:20])[0] == 0xff); // Disabled because of Spacer nondeterminism //assert(bytes(b[10:20])[5] == 0xff); } diff --git a/test/libsolidity/smtCheckerTests/operators/unary_add_array.sol b/test/libsolidity/smtCheckerTests/operators/unary_add_array.sol index 401e4af62..72528553a 100644 --- a/test/libsolidity/smtCheckerTests/operators/unary_add_array.sol +++ b/test/libsolidity/smtCheckerTests/operators/unary_add_array.sol @@ -15,4 +15,4 @@ contract C } } // ---- -// Warning 6328: (240-253): CHC: Assertion violation happens here. +// Warning 6328: (240-253): CHC: Assertion violation happens here.\nCounterexample:\narray = []\nx = 0\n\n\nTransaction trace:\nconstructor()\nState: array = []\nf(0) diff --git a/test/libsolidity/smtCheckerTests/operators/unary_sub_mapping.sol b/test/libsolidity/smtCheckerTests/operators/unary_sub_mapping.sol index 0c40ad544..0d91d3638 100644 --- a/test/libsolidity/smtCheckerTests/operators/unary_sub_mapping.sol +++ b/test/libsolidity/smtCheckerTests/operators/unary_sub_mapping.sol @@ -14,5 +14,7 @@ contract C assert(b > 4); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (244-257): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\n\nTransaction trace:\nconstructor()\nf(0) +// Warning 6328: (244-257): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/overflow/overflow_mul_cex_with_array.sol b/test/libsolidity/smtCheckerTests/overflow/overflow_mul_cex_with_array.sol index d2452f7ce..f33bf9f6e 100644 --- a/test/libsolidity/smtCheckerTests/overflow/overflow_mul_cex_with_array.sol +++ b/test/libsolidity/smtCheckerTests/overflow/overflow_mul_cex_with_array.sol @@ -7,4 +7,4 @@ contract C { } } // ---- -// Warning 4984: (118-121): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\ny = 23158417847463239084714197001737581570653996933128112807891516801582625927988\n\n\nTransaction trace:\nconstructor()\nf(x, 23158417847463239084714197001737581570653996933128112807891516801582625927988) +// Warning 4984: (118-121): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = [19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 22, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19]\ny = 23158417847463239084714197001737581570653996933128112807891516801582625927988\n\n\nTransaction trace:\nconstructor()\nf([19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 22, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19, 19], 23158417847463239084714197001737581570653996933128112807891516801582625927988) diff --git a/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol index fb67403e4..f36131e85 100644 --- a/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol +++ b/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol @@ -7,4 +7,4 @@ contract C { } // ---- // Warning 4281: (110-115): CHC: Division by zero happens here.\nCounterexample:\n\nx = 0\ny = 0\n = 0\n\nTransaction trace:\nconstructor()\nf(0, 0) -// Warning 4984: (110-115): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here. +// Warning 4984: (110-115): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\ny = (- 1)\n = 0\n\nTransaction trace:\nconstructor()\nf((- 57896044618658097711785492504343953926634992332820282019728792003956564819968), (- 1)) diff --git a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol index 94a71b1fa..44186cf53 100644 --- a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol +++ b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol @@ -11,8 +11,6 @@ contract C { // Warning 8364: (231-237): Assertion checker does not yet implement type type(uint256[] memory) // Warning 8364: (231-240): Assertion checker does not yet implement type type(uint256[] memory[2] memory) // Warning 8364: (221-222): Assertion checker does not yet implement type type(struct C.S storage pointer) -// Warning 4588: (202-242): Assertion checker does not yet implement this type of function call. // Warning 8364: (231-237): Assertion checker does not yet implement type type(uint256[] memory) // Warning 8364: (231-240): Assertion checker does not yet implement type type(uint256[] memory[2] memory) // Warning 8364: (221-222): Assertion checker does not yet implement type type(struct C.S storage pointer) -// Warning 4588: (202-242): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2_value_types.sol b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2_value_types.sol index 1031aa12a..0b48ec3b3 100644 --- a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2_value_types.sol +++ b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2_value_types.sol @@ -2,18 +2,12 @@ pragma experimental SMTChecker; pragma experimental "ABIEncoderV2"; contract C { - function f() public pure { - (uint x1, bool b1) = abi.decode("abc", (uint, bool)); - (uint x2, bool b2) = abi.decode("abc", (uint, bool)); - // False positive until abi.* are implemented as uninterpreted functions. + function f(bytes memory data) public pure { + (uint x1, bool b1) = abi.decode(data, (uint, bool)); + (uint x2, bool b2) = abi.decode(data, (uint, bool)); assert(x1 == x2); } } // ---- -// Warning 2072: (122-129): Unused local variable. -// Warning 2072: (178-185): Unused local variable. -// Warning 4588: (133-164): Assertion checker does not yet implement this type of function call. -// Warning 4588: (189-220): Assertion checker does not yet implement this type of function call. -// Warning 6328: (300-316): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf() -// Warning 4588: (133-164): Assertion checker does not yet implement this type of function call. -// Warning 4588: (189-220): Assertion checker does not yet implement this type of function call. +// Warning 2072: (139-146): Unused local variable. +// Warning 2072: (194-201): Unused local variable. diff --git a/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol b/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol index 1902fd5e5..369273a07 100644 --- a/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol +++ b/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol @@ -1,25 +1,19 @@ pragma experimental SMTChecker; contract C { - function f() public pure { - (uint a1, bytes32 b1, C c1) = abi.decode("abc", (uint, bytes32, C)); - (uint a2, bytes32 b2, C c2) = abi.decode("abc", (uint, bytes32, C)); - // False positive until abi.* are implemented as uninterpreted functions. + function f(bytes memory data) public pure { + (uint a1, bytes32 b1, C c1) = abi.decode(data, (uint, bytes32, C)); + (uint a2, bytes32 b2, C c2) = abi.decode(data, (uint, bytes32, C)); assert(a1 == a2); assert(a1 != a2); } } // ---- -// Warning 2072: (85-95): Unused local variable. -// Warning 2072: (97-101): Unused local variable. -// Warning 2072: (156-166): Unused local variable. -// Warning 2072: (168-172): Unused local variable. -// Warning 8364: (139-140): Assertion checker does not yet implement type type(contract C) -// Warning 4588: (105-142): Assertion checker does not yet implement this type of function call. -// Warning 8364: (210-211): Assertion checker does not yet implement type type(contract C) -// Warning 4588: (176-213): Assertion checker does not yet implement this type of function call. -// Warning 6328: (293-309): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf() -// Warning 6328: (313-329): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf() -// Warning 8364: (139-140): Assertion checker does not yet implement type type(contract C) -// Warning 4588: (105-142): Assertion checker does not yet implement this type of function call. -// Warning 8364: (210-211): Assertion checker does not yet implement type type(contract C) -// Warning 4588: (176-213): Assertion checker does not yet implement this type of function call. +// Warning 2072: (102-112): Unused local variable. +// Warning 2072: (114-118): Unused local variable. +// Warning 2072: (172-182): Unused local variable. +// Warning 2072: (184-188): Unused local variable. +// Warning 8364: (155-156): Assertion checker does not yet implement type type(contract C) +// Warning 8364: (225-226): Assertion checker does not yet implement type type(contract C) +// Warning 6328: (252-268): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 20, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17]\n\n\nTransaction trace:\nconstructor()\nf([17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 20, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17]) +// Warning 8364: (155-156): Assertion checker does not yet implement type type(contract C) +// Warning 8364: (225-226): Assertion checker does not yet implement type type(contract C) diff --git a/test/libsolidity/smtCheckerTests/special/abi_encode_slice.sol b/test/libsolidity/smtCheckerTests/special/abi_encode_slice.sol index b56c7780a..0f6e57222 100644 --- a/test/libsolidity/smtCheckerTests/special/abi_encode_slice.sol +++ b/test/libsolidity/smtCheckerTests/special/abi_encode_slice.sol @@ -5,5 +5,3 @@ contract C { } } // ---- -// Warning 4588: (126-154): Assertion checker does not yet implement this type of function call. -// Warning 4588: (126-154): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/special/tx_data_gasleft_changes.sol b/test/libsolidity/smtCheckerTests/special/tx_data_gasleft_changes.sol index 0f3c7a3be..1e8f375fe 100644 --- a/test/libsolidity/smtCheckerTests/special/tx_data_gasleft_changes.sol +++ b/test/libsolidity/smtCheckerTests/special/tx_data_gasleft_changes.sol @@ -16,6 +16,8 @@ contract C { assert(gleft == gasleft()); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (124-150): CHC: Assertion violation happens here.\nCounterexample:\ngleft = 1\n\n\n\nTransaction trace:\nconstructor()\nState: gleft = 0\nf() -// Warning 6328: (219-245): CHC: Assertion violation happens here.\nCounterexample:\ngleft = 1\n\n\n\nTransaction trace:\nconstructor()\nState: gleft = 0\nf() +// Warning 6328: (124-150): CHC: Assertion violation happens here. +// Warning 6328: (219-245): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/address_call.sol b/test/libsolidity/smtCheckerTests/types/address_call.sol index 9bcbd1f02..e7130c2dd 100644 --- a/test/libsolidity/smtCheckerTests/types/address_call.sol +++ b/test/libsolidity/smtCheckerTests/types/address_call.sol @@ -19,7 +19,9 @@ contract C // EVMVersion: >spuriousDragon // ---- // Warning 2072: (224-240): Unused local variable. -// Warning 6328: (260-275): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\ndata = []\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0, []) -// Warning 6328: (279-293): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\ndata = []\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0, []) -// Warning 6328: (297-316): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\ndata = []\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0, []) -// Warning 6328: (320-344): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\ndata = []\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0, []) +// Warning 4588: (244-256): Assertion checker does not yet implement this type of function call. +// Warning 6328: (260-275): CHC: Assertion violation happens here. +// Warning 6328: (279-293): CHC: Assertion violation happens here. +// Warning 6328: (297-316): CHC: Assertion violation happens here. +// Warning 6328: (320-344): CHC: Assertion violation happens here. +// Warning 4588: (244-256): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/types/address_delegatecall.sol b/test/libsolidity/smtCheckerTests/types/address_delegatecall.sol index 2da8f1669..7301bf594 100644 --- a/test/libsolidity/smtCheckerTests/types/address_delegatecall.sol +++ b/test/libsolidity/smtCheckerTests/types/address_delegatecall.sol @@ -19,7 +19,9 @@ contract C // EVMVersion: >spuriousDragon // ---- // Warning 2072: (224-240): Unused local variable. -// Warning 6328: (268-283): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\ndata = []\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0, []) -// Warning 6328: (287-301): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\ndata = []\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0, []) -// Warning 6328: (305-324): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\ndata = []\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0, []) -// Warning 6328: (328-352): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\ndata = []\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0, []) +// Warning 4588: (244-264): Assertion checker does not yet implement this type of function call. +// Warning 6328: (268-283): CHC: Assertion violation happens here. +// Warning 6328: (287-301): CHC: Assertion violation happens here. +// Warning 6328: (305-324): CHC: Assertion violation happens here. +// Warning 6328: (328-352): CHC: Assertion violation happens here. +// Warning 4588: (244-264): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/types/address_staticcall.sol b/test/libsolidity/smtCheckerTests/types/address_staticcall.sol index 93abd09b2..721d863d1 100644 --- a/test/libsolidity/smtCheckerTests/types/address_staticcall.sol +++ b/test/libsolidity/smtCheckerTests/types/address_staticcall.sol @@ -19,4 +19,4 @@ contract C // EVMVersion: >spuriousDragon // ---- // Warning 2072: (224-240): Unused local variable. -// Warning 6328: (266-281): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\ndata = [10, 10]\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0, [10, 10]) +// Warning 6328: (266-281): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\ndata = [5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 18, 5, 21, 5, 5, 5, 5, 5, 5, 5, 5, 5, 31, 5, 5, 5, 5, 5, 5, 5, 5]\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf(0, [5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 18, 5, 21, 5, 5, 5, 5, 5, 5, 5, 5, 5, 31, 5, 5, 5, 5, 5, 5, 5, 5]) diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol b/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol index d1e64336f..5c29dd5f2 100644 --- a/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol +++ b/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol @@ -14,6 +14,6 @@ contract C } } // ---- -// Warning 6328: (295-324): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 100\na = 7720\nb = 7719\n\n\nTransaction trace:\nconstructor()\nf(100, 7720, 7719) +// Warning 6328: (295-324): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 100\na = 7719\nb = 7720\n\n\nTransaction trace:\nconstructor()\nf(100, 7719, 7720) // Warning 1236: (217-232): BMC: Insufficient funds happens here. // Warning 1236: (236-251): BMC: Insufficient funds happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_2.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_2.sol index 85a868505..3f50752db 100644 --- a/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_2.sol +++ b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_2.sol @@ -20,4 +20,4 @@ contract C } } // ---- -// Warning 6328: (436-453): CHC: Assertion violation happens here.\nCounterexample:\narray2d = []\nx = 0\ny = 0\nc = [38, 8, 8, 8, 8, 8, 8, 8, 8]\n\n\nTransaction trace:\nconstructor()\nState: array2d = []\ng(0, 0, [38, 8, 8, 8, 8, 8, 8, 8, 8]) +// Warning 6328: (436-453): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 0\n\n\nTransaction trace:\nconstructor()\nState: array2d = []\ng(0, 0, c) diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_4.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_4.sol index e3a5c1bf9..01a301096 100644 --- a/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_4.sol +++ b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_4.sol @@ -18,6 +18,8 @@ contract C f(array2d[x], array2d[y]); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (225-242): CHC: Assertion violation happens here.\nCounterexample:\narray = [1, 19, 19, 19, 19], array2d = []\nx = 0\ny = 0\n\n\nTransaction trace:\nconstructor()\nState: array = [], array2d = []\ng(0, 0) -// Warning 6328: (289-307): CHC: Assertion violation happens here.\nCounterexample:\narray = [1, 19, 19, 19, 19], array2d = []\nx = 0\ny = 0\n\n\nTransaction trace:\nconstructor()\nState: array = [], array2d = []\ng(0, 0) +// Warning 6328: (225-242): CHC: Assertion violation happens here. +// Warning 6328: (289-307): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol index efa958d55..02d3d9903 100644 --- a/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol +++ b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol @@ -27,4 +27,4 @@ contract C } } // ---- -// Warning 6328: (572-589): CHC: Assertion violation happens here.\nCounterexample:\nb = [1, 20, 20, 20, 20], d = [], array2d = []\nx = 0\nc = [0, 9, 9, 9, 9, 9, 9, 9, 9, 9]\n\n\nTransaction trace:\nconstructor()\nState: b = [], d = [], array2d = []\ng(0, [0, 9, 9, 9, 9, 9, 9, 9, 9, 9]) +// Warning 6328: (572-589): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_branch_1d.sol b/test/libsolidity/smtCheckerTests/types/array_branch_1d.sol index 80769e6db..40018ec36 100644 --- a/test/libsolidity/smtCheckerTests/types/array_branch_1d.sol +++ b/test/libsolidity/smtCheckerTests/types/array_branch_1d.sol @@ -11,4 +11,4 @@ contract C } // ---- // Warning 2018: (47-148): Function state mutability can be restricted to pure -// Warning 6328: (128-144): CHC: Assertion violation happens here.\nCounterexample:\n\nb = false\nc = [0, 5, 5, 5, 5, 5]\n\n\nTransaction trace:\nconstructor()\nf(false, [38, 5, 5, 5, 5, 5]) +// Warning 6328: (128-144): CHC: Assertion violation happens here.\nCounterexample:\n\nb = false\nc = [0, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 18, 14, 14, 21, 14, 14, 23, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14]\n\n\nTransaction trace:\nconstructor()\nf(false, [7719, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 18, 14, 14, 21, 14, 14, 23, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14]) diff --git a/test/libsolidity/smtCheckerTests/types/array_dynamic_parameter_1_fail.sol b/test/libsolidity/smtCheckerTests/types/array_dynamic_parameter_1_fail.sol index 69a78e925..486538a46 100644 --- a/test/libsolidity/smtCheckerTests/types/array_dynamic_parameter_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/types/array_dynamic_parameter_1_fail.sol @@ -9,4 +9,4 @@ contract C } } // ---- -// Warning 6328: (148-170): CHC: Assertion violation happens here.\nCounterexample:\n\narray = [15, 15, 15, 15, 15]\nx = 38\ny = 38\n\n\nTransaction trace:\nconstructor()\nf([15, 15, 15, 15, 15], 38, 38) +// Warning 6328: (148-170): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\ny = 38\n\n\nTransaction trace:\nconstructor()\nf(array, 38, 38) diff --git a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol index 82cfd36ae..84cd76555 100644 --- a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol +++ b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol @@ -24,4 +24,4 @@ contract C } } // ---- -// Warning 6328: (421-452): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\n\n\nTransaction trace:\nconstructor()\ng(38) +// Warning 6328: (421-452): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 8855\n\n\nTransaction trace:\nconstructor()\ng(8855) diff --git a/test/libsolidity/smtCheckerTests/types/array_static_aliasing_storage_5.sol b/test/libsolidity/smtCheckerTests/types/array_static_aliasing_storage_5.sol index 60d9979dc..f37c4a536 100644 --- a/test/libsolidity/smtCheckerTests/types/array_static_aliasing_storage_5.sol +++ b/test/libsolidity/smtCheckerTests/types/array_static_aliasing_storage_5.sol @@ -12,7 +12,8 @@ contract C // erase knowledge about memory references. assert(c[0] == 42); // Fails because b1 == a is possible. - assert(a[0] == 2); + // Disabled because Spacer seg faults. + //assert(a[0] == 2); assert(b1[0] == 1); } function g(bool x, uint[2] memory c) public { @@ -23,4 +24,3 @@ contract C // ==== // SMTIgnoreCex: yes // ---- -// Warning 6328: (338-355): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol index 899b72fbc..96dc649da 100644 --- a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol +++ b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol @@ -24,4 +24,4 @@ contract C } } // ---- -// Warning 6328: (425-456): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\n\n\nTransaction trace:\nconstructor()\ng(38) +// Warning 6328: (425-456): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 8855\n\n\nTransaction trace:\nconstructor()\ng(8855) diff --git a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol index b1a5c7532..94dee80ee 100644 --- a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol +++ b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol @@ -27,4 +27,4 @@ contract C } } // ---- -// Warning 6328: (830-850): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\n\nTransaction trace:\nconstructor()\ng(0) +// Warning 6328: (830-850): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/bytes_2_fail.sol b/test/libsolidity/smtCheckerTests/types/bytes_2_fail.sol index 0e3e1160e..9a582ab79 100644 --- a/test/libsolidity/smtCheckerTests/types/bytes_2_fail.sol +++ b/test/libsolidity/smtCheckerTests/types/bytes_2_fail.sol @@ -8,4 +8,4 @@ contract C } } // ---- -// Warning 6328: (119-141): CHC: Assertion violation happens here.\nCounterexample:\n\nb1 = [28958, 28957, 28958, 28958, 28958]\nb2 = [28958, 28957, 28958, 28958, 28958]\n\n\nTransaction trace:\nconstructor()\nf([], [28958, 28957, 28958, 28958, 28958]) +// Warning 6328: (119-141): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf(b1, b2) diff --git a/test/libsolidity/smtCheckerTests/types/contract.sol b/test/libsolidity/smtCheckerTests/types/contract.sol index 6a489d479..39b6a024d 100644 --- a/test/libsolidity/smtCheckerTests/types/contract.sol +++ b/test/libsolidity/smtCheckerTests/types/contract.sol @@ -6,5 +6,7 @@ contract C assert(c == d); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (84-98): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0\nd = 1\n\n\nTransaction trace:\nconstructor()\nf(0, 1) +// Warning 6328: (84-98): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/contract_2.sol b/test/libsolidity/smtCheckerTests/types/contract_2.sol index 285dfff04..c9e8c8ded 100644 --- a/test/libsolidity/smtCheckerTests/types/contract_2.sol +++ b/test/libsolidity/smtCheckerTests/types/contract_2.sol @@ -11,5 +11,7 @@ contract C assert(c == d); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (109-123): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0\nd = 1\n\n\nTransaction trace:\nconstructor()\nf(0, 1) +// Warning 6328: (109-123): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_2.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_2.sol index 264b92a7b..59832a2ba 100644 --- a/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_2.sol +++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_access_2.sol @@ -6,4 +6,4 @@ contract C { } } // ---- -// Warning 4281: (117-120): CHC: Division by zero happens here.\nCounterexample:\n\nx = [7, 7]\ny = 0\n\n\nTransaction trace:\nconstructor()\nf([7, 7], 0) +// Warning 4281: (117-120): CHC: Division by zero happens here.\nCounterexample:\n\nx = [17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 20, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17]\ny = 0\n\n\nTransaction trace:\nconstructor()\nf([17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 20, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17, 17], 0) diff --git a/test/libsolidity/smtCheckerTests/types/mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/mapping_aliasing_2.sol index e13b2fd5b..05613cef7 100644 --- a/test/libsolidity/smtCheckerTests/types/mapping_aliasing_2.sol +++ b/test/libsolidity/smtCheckerTests/types/mapping_aliasing_2.sol @@ -30,6 +30,8 @@ contract C f(maps[x], maps[y]); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (397-417): CHC: Assertion violation happens here.\nCounterexample:\n\nb = true\nx = 0\ny = 0\n\n\nTransaction trace:\nconstructor()\ng(true, 0, 0) -// Warning 6328: (463-481): CHC: Assertion violation happens here.\nCounterexample:\n\nb = true\nx = 0\ny = 0\n\n\nTransaction trace:\nconstructor()\ng(true, 0, 0) +// Warning 6328: (397-417): CHC: Assertion violation happens here. +// Warning 6328: (463-481): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol b/test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol index 18b7efb43..880dd8aa9 100644 --- a/test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol +++ b/test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol @@ -12,4 +12,4 @@ contract c { } } // ---- -// Warning 6328: (289-306): CHC: Assertion violation happens here.\nCounterexample:\n\na = 7719\nb = 38\n\n\nTransaction trace:\nconstructor()\ng(7719, 38) +// Warning 6328: (289-306): CHC: Assertion violation happens here.\nCounterexample:\n\na = 38\nb = 21239\n\n\nTransaction trace:\nconstructor()\ng(38, 21239) diff --git a/test/libsolidity/smtCheckerTests/types/string_literal_comparison_2.sol b/test/libsolidity/smtCheckerTests/types/string_literal_comparison_2.sol index 476114d86..0ccc660af 100644 --- a/test/libsolidity/smtCheckerTests/types/string_literal_comparison_2.sol +++ b/test/libsolidity/smtCheckerTests/types/string_literal_comparison_2.sol @@ -10,5 +10,5 @@ contract C { } } // ---- -// Warning 6328: (147-166): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 0\n\n\nTransaction trace:\nconstructor()\nf(0) +// Warning 6328: (147-166): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538817385212172903286807934654968315727694643370704309751478220717293569\n\n\nTransaction trace:\nconstructor()\nf(52647538817385212172903286807934654968315727694643370704309751478220717293569) // Warning 6328: (170-190): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538830022687173130149211684818290356179572910782152375644828738034597888\n\n\nTransaction trace:\nconstructor()\nf(52647538830022687173130149211684818290356179572910782152375644828738034597888) diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_state_var_array_pop_2.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_state_var_array_pop_2.sol index 10052f693..a50072b12 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_state_var_array_pop_2.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_state_var_array_pop_2.sol @@ -17,6 +17,8 @@ contract C { s.a.pop(); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 2529: (133-142): CHC: Empty array "pop" happens here.\nCounterexample:\ns = {x: 38, a: []}\n_x = 38\n\n\nTransaction trace:\nconstructor()\nState: s = {x: 0, a: []}\nf(38) -// Warning 6328: (189-213): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 115792089237316195423570985008687907853269984665640564039457584007913129639897, a: [115792089237316195423570985008687907853269984665640564039457584007913129639897, 0]}\n_x = 115792089237316195423570985008687907853269984665640564039457584007913129639897\n\n\nTransaction trace:\nconstructor()\nState: s = {x: 0, a: []}\nf(115792089237316195423570985008687907853269984665640564039457584007913129639897) +// Warning 2529: (133-142): CHC: Empty array "pop" happens here. +// Warning 6328: (189-213): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/tuple_assignment_array_empty.sol b/test/libsolidity/smtCheckerTests/types/tuple_assignment_array_empty.sol index d2f5e9f9e..e3111cce3 100644 --- a/test/libsolidity/smtCheckerTests/types/tuple_assignment_array_empty.sol +++ b/test/libsolidity/smtCheckerTests/types/tuple_assignment_array_empty.sol @@ -10,5 +10,7 @@ contract C assert(a[y] == 4); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (136-153): CHC: Assertion violation happens here.\nCounterexample:\na = []\nx = 39\ny = 0\n\n\nTransaction trace:\nconstructor()\nState: a = []\ng(39, 0) +// Warning 6328: (136-153): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol b/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol index 254e58f7b..fc4a4053f 100644 --- a/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol +++ b/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol @@ -11,3 +11,5 @@ contract C { } } // ---- +// Warning 4588: (142-161): Assertion checker does not yet implement this type of function call. +// Warning 4588: (142-161): Assertion checker does not yet implement this type of function call.