OSTRICH 1.4

[pruemmer]

No description provided.

[github-actions]

Summary of modified submissions

OSTRICH
├── 6 authors
├── website: https://github.com/uuverifiers/ostrich
└── Participations
    └── SingleQuery
        └── QF_Strings
            └── all

[martinjonas]

@pruemmer Thanks for submitting OSTRICH to SMT-COMP! The command list is expected to contain one string for the executable and then one string per command line argument (similarly to how Python's subprocess.run is called). Could you change it in the pull request? In your case, it would be something like "command": ["./ostrich", "-portfolio=strings", "+quiet"].

I fixed that locally and tried running the current submission on our competition infrastructure with some trivial benchmarks. Everything else seems to be working so far!

[pruemmer]

Sure, thanks for the fix! I wasn't sure about the expected format here.

[martinjonas]

@pruemmer We have executed the latest version of OSTRICH 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/ostrich.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.

[pruemmer]

Thanks; we have now made a new version of Ostrich 1.4 (pre) available:
https://philipp.ruemmer.org/ostrich-2024.tar.gz
Could you do test runs with this version as well?

[martinjonas]

Thanks; we have now made a new version of Ostrich 1.4 (pre) available: https://philipp.ruemmer.org/ostrich-2024.tar.gz Could you do test runs with this version as well?

Done! You can find the new results on the same URL as before: https://www.fi.muni.cz/~xjonas/smtcomp/ostrich.table.html#/table

[pruemmer]

Great, thanks! We have now made the final version of Ostrich available, under the same link: https://philipp.ruemmer.org/ostrich-2024.tar.gz