Thank you for making this tool available to the public.
I am trying to annotate a set of smart contracts, the set contains a large number of contracts. I want to reduce processing time while maintaining detection performance.
I have set the following two parameters, however, the number of generated paths for some contracts is too high (e.g., 4000 or > 100,000), which takes time to process them all.
-verify_timeout 60 -z3timeout 10000
Do you have any observations on the effect of other factors such as depth on detection performance?
I don't want to set parameters arbitrarily, can you make a recommendation based on your testing of the tool?
Thank you.
Thank you for making this tool available to the public.
I am trying to annotate a set of smart contracts, the set contains a large number of contracts. I want to reduce processing time while maintaining detection performance.
I have set the following two parameters, however, the number of generated paths for some contracts is too high (e.g., 4000 or > 100,000), which takes time to process them all.
-verify_timeout 60 -z3timeout 10000Do you have any observations on the effect of other factors such as depth on detection performance?
I don't want to set parameters arbitrarily, can you make a recommendation based on your testing of the tool?
Thank you.