cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Add and update tests

Browse Source
This commit is contained in:
Leonardo Alt 2020-12-10 14:06:34 +01:00
parent 7ba91cdc33
commit 50be39fc21
87 changed files with 1434 additions and 642 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
test/cmdlineTests/standard_model_checker_engine_bmc/output.json
View File

@ -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)

236
test/cmdlineTests/standard_model_checker_timeout_all/output.json
View File

@ -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:

834
test/cmdlineTests/standard_model_checker_timeout_bmc/output.json
View File

@ -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:
|

67
test/libsolidity/smtCheckerTests/abi/abi_decode_array.sol Normal file
View File

@ -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)

30
test/libsolidity/smtCheckerTests/abi/abi_decode_simple.sol Normal file
View File

@ -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.

31
test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice.sol Normal file
View File

@ -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.

31
test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice_2.sol Normal file
View File

@ -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.

9
test/libsolidity/smtCheckerTests/abi/abi_encode_hash.sol Normal file
View File

@ -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));
}
}

36
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice.sol Normal file
View File

@ -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.

37
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice_2.sol Normal file
View File

@ -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.

16
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_hash.sol Normal file
View File

@ -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.

34
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_simple.sol Normal file
View File

@ -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.

38
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol Normal file
View File

@ -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.

30
test/libsolidity/smtCheckerTests/abi/abi_encode_simple.sol Normal file
View File

@ -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.

32
test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol Normal file
View File

@ -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.

37
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol Normal file
View File

@ -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.

37
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol Normal file
View File

@ -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.

20
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol Normal file
View File

@ -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.

32
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_simple.sol Normal file
View File

@ -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.

36
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal.sol Normal file
View File

@ -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.

12
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_vs_sig.sol Normal file
View File

@ -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.

37
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol Normal file
View File

@ -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.

37
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol Normal file
View File

@ -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.

20
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_hash.sol Normal file
View File

@ -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.

34
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_simple.sol Normal file
View File

@ -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.

36
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_string_literal.sol Normal file
View File

@ -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.

2
test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol
View File

@ -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()

4
test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol
View File

File diff suppressed because one or more lines are too long

2
test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol
View File

@ -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)

4
test/libsolidity/smtCheckerTests/complex/MerkleProof.sol
View File

@ -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.

8
test/libsolidity/smtCheckerTests/complex/slither/external_function.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init_chain_alternate.sol
View File

@ -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)

2
test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructors.sol
View File

@ -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)

8
test/libsolidity/smtCheckerTests/crypto/crypto_functions_compare_hashes.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/crypto/crypto_functions_not_same.sol
View File

@ -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)

4
test/libsolidity/smtCheckerTests/external_calls/external_inc.sol
View File

@ -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.

4
test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_4.sol
View File

@ -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)

6
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_2.sol
View File

@ -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.

8
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol
View File

@ -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)

2
test/libsolidity/smtCheckerTests/functions/constructor_state_value_inherited.sol
View File

@ -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)

4
test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol
View File

@ -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)

2
test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol
View File

@ -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()

4
test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_5.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_1.sol
View File

@ -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()

6
test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_2.sol
View File

@ -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.

4
test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_with_side_effects_5.sol
View File

@ -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.

9
test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol
View File

@ -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.

10
test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol
View File

@ -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)

9
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/loops/while_nested_break_fail.sol
View File

@ -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)

4
test/libsolidity/smtCheckerTests/operators/compound_sub_array_index.sol
View File

@ -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.

4
test/libsolidity/smtCheckerTests/operators/compound_sub_mapping.sol
View File

@ -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.

3
test/libsolidity/smtCheckerTests/operators/slice.sol
View File

@ -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);
}

2
test/libsolidity/smtCheckerTests/operators/unary_add_array.sol
View File

@ -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)

4
test/libsolidity/smtCheckerTests/operators/unary_sub_mapping.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/overflow/overflow_mul_cex_with_array.sol
View File

@ -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)

2
test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol
View File

@ -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))

2
test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol
View File

@ -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.

16
test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2_value_types.sol
View File

@ -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.

30
test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol
View File

@ -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)

2
test/libsolidity/smtCheckerTests/special/abi_encode_slice.sol
View File

@ -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.

6
test/libsolidity/smtCheckerTests/special/tx_data_gasleft_changes.sol
View File

@ -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.

10
test/libsolidity/smtCheckerTests/types/address_call.sol
View File

@ -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.

10
test/libsolidity/smtCheckerTests/types/address_delegatecall.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/types/address_staticcall.sol
View File

@ -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])

2
test/libsolidity/smtCheckerTests/types/address_transfer_2.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/types/array_aliasing_storage_2.sol
View File

@ -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)

6
test/libsolidity/smtCheckerTests/types/array_aliasing_storage_4.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/types/array_branch_1d.sol
View File

@ -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])

2
test/libsolidity/smtCheckerTests/types/array_dynamic_parameter_1_fail.sol
View File

@ -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)

2
test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol
View File

@ -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)

4
test/libsolidity/smtCheckerTests/types/array_static_aliasing_storage_5.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol
View File

@ -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)

2
test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/types/bytes_2_fail.sol
View File

@ -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)

4
test/libsolidity/smtCheckerTests/types/contract.sol
View File

@ -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.

4
test/libsolidity/smtCheckerTests/types/contract_2.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/types/fixed_bytes_access_2.sol
View File

@ -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)

6
test/libsolidity/smtCheckerTests/types/mapping_aliasing_2.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol
View File

@ -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)

2
test/libsolidity/smtCheckerTests/types/string_literal_comparison_2.sol
View File

@ -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)

6
test/libsolidity/smtCheckerTests/types/struct/struct_state_var_array_pop_2.sol
View File

@ -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.

4
test/libsolidity/smtCheckerTests/types/tuple_assignment_array_empty.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol
View File

@ -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.