You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
The text was updated successfully, but these errors were encountered: