Closed Tomaqa closed 5 months ago
Another thing I noticed:
typically we try to follow the order of the first couple commands as outlined in the README. In your case :license
and :category
should come after :source
, and set-logic
right after :smt-lib-version
.
Thank you very much for the benchmarks. I removed the extra commands and will merge the pull requests now. We will run some other tests on our side, but if nothing surprising happens they should show up in the next release.
Thank you for your benchmark submission!
There are multiple duplicated benchmarks. See the CI log for a list of them.
I noticed that the benchmarks also contain
set-option
andget-value
commands. Those should be removed from the benchmarks. If you think that model production is what makes the benchmarks interesting, (e.g., because it exposes a performance regression in proof production mode) then we add a note about this to the description of the benchmarks.