VeriSmart-public icon indicating copy to clipboard operation
VeriSmart-public copied to clipboard

Published 20 hours ago • verified publisher icon kupl

Verify timeout

Open acmRecife opened this issue 2 years ago • 1 comments

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!

acmRecife avatar Jul 21 '22 15:07 acmRecife

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?

sunbeomso avatar Nov 21 '22 02:11 sunbeomso