Samet submission for SMT-COMP 2026

[blishko]

No description provided.

[github-actions]

Summary of modified submissions

Samet

• 1 authors
• website: https://github.com/blishko/
• Participations
  • SingleQuery
    • QF_LinearRealArith
      • QF_LRA

[Tomaqa]

Dear @blishko, do I understand correctly that there are no external tools employed, including the underlying SAT solver?

[blishko]

That's correct. There are no external tools. The SAT solver is custom made.

[Tomaqa]

OK!

[martinjonas]

@blishko Thanks for submitting Samet 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/samet.table.html#/table

It seems that there is some problem with your submission as all the executions end up with an error

libc++abi: terminating due to uncaught exception of type std::logic_error: Missing implementation
   in bool samet::frontend::smt::(anonymous namespace)::Session::execute_command()
   at /samet/src/frontend/smt/Interpreter.cpp:68

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

[blishko]

Hi @martinjonas! Thanks for letting me know. I have uploaded a new version which should be able to run.
Fun fact: None of the QF_LRA single-query SMT-LIB benchmarks contains set-option command.

[martinjonas]

@blishko I updated the tables linked from the previous post with the new results. It looks much better now. :-)

[blishko]

I have uploaded the final version of the solver.