From 0e744f5bac943ef7b3bae83eb055ca6fba176b63 Mon Sep 17 00:00:00 2001 From: Xiang Zhang <101581443+Andeviking@users.noreply.github.com> Date: Thu, 28 May 2026 01:16:19 +0800 Subject: [PATCH 1/5] Bitwuzla-MachBV Submission for SMT-COMP 2026 --- .../Bitwuzla-MachBV-at-SMT-COMP-2026.json | 35 +++++++++++++++++++ ...Bitwuzla-MachBV-base-at-SMT-COMP-2026.json | 32 +++++++++++++++++ 2 files changed, 67 insertions(+) create mode 100644 submissions/Bitwuzla-MachBV-at-SMT-COMP-2026.json create mode 100644 submissions/Bitwuzla-MachBV-base-at-SMT-COMP-2026.json diff --git a/submissions/Bitwuzla-MachBV-at-SMT-COMP-2026.json b/submissions/Bitwuzla-MachBV-at-SMT-COMP-2026.json new file mode 100644 index 000000000..dfc5c878a --- /dev/null +++ b/submissions/Bitwuzla-MachBV-at-SMT-COMP-2026.json @@ -0,0 +1,35 @@ +{ + "name": "Bitwuzla-MachBV", + "contributors": [ + "Xiang Zhang", + "Shaohuang Chen", + "Mengyu Zhao", + "Shaowei Cai" + ], + "contacts": [ + "Xiang Zhang " + ], + "archive": { + "url": "https://zenodo.org/records/15752452/files/Bitwuzla-MachBV.zip", + "h": { + "sha256": "7267c86005f3c57bf22fccd8b6d868651be109a9231aeaa01a93d07843d14555" + } + }, + "website": "https://github.com/Andeviking/Bitwuzla-MachBV-at-SMT-COMP-2026", + "system_description": "https://github.com/Andeviking/Bitwuzla-MachBV-at-SMT-COMP-2026/blob/main/Bitwuzla_MachBV_at_SMT_COMP_2026.pdf", + "command": [ + "./MachBV" + ], + "solver_type": "derived", + "seed": "1126300213", + "participations": [ + { + "tracks": [ + "SingleQuery" + ], + "logics": [ + "QF_BV" + ] + } + ] +} \ No newline at end of file diff --git a/submissions/Bitwuzla-MachBV-base-at-SMT-COMP-2026.json b/submissions/Bitwuzla-MachBV-base-at-SMT-COMP-2026.json new file mode 100644 index 000000000..9758765e8 --- /dev/null +++ b/submissions/Bitwuzla-MachBV-base-at-SMT-COMP-2026.json @@ -0,0 +1,32 @@ +{ + "name": "Bitwuzla-MachBV-base", + "archive": { + "url": "https://zenodo.org/records/15752452/files/Bitwuzla-0-7-0.zip", + "h": { + "sha256": "a85ffea4009c096be3bf627c720fed903bbff1ae3655ac1bd169519ae4403c00" + } + }, + "contributors": [ + "Aina Niemetz", + "Mathias Preiner" + ], + "contacts": [ + "Mathias Preiner " + ], + "website": "https://github.com/bitwuzla/bitwuzla/tree/0.9.1", + "system_description": "https://link.springer.com/content/pdf/10.1007/978-3-031-37703-7_1", + "command": [ + "./bitwuzla" + ], + "solver_type": "Standalone", + "seed": 42, + "participations": [ + { + "tracks": [ + "SingleQuery" + ], + "logics": "QF_BV" + } + ], + "competitive": false +} \ No newline at end of file From 5ac82b8c2937468e4dd4cffb1e89709bfa427e27 Mon Sep 17 00:00:00 2001 From: Xiang Zhang <101581443+Andeviking@users.noreply.github.com> Date: Tue, 9 Jun 2026 20:07:33 +0800 Subject: [PATCH 2/5] Update archive URL and command in JSON file --- submissions/Bitwuzla-MachBV-at-SMT-COMP-2026.json | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/submissions/Bitwuzla-MachBV-at-SMT-COMP-2026.json b/submissions/Bitwuzla-MachBV-at-SMT-COMP-2026.json index dfc5c878a..51a579244 100644 --- a/submissions/Bitwuzla-MachBV-at-SMT-COMP-2026.json +++ b/submissions/Bitwuzla-MachBV-at-SMT-COMP-2026.json @@ -10,15 +10,15 @@ "Xiang Zhang " ], "archive": { - "url": "https://zenodo.org/records/15752452/files/Bitwuzla-MachBV.zip", + "url": "https://zenodo.org/records/20610415/files/Bitwuzla-MachBV.zip", "h": { - "sha256": "7267c86005f3c57bf22fccd8b6d868651be109a9231aeaa01a93d07843d14555" + "sha256": "8760165be6d79806e3ae17567e12702366de738eff7dc7dd20ec8d99c12684b5" } }, "website": "https://github.com/Andeviking/Bitwuzla-MachBV-at-SMT-COMP-2026", "system_description": "https://github.com/Andeviking/Bitwuzla-MachBV-at-SMT-COMP-2026/blob/main/Bitwuzla_MachBV_at_SMT_COMP_2026.pdf", "command": [ - "./MachBV" + "./bin/SMTStabilizer" ], "solver_type": "derived", "seed": "1126300213", @@ -32,4 +32,4 @@ ] } ] -} \ No newline at end of file +} From af31a6da603245605185b1b2675b737c0f212aa1 Mon Sep 17 00:00:00 2001 From: Xiang Zhang <101581443+Andeviking@users.noreply.github.com> Date: Tue, 9 Jun 2026 20:07:57 +0800 Subject: [PATCH 3/5] Update archive URL and SHA256 hash in JSON --- submissions/Bitwuzla-MachBV-base-at-SMT-COMP-2026.json | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/submissions/Bitwuzla-MachBV-base-at-SMT-COMP-2026.json b/submissions/Bitwuzla-MachBV-base-at-SMT-COMP-2026.json index 9758765e8..585cb7b65 100644 --- a/submissions/Bitwuzla-MachBV-base-at-SMT-COMP-2026.json +++ b/submissions/Bitwuzla-MachBV-base-at-SMT-COMP-2026.json @@ -1,9 +1,9 @@ { "name": "Bitwuzla-MachBV-base", "archive": { - "url": "https://zenodo.org/records/15752452/files/Bitwuzla-0-7-0.zip", + "url": "https://zenodo.org/records/20610415/files/Bitwuzla.zip", "h": { - "sha256": "a85ffea4009c096be3bf627c720fed903bbff1ae3655ac1bd169519ae4403c00" + "sha256": "2271688b0f6ffe3d18efb763bd48dda0a5cce8dbbc07ef1be7a9cb5636ebf70f" } }, "contributors": [ @@ -29,4 +29,4 @@ } ], "competitive": false -} \ No newline at end of file +} From 3dcfbaf2f9711fc832e2f5d3b825b578e325e841 Mon Sep 17 00:00:00 2001 From: Xiang Zhang <101581443+Andeviking@users.noreply.github.com> Date: Thu, 11 Jun 2026 18:45:00 +0800 Subject: [PATCH 4/5] Add 'final' field to submission JSON --- submissions/Bitwuzla-MachBV-at-SMT-COMP-2026.json | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/submissions/Bitwuzla-MachBV-at-SMT-COMP-2026.json b/submissions/Bitwuzla-MachBV-at-SMT-COMP-2026.json index 51a579244..0f40ffcf6 100644 --- a/submissions/Bitwuzla-MachBV-at-SMT-COMP-2026.json +++ b/submissions/Bitwuzla-MachBV-at-SMT-COMP-2026.json @@ -31,5 +31,6 @@ "QF_BV" ] } - ] + ], + "final": true } From 71f3a3d891568f43630774f42f9ede7fd3b19313 Mon Sep 17 00:00:00 2001 From: Xiang Zhang <101581443+Andeviking@users.noreply.github.com> Date: Thu, 11 Jun 2026 18:46:09 +0800 Subject: [PATCH 5/5] Add 'final' field to Bitwuzla submission JSON --- submissions/Bitwuzla-MachBV-base-at-SMT-COMP-2026.json | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/submissions/Bitwuzla-MachBV-base-at-SMT-COMP-2026.json b/submissions/Bitwuzla-MachBV-base-at-SMT-COMP-2026.json index 585cb7b65..e56ed4121 100644 --- a/submissions/Bitwuzla-MachBV-base-at-SMT-COMP-2026.json +++ b/submissions/Bitwuzla-MachBV-base-at-SMT-COMP-2026.json @@ -28,5 +28,6 @@ "logics": "QF_BV" } ], - "competitive": false + "competitive": false, + "final": true }