Skip to content

Yices2 Submission to SMTCOMP 2026 - #281

Merged
martinjonas merged 4 commits into
SMT-COMP:masterfrom
ahmed-irfan:yices2-2026
Jun 12, 2026
Merged

Yices2 Submission to SMTCOMP 2026#281
martinjonas merged 4 commits into
SMT-COMP:masterfrom
ahmed-irfan:yices2-2026

Conversation

@ahmed-irfan

@ahmed-irfan ahmed-irfan commented May 28, 2026

Copy link
Copy Markdown
Contributor

No description provided.

@github-actions

github-actions Bot commented May 28, 2026 •
edited
Loading

Copy link
Copy Markdown
Summary of modified submissions

Yices2

  • 10 authors
  • website: https://yices.csl.sri.com/
  • Participations
    • UnsatCore
      • QF_Bitvec
        • all
      • QF_Equality
        • all
      • QF_Equality+Bitvec
        • QF_UFBVDT
      • QF_Equality+LinearArith
        • QF_UFDTLIA
        • QF_UFDTLIRA
      • QF_Equality+NonLinearArith
        • QF_UFDTNIA
      • QF_LinearIntArith
        • all
      • QF_LinearRealArith
        • all
      • QF_NonLinearIntArith
        • all
      • QF_NonLinearRealArith
        • all
    • SingleQuery
      • Equality
        • UF
      • QF_Bitvec
        • all
      • QF_Equality
        • all
      • QF_Equality+Bitvec
        • QF_UFBVDT
      • QF_Equality+LinearArith
        • QF_UFDTLIA
        • QF_UFDTLIRA
      • QF_Equality+NonLinearArith
        • QF_UFDTNIA
      • QF_LinearIntArith
        • all
      • QF_LinearRealArith
        • all
      • QF_NonLinearIntArith
        • all
      • QF_NonLinearRealArith
        • all
    • ModelValidation
      • QF_ADT+BitVec
        • QF_UFBVDT
      • QF_ADT+LinArith
        • QF_UFDTLIA
        • QF_UFDTLIRA
      • QF_Bitvec
        • all
      • QF_Equality
        • all
      • QF_Equality+Bitvec
        • all
      • QF_Equality+LinearArith
        • all
      • QF_Equality+NonLinearArith
        • QF_UFDTNIA
      • QF_LinearIntArith
        • all
      • QF_LinearRealArith
        • all
      • QF_NonLinearIntArith
        • all
      • QF_NonLinearRealArith
        • all
    • Incremental
      • 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
    • Parallel
      • QF_Equality+NonLinearArith
        • QF_UFDTNIA
      • QF_NonLinearIntArith
        • all
      • QF_NonLinearRealArith
        • all

@wintered wintered added the submission Submissions for SMT-COMP label May 29, 2026
Tomaqa
Tomaqa approved these changes Jun 5, 2026
View reviewed changes

@Tomaqa Tomaqa left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK!

@martinjonas

martinjonas commented Jun 5, 2026

Copy link
Copy Markdown
Contributor

@ahmed-irfan Thanks for submitting Yices2 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:

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

@ahmed-irfan

ahmed-irfan commented Jun 9, 2026

Copy link
Copy Markdown
Contributor Author

@martinjonas can you please run the tests again.

Thanks

@martinjonas

martinjonas commented Jun 9, 2026

Copy link
Copy Markdown
Contributor

@ahmed-irfan Sure, done! I updated the tables linked from the previous post with the new results.

@ahmed-irfan

ahmed-irfan commented Jun 10, 2026

Copy link
Copy Markdown
Contributor Author

@martinjonas
For Incremental Track: https://www.fi.muni.cz/~xjonas/smtcomp/tables/yices2_inc.table.html#/table, I see there are some QF_BV benchmarks that have errors. However, I tried some on my machine (smtlib-inc original file) and I don't see any issue. Can you please check that and also share the log as I don't have access to that? thanks

@martinjonas

martinjonas commented Jun 10, 2026

Copy link
Copy Markdown
Contributor

@ahmed-irfan Thanks for letting us know, I will look into that. (And extend the deadline for your version of final solver if it is a problem on our side and you need more time.)

You can see the log if you click the status cell in the table (e.g., the text DONE (0 correct)). If it helps your investigation, I uploaded the used scrambled QF_BV incremental files here: https://www.fi.muni.cz/~xjonas/smtcomp/QF_BV_inc.tar.gz . You can find the name of the scrambled *.smt2 file in the *.yml file that defines the task.

@ahmed-irfan

ahmed-irfan commented Jun 11, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor Author

@martinjonas Thanks. I have looked into the scrambled benchmarks. They all start with sat/unsat results and that's why Yices2 is complaining when parsing them. I believe some preprocessing on your end didn't work properly. Can you please confirm?

Here is a snapshot of one benchmark:

sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
unsat
sat
unsat
--- BENCHMARK BEGINS HERE ---
(set-logic QF_BV)
(declare-fun x12325 () Bool)
(declare-fun x27661 () Bool)
(declare-fun x12693 () Bool)
(declare-fun x7338 () Bool)

@martinjonas

martinjonas commented Jun 11, 2026

Copy link
Copy Markdown
Contributor

