Adding benchmarks from Verus (a Rust Verification tool)

[amarshah1]

No description provided.

[hansjoergschurr]

Thank you for the submissions, these are very interesting benchmarks.

Before we can merge the benchmarks there is some editing that needs to be done.

• The set-option commands should be removed, because those are solver specific.
• The set-info :comment commands should be removed.
• This benchmark set is very large with over 7500 benchmarks. While we don't have any strict rules about benchmark set size, we encourage submitters to select a representative subset of the benchmarks in such cases. Do you think it's possible to select a representative subset of benchmarks (500 - 3000).

[amarshah1]

Before we can merge the benchmarks there is some editing that needs to be done.

I can do this. Is it alright if I leave the options as a comment. This way people can see the options that the query is designed to be run with:

Like:

(set-info :comment |
These were the default configurations used with z3:
  (set-option :auto_config false)
  (set-option :smt.mbqi false)
  (set-option :smt.case_split 3)
  (set-option :smt.qi.eager_threshold 100.0)
  (set-option :smt.delay_units true)
  (set-option :smt.arith.solver 2)
  (set-option :smt.arith.nl false)
  (set-option :pi.enabled false)
  (set-option :rewriter.sort_disjunctions false)
  (set-option :sat.euf true)
  (set-option :tactic.default_tactic sat)
  (set-option :smt.ematching false)
  (set-option :smt.case_split 0)
|)

I can make the other two changes as well.

[hansjoergschurr]

We don't include any set-info commands that use attributes not predefined by SMT-LIB.

Such a comment should instead go to the end the :source metadata.
We now have tooling to extract this metadata automatically from the :source header.

[hansjoergschurr]

We also noticed that you split your submission into multiple distinct families (20241211-verusatmosphere, 20241211-verusverismo, etc.). It would be more idiomatic to move these into a common family and use sub folders (i.e., 20241211-verus/{atmosphere, verismo, ...}/..).

I would suggest to then limit the number of benchmarks per sub-family to 500.

[amarshah1]

This should (hopefully) fix all the issues! Let me know if you want any more changes

[hansjoergschurr]

Looks great! Thank you for the benchmarks!