cerc-io/solidity
16
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

Merge pull request #10056 from ethereum/smt_fix_develop

Browse Source 
Fix SMT command line test
This commit is contained in:
Leonardo 2020-10-16 18:37:55 +01:00 committed by GitHub
commit eedd12ad1d
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 4 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x4ca2adc24a17cd524cf3113f3b2cddff216f428f804e884cf76d27dd3e72cd68":"(set-option :produce-models true) {"auxiliaryInputRequested":{"smtlib2queries":{"0x8b2c3058077c75f8fff85d2d387198b91b4e591448624f4bef0ab6c7b87d5ec1":"(set-option :produce-models true)
(set-logic ALL) (set-logic ALL)
(declare-fun |error_0| () Int) (declare-fun |error_0| () Int)
(declare-fun |this_0| () Int) (declare-fun |this_0| () Int)
@ -7,6 +7,9 @@
(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) (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-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-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 |x_4_0| () Int)
(declare-fun |expr_8_0| () Int) (declare-fun |expr_8_0| () Int)
(declare-fun |expr_9_0| () Int) (declare-fun |expr_9_0| () Int)