Z3-alpha draft PR

[JohnLyu2]

No description provided.

[bobot]

I added the extension .json

[github-actions]

Summary of modified submissions

Z3-alpha

• 5 authors
• website: https://github.com/JohnLyu2/z3alpha
• Participations
  • SingleQuery
    • Bitvec
      • all
    • QF_Bitvec
      • all
    • QF_Datatypes
      • all
    • QF_Equality
      • all
    • QF_Equality+Bitvec
      • QF_AUFBV
      • QF_UFBV
    • QF_LinearIntArith
      • all
    • QF_LinearRealArith
      • all
    • QF_NonLinearIntArith
      • all
    • QF_NonLinearRealArith
      • all
    • QF_Strings
      • all

[martinjonas]

@JohnLyu2 Thanks for the changes! I was able to execute the test runs without any major issues (the only thing is that "command": ["z3alpha.py"] should be replaced by "command": ["z3alpha_submission/z3alpha.py"]).

In particular, we have executed the latest version of Z3-alpha 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/z3alpha.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.

[JohnLyu2]

@JohnLyu2 Thanks for the changes! I was able to execute the test runs without any major issues (the only thing is that "command": ["z3alpha.py"] should be replaced by "command": ["z3alpha_submission/z3alpha.py"]).

In particular, we have executed the latest version of Z3-alpha 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/z3alpha.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.

Hi @martinjonas , thanks! I just made a new submission (with slight updates). Can you help me do a quick check? If it is problem-free, it will be our final submission.