Skip to content

SMTInterpol submission 2025 #168

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 5 commits into from
Jul 2, 2025
Merged

SMTInterpol submission 2025 #168

merged 5 commits into from
Jul 2, 2025

Conversation

@jhoenicke
Copy link
Member

@jhoenicke jhoenicke commented Jun 10, 2025

Solver submission for SMT-COMP: SMTInterpol

@github-actions
Copy link

github-actions bot commented Jun 10, 2025

Summary of modified submissions

SMTInterpol

  • 14 authors
  • website: https://ultimate.informatik.uni-freiburg.de/smtinterpol
  • Participations
    • UnsatCore
      • Arith
        • all
      • Bitvec
        • all
      • Equality
        • all
      • Equality+LinearArith
        • all
      • Equality+MachineArith
        • ABV
        • AUFBV
        • AUFBVDTLIA
        • AUFBVDTNIA
        • AUFBVDTNIRA
        • UFBV
        • UFBVDT
        • UFBVDTLIA
        • UFBVDTNIA
        • UFBVDTNIRA
        • UFBVLIA
      • Equality+NonLinearArith
        • all
      • QF_Bitvec
        • all
      • QF_Datatypes
        • all
      • QF_Equality
        • all
      • QF_Equality+Bitvec
        • all
      • QF_Equality+LinearArith
        • all
      • QF_Equality+NonLinearArith
        • all
      • QF_LinearIntArith
        • all
      • QF_LinearRealArith
        • all
      • QF_NonLinearIntArith
        • all
      • QF_NonLinearRealArith
        • all
    • SingleQuery
      • Arith
        • all
      • Bitvec
        • all
      • Equality
        • all
      • Equality+LinearArith
        • all
      • Equality+MachineArith
        • ABV
        • AUFBV
        • AUFBVDTLIA
        • AUFBVDTNIA
        • AUFBVDTNIRA
        • UFBV
        • UFBVDT
        • UFBVDTLIA
        • UFBVDTNIA
        • UFBVDTNIRA
        • UFBVLIA
      • Equality+NonLinearArith
        • all
      • QF_Bitvec
        • all
      • QF_Datatypes
        • all
      • QF_Equality
        • all
      • QF_Equality+Bitvec
        • all
      • QF_Equality+LinearArith
        • all
      • QF_Equality+NonLinearArith
        • all
      • QF_LinearIntArith
        • all
      • QF_LinearRealArith
        • all
      • QF_NonLinearIntArith
        • all
      • QF_NonLinearRealArith
        • all
    • ModelValidation
      • QF_ADT+BitVec
        • all
      • QF_ADT+LinArith
        • all
      • QF_Bitvec
        • all
      • QF_Datatypes
        • all
      • QF_Equality
        • all
      • QF_Equality+Bitvec
        • all
      • QF_Equality+LinearArith
        • all
      • QF_Equality+NonLinearArith
        • all
      • QF_LinearIntArith
        • all
      • QF_LinearRealArith
        • all
      • QF_NonLinearIntArith
        • all
      • QF_NonLinearRealArith
        • all
    • Incremental
      • Arith
        • all
      • Bitvec
        • all
      • Equality
        • all
      • Equality+LinearArith
        • all
      • Equality+NonLinearArith
        • all
      • QF_Bitvec
        • all
      • QF_Equality
        • all
      • QF_Equality+Bitvec
        • all
      • QF_Equality+Bitvec+Arith
        • all
      • QF_Equality+LinearArith
        • all
      • QF_Equality+NonLinearArith
        • all
      • QF_LinearIntArith
        • all
      • QF_LinearRealArith
        • all
      • QF_NonLinearIntArith
        • all

@bobot bobot added the submission Submissions for SMT-COMP label Jun 14, 2025
martinjonas pushed a commit that referenced this pull request Jun 23, 2025
merge submissions
a50e349 
#189: UltimateEliminator submission 2025
#188: Z3-Siri Submission 2025
#187: OSTRICH version 2
#186: yicesQS submission to the 2025 SMT comp
#185: Bitwuzla 2025 submission.
#184: Yices2 Submission SMTCOMP 2025
#183: cvc5 for SMT-COMP 2025
#182: Create iProver
#181: Z3-Owl Submission 2025
#179: Z3-alpha SMT-COMP 2025
#178: Z3-Noodler-Mocha Submission for SMT-COMP 2025
#177: `bv_decide` submission 2025
#176: OpenSMT (min-ucore) submission 2025
#175: Z3-Noodler submission 2025
#172: SMTS submission 2025
#171: Bitwuzla-MachBV Submission for SMT-COMP 2025
#170: Z3-Parti-Z3++ Submission for SMT-COMP 2025
#169: STP-Parti-Bitwuzla Submission for SMT-COMP 2025
#168: SMTInterpol submission 2025
#167: OpenSMT submission 2025
#165: Amaya 2025
#164: SMT-RAT submission
#163: COLIBRI submission
#162: [Submission] colibri2
#156: upload z3-inc-z3++
@martinjonas
Copy link
Contributor

