From 0cb08c245279137971a81da5fbd8f81bc42bbf4b Mon Sep 17 00:00:00 2001 From: douglaslee01 <2205459936@qq.com> Date: Tue, 27 May 2025 07:54:24 +0000 Subject: [PATCH 1/5] upload z3-inc-z3++, the base solver is z3-4-13-4-inc --- submissions/Z3-4-13-4-inc.json | 14 ++++++++++++++ submissions/Z3-Inc-Z3++.json | 19 +++++++++++++++++++ 2 files changed, 33 insertions(+) create mode 100644 submissions/Z3-4-13-4-inc.json create mode 100644 submissions/Z3-Inc-Z3++.json diff --git a/submissions/Z3-4-13-4-inc.json b/submissions/Z3-4-13-4-inc.json new file mode 100644 index 00000000..678f2804 --- /dev/null +++ b/submissions/Z3-4-13-4-inc.json @@ -0,0 +1,14 @@ +{ + "name": "Z3-4-13-4-inc", + "archive": { + "url": "https://zenodo.org/records/15524795/files/z3.zip" + }, + "website": "https://github.com/Z3Prover/z3/wiki", + "command": [ "./smtcomp_run_incremental" ], + "solver_type": "Standalone", + "seed": 174228, + "participations": [ + { "tracks": ["Incremental"], "logics": "QF_NIA" } + ], + "competitive": false +} diff --git a/submissions/Z3-Inc-Z3++.json b/submissions/Z3-Inc-Z3++.json new file mode 100644 index 00000000..75bbfdb3 --- /dev/null +++ b/submissions/Z3-Inc-Z3++.json @@ -0,0 +1,19 @@ +{ + "name": "Z3-Inc-Z3++", + "contributors": [ + "Bohan Li", + "Shaowei Cai" + ], + "contacts": ["Bohan Li ", "Shaowei Cai "], + "archive": { + "url": "https://zenodo.org/records/15516426/files/new.zip" + }, + "website": "https://z3-plus-plus.github.io/", + "system_description": "https://github.com/z3-plus-plus/z3-plus-plus.github.io/blob/main/Z3%2B%2B_in_SMT_COMP_2025.pdf", + "command": [ "./smtcomp_run_incremental" ], + "solver_type": "derived", + "seed": "19970530", + "participations": [ + { "tracks": ["Incremental"], "logics": "QF_NIA" } + ] +} From a4d5ffbc666d7a6e8c31c5fb02d1492786c80c88 Mon Sep 17 00:00:00 2001 From: douglaslee01 <2205459936@qq.com> Date: Tue, 27 May 2025 07:54:24 +0000 Subject: [PATCH 2/5] upload z3-inc-z3++, the base solver is z3-4-13-4-inc --- submissions/Z3-4-13-4-inc.json | 14 ++++++++++++++ submissions/Z3-Inc-Z3++.json | 19 +++++++++++++++++++ 2 files changed, 33 insertions(+) create mode 100644 submissions/Z3-4-13-4-inc.json create mode 100644 submissions/Z3-Inc-Z3++.json diff --git a/submissions/Z3-4-13-4-inc.json b/submissions/Z3-4-13-4-inc.json new file mode 100644 index 00000000..678f2804 --- /dev/null +++ b/submissions/Z3-4-13-4-inc.json @@ -0,0 +1,14 @@ +{ + "name": "Z3-4-13-4-inc", + "archive": { + "url": "https://zenodo.org/records/15524795/files/z3.zip" + }, + "website": "https://github.com/Z3Prover/z3/wiki", + "command": [ "./smtcomp_run_incremental" ], + "solver_type": "Standalone", + "seed": 174228, + "participations": [ + { "tracks": ["Incremental"], "logics": "QF_NIA" } + ], + "competitive": false +} diff --git a/submissions/Z3-Inc-Z3++.json b/submissions/Z3-Inc-Z3++.json new file mode 100644 index 00000000..75bbfdb3 --- /dev/null +++ b/submissions/Z3-Inc-Z3++.json @@ -0,0 +1,19 @@ +{ + "name": "Z3-Inc-Z3++", + "contributors": [ + "Bohan Li", + "Shaowei Cai" + ], + "contacts": ["Bohan Li ", "Shaowei Cai "], + "archive": { + "url": "https://zenodo.org/records/15516426/files/new.zip" + }, + "website": "https://z3-plus-plus.github.io/", + "system_description": "https://github.com/z3-plus-plus/z3-plus-plus.github.io/blob/main/Z3%2B%2B_in_SMT_COMP_2025.pdf", + "command": [ "./smtcomp_run_incremental" ], + "solver_type": "derived", + "seed": "19970530", + "participations": [ + { "tracks": ["Incremental"], "logics": "QF_NIA" } + ] +} From 80bdf2681f0ef9cadff3d124f0f4f798e4c3f8e9 Mon Sep 17 00:00:00 2001 From: douglaslee01 <2205459936@qq.com> Date: Tue, 27 May 2025 08:16:51 +0000 Subject: [PATCH 3/5] set the empty contributor/contacts/system_description for z3-4-13-4 --- submissions/Z3-4-13-4-inc.json | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/submissions/Z3-4-13-4-inc.json b/submissions/Z3-4-13-4-inc.json index 678f2804..a6492702 100644 --- a/submissions/Z3-4-13-4-inc.json +++ b/submissions/Z3-4-13-4-inc.json @@ -3,7 +3,12 @@ "archive": { "url": "https://zenodo.org/records/15524795/files/z3.zip" }, + "contributors": [ + "TBA" + ], + "contacts": ["TBA"], "website": "https://github.com/Z3Prover/z3/wiki", + "system_description": "TBA", "command": [ "./smtcomp_run_incremental" ], "solver_type": "Standalone", "seed": 174228, From 5a08067c1abac54ff391eb9bc4d9417826d2bea1 Mon Sep 17 00:00:00 2001 From: douglaslee01 <2205459936@qq.com> Date: Tue, 27 May 2025 08:22:39 +0000 Subject: [PATCH 4/5] update the system description of z3 --- submissions/Z3-4-13-4-inc.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submissions/Z3-4-13-4-inc.json b/submissions/Z3-4-13-4-inc.json index a6492702..b35f7b69 100644 --- a/submissions/Z3-4-13-4-inc.json +++ b/submissions/Z3-4-13-4-inc.json @@ -8,7 +8,7 @@ ], "contacts": ["TBA"], "website": "https://github.com/Z3Prover/z3/wiki", - "system_description": "TBA", + "system_description": "https://link.springer.com/chapter/10.1007/978-3-540-78800-3_24", "command": [ "./smtcomp_run_incremental" ], "solver_type": "Standalone", "seed": 174228, From b4699684f1d10e9ad795a737e1099c0e017ee424 Mon Sep 17 00:00:00 2001 From: douglaslee01 <2205459936@qq.com> Date: Tue, 27 May 2025 08:27:22 +0000 Subject: [PATCH 5/5] update contributors --- submissions/Z3-4-13-4-inc.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/submissions/Z3-4-13-4-inc.json b/submissions/Z3-4-13-4-inc.json index b35f7b69..16ce5501 100644 --- a/submissions/Z3-4-13-4-inc.json +++ b/submissions/Z3-4-13-4-inc.json @@ -4,9 +4,9 @@ "url": "https://zenodo.org/records/15524795/files/z3.zip" }, "contributors": [ - "TBA" + "Nikolaj Bjørner" ], - "contacts": ["TBA"], + "contacts": ["Nikolaj Bjørner "], "website": "https://github.com/Z3Prover/z3/wiki", "system_description": "https://link.springer.com/chapter/10.1007/978-3-540-78800-3_24", "command": [ "./smtcomp_run_incremental" ],