SMTS submission 2026

[Tomaqa]

The archive is currently the same as in previous year.

[github-actions]

Summary of modified submissions

OpenSMT-SMTS-base

• 2 authors
• website: https://github.com/usi-verification-and-security/opensmt
• Participations
  • Parallel
    • QF_Equality
      • all
    • QF_Equality+LinearArith
      • QF_UFDTLIA
      • QF_UFDTLIRA
    • QF_LinearIntArith
      • QF_LIRA
    • QF_LinearRealArith
      • all

OpenSMT-SMTS

• 3 authors
• website: https://github.com/usi-verification-and-security/SMTS
• Participations
  • Parallel
    • QF_Equality
      • all
    • QF_Equality+LinearArith
      • QF_UFDTLIA
      • QF_UFDTLIRA
    • QF_LinearIntArith
      • QF_LIRA
    • QF_LinearRealArith
      • all

[Tomaqa]

I am wondering if it should be submitted as a wrapper tool (over OpenSMT)?

[Tomaqa]

(Updated the archive)

[Tomaqa]

I changed the solver from standalone to derived

[martinjonas]

@Tomaqa Thanks for submitting SMTS to this year's SMT-COMP! As you already know, we decided to extend the deadline for solvers competing in Parallel track to Sunday, June 21 (AoE). Feel free to update your solver until then.

In the meantime, I have executed your solver on a small number of benchmarks from each competitive logic your solver competes in. You can find the results here:

• https://www.fi.muni.cz/~xjonas/smtcomp/tables/opensmtsmts_parallel.table.html#/table

We have not seen any incorrect results returned by your solver (compared to the expected status of the benchmarks) and everything seems to be looking fine.

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. Related to this, I also had to change the command-line options of SMTS to -o 8 instead of -o 128, because 128 threads with only 8 available cores introduced a lot of overhead and did not solve any benchmark.
• 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