Closed JohnLyu2 closed 1 year ago
I also submitted the rest of the benchmarks.
Automatark page: https://github.com/JohnLyu2/automatark_smt
I noticed that you added a Description:
line to the benchmarks. Thank you!
Unfortunately, the idea is that such extra lines come after the last of the predefined lines in the set-info :source
command. So we will have to move your Description:
line after the Publications:
line.
I realize that the README is not very clear in this regard. We will improve it.
I will merge this branch and perform the edit on our side. I did this on your other submission.
Thank you again for your benchmark submission!
Thank you so much! Have a nice weekend : )
From: Hans-Jörg @.> Sent: April 6, 2023 1:26 PM To: SMT-LIB/benchmark-submission @.> Cc: JohnLyu2 @.>; Author @.> Subject: Re: [SMT-LIB/benchmark-submission] Submit Woorpje Track05 Benchmarks (PR #10)
I will merge this branch and perform the edit on our side. I did this on your other submission.
Thank you again for your benchmark submission!
— Reply to this email directly, view it on GitHubhttps://github.com/SMT-LIB/benchmark-submission/pull/10#issuecomment-1499393241, or unsubscribehttps://github.com/notifications/unsubscribe-auth/APRX4LY5CZ3LRGGTRITKA73W734CZANCNFSM6AAAAAAWMDNW6U. You are receiving this because you authored the thread.Message ID: @.***>
Benchmark Suite Description: https://github.com/JohnLyu2/woorpje_we
On my MAC, when I run dolmen on this track05, it usually throw errors. I checked the reason is that there are linear integer constraints like: (assert (>=(* (str.len H) 8) 8)). I think this is a valid assertion in QF_SLIA. Can you help me check does dolmen report error on your side? Thx.