z3-alpha2 first version submission

[JohnLyu2]

As title

[github-actions]

Summary of modified submissions

Z3-alpha2-base

• 1 authors
• website: https://github.com/z3prover/z3
• Participations
  • SingleQuery
    • Arith
      • all
    • QF_Bitvec
      • all
    • QF_Datatypes
      • all
    • QF_Equality+NonLinearArith
      • all
    • QF_LinearIntArith
      • all
    • QF_NonLinearIntArith
      • all
    • QF_NonLinearRealArith
      • all

Z3-alpha2-debug

• 5 authors
• website: https://github.com/JohnLyu2/z3alpha
• Participations
  • SingleQuery
    • Arith
      • all
    • QF_Bitvec
      • all
    • QF_Datatypes
      • all
    • QF_Equality+NonLinearArith
      • all
    • QF_LinearIntArith
      • all
    • QF_NonLinearIntArith
      • all
    • QF_NonLinearRealArith
      • all

Z3-alpha2

• 5 authors
• website: https://github.com/JohnLyu2/z3alpha
• Participations
  • SingleQuery
    • Arith
      • all
    • QF_Bitvec
      • all
    • QF_Datatypes
      • all
    • QF_Equality+NonLinearArith
      • all
    • QF_LinearIntArith
      • all
    • QF_NonLinearIntArith
      • all
    • QF_NonLinearRealArith
      • all

[Tomaqa]

Dear authors, thank you for the submission. Please acknowledge the solver that you are basing on explicitly in the system description. Could you also please, instead of just including the binary of z3 in the archive, make a separate submission for the base solver (take a look e.g. here), marking it as non-competing? Thank you very much.

[martinjonas]

@JohnLyu2 Thanks for submitting z3-alpha2 to this year's SMT-COMP!

We have executed your solver on a small number of benchmarks from each logic it should compete in (except for the parallel track). You can find the results here:

• Single Query Track: https://www.fi.muni.cz/~xjonas/smtcomp/tables/z3alpha2.table.html#/table

We have not seen any incorrect results returned by your solver (compared to the expected status of the benchmarks).

You can check whether all the results we have obtained are expected. If not, please let us know here.

Some notes:

• We have used smaller resource limits than will be used in the final runs.
• The benchmarks are scrambled by the official scrambler with seed 1.
• The column status shows whether your solver decided the benchmark as sat (true) or unsat (false).
• You can click on the value in the status column to see the output of your solver on that benchmark.

If you upload a new version of the solver and want to have another test run, let me know. We still have some time for that.

Happy rest of the competition!
Martin

[JohnLyu2]

@Tomaqa @martinjonas Thank you! I've updated the description and added the base-solver submission. I've updated the artifact to a new version; if time still allows, a test run would be appreciated! (no worries if it is too late)

[Tomaqa]

OK!

[martinjonas]

@JohnLyu2 I executed the test run with the new version. I updated the table with the results at the link above.

[JohnLyu2]

@martinjonas Thank you so much! I've checked the results and noticed that for three instances, i.e.,

• QF_UFDTNIA/393160_QF_UFDTNIA_20230314-Jaroslav-Bendik-Certora_38347_092cc73601c78e45f4f9_57_QF_UFDTNIA.yml
• QF_UFDTNIA/393215_QF_UFDTNIA_20230314-Jaroslav-Bendik-Certora_940_590f27b1c3c800d3243e_32_QF_UFDTNIA.yml
• QF_UFDTNIA/393220_QF_UFDTNIA_20240410-certora__nia-splits_0010.yml

the submitted solver is consistently able to solve the corresponding SMT-LIB instances quite quickly on my end when run inside the competition Docker image. However, the test run reports timeout for them. I am curious about the reason. Are they scrambled instances? Is it possible for me to obtain these instances? Thanks.

[martinjonas]

@JohnLyu2 Yes, the benchmarks are scrambled by the official SMT-COMP scrambler: https://github.com/SMT-COMP/scrambler/ For the test runs, we used fixed seed 1. It will be different for the final runs.

[JohnLyu2]

@martinjonas Thank you! I tested with the scrambled instances, and the submission on my end (tested with the competition docker) seems to be robust to the scrambler. I'm not sure what may cause the discrepancy. One possible source of issues: our submission bundles pre-built Python wheels (numpy etc) compiled for the competition environment (Python 3.12 etc). Since the competition rule, I muted any error message, so if there is a compatibility issue, the solver won't report. Can you help run our submission with debug mode (command: ./z3alpha2.py --debug) on any QF_UFDTNIA instance (e.g., QF_UFDTNIA/393160_QF_UFDTNIA_20230314-Jaroslav-Bendik-Certora_38347_092cc73601c78e45f4f9_57_QF_UFDTNIA.yml) and let me know the debug message (from stderr)? Thank you!

Some updates: I added a debugger version in my submission to check some CI test results. It seems there is no environemnt problem in CI tests, and my local test environment uses the same logic as CI. It seems the scrambler and bundling (at least on CI) are not the problem. I am not sure why the aforementioned instances cannot be solved in the test run. They can be consistently solved on my end (in ~1s, ~6s, and ~25s).