martinjonas commented Jun 25, 2025

@jhoenicke Thanks for submitting SMTInterpol 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:

We have not seen any incorrect results returned by your solver (compared to the expected status of the benchmarks). We have noticed some errors (error "<stdin>:763:10: Proof-check failed") on the incremental 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).
  • 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

@jhoenicke
Copy link
Member Author

jhoenicke commented Jun 25, 2025

@martinjonas Is it possible to download the log files? Or can you point me to the benchmarks where the proof-check failed happened?

@jhoenicke
Copy link
Member Author

jhoenicke commented Jun 26, 2025

I found some instances in QF_BVLRA. This is a new logic, we didn't test on. Since we use integers to handle bitvectors, we internally use LIRA logic, but the proof checker didn't consider this and rejects the proof when it uses LIRA operators. There also seems to be a problem with my internal model validator; the unknown should all be sat. There may also be type-checking problems as we think that "5" is of type Int, but the standard says it's of type Real, since it's QF_BVLRA.

I will try to fix these problems and provide a new version. Is there a way to record output to stderr produced in the competition? It would be good to know after the competition in which benchmarks there were proof/model problems instead of just having unknown which could mean anything, especially for undecidable logics.

@martinjonas
Copy link
Contributor

martinjonas commented Jun 26, 2025

I found some instances in QF_BVLRA. This is a new logic, we didn't test on. Since we use integers to handle bitvectors, we internally use LIRA logic, but the proof checker didn't consider this and rejects the proof when it uses LIRA operators. There also seems to be a problem with my internal model validator; the unknown should all be sat. There may also be type-checking problems as we think that "5" is of type Int, but the standard says it's of type Real, since it's QF_BVLRA.

Thanks for the insight, that makes sense. I tried to improve the result tables so that you can now identify the errors more easily. For example, in
https://www.fi.muni.cz/~xjonas/smtcomp/tables/smtinterpol_inc.table.html#/table
there are now rows with status ERROR (0 correct) instead of DONE (0 correct), which means that the solver returned 0 correct answers and crashed.

The same thing should be present in the other tables that now distinguish between unknown and ERROR. Currently, the model validation and unsat core benchmarks are classified as unknown if the response to (check-sat) command is unknown, even if it is followed by an error. I can change that if you want.

Is there a way to record output to stderr produced in the competition?

All output, both stdout and stderr, are recorded (and merged). You can download find it here:

In each of these directories, if you go to the subdirectories corresponding to the division and solver of interest, you can find a *.logfiles.zip file with the outputs (among other things). For example https://www.fi.muni.cz/~xjonas/smtcomp/results_inc/QF_Bitvec/smtinterpol/smtinterpol_inc_QF_Bitvec.2025-06-26_20-23-06.logfiles.zip

@jhoenicke
Copy link
Member Author

jhoenicke commented Jun 26, 2025

I updated the binary. It fixes the problems with QF_BVLRA, also the models work now.

@martinjonas
Copy link
Contributor

martinjonas commented Jun 27, 2025

Thanks! I updated the tables with the new results. If anything is still unexpected, let me know.

@martinjonas
Copy link
Contributor

martinjonas commented Jul 1, 2025

@jhoenicke The final versions of solvers should be uploaded to Zenodo. Please, do this as soon as possible and change the archive url. Thanks!

@jhoenicke
Copy link
Member Author

jhoenicke commented Jul 2, 2025

I submitted the zenodo for review.
The sha256sum should be the same, the url will be probably https://zenodo.org/records/15756957/files/smtinterpol-2.5-1405-gae7e68ef.tar.gz?download=1

@martinjonas
Copy link
Contributor

martinjonas commented Jul 2, 2025

@jhoenicke Thanks a lot, I have just approved it. When you modify the archive url in this pull request, I will merge it right away.

@martinjonas martinjonas merged commit 6b804b9 into master Jul 2, 2025
5 checks passed
@martinjonas martinjonas deleted the jhoenicke-smtinterpol branch July 2, 2025 08:17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

submission Submissions for SMT-COMP

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@jhoenicke @martinjonas @bobot