Yices2 SMTCOMP 2024 Submission

[ahmed-irfan]

No description provided.

[github-actions]

Summary of modified submissions

Yices2

• 7 authors
• website: https://yices.csl.sri.com/
• Participations
  • UnsatCore
    • Equality
      • UF
    • QF_Bitvec
      • all
    • QF_Equality
      • all
    • QF_Equality+Bitvec
      • QF_UFBVDT
    • QF_Equality+LinearArith
      • QF_UFDTLIA
      • QF_UFDTLIRA
    • QF_LinearIntArith
      • all
    • QF_LinearRealArith
      • 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_Bitvec
      • all
    • QF_Equality
      • all
    • QF_Equality+Bitvec
      • all
    • QF_Equality+LinearArith
      • all
    • QF_Equality+NonLinearArith
      • QF_UFNIA
      • QF_UFNRA
    • 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

[ahmed-irfan]

@bobot The summary is showing logics which we didn't submit to. e.g. we didn't submit Yices2 to QF_UFBVDT in the unsatcore track, but it is shown in the summary.

[bobot]

Indeed the markdown removed the strike that where in the original output. Thank you for catching it!

[bobot]

FYI, The output is normally the following. I'm going to fix it (I hope).

[martinjonas]

@ahmed-irfan We have executed the latest version of Yices2 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/yices2.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 called 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.

[martinjonas]

@ahmed-irfan Here are also results of the test run on a small subset of incremental benchmarks: https://www.fi.muni.cz/~xjonas/smtcomp/yices2_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.

IMPORTANT: It seems that the current version of Yices2 produces some wrong results on one of the benchmarks. Note that this occurs only after scrambling, e.g.,

> ~/Repositories/tmp/execution/unpack/1c7b0a3967c19f827b5106f5553956f14149b8847be1efec70065328b36662c8/yices_smt2 --incremental < ~/Projects/SMT-COMP/benchmarks/incremental/QF_AUFBVNIA/20190307-CPAchecker_kInduction-SoSy_Lab/linux-4.0-rc1---drivers--video--fbdev--s3fb.ko.cil_smt-query.0.smt2
sat
sat
> ~/Repositories/scrambler/scrambler -seed 1 -incremental true < ~/Projects/SMT-COMP/benchmarks/incremental/QF_AUFBVNIA/20190307-CPAchecker_kInduction-SoSy_Lab/linux-4.0-rc1---drivers--video--fbdev--s3fb.ko.cil_smt-query.0.smt2 > scrambled.smt2
> ~/Repositories/tmp/execution/unpack/1c7b0a3967c19f827b5106f5553956f14149b8847be1efec70065328b36662c8/yices_smt2 --incremental < scrambled.smt2 
unsat
unsat

If there are any other discrepancies (missing/extra logics, unexpected results), please let me know.

Note that for the execution on our cluster, I had to create a new script yices_smt2_wrapped, because smtlib2_trace_executor does not handle commands with command line options. The content of yices_smt2_wrapped is

#!/usr/bin/env bash                                                                                      
                                                                                                         
DIR=$(dirname "$0")                                                                                      
exec $DIR/yices_smt2 --incremental

and this is the script executed in the runs. This is unrelated to the wrong results, as they occur even without this wrapper.

[ahmed-irfan]

@martinjonas I have updated the solver. Can you please run the tests again?
Also note that I have updated the json configuration file for running the single-query QF_BV benchmarks. It now requires passing a command line argument.
Thanks!

[martinjonas]

@martinjonas I have updated the solver. Can you please run the tests again? Also note that I have updated the json configuration file for running the single-query QF_BV benchmarks. It now requires passing a command line argument. Thanks!

Sure, done! You can find the new results using the same links as before.

And I am glad to see that you managed to fix that wrong result.

[martinjonas]

@ahmed-irfan 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/yices2_model.table.html#/table
• https://www.fi.muni.cz/~xjonas/smtcomp/yices2_unsatcore.table.html#/table

The run already uses your updated version of Yices2.

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 found one wrong model
Yices2.zip .

File "tmp/bad_models/Yices2/scrambled42344.smt2", line 12, character 0-37:
12 | (assert (not (= (x3 (- x6 x5)) 0.0)))
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error This hypothesis/assertion evaluates to false

(We can give more time for fixing the participation in model track)

[ahmed-irfan]

@bobot I have updated the Yices2 executable.
Can you please run the model validation tests again?

Thanks!