Verify timeout

[acmRecife]

Dear,

I am using a MacOS Monterey 12.4, 8GB RAM, i7 2-Core, 2,2 GHz. I tested VeriSmart on small contracts (examples folder) and it worked as expected. But in this contract

[CHECKER] Integer Over/Underflows
[CHECKER] Division-by-zero
[CHECKER] Suicidal
[CHECKER] Ether-Leaking

• all funcs : 815
• reachable : 80

• [STEP] Generating Paths ... took 0.955925s

• #paths : 4012

[INFO] Violate CEI: true
[INFO] msg.sender = this possible: false

• Performing Interval Analysis ... took 6.659553s

it does not give any response (except when I put "-verify_timeout 1", but in this case Z3 cannot prove anything. Any value above 1 and it (seems to) freezes. SmarTest is almost instantaneous...).

Could you please help me?

Thanks!

[sunbeomso]

Hi @acmRecife,

In order to diagnose the problem concretely, could you provide the source code of your input Solidity contract and the entire command that can reproduce the problem you mentioned?