Open msooseth opened 6 months ago
The CI complains about some duplicated benchmarks right now, we will have to remove those.
I think the benchmarks can also be polish to make them a bit nicer to work with:
:status
should move to the end.(exit)
.:source
header should contain a Generated by
(can be an institution) and a Generated on
line. I think in your case it might also make sense to include Application
.The idea is that we polish benchmarks that use widely used, but non-standard, features, and then include them in a benchmark release as soon as those features become standard.
Hi,
First of all, thanks for all the feedback! Sorry, I am currently on a bit of a break for industry (i.e. HEVM). Let me try to respond to your comments, here:
1) Fair point, sorry. It's a bit painful to change it now, though. This kind of large-scale text editing takes lots of time. 2) These are actually incredibly useful for us, and they map to the problem 1-to-1, I think they are relatively easy to read and should be helpful to understand the problem. I'd prefer leaving them in. 3) Sorry about the newline, that's an easy fix :) 4) Yeah, good point, I can add, though editing these text files automatically can be quite fragile. 5) It seems like we added both too much and too little :D If it's not a problem, I'll leave in the comments, and try to also add something about the github repository. It was just a bit confusing to me, sorry.
Do you know if someone could help us with this? There are too many deadlines, too many things that are on my plate and I'm afraid this will fall off. I'd really appreciate some help :)
I am happy to do the changes, and should be able to push to this pull request. We are currently in the process of finishing up this years release and then I will come back to it.
I finally got around to do the edits. Since the benchmarks contain (as const
I will not merge the the benchmarks, but mark them with a tag.
That’s awesome! Thank you so much! I’ll be at CAV so I’ll try my best to repay the favour with dinner&drinks sometime :) Thank you so much! See you at CAV hopefully,
Mate
On Thu 20. Jun 2024 at 11:12, Hans-Jörg @.***> wrote:
I finally got around to do the edits. Since the benchmarks contain (as const I will not merge the the benchmarks, but mark them with a tag.
— Reply to this email directly, view it on GitHub https://github.com/SMT-LIB/benchmark-submission/pull/7#issuecomment-2180948844, or unsubscribe https://github.com/notifications/unsubscribe-auth/AXYLY5C4MPY6U732ZMHQH2LZILWONAVCNFSM6AAAAABFJBVZ6OVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCOBQHE2DQOBUGQ . You are receiving this because you authored the thread.Message ID: @.***>
I will unfortunately not be at CAV, but I think Mathias will be. He does a ton of work on the benchmark that is a bit less submitter-visible. I am happy to forward my drink to him ^^.
Haha, okay, Mathias it is!
@msooseth - sorry to hijack this thread, but I sent an email to your gmail that is kind of urgent - could you have a look? Thanks!
Oh, I'm so sorry. I had a look but couldn't find an email from you :( Can you please re-send it? My address is a bit confusing, it's soos.mate@gmail.com (and not mate.soos@)
Sorry again,
Mate
Just resent to your gmail. Maybe check spam? It's from barrettc@stanford.edu
@hansjoergschurr was this merged in the end? Or is there something I can do to help merge it?
Actually, sorry, I see it hasn't been merged, but "only" because of the as const
. Is that support coming to SMTLib sometime?
Yes the support for const arrays should be coming soon - it's on my to-do list
Nice! Thank you, that'd be awesome!
Hi All,
This is a set of files generated by the hevm symbolic execution framework [1] running on
eth-sc-comp
benchmarks [2] set with--dumpsmt
flag set on./bench.py
in [2]. The files have been massaged to fit the requirements by the SMT-LIB benchmark set: status, license info, etc. Unfortunately, theas const
syntax such as:is not standardized but needed by hevm. However, it is supported by all SMT solvers we use: Z3, CVC5, Bitwuzla, though Z3 strangely only supports it in
ALL
logic, not inQF_AUFBV
. I have been told that I should just submit these as-is, as the LIB-SMT standardization committee may make progress on this feature.Let me know if there is something amiss and looking forward to meeting in Montreal,
Mate
[1] https://github.com/ethereum/hevm [2] https://github.com/eth-sc-comp/benchmarks