From fd2c4a764c7c5b73f642b125cc550175ac78d02d Mon Sep 17 00:00:00 2001 From: John Lu Date: Tue, 26 May 2026 22:37:18 -0400 Subject: [PATCH 01/11] z3-alpha2 smtcomp26 first version submission json --- submissions/z3-alpha2.json | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 submissions/z3-alpha2.json diff --git a/submissions/z3-alpha2.json b/submissions/z3-alpha2.json new file mode 100644 index 000000000..92e4c82af --- /dev/null +++ b/submissions/z3-alpha2.json @@ -0,0 +1,35 @@ +{ + "name": "Z3-alpha2", + "contributors": [ + "John Lu", + "Avik Kumar", + "Piyush Jha", + "Arie Gurfinkel", + "Vijay Ganesh" + ], + "contacts": ["John Lu "], + "archive": { + "url": "https://drive.google.com/uc?id=1jSlGFgb93Odbqa1mTolKqPWnwsy-Y6r0&export=download", + "h": { "sha256": "a3b04a21c61d527b74f4e69d52e825bd0fc08abbf86d21bb0fa95db264153fe3" } + }, + "website": "https://github.com/JohnLyu2/z3alpha", + "system_description": "https://drive.google.com/uc?id=18yWr0duq3X2l0_ZfvAsr5otPMAH1GtD9&export=download", + "solver_type": "derived", + "command": ["./z3alpha2.py"], + "seed": "33", + "participations": [ + { + "tracks": ["SingleQuery"], + "divisions": [ + "Arith", + "QF_Bitvec", + "QF_Datatypes", + "QF_LinearIntArith", + "QF_LinearRealArith", + "QF_NonLinearIntArith", + "QF_NonLinearRealArith" + ] + } + ], + "final" : false +} From 219c2a611bf6bf8f63ec21b31d3f174d5485f8ff Mon Sep 17 00:00:00 2001 From: John Lu Date: Tue, 26 May 2026 22:48:24 -0400 Subject: [PATCH 02/11] replace archive as a .tar.gz --- submissions/z3-alpha2.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/submissions/z3-alpha2.json b/submissions/z3-alpha2.json index 92e4c82af..0ce03c809 100644 --- a/submissions/z3-alpha2.json +++ b/submissions/z3-alpha2.json @@ -9,8 +9,8 @@ ], "contacts": ["John Lu "], "archive": { - "url": "https://drive.google.com/uc?id=1jSlGFgb93Odbqa1mTolKqPWnwsy-Y6r0&export=download", - "h": { "sha256": "a3b04a21c61d527b74f4e69d52e825bd0fc08abbf86d21bb0fa95db264153fe3" } + "url": "https://drive.google.com/uc?export=download&id=1Mk6iz1DFvEDf2F8Zzplg4VQZ6M7dkNwJ", + "h": { "sha256": "46e4da57c65e9007ff1d241ff1f6970fbf871ca6515aaec3a4170f4658b994bb" } }, "website": "https://github.com/JohnLyu2/z3alpha", "system_description": "https://drive.google.com/uc?id=18yWr0duq3X2l0_ZfvAsr5otPMAH1GtD9&export=download", From bb2dd4e34dfee62c398e9ca92c24cc3ed4fb5f52 Mon Sep 17 00:00:00 2001 From: John Lu Date: Tue, 26 May 2026 23:05:40 -0400 Subject: [PATCH 03/11] change archive url to github release --- submissions/z3-alpha2.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submissions/z3-alpha2.json b/submissions/z3-alpha2.json index 0ce03c809..d44f7bac8 100644 --- a/submissions/z3-alpha2.json +++ b/submissions/z3-alpha2.json @@ -9,7 +9,7 @@ ], "contacts": ["John Lu "], "archive": { - "url": "https://drive.google.com/uc?export=download&id=1Mk6iz1DFvEDf2F8Zzplg4VQZ6M7dkNwJ", + "url": "https://github.com/JohnLyu2/z3alpha/releases/download/z3alpha2-smtcomp26-1st/z3alpha2_smtcomp26.tar.gz", "h": { "sha256": "46e4da57c65e9007ff1d241ff1f6970fbf871ca6515aaec3a4170f4658b994bb" } }, "website": "https://github.com/JohnLyu2/z3alpha", From 38276a5cb0a50d59db56f25b585da6e223dbe103 Mon Sep 17 00:00:00 2001 From: John Lu Date: Mon, 8 Jun 2026 09:26:52 -0400 Subject: [PATCH 04/11] modify z3alpha2 participations --- submissions/z3-alpha2.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submissions/z3-alpha2.json b/submissions/z3-alpha2.json index d44f7bac8..165c07d2f 100644 --- a/submissions/z3-alpha2.json +++ b/submissions/z3-alpha2.json @@ -25,7 +25,7 @@ "QF_Bitvec", "QF_Datatypes", "QF_LinearIntArith", - "QF_LinearRealArith", + "QF_Equality+NonLinearArith", "QF_NonLinearIntArith", "QF_NonLinearRealArith" ] From 283ba6820e239fd627f0dbbbe0a3af619527c35d Mon Sep 17 00:00:00 2001 From: John Lu Date: Mon, 8 Jun 2026 10:03:35 -0400 Subject: [PATCH 05/11] base solver submission --- submissions/z3-alpha2-base.json | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 submissions/z3-alpha2-base.json diff --git a/submissions/z3-alpha2-base.json b/submissions/z3-alpha2-base.json new file mode 100644 index 000000000..a8a0fdfb8 --- /dev/null +++ b/submissions/z3-alpha2-base.json @@ -0,0 +1,31 @@ +{ + "name": "Z3-alpha2-base", + "contributors": [ + "Nikolaj Bjørner et al." + ], + "contacts": ["Nikolaj Bjørner "], + "archive": { + "url": "https://zenodo.org/records/20595207/files/z3-4.16.0.tar.gz?download=1" + }, + "website": "https://github.com/z3prover/z3", + "system_description": "https://link.springer.com/chapter/10.1007/978-3-540-78800-3_24", + "solver_type": "Standalone", + "command": ["./z3"], + "seed": "33", + "participations": [ + { + "tracks": ["SingleQuery"], + "divisions": [ + "Arith", + "QF_Bitvec", + "QF_Datatypes", + "QF_LinearIntArith", + "QF_Equality+NonLinearArith", + "QF_NonLinearIntArith", + "QF_NonLinearRealArith" + ] + } + ], + "competitive": false, + "final" : true +} From 7b13c81d8569244ee6f336aa406b50aae08e39d8 Mon Sep 17 00:00:00 2001 From: John Lu Date: Mon, 8 Jun 2026 15:18:19 -0400 Subject: [PATCH 06/11] 2nd version of description --- submissions/z3-alpha2.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submissions/z3-alpha2.json b/submissions/z3-alpha2.json index 165c07d2f..ae6e9db97 100644 --- a/submissions/z3-alpha2.json +++ b/submissions/z3-alpha2.json @@ -13,7 +13,7 @@ "h": { "sha256": "46e4da57c65e9007ff1d241ff1f6970fbf871ca6515aaec3a4170f4658b994bb" } }, "website": "https://github.com/JohnLyu2/z3alpha", - "system_description": "https://drive.google.com/uc?id=18yWr0duq3X2l0_ZfvAsr5otPMAH1GtD9&export=download", + "system_description": "https://drive.google.com/uc?export=download&id=1Fy4tiFo65ADRk7H2Dc_ykGR2i7ksXxkQ", "solver_type": "derived", "command": ["./z3alpha2.py"], "seed": "33", From 408b426d5438bad8713be4685931155ccae7fa43 Mon Sep 17 00:00:00 2001 From: John Lu Date: Tue, 9 Jun 2026 13:48:34 -0400 Subject: [PATCH 07/11] update artifact to version 2 --- submissions/z3-alpha2.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submissions/z3-alpha2.json b/submissions/z3-alpha2.json index ae6e9db97..29289a5b9 100644 --- a/submissions/z3-alpha2.json +++ b/submissions/z3-alpha2.json @@ -10,7 +10,7 @@ "contacts": ["John Lu "], "archive": { "url": "https://github.com/JohnLyu2/z3alpha/releases/download/z3alpha2-smtcomp26-1st/z3alpha2_smtcomp26.tar.gz", - "h": { "sha256": "46e4da57c65e9007ff1d241ff1f6970fbf871ca6515aaec3a4170f4658b994bb" } + "h": { "sha256": "9d1341cffd9a847d817306e85aa374d7c75d9b60b03b8f23af58ab096f2ef819" } }, "website": "https://github.com/JohnLyu2/z3alpha", "system_description": "https://drive.google.com/uc?export=download&id=1Fy4tiFo65ADRk7H2Dc_ykGR2i7ksXxkQ", From cccf6390468cdb5c3bc50efb04d7394e9e80bc98 Mon Sep 17 00:00:00 2001 From: John Lu Date: Thu, 11 Jun 2026 00:02:10 -0400 Subject: [PATCH 08/11] update the Zenodo final version --- submissions/z3-alpha2.json | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/submissions/z3-alpha2.json b/submissions/z3-alpha2.json index 29289a5b9..37b69c676 100644 --- a/submissions/z3-alpha2.json +++ b/submissions/z3-alpha2.json @@ -9,8 +9,7 @@ ], "contacts": ["John Lu "], "archive": { - "url": "https://github.com/JohnLyu2/z3alpha/releases/download/z3alpha2-smtcomp26-1st/z3alpha2_smtcomp26.tar.gz", - "h": { "sha256": "9d1341cffd9a847d817306e85aa374d7c75d9b60b03b8f23af58ab096f2ef819" } + "url": "https://zenodo.org/records/20636095/files/z3alpha2_smtcomp26.tar.gz?download=1" }, "website": "https://github.com/JohnLyu2/z3alpha", "system_description": "https://drive.google.com/uc?export=download&id=1Fy4tiFo65ADRk7H2Dc_ykGR2i7ksXxkQ", @@ -31,5 +30,5 @@ ] } ], - "final" : false + "final" : true } From 73851211762166cb50435e1f3e33a65880f0b793 Mon Sep 17 00:00:00 2001 From: John Lu Date: Thu, 11 Jun 2026 12:37:31 -0400 Subject: [PATCH 09/11] a debugger version for CI test --- submissions/z3-alpha2-debug.json | 36 ++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 submissions/z3-alpha2-debug.json diff --git a/submissions/z3-alpha2-debug.json b/submissions/z3-alpha2-debug.json new file mode 100644 index 000000000..65a036a9d --- /dev/null +++ b/submissions/z3-alpha2-debug.json @@ -0,0 +1,36 @@ +{ + "name": "Z3-alpha2", + "contributors": [ + "John Lu", + "Avik Kumar", + "Piyush Jha", + "Arie Gurfinkel", + "Vijay Ganesh" + ], + "contacts": ["John Lu "], + "archive": { + "url": "https://github.com/JohnLyu2/z3alpha/releases/download/z3alpha2-smtcomp26-1st/z3alpha2_smtcomp26.tar.gz", + "sha256": "91b0036aac233c8b35f3cb05aa5e833d26e8fd584cec97f6010f8027306d14ab" + }, + "website": "https://github.com/JohnLyu2/z3alpha", + "system_description": "https://drive.google.com/uc?export=download&id=1Fy4tiFo65ADRk7H2Dc_ykGR2i7ksXxkQ", + "solver_type": "derived", + "command": ["./z3alpha2_debug.py"], + "seed": "33", + "participations": [ + { + "tracks": ["SingleQuery"], + "divisions": [ + "Arith", + "QF_Bitvec", + "QF_Datatypes", + "QF_LinearIntArith", + "QF_Equality+NonLinearArith", + "QF_NonLinearIntArith", + "QF_NonLinearRealArith" + ] + } + ], + "competitive": false, + "final" : false +} From 88b3ab49192bfbd1e0faee068bc4f71406a343a2 Mon Sep 17 00:00:00 2001 From: John Lu Date: Thu, 11 Jun 2026 14:42:23 -0400 Subject: [PATCH 10/11] mute stderr when no error --- submissions/z3-alpha2-debug.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submissions/z3-alpha2-debug.json b/submissions/z3-alpha2-debug.json index 65a036a9d..c7db4a635 100644 --- a/submissions/z3-alpha2-debug.json +++ b/submissions/z3-alpha2-debug.json @@ -10,7 +10,7 @@ "contacts": ["John Lu "], "archive": { "url": "https://github.com/JohnLyu2/z3alpha/releases/download/z3alpha2-smtcomp26-1st/z3alpha2_smtcomp26.tar.gz", - "sha256": "91b0036aac233c8b35f3cb05aa5e833d26e8fd584cec97f6010f8027306d14ab" + "sha256": "87bcd6b9a0b7ee864b63fe906840716f2cfbcfc83bdab31a8708f3b9d98bae5d" }, "website": "https://github.com/JohnLyu2/z3alpha", "system_description": "https://drive.google.com/uc?export=download&id=1Fy4tiFo65ADRk7H2Dc_ykGR2i7ksXxkQ", From b842fcb35ece91dafd1437bb9a0673f8b43a1ed2 Mon Sep 17 00:00:00 2001 From: John Lu Date: Thu, 11 Jun 2026 14:48:11 -0400 Subject: [PATCH 11/11] rename debugger version --- submissions/z3-alpha2-debug.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submissions/z3-alpha2-debug.json b/submissions/z3-alpha2-debug.json index c7db4a635..f19065beb 100644 --- a/submissions/z3-alpha2-debug.json +++ b/submissions/z3-alpha2-debug.json @@ -1,5 +1,5 @@ { - "name": "Z3-alpha2", + "name": "Z3-alpha2-debug", "contributors": [ "John Lu", "Avik Kumar",