From 1dd9e72c46d4acf0bc821506e2f9d66f8f24c07c Mon Sep 17 00:00:00 2001 From: bluerar <2351320068@qq.com> Date: Tue, 26 May 2026 13:02:09 +0000 Subject: [PATCH 01/13] new file: submissions/z3gex-base.json new file: submissions/z3gex.json --- submissions/z3gex-base.json | 30 ++++++++++++++++++++++++++++++ submissions/z3gex.json | 30 ++++++++++++++++++++++++++++++ 2 files changed, 60 insertions(+) create mode 100644 submissions/z3gex-base.json create mode 100644 submissions/z3gex.json diff --git a/submissions/z3gex-base.json b/submissions/z3gex-base.json new file mode 100644 index 000000000..8bb6ae748 --- /dev/null +++ b/submissions/z3gex-base.json @@ -0,0 +1,30 @@ +{ + "name": "z3siri-base", + "contributors": [ + "Nikolaj Bjørner et al." + ], + "contacts": ["Nikolaj Bjørner "], + "archive": { + "url": "https://zenodo.org/records/20393505/files/z3.zip?download=1" + }, + "website": "https://github.com/Z3Prover/z3", + "system_description": "https://link.springer.com/content/pdf/10.1007/978-3-540-78800-3_24.pdf", + "solver_type": "Standalone", + "command": ["./z3"], + "seed": "33", + "participations": [ + { + "tracks": ["SingleQuery"], + "divisions": [ + "Arith", + "Bitvec", + "QF_Bitvec", + "QF_LinearIntArith", + "QF_LinearRealArith", + "QF_NonLinearIntArith", + "QF_NonLinearRealArith", + "QF_Strings" + ] + } + ] +} \ No newline at end of file diff --git a/submissions/z3gex.json b/submissions/z3gex.json new file mode 100644 index 000000000..17a261dcb --- /dev/null +++ b/submissions/z3gex.json @@ -0,0 +1,30 @@ +{ + "name": "Z3-GEX", + "contributors": [ + "Shuming Shi", + "Wenbo Wei" + ], + "contacts": ["Wenbo Wei "], + "archive": { + "url": "https://zenodo.org/records/20393652/files/z3gex.zip?download=1" + }, + "website": "http://example.com/", + "system_description": "http://example.com/system.pdf", + "command": ["z3gex"], + "solver_type": "derived", + "seed": "42", + "participations": [ + { + "tracks": ["SingleQuery"], + "divisions": [ + "Arith", + "QF_Bitvec", + "QF_LinearIntArith", + "QF_LinearRealArith", + "QF_NonLinearIntArith", + "QF_NonLinearRealArith", + "QF_Strings" + ] + } + ] +} From 09783f2b39bf9c01305b0c267ffb6726442bdb74 Mon Sep 17 00:00:00 2001 From: bluerar <2351320068@qq.com> Date: Tue, 26 May 2026 14:02:02 +0000 Subject: [PATCH 02/13] modified: submissions/z3gex.json --- submissions/z3gex.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/submissions/z3gex.json b/submissions/z3gex.json index 17a261dcb..8606907a4 100644 --- a/submissions/z3gex.json +++ b/submissions/z3gex.json @@ -8,8 +8,8 @@ "archive": { "url": "https://zenodo.org/records/20393652/files/z3gex.zip?download=1" }, - "website": "http://example.com/", - "system_description": "http://example.com/system.pdf", + "website": "https://github.com/b1uerar/SMT", + "system_description": "https://github.com/b1uerar/SMT/blob/main/SMT.pdf", "command": ["z3gex"], "solver_type": "derived", "seed": "42", From 4de83ddaf6f59feef1eb26730bfe5a1663de4be2 Mon Sep 17 00:00:00 2001 From: bluerar <2351320068@qq.com> Date: Tue, 26 May 2026 14:04:52 +0000 Subject: [PATCH 03/13] modified: submissions/z3gex-base.json --- submissions/z3gex-base.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submissions/z3gex-base.json b/submissions/z3gex-base.json index 8bb6ae748..83bd40cb8 100644 --- a/submissions/z3gex-base.json +++ b/submissions/z3gex-base.json @@ -1,5 +1,5 @@ { - "name": "z3siri-base", + "name": "z3-GEX-base", "contributors": [ "Nikolaj Bjørner et al." ], From a776011fb7677d73eaa1dd12232f3691701b22fd Mon Sep 17 00:00:00 2001 From: bluerar <2351320068@qq.com> Date: Tue, 26 May 2026 14:10:27 +0000 Subject: [PATCH 04/13] modified: submissions/z3gex-base.json --- submissions/z3gex-base.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submissions/z3gex-base.json b/submissions/z3gex-base.json index 83bd40cb8..d8cc0163d 100644 --- a/submissions/z3gex-base.json +++ b/submissions/z3gex-base.json @@ -1,5 +1,5 @@ { - "name": "z3-GEX-base", + "name": "Z3-GEX-base", "contributors": [ "Nikolaj Bjørner et al." ], From 3e1ffbe081561fad2f42103f3af790a863cf38e6 Mon Sep 17 00:00:00 2001 From: bluerar <2351320068@qq.com> Date: Tue, 26 May 2026 14:27:17 +0000 Subject: [PATCH 05/13] modified: submissions/z3gex.json --- submissions/z3gex.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/submissions/z3gex.json b/submissions/z3gex.json index 8606907a4..119e1861b 100644 --- a/submissions/z3gex.json +++ b/submissions/z3gex.json @@ -8,8 +8,8 @@ "archive": { "url": "https://zenodo.org/records/20393652/files/z3gex.zip?download=1" }, - "website": "https://github.com/b1uerar/SMT", - "system_description": "https://github.com/b1uerar/SMT/blob/main/SMT.pdf", + "website": "https://github.com/moyvbai/smt-comp2026", + "system_description": "https://github.com/moyvbai/smt-comp2026/blob/main/SMT.pdf", "command": ["z3gex"], "solver_type": "derived", "seed": "42", From 0c19a236f833a5f05da9b314bd6bfa900df1f7b2 Mon Sep 17 00:00:00 2001 From: bluerar <2351320068@qq.com> Date: Tue, 26 May 2026 14:41:09 +0000 Subject: [PATCH 06/13] modified: submissions/z3gex-base.json --- submissions/z3gex-base.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submissions/z3gex-base.json b/submissions/z3gex-base.json index d8cc0163d..15459734e 100644 --- a/submissions/z3gex-base.json +++ b/submissions/z3gex-base.json @@ -5,7 +5,7 @@ ], "contacts": ["Nikolaj Bjørner "], "archive": { - "url": "https://zenodo.org/records/20393505/files/z3.zip?download=1" + "url": "https://zenodo.org/records/20397251/files/Z3_base.zip?download=1" }, "website": "https://github.com/Z3Prover/z3", "system_description": "https://link.springer.com/content/pdf/10.1007/978-3-540-78800-3_24.pdf", From 0d38a8523543c110b31d512235fd42533f15c8bf Mon Sep 17 00:00:00 2001 From: bluerar <2351320068@qq.com> Date: Tue, 26 May 2026 14:46:13 +0000 Subject: [PATCH 07/13] modified: submissions/z3gex.json --- submissions/z3gex.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submissions/z3gex.json b/submissions/z3gex.json index 119e1861b..36d1e14b0 100644 --- a/submissions/z3gex.json +++ b/submissions/z3gex.json @@ -6,7 +6,7 @@ ], "contacts": ["Wenbo Wei "], "archive": { - "url": "https://zenodo.org/records/20393652/files/z3gex.zip?download=1" + "url": "https://zenodo.org/records/20397315/files/Z3_GEX.zip?download=1" }, "website": "https://github.com/moyvbai/smt-comp2026", "system_description": "https://github.com/moyvbai/smt-comp2026/blob/main/SMT.pdf", From 3616d898128d691dcf70a47eb0d4306fb048b1f0 Mon Sep 17 00:00:00 2001 From: bluerar <2351320068@qq.com> Date: Tue, 9 Jun 2026 18:08:34 +0000 Subject: [PATCH 08/13] update format of z3gex and update z3 version to 4.15.0 --- submissions/z3gex-base.json | 16 +++++++++++----- submissions/z3gex.json | 18 ++++++++++++------ 2 files changed, 23 insertions(+), 11 deletions(-) diff --git a/submissions/z3gex-base.json b/submissions/z3gex-base.json index 15459734e..9279edcd7 100644 --- a/submissions/z3gex-base.json +++ b/submissions/z3gex-base.json @@ -3,18 +3,24 @@ "contributors": [ "Nikolaj Bjørner et al." ], - "contacts": ["Nikolaj Bjørner "], + "contacts": [ + "Nikolaj Bjørner " + ], "archive": { - "url": "https://zenodo.org/records/20397251/files/Z3_base.zip?download=1" + "url": "https://zenodo.org/records/20615910/files/Z3_base.zip?download=1" }, "website": "https://github.com/Z3Prover/z3", "system_description": "https://link.springer.com/content/pdf/10.1007/978-3-540-78800-3_24.pdf", "solver_type": "Standalone", - "command": ["./z3"], + "command": [ + "./z3" + ], "seed": "33", "participations": [ - { - "tracks": ["SingleQuery"], + { + "tracks": [ + "SingleQuery" + ], "divisions": [ "Arith", "Bitvec", diff --git a/submissions/z3gex.json b/submissions/z3gex.json index 36d1e14b0..a0a8cd84f 100644 --- a/submissions/z3gex.json +++ b/submissions/z3gex.json @@ -4,18 +4,24 @@ "Shuming Shi", "Wenbo Wei" ], - "contacts": ["Wenbo Wei "], + "contacts": [ + "Wenbo Wei " + ], "archive": { - "url": "https://zenodo.org/records/20397315/files/Z3_GEX.zip?download=1" + "url": "https://zenodo.org/records/20616042/files/Z3_GEX.zip?download=1" }, "website": "https://github.com/moyvbai/smt-comp2026", "system_description": "https://github.com/moyvbai/smt-comp2026/blob/main/SMT.pdf", - "command": ["z3gex"], + "command": [ + "z3gex" + ], "solver_type": "derived", "seed": "42", "participations": [ - { - "tracks": ["SingleQuery"], + { + "tracks": [ + "SingleQuery" + ], "divisions": [ "Arith", "QF_Bitvec", @@ -27,4 +33,4 @@ ] } ] -} +} \ No newline at end of file From d30bcac3aa4eec43110414aa4cf6e2ac55ada6f7 Mon Sep 17 00:00:00 2001 From: bluerar <2351320068@qq.com> Date: Wed, 10 Jun 2026 10:37:36 +0000 Subject: [PATCH 09/13] update z3gex --- submissions/z3gex.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submissions/z3gex.json b/submissions/z3gex.json index a0a8cd84f..49a55a8b5 100644 --- a/submissions/z3gex.json +++ b/submissions/z3gex.json @@ -8,7 +8,7 @@ "Wenbo Wei " ], "archive": { - "url": "https://zenodo.org/records/20616042/files/Z3_GEX.zip?download=1" + "url": "https://zenodo.org/records/20625497/files/Z3_GEX.zip?download=1" }, "website": "https://github.com/moyvbai/smt-comp2026", "system_description": "https://github.com/moyvbai/smt-comp2026/blob/main/SMT.pdf", From 5d719f3814f5b2ab4a709431c3b7f2029a04f5ee Mon Sep 17 00:00:00 2001 From: bluerar <2351320068@qq.com> Date: Wed, 10 Jun 2026 13:03:50 +0000 Subject: [PATCH 10/13] correct base divisions --- submissions/z3gex-base.json | 1 - 1 file changed, 1 deletion(-) diff --git a/submissions/z3gex-base.json b/submissions/z3gex-base.json index 9279edcd7..4a3563f82 100644 --- a/submissions/z3gex-base.json +++ b/submissions/z3gex-base.json @@ -23,7 +23,6 @@ ], "divisions": [ "Arith", - "Bitvec", "QF_Bitvec", "QF_LinearIntArith", "QF_LinearRealArith", From f9ad31e1b4c7fd07ad6baa8411dafd710c6ced1e Mon Sep 17 00:00:00 2001 From: bluerar <2351320068@qq.com> Date: Wed, 10 Jun 2026 17:49:37 +0000 Subject: [PATCH 11/13] update contributors --- submissions/z3gex.json | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/submissions/z3gex.json b/submissions/z3gex.json index 49a55a8b5..0fd3b04fa 100644 --- a/submissions/z3gex.json +++ b/submissions/z3gex.json @@ -2,7 +2,9 @@ "name": "Z3-GEX", "contributors": [ "Shuming Shi", - "Wenbo Wei" + "Wenbo Wei", + "Zhengfeng Yang", + "Jianlin Wang" ], "contacts": [ "Wenbo Wei " From 09f0d2ec03c39bc1089e40de56bddfa82915fbc6 Mon Sep 17 00:00:00 2001 From: bluerar <2351320068@qq.com> Date: Thu, 11 Jun 2026 11:35:11 +0000 Subject: [PATCH 12/13] final version --- submissions/z3gex-base.json | 3 ++- submissions/z3gex.json | 5 +++-- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/submissions/z3gex-base.json b/submissions/z3gex-base.json index 4a3563f82..0e772c89e 100644 --- a/submissions/z3gex-base.json +++ b/submissions/z3gex-base.json @@ -31,5 +31,6 @@ "QF_Strings" ] } - ] + ], + "final" : true } \ No newline at end of file diff --git a/submissions/z3gex.json b/submissions/z3gex.json index 0fd3b04fa..5f278b73a 100644 --- a/submissions/z3gex.json +++ b/submissions/z3gex.json @@ -10,7 +10,7 @@ "Wenbo Wei " ], "archive": { - "url": "https://zenodo.org/records/20625497/files/Z3_GEX.zip?download=1" + "url": "https://zenodo.org/records/20642639/files/Z3_GEX.zip?download=1" }, "website": "https://github.com/moyvbai/smt-comp2026", "system_description": "https://github.com/moyvbai/smt-comp2026/blob/main/SMT.pdf", @@ -34,5 +34,6 @@ "QF_Strings" ] } - ] + ], + "final": true } \ No newline at end of file From dbbc6c9170a50699348eed9c0939c6435f5858ce Mon Sep 17 00:00:00 2001 From: bluerar <2351320068@qq.com> Date: Fri, 12 Jun 2026 09:33:09 +0000 Subject: [PATCH 13/13] add ("competitive": false) for z3gex_base --- submissions/z3gex-base.json | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/submissions/z3gex-base.json b/submissions/z3gex-base.json index 0e772c89e..42cdc9839 100644 --- a/submissions/z3gex-base.json +++ b/submissions/z3gex-base.json @@ -32,5 +32,6 @@ ] } ], - "final" : true + "competitive": false, + "final": true } \ No newline at end of file