diff --git a/submissions/STP-Parti-Bitwuzla-p16.json b/submissions/STP-Parti-Bitwuzla-p16.json new file mode 100644 index 00000000..e343e55e --- /dev/null +++ b/submissions/STP-Parti-Bitwuzla-p16.json @@ -0,0 +1,26 @@ +{ + "name": "STP-Parti-Bitwuzla", + "contributors": [ + "Mengyu Zhao", + "Zhenghang Xu", + "Jinkun Lin", + "Shaowei Cai" + ], + "contacts": ["Mengyu Zhao "], + "archive": { + "url": "https://zenodo.org/records/15920866/files/STP-Parti-Bitwuzla-at-SMT-COMP-2025-build.zip" + }, + "website": "https://github.com/shaowei-cai-group/STP-Parti-Bitwuzla-at-SMT-COMP-2025", + "system_description": "https://github.com/shaowei-cai-group/STP-Parti-Bitwuzla-at-SMT-COMP-2025/blob/master/STP_Parti_Bitwuzla_at_SMT_COMP_2025.pdf", + "command": ["./STP-Parti-Bitwuzla-at-SMT-COMP-2025-build/solver/run_BVParti.py", "16"], + "solver_type": "wrapped", + "seed": "998244353", + "participations": [ + { + "tracks": ["Parallel"], + "logics": ["QF_BV"] + } + ], + "competitive": false, + "final": true +} diff --git a/submissions/STP-Parti-Bitwuzla-p32.json b/submissions/STP-Parti-Bitwuzla-p32.json new file mode 100644 index 00000000..e72bf73b --- /dev/null +++ b/submissions/STP-Parti-Bitwuzla-p32.json @@ -0,0 +1,26 @@ +{ + "name": "STP-Parti-Bitwuzla", + "contributors": [ + "Mengyu Zhao", + "Zhenghang Xu", + "Jinkun Lin", + "Shaowei Cai" + ], + "contacts": ["Mengyu Zhao "], + "archive": { + "url": "https://zenodo.org/records/15920866/files/STP-Parti-Bitwuzla-at-SMT-COMP-2025-build.zip" + }, + "website": "https://github.com/shaowei-cai-group/STP-Parti-Bitwuzla-at-SMT-COMP-2025", + "system_description": "https://github.com/shaowei-cai-group/STP-Parti-Bitwuzla-at-SMT-COMP-2025/blob/master/STP_Parti_Bitwuzla_at_SMT_COMP_2025.pdf", + "command": ["./STP-Parti-Bitwuzla-at-SMT-COMP-2025-build/solver/run_BVParti.py", "32"], + "solver_type": "wrapped", + "seed": "998244353", + "participations": [ + { + "tracks": ["Parallel"], + "logics": ["QF_BV"] + } + ], + "competitive": false, + "final": true +} diff --git a/submissions/STP-Parti-Bitwuzla-p8.json b/submissions/STP-Parti-Bitwuzla-p8.json new file mode 100644 index 00000000..f314ddfe --- /dev/null +++ b/submissions/STP-Parti-Bitwuzla-p8.json @@ -0,0 +1,26 @@ +{ + "name": "STP-Parti-Bitwuzla", + "contributors": [ + "Mengyu Zhao", + "Zhenghang Xu", + "Jinkun Lin", + "Shaowei Cai" + ], + "contacts": ["Mengyu Zhao "], + "archive": { + "url": "https://zenodo.org/records/15920866/files/STP-Parti-Bitwuzla-at-SMT-COMP-2025-build.zip" + }, + "website": "https://github.com/shaowei-cai-group/STP-Parti-Bitwuzla-at-SMT-COMP-2025", + "system_description": "https://github.com/shaowei-cai-group/STP-Parti-Bitwuzla-at-SMT-COMP-2025/blob/master/STP_Parti_Bitwuzla_at_SMT_COMP_2025.pdf", + "command": ["./STP-Parti-Bitwuzla-at-SMT-COMP-2025-build/solver/run_BVParti.py", "8"], + "solver_type": "wrapped", + "seed": "998244353", + "participations": [ + { + "tracks": ["Parallel"], + "logics": ["QF_BV"] + } + ], + "competitive": false, + "final": true +} diff --git a/submissions/STP-Parti-Bitwuzla.json b/submissions/STP-Parti-Bitwuzla.json index 99ce499f..5dedf932 100644 --- a/submissions/STP-Parti-Bitwuzla.json +++ b/submissions/STP-Parti-Bitwuzla.json @@ -8,11 +8,11 @@ ], "contacts": ["Mengyu Zhao "], "archive": { - "url": "https://zenodo.org/records/15640499/files/STP-Parti-Bitwuzla-at-SMT-COMP-2025-build.zip" + "url": "https://zenodo.org/records/15920866/files/STP-Parti-Bitwuzla-at-SMT-COMP-2025-build.zip" }, "website": "https://github.com/shaowei-cai-group/STP-Parti-Bitwuzla-at-SMT-COMP-2025", "system_description": "https://github.com/shaowei-cai-group/STP-Parti-Bitwuzla-at-SMT-COMP-2025/blob/master/STP_Parti_Bitwuzla_at_SMT_COMP_2025.pdf", - "command": ["./STP-Parti-Bitwuzla-at-SMT-COMP-2025-build/solver/run_BVParti.py"], + "command": ["./STP-Parti-Bitwuzla-at-SMT-COMP-2025-build/solver/run_BVParti.py", "64"], "solver_type": "wrapped", "seed": "998244353", "participations": [ diff --git a/submissions/Z3-Parti-Z3pp-p16.json b/submissions/Z3-Parti-Z3pp-p16.json new file mode 100644 index 00000000..306bbfb8 --- /dev/null +++ b/submissions/Z3-Parti-Z3pp-p16.json @@ -0,0 +1,24 @@ +{ + "name": "Z3-Parti-Z3pp", + "contributors": [ + "Mengyu Zhao", + "Shaowei Cai" + ], + "contacts": ["Mengyu Zhao "], + "archive": { + "url": "https://zenodo.org/records/15920863/files/Z3-Parti-Z3pp-at-SMT-COMP-2025-build.zip" + }, + "website": "https://github.com/shaowei-cai-group/Z3-Parti-Z3pp-at-SMT-COMP-2025", + "system_description": "https://github.com/shaowei-cai-group/Z3-Parti-Z3pp-at-SMT-COMP-2025/blob/master/Z3_Parti_Z3pp_at_SMT_COMP_2025.pdf", + "command": ["./Z3-Parti-Z3pp-at-SMT-COMP-2025-build/solver/run_AriParti.py", "16"], + "solver_type": "wrapped", + "seed": "998244353", + "participations": [ + { + "tracks": ["Parallel"], + "logics": ["QF_RDL", "QF_IDL", "QF_LRA", "QF_LIA", "QF_NRA", "QF_NIA"] + } + ], + "competitive": false, + "final": true +} diff --git a/submissions/Z3-Parti-Z3pp-p32.json b/submissions/Z3-Parti-Z3pp-p32.json new file mode 100644 index 00000000..2779c767 --- /dev/null +++ b/submissions/Z3-Parti-Z3pp-p32.json @@ -0,0 +1,24 @@ +{ + "name": "Z3-Parti-Z3pp", + "contributors": [ + "Mengyu Zhao", + "Shaowei Cai" + ], + "contacts": ["Mengyu Zhao "], + "archive": { + "url": "https://zenodo.org/records/15920863/files/Z3-Parti-Z3pp-at-SMT-COMP-2025-build.zip" + }, + "website": "https://github.com/shaowei-cai-group/Z3-Parti-Z3pp-at-SMT-COMP-2025", + "system_description": "https://github.com/shaowei-cai-group/Z3-Parti-Z3pp-at-SMT-COMP-2025/blob/master/Z3_Parti_Z3pp_at_SMT_COMP_2025.pdf", + "command": ["./Z3-Parti-Z3pp-at-SMT-COMP-2025-build/solver/run_AriParti.py", "32"], + "solver_type": "wrapped", + "seed": "998244353", + "participations": [ + { + "tracks": ["Parallel"], + "logics": ["QF_RDL", "QF_IDL", "QF_LRA", "QF_LIA", "QF_NRA", "QF_NIA"] + } + ], + "competitive": false, + "final": true +} diff --git a/submissions/Z3-Parti-Z3pp-p8.json b/submissions/Z3-Parti-Z3pp-p8.json new file mode 100644 index 00000000..b347c9f1 --- /dev/null +++ b/submissions/Z3-Parti-Z3pp-p8.json @@ -0,0 +1,24 @@ +{ + "name": "Z3-Parti-Z3pp", + "contributors": [ + "Mengyu Zhao", + "Shaowei Cai" + ], + "contacts": ["Mengyu Zhao "], + "archive": { + "url": "https://zenodo.org/records/15920863/files/Z3-Parti-Z3pp-at-SMT-COMP-2025-build.zip" + }, + "website": "https://github.com/shaowei-cai-group/Z3-Parti-Z3pp-at-SMT-COMP-2025", + "system_description": "https://github.com/shaowei-cai-group/Z3-Parti-Z3pp-at-SMT-COMP-2025/blob/master/Z3_Parti_Z3pp_at_SMT_COMP_2025.pdf", + "command": ["./Z3-Parti-Z3pp-at-SMT-COMP-2025-build/solver/run_AriParti.py", "8"], + "solver_type": "wrapped", + "seed": "998244353", + "participations": [ + { + "tracks": ["Parallel"], + "logics": ["QF_RDL", "QF_IDL", "QF_LRA", "QF_LIA", "QF_NRA", "QF_NIA"] + } + ], + "competitive": false, + "final": true +} diff --git a/submissions/Z3-Parti-Z3pp.json b/submissions/Z3-Parti-Z3pp.json index 78890447..6a7ba487 100644 --- a/submissions/Z3-Parti-Z3pp.json +++ b/submissions/Z3-Parti-Z3pp.json @@ -6,11 +6,11 @@ ], "contacts": ["Mengyu Zhao "], "archive": { - "url": "https://zenodo.org/records/15763079/files/Z3-Parti-Z3pp-at-SMT-COMP-2025-build.zip" + "url": "https://zenodo.org/records/15920863/files/Z3-Parti-Z3pp-at-SMT-COMP-2025-build.zip" }, "website": "https://github.com/shaowei-cai-group/Z3-Parti-Z3pp-at-SMT-COMP-2025", "system_description": "https://github.com/shaowei-cai-group/Z3-Parti-Z3pp-at-SMT-COMP-2025/blob/master/Z3_Parti_Z3pp_at_SMT_COMP_2025.pdf", - "command": ["./Z3-Parti-Z3pp-at-SMT-COMP-2025-build/solver/run_AriParti.py"], + "command": ["./Z3-Parti-Z3pp-at-SMT-COMP-2025-build/solver/run_AriParti.py", "64"], "solver_type": "wrapped", "seed": "998244353", "participations": [