yicesQS submission to the 2024 SMT comp

[disteph]

No description provided.

[github-actions]

Summary of modified submissions

YicesQS

• 1 authors
• website: https://github.com/disteph/yicesQS
• Participations
  • SingleQuery
    • Arith
      • all
    • Bitvec
      • all

[martinjonas]

@disteph We have executed the latest version of yicesQS on a randomly chosen subset of 20 single-query benchmarks from each logic where it participates. The benchmarks are also scrambled by the competition scrambler (with seed 1). You can find the results here: https://www.fi.muni.cz/~xjonas/smtcomp/yicesqs.table.html#/table

Quick explanation:

• Green status means that the result agrees with the (set-info :status _) annotation from the benchmark.
• Blue status means that the benchmark has annotation (set-info :status unknown).
• By clicking on the result (e.g. false, true, ABORTED, …) you can see the command-line arguments with which your solver was called and its output on the benchmark.
• By clicking on the benchmark name (i.e., *scrambled*.yml), you can see the details of the benchmark including its contents (by clicking on the file link in input_files) and the name of the original bennchmark before scrambling (e.g., # original_files: 'non-incremental/AUFBVFP/20210301-Alive2-partial-undef/ph7/583_ph7.smt2').

Please check whether there are some discrepancies, such as missing/extra logics, unexpected aborts or unknowns, and similar. If you update the solver, let me know and I can execute further test runs. We still have plenty of time for several follow-up test runs.

[bobot]

The error in TestSolver is on our side.

[disteph]

OK, great! Thanks!