yicesQS submission to the 2025 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]

The link is currently returning error 404. Can you fix that? Thanks!

[disteph]

I certainly can. But I do like to put into this description the git commit hash of the (final) solver that was submitted to the competition. I don't have that hash yet, since the final version is still up to come. My current pdf has that hash set to "TBD"; if I make it available to you now, will I get the chance to update the pdf later so that the version on the SMT website ends up being the one with the actual hash?

[martinjonas]

Sure, no problem. You can edit the PDF until the final deadline. We just want to go through all the system descriptions now to check that all the solvers are correctly marked as wrapper/derived solvers.

[disteph]

Perfect; done!

[martinjonas]

@disteph Thanks for submitting yicesQS to this year's SMT-COMP!

We have executed your solver on a small number of benchmarks from each logic it should compete in. You can find the results here:

• Single Query Track: https://www.fi.muni.cz/~xjonas/smtcomp/tables/yicesqs.table.html#/table

We have not seen any incorrect results returned by your solver (compared to the expected status of the benchmarks).

You can check whether all the results we have obtained are expected. If not, please let us know here.

Some notes:

• We have used less resources than will be used in the final runs.
• The benchmarks are scrambled by the official scrambler with seed 1.
• The column status shows whether your solver decided the benchmark as sat (true) or unsat (false).
• You can click on the value in the status column to see the output of your solver on that benchmark.

If you upload a new version of the solver and want to have another test run, let me know. We still have some time for that.

Happy rest of the competition!
Martin

[martinjonas]

Although the rules require submitting also the corresponding base solver for each derived solver, we discussed this with the rest of the organizers and decided it does not make sense for yicesQS. The base solver does not support general quantified formulas and thus is not comparable with the submitted derived solver. (I am writing the comment here just for future reference in case somebody wonders why yicesQS has no base solver. You do not need to react or do anything. :-) )

[disteph]

Although the rules require submitting also the corresponding base solver for each derived solver, we discussed this with the rest of the organizers and decided it does not make sense for yicesQS. The base solver does not support general quantified formulas and thus is not comparable with the submitted derived solver. (I am writing the comment here just for future reference in case somebody wonders why yicesQS has no base solver. You do not need to react or do anything. :-) )

Thanks! We did submit Yices to the SMT-comp, though mostly for quantifier-free logics. I hadn't realized that, in theory, the base solver should be submitted for the same logics as the derived solver. For the next competitions, I'm happy to revise whether yicesQS should be declared as a solver derived from yices. It "builds on it". Let me know if you think we should revise that next time.