plat-smt submission

[dewert99]

No description provided.

[github-actions]

Summary of modified submissions

plat-smt

• 1 authors
• website: https://github.com/dewert99/plat-smt
• Participations
  • UnsatCore
    • QF_Equality
      • QF_UF
  • SingleQuery
    • QF_Equality
      • QF_UF
  • ModelValidation
    • QF_Equality
      • all
  • Incremental
    • QF_Equality
      • all

[Tomaqa]

Dear @dewert99, why did you categorize your solver as wrapped and not as standalone?

[dewert99]

Looking back I saw that I categorized it as wrapped last time I submitted #55. I think it was because I used a fork of an existing sat solver

[Tomaqa]

The rules only ask for special treatment if other SMT solvers are used, not SAT solvers. The underlying SAT solvers are only required to be clearly acknowledged in the report.

Could you change the category to standalone?

Thanks!

[Tomaqa]

Thanks, looks good!

[martinjonas]

@dewert99 Thanks for submitting plat-smt 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/platsmt.table.html#/table
• Incremental Track: https://www.fi.muni.cz/~xjonas/smtcomp/tables/platsmt_inc.table.html#/table
• Unsat Core Track: https://www.fi.muni.cz/~xjonas/smtcomp/tables/platsmt_unsatcore.table.html#/table
• Model Validation Track: https://www.fi.muni.cz/~xjonas/smtcomp/tables/platsmt_model.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).
• 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

[dewert99]

Thanks

[martinjonas]

@dewert99 Thanks again for submitting plat-smt to SMT-COMP. According to the rules, final submissions of all solvers have to be on Zenodo. If you want to participate in this year's SMT-COMP, please reupload the archive without changes (the submission deadline is already over) to Zenodo and update the archive url in the submission. Thanks a lot!

[Tomaqa]

Thanks. Also, make sure that the Zenodo record title states 2026 and not 2024. Thanks!