How to configure ETHBMC to reduce timeout events

[step-xiaoyu-ka]

Summary of the problem

Hi, I ran a multiprocess script on top of ETHMBMC to analyze multiple smart contracts offline where a timeout of 30 minutes for each contract is set. The result showed a total of 9 contracts, with a timeout rate of 55.6%.

SMT Solver

Yices 2.6.2

Expected behavior

EthBMC successfully completes the analysis of 9 contracts and the timeout rate does not exceed 22%.

Actual behavior

Timeout occurred in 5 contracts. All contracts use the same command options-b1 --json and real-world bytecode and account address in yml file but balance fixed at "0x100000" and nonce at "0x1000000". There is only one contract in each yml file.

I summarized the command options that might avoid timeouts:

• -b is limit to 1

• --concrete-copy is used(It seems to affect code coverage due to the use of concrete values instead of symbolic values)

• --solver-timeout(The default is 2 minutes, but I often observe it timeout in the running log)

Please give me some suggestions to reduce the timeout rate, even at the expense of code coverage.