STP v2.3.4 submission

[TrevorHansen]

No description provided.

[github-actions]

Summary of modified submissions

STP

• 6 authors
• website: https://stp.github.io/
• Participations
  • SingleQuery
    • QF_Bitvec
      • all
  • ModelValidation
    • QF_Bitvec
      • all
  • Incremental
    • QF_Bitvec
      • all

[bobot]

https://github.com/stp/stp/releases/download/smtcomp2024/smtcomp-2024.zip is not found

[TrevorHansen]

https://github.com/stp/stp/releases/download/smtcomp2024/smtcomp-2024.zip is not found

Thanks. Now fixed.

[martinjonas]

@TrevorHansen Thanks for the update! We have managed to run test runs of STP for single query, incremental, and model-validation tracks on a small subset of benchmarks. You can find the results here:

• https://www.fi.muni.cz/~xjonas/smtcomp/stp.table.html#/table
• https://www.fi.muni.cz/~xjonas/smtcomp/stp_inc.table.html#/table
• https://www.fi.muni.cz/~xjonas/smtcomp/stp_model.table.html#/table

Quick explanation for the single-query track:

• 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').

For the incremental track, 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.

Please let me know if you find any discrepancies or any logics to which you subscribed and seem to be missing (or the other way round).