OpenSMT (min-ucore) submission 2025

[Tomaqa]

No description provided.

[github-actions]

Summary of modified submissions

OpenSMT (min-ucore)

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

[Tomaqa]

I am a bit confused that all checks have passed. Do the tests run the solver on concrete benchmarks? Because the command I configured uses option --minimal-unsat-cores, which however is not yet implemented in the supplied archive :)

[martinjonas]

@Tomaqa Thanks for submitting OpenSMT (min-ucore) 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:

• Unsat Core Track: https://www.fi.muni.cz/~xjonas/smtcomp/tables/opensmtminucore_unsatcore.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).
• The purpose of the evaluation is just to perform a technical sanity check, whether your solver works fine on our infrastructure. We have therefore not checked the returned unsat cores. The status column for unsat core track just shows the satisfiability of the input formula, not validity of the returned unsat core.
• 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