Z3-Parti-Z3++ Submission for SMT-COMP 2025

[zmylinxi99]

No description provided.

[github-actions]

Summary of modified submissions

Z3-Parti-Z3pp-at-SMT-COMP-2025

• 2 authors
• website: https://github.com/shaowei-cai-group/Z3-Parti-Z3pp-at-SMT-COMP-2025
• Participations
  • Parallel
    • QF_LinearIntArith
      • QF_LIRA
    • QF_LinearRealArith
      • all
    • QF_NonLinearIntArith
      • QF_NIA
    • QF_NonLinearRealArith
      • all

[wintered]

@zmylinxi99 Thank you for submitting your derived tool! Please also submit the corresponding base solver.

[wintered]

On reviewing the submission, we find that categorizing it as a "Wrapper" is more appropriate.
@zmylinxi99 Could you please change the solver type from "Derived" to "Wrapper"? Thanks!

[zmylinxi99]

On reviewing the submission, we find that categorizing it as a "Wrapper" is more appropriate. @zmylinxi99 Could you please change the solver type from "Derived" to "Wrapper"? Thanks!

Thank you for the reminder, and apologies for the delayed response. I've updated the solver type to "wrapped" as requested.

[martinjonas]

@zmylinxi99 Thanks for submitting Z3-Parti-Z3++ to SMT-COMP 2025! We have tried running test runs and we ran into few technical problems. Some are the same as for STP-Parti-Bitwuzla, but even after fixing those, I could not get any result from the solver.

As for STP-Parti-Bitwuzla:

• The path to the executable in the command field has to be relative to the directory where the archive was unpacked.
• Ideally also do not call python3 executable, but directly your solver's entry point (so make the .py file executable and add a shebang to it).
• There is no variable <instance_path>, the input file name is added as a parameter automatically.

When I changed the command in your submission from
"command": ["python3 run_AriParti.py", "<instance_path>"],"
to
"command": ["./Z3-Parti-Z3pp-at-SMT-COMP-2025-build/solver/run_AriParti.py"],
I was able to execute your solver on our infrastructure. Can you make such a change in your submission? Thanks!

But even though I am able to execute the solver after the change, it immediately terminates without any output. This happens even on my machine, unscrambled benchmarks, and when the solver is called using python3. For example,
both

> unpack/2f5dbbc1d87452cf05929a30710aa7552c179606b1cb89e7d2373ed6c4c5ba84/Z3-Parti-Z3pp-at-SMT-COMP-2025-build/solver/run_AriParti.py ~/Projects/SMT-COMP/benchmarks/non-incremental/QF_IDL/20210312-Bouvier/vlsat3_c00.smt2
> python unpack/2f5dbbc1d87452cf05929a30710aa7552c179606b1cb89e7d2373ed6c4c5ba84/Z3-Parti-Z3pp-at-SMT-COMP-2025-build/solver/run_AriParti.py ~/Projects/SMT-COMP/benchmarks/non-incremental/QF_IDL/20210312-Bouvier/vlsat3_c00.smt2

terminate without any output. Can you investigate whether the problem is on my side or yours?

We are going to announce a deadline extension until the end of Sunday (GMT) soon. If you update the submission by then, I can rerun the test runs.

[zmylinxi99]

@martinjonas Thank you very much again for your detailed feedback and assistance.
We have revised our submission Z3-Parti-Z3++ according to your recommendations:

• Added a shebang line and made the run_AriParti.py script executable.
• Updated the "command" field to use a relative path without invoking python3.
• Removed the <instance_path> placeholder, relying on the default input file handling.

Additionally, we would like to kindly ask for one more favor:
Our solver depends on MPI and the mpi4py Python package. In order for the solver to run correctly on your infrastructure, could you please install the following package:

apt-get install python3-mpi4py 

You can test the solver on a benchmark using the following command:

./Z3-Parti-Z3pp-at-SMT-COMP-2025-build/solver/run_AriParti.py ./Z3-Parti-Z3pp-at-SMT-COMP-2025-build/test-instances/lia-sat-10.4.smt2 

Thanks again for the extended deadline — we have updated and re-uploaded our submission accordingly.
Could you kindly rerun the test runs? We hope the solver will now behave correctly.

[martinjonas]

Thanks for all of the fixes, most of the problems are now solved. As for mpi4py, I am not able to install it myself, as the cluster is not under our control. I will contact the administrators of the cluster and it is very likely that they will install it (but I cannot promise anything). It might take a while so I would not count on mpi4py being installed before the deadline for submission of final solvers.

As I said, it is very likely that we will be able to install MPI and mpy4py. But if it is not much work for you and if you want to be certain, wouldn't it be possible to package it together with your solver? This might actually also be better for the other users of you tool.

[zmylinxi99]

@martinjonas Thank you for the update.

Previously, I did try packaging OpenMPI and mpi4py together with the solver and uploading the entire bundle. However, when I tested it in the Docker environment you provided, I encountered various errors due to version mismatches and library incompatibilities. I will continue working on resolving these issues as soon as possible.

If it turns out to be infeasible to make MPI work within the given environment in time, I will consider rolling back the codebase from the distributed version to a purely parallel one. However, that would require substantial changes, and I'm not sure whether I can complete it before the final submission deadline.

Thanks again for your support and patience.

[zmylinxi99]

I’m very sorry for the additional work this has caused for you and the administrators of the cluster. I truly appreciate all the effort you’ve put in and your continued support for the competition — thank you again!

[martinjonas]

@zmylinxi99 Just to keep you informed: I managed to install OpenMPI and mpi4py on the parallel computer we are using for benchmarking. It was a little bit of struggle (OpenMPI 4.* that you depend on is not compatible with cgroups v2), but I managed to get your solver working in the end. The execution is finished and everything seems to be looking fine.

[zmylinxi99]

@zmylinxi99 Just to keep you informed: I managed to install OpenMPI and mpi4py on the parallel computer we are using for benchmarking. It was a little bit of struggle (OpenMPI 4.* that you depend on is not compatible with cgroups v2), but I managed to get your solver working in the end. The execution is finished and everything seems to be looking fine.

Thank you very much!
We’ll keep improving AriParti and make the solver more robust with further efforts.