@ahmed-irfan Good question. This is actually intended. The preprocessed benchmark is not sent directly to the solver, but fed to the official SMT-COMP trace executor (https://github.com/SMT-COMP/trace-executor) that strips the part of benchmark before --- BENCHMARK BEGINS HERE --- and sends the commands that follow to the solver command by command. We use it to prevent the solvers to "look ahead" at the next commands to simulate the real incremental usage of the solver.

@martinjonas

martinjonas commented Jun 11, 2026

Copy link
Copy Markdown
Contributor

@disteph Thanks for the comment. It seems that Ahmed is online, but if he will not be able to update the pull request before the deadline, it is not a large problem. Just update it after the deadline and I will check that the changes are the ones you wrote here. Alternatively, I can change it myself later.

@disteph

disteph commented Jun 11, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

@ahmed-irfan Good question. This is actually intended. The preprocessed benchmark is not sent directly to the solver, but fed to the official SMT-COMP trace executor (https://github.com/SMT-COMP/trace-executor) that strips the part of benchmark before --- BENCHMARK BEGINS HERE --- and sends the commands that follow to the solver command by command. We use it to prevent the solvers to "look ahead" at the next commands to simulate the real incremental usage of the solver.

It still looks like the trace-executor hasn’t run correctly before yices is called, then... since Yices seems to see what should have been stripped

@martinjonas

martinjonas commented Jun 11, 2026

Copy link
Copy Markdown
Contributor

I checked it and the executor is correctly executed before yices and I can reproduce the error on my machine as well:

> ./smtlib2_trace_executor --continue-after-unknown unpack/88c873c842e2c08a87f9650b4a21796c1bce579a22a55ed61f993adbab1bc65f/yices_smt2 --incremental --delegate=cadical benchmarks/files_inc/QF_BV/scrambled21185.smt2
BAD response to set-option command: unexpected EOF

I played with it a little bit more and it seems that there actually is a problem with the --delegate=cadical option that you use only for QF_BV. If I run yices separately with this option, it ends with an error:

> unpack/88c873c842e2c08a87f9650b4a21796c1bce579a22a55ed61f993adbab1bc65f/yices_smt2 --incremental --delegate=cadical ~/temp/debug.smt2 
yices_smt2: unsupported delegate: this version was not compiled to support cadical
Usage: yices_smt2 [options] filename
Try 'yices_smt2 --help' for more information

Moreover, if I do not use the option, the execution with trace executor works fine:

> ./smtlib2_trace_executor --continue-after-unknown unpack/88c873c842e2c08a87f9650b4a21796c1bce579a22a55ed61f993adbab1bc65f/yices_smt2 --incremental benchmarks/files_inc/QF_BV/scrambled21185.smt2
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
[...]

@ahmed-irfan

ahmed-irfan commented Jun 11, 2026

Copy link
Copy Markdown
Contributor Author

@martinjonas I downloaded the zenedo zip file and ran on our linux server and it runs fine. Is it possible the zip file on the benchexec server didn't get updated?
To be sure, I updated the json config with the checksum hash.
Can you please check it again?

@martinjonas

martinjonas commented Jun 11, 2026

Copy link
Copy Markdown
Contributor

@ahmed-irfan Thanks, I will try and run it as soon as possible. If it still does not work, we can slightly extend the submission deadline for your solver.

@martinjonas

martinjonas commented Jun 11, 2026

Copy link
Copy Markdown
Contributor

@ahmed-irfan I updated the table of the Incremental track with the new results. It seems that the issue is fixed. 🎉

@martinjonas

martinjonas commented Jun 11, 2026

Copy link
Copy Markdown
Contributor

@ahmed-irfan Just note that there are some errors "mcsat: unsupported theory" in QF_AUFBVNIA benchmarks. Is this expected?

@disteph

disteph commented Jun 11, 2026

Copy link
Copy Markdown
Contributor

@ahmed-irfan I updated the table of the Incremental track with the new results. It seems that the issue is fixed. 🎉

Thank you so much!

@disteph

disteph commented Jun 11, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

@ahmed-irfan Just note that there are some errors "mcsat: unsupported theory" in QF_AUFBVNIA benchmarks. Is this expected?

Unfortunately yes. We recently discovered a soundness bug in MCSAT (it could say SAT when instance is UNSAT) when extensional equality of arrays is used on array sorts with finite domain or unit range. We've protected those cases with a temporary "mcsat: unsupported theory" exception (SRI-CSL/yices2#590) and left the proper handling of such cases as a to-do (SRI-CSL/yices2#621).

So that would affect logics with Arrays + bitvectors + non-linear arithmetic (otherwise MCSAT is not used), as soon as there's an array equality as above in the instance (which I would guess is a lot, in those logics).

@martinjonas

martinjonas commented Jun 12, 2026

Copy link
Copy Markdown
Contributor

@ahmed-irfan Thanks for submitting Yices2 also to the Parallel track! One important information: we decided to extend the deadline for submissions to the Parallel track to Sunday, June 21 (AoE). Feel free to make a new submission of your parallel solver until then.

In the meantime, we also executed your solver on a small number of benchmarks from each competitive logic in the Parallel track. 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) and everything seems to be looking fine.

You can check whether all the results we have obtained are expected. If not, please let us know here.

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.

@martinjonas

martinjonas commented Jun 12, 2026

Copy link
Copy Markdown
Contributor

I am merging this submissions so that we can start running Yices2 in all the tracks except for the Parallel track. If you want to update the parallel solver, you are welcome to create a new pull request.

@martinjonas
martinjonas merged commit 5180bbb into SMT-COMP:master Jun 12, 2026
5 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

1 more reviewer
@Tomaqa Tomaqa Tomaqa approved these changes
Reviewers whose approvals may not affect merge requirements

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.

5 participants

@ahmed-irfan @martinjonas @disteph @Tomaqa @wintered