Amaya's submission for SMT-COMP 2024

[ondrik]

No description provided.

[github-actions]

Summary of modified submissions

Amaya

• 4 authors
• website: https://github.com/MichalHe/amaya
• Participations
  • SingleQuery
    • Arith
      • LIA
      • NIA

[bobot]

Hi it seems that the archive contains a .venv directory with symbolic link to /usr. If you have problems, don't hesitate to reach us.

[ondrik]

@bobot thanks, we're trying to fix the issues to pass the CI. I, however, noticed, that the CI does not seem to take into account the logics field: we specify "divisions": ["Arith"], "logics": ["LIA", "NIA"], but the tests also try NRA and LRA.

[martinjonas]

@ondrik We have executed the latest version of Amaya 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/amaya.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.

[ondrik]

@martinjonas thank you! can you please run the new version?

[martinjonas]

@martinjonas thank you! can you please run the new version?

Sure, done! You can find the new results on the same webpage as before.