OpenSMT submission 2025

[Tomaqa]

No description provided.

[github-actions]

Summary of modified submissions

OpenSMT

• 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
  • SingleQuery
    • QF_Equality
      • all
    • QF_Equality+LinearArith
      • QF_UFDTLIA
      • QF_UFDTLIRA
    • QF_LinearIntArith
      • QF_LIRA
    • QF_LinearRealArith
      • all
  • ModelValidation
    • QF_Equality
      • all
    • QF_Equality+LinearArith
      • all
    • QF_LinearIntArith
      • QF_LIRA
    • QF_LinearRealArith
      • all
  • Incremental
    • QF_Equality
      • all
    • QF_Equality+LinearArith
      • all
    • QF_LinearIntArith
      • all
    • QF_LinearRealArith
      • all

[Tomaqa]

I would like to ask if it is possible to add an orthogonal participation using a different configuration of the solver? I am not sure if specialized configurations override the original one, always resulting in at most one participation per track/logic, or if multiple participations are possible.

Concretely, would adding the following

        ,
        {
            "tracks": ["UnsatCore"],
            "command": ["./opensmt", "--minimal-unsat-cores"],
            "logics": [
                "QF_UF", "QF_AX",
                "QF_IDL", "QF_RDL", "QF_LIA", "QF_LRA",
                "QF_UFIDL", "QF_UFLIA", "QF_UFLRA",
                "QF_ALIA",
                "QF_AUFLIA"
            ]
        }

into the field participations in our JSON file result in the second participation in the Unsat Core Track, or is it necessary to create a new submission for that?

[martinjonas]

@Tomaqa Good question! Multiple overlapping participations are not allowed (unfortunately, this is currently not checked by the CI).

If you also want to run an alternative version of OpenSMT on the unsat core benchmarks, please create a new submission for it. This is better as the alternative version will have a more telling name in the result tables and also can have its own dedicated system description that describes the used algorithm in more detail. You can still reuse the same archive url for the two submissions.

[martinjonas]

@Tomaqa Thanks for submitting OpenSMT 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/opensmt.table.html#/table
• Incremental Track: https://www.fi.muni.cz/~xjonas/smtcomp/tables/opensmt_inc.table.html#/table
• Unsat Core Track: https://www.fi.muni.cz/~xjonas/smtcomp/tables/opensmt_unsatcore.table.html#/table
• Model Validation Track: https://www.fi.muni.cz/~xjonas/smtcomp/tables/opensmt_model.table.html#/table

We have not seen any incorrect results returned by your solver (compared to the expected status of the benchmarks). But there are some errors (error "Unknown command encountered: define-sort") in the incremental track.

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).
• For the incremental track, the column status also shows the number of correct answers.
• 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 and models. The status column for unsat core and model validation tracks just shows the satisfiability of the input formula, not validity of the returned unsat core/model.
• 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]

Thank you, we are aware of the issue regarding the define-sort command, but still have not fixed it 😇 Hopefully next year.