Add 2024 Bitwuzla submission.

[mpreiner]

No description provided.

[github-actions]

Summary of modified submissions

Bitwuzla

• 2 authors
• website: https://bitwuzla.github.io/
• Participations
  • UnsatCore
    • Bitvec
      • all
    • Equality+MachineArith
      • ABV
      • ABVFP
      • ABVFPLRA
      • AUFBV
      • AUFBVFP
      • UFBV
      • UFBVFP
    • FPArith
      • all
    • QF_Bitvec
      • all
    • QF_Equality+Bitvec
      • QF_UFBVDT
    • QF_FPArith
      • QF_UFFPDTNIRA
  • SingleQuery
    • Bitvec
      • all
    • Equality+MachineArith
      • ABV
      • ABVFP
      • ABVFPLRA
      • AUFBV
      • AUFBVFP
      • UFBV
      • UFBVFP
    • FPArith
      • all
    • QF_Bitvec
      • all
    • QF_Equality+Bitvec
      • QF_UFBVDT
    • QF_FPArith
      • QF_UFFPDTNIRA
  • ModelValidation
    • QF_ADT+BitVec
      • QF_UFBVDT
    • QF_Bitvec
      • all
    • QF_Equality+Bitvec
      • all
    • QF_FPArith
      • QF_UFFPDTNIRA
  • Incremental
    • Bitvec
      • all
    • Equality+MachineArith
      • all
    • FPArith
      • all
    • QF_Bitvec
      • all
    • QF_Equality+Bitvec
      • all
    • QF_FPArith
      • all

[martinjonas]

@mpreiner We have executed the latest version of Bitwuzla on a randomly chosen subset of 20 single query benchmarks from each logic where it participates. The benchmarks are also scrambled by the competition scrambler (with seed 1). You can find the results here: https://www.fi.muni.cz/~xjonas/smtcomp/bitwuzla.table.html#/table

Quick explanation:

• Green status means that the result agrees with the (set-info :status _) annotation from the benchmark.
• Blue status means that the benchmark has annotation (set-info :status unknown).
• By clicking on the result (e.g. false, true, ABORTED, …) you can see the command-line arguments with which your solver was executed and its output on the benchmark.
• By clicking on the benchmark name (i.e., *scrambled*.yml), you can see the details of the benchmark including its contents (by clicking on the file link in input_files) and the name of the original bennchmark before scrambling (e.g., # original_files: 'non-incremental/AUFBVFP/20210301-Alive2-partial-undef/ph7/583_ph7.smt2').

Please check whether there are some discrepancies, such as missing/extra logics, unexpected aborts or unknowns, and similar. If you update the solver, let me know and I can execute further test runs. We still have plenty of time for several follow-up test runs.

[mpreiner]

@martinjonas Thanks for the update! The runs look good to me! All 24 supported non-incremental logics are included and the command line options are correct.

[martinjonas]

@mpreiner Thanks for checking and for the confirmation that everything seems to be working. I am glad to hear that.

Here are also results of the test run on a small subset of incremental benchmarks: https://www.fi.muni.cz/~xjonas/smtcomp/bitwuzla_inc.table.html#/table

The status column has the following meaning:

• DONE (X correct): the solver terminated successfully and correctly decided X (check-sat) queries before that.
• SOMETHING_ELSE (X correct) (e.g., TIMEOUT (10 correct) or ABORTED (10 correct)): The solver did not terminate successfully, but correctly decided X (check-sat) queries before it crashed or was killed.
• WRONG: There was at least one answer to (check-sat) that did not agree with the status specified in the benchmark.

Again, if there are discrepancies (missing/extra logics, unexpected results), please let me know.

[martinjonas]

@mpreiner We have finished test runs of model-validation and unsat-core generation tracks. You can find the results here:

• https://www.fi.muni.cz/~xjonas/smtcomp/bitwuzla_model.table.html#/table
• https://www.fi.muni.cz/~xjonas/smtcomp/bitwuzla_unsatcore.table.html#/table

As before, you can click on the status of the benchmark to see the output of your solver. If you find any discrepancies or extra/missing logics, please let me know.

Note that we selected only SAT benchmarks for model validation and only UNSAT for unsat-core generation. As a result of that, some logics do not contain any benchmarks. So do not be surprised if you have subscribed to one of these logics and you do not have any result for it. In particular, the logics are:

For model-generation: QF_UFFP, QF_UFBVDT, QF_UFDTNIA, QF_NIRA.

For unsat-core: UFBVDT, FPLRA, QF_AUFBVFP, QF_ABVFPLRA, QF_UFBVDT, QF_UFDTNIA, QF_UFDT, QF_NIA, QF_SNIA.

[bobot]

The verification of the model, using dolmen, failed in two cases
Bitwuzla.zip . In both case an undefined function symbol, e.g. x862 in scrambled126416.smt2, appears strangely defined in the model, (define-fun x862 () x706 x862). Moreover it is used during the definition of another symbol before its definition.

I think dolmen is not at fault to refute this model (@Gbury ?) but I'm not sure for both problem or only one of them.

(We can give more time for fixes for the model validation)

[mpreiner]

Yeah, this doesn't look right, I'll have a look.

[mpreiner]

@bobot It was an issue in the model printer for uninterpreted consts, Dolmen was correct here. I'll upload a fixed version by tomorrow. Thanks for the heads-up!