cvc5-xyz for SMT-COMP 2026

[namasikanam]

No description provided.

[github-actions]

Summary of modified submissions

cvc5-cvc5-xyz-base

• 1 authors
• website: https://github.com/cvc5/cvc5
• Participations
  • SingleQuery
    • Arith
      • all
    • Bitvec
      • all
    • Equality
      • all
    • Equality+LinearArith
      • all
    • Equality+MachineArith
      • all
    • Equality+NonLinearArith
      • all
    • FPArith
      • all
    • QF_Bitvec
      • all
    • QF_Datatypes
      • all
    • QF_Equality
      • all
    • QF_Equality+Bitvec
      • all
    • QF_Equality+LinearArith
      • all
    • QF_Equality+NonLinearArith
      • all
    • QF_FPArith
      • all
    • QF_LinearIntArith
      • all
    • QF_LinearRealArith
      • all
    • QF_NonLinearIntArith
      • all
    • QF_NonLinearRealArith
      • all
    • QF_Strings
      • all

cvc5-cvc5-xyz

• 3 authors
• website: https://zenodo.org/records/20642185
• Participations
  • SingleQuery
    • Arith
      • all
    • Bitvec
      • all
    • Equality
      • all
    • Equality+LinearArith
      • all
    • Equality+MachineArith
      • all
    • Equality+NonLinearArith
      • all
    • FPArith
      • all
    • QF_Bitvec
      • all
    • QF_Datatypes
      • all
    • QF_Equality
      • all
    • QF_Equality+Bitvec
      • all
    • QF_Equality+LinearArith
      • all
    • QF_Equality+NonLinearArith
      • all
    • QF_FPArith
      • all
    • QF_LinearIntArith
      • all
    • QF_LinearRealArith
      • all
    • QF_NonLinearIntArith
      • all
    • QF_NonLinearRealArith
      • all
    • QF_Strings
      • all

[martinjonas]

@namasikanam Thanks for submitting cvc5-xyz to this year's SMT-COMP!

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

• Single Query Track: https://www.fi.muni.cz/~xjonas/smtcomp/tables/cvc5cvc5xyz.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 smaller resource limits 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

[Tomaqa]

Dear authors, thank you for the submission. In the system description, please add more details about the technique, as most of the document describes related work rather than the "Heuristic Learning" technique it claims to use. It also contains a broken reference.

Furthermore, could you clarify why AUTHORS in your solver's archive is a binary file having almost 100MB?

Thanks!

[namasikanam]

Hi @martinjonas , I updated my submission. Could you kindly help me test again, if there is still an opportunity before the final run?

[martinjonas]

@namasikanam I ran the tests with the new version and updated the table at the link above.

[namasikanam]

Hi @martinjonas, I updated my solver again. Would you mind running the test again? Sorry for updating in the last minute!

[Tomaqa]

Remember to set the final flag to true.

[namasikanam]

@Tomaqa Thanks! The final flags have been set to true.