From b93bed9008e0eb23f62c529a5e4f68c6b139096f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hans-J=C3=B6rg?= Date: Fri, 13 Jun 2025 16:01:24 -0500 Subject: [PATCH 1/3] cvc5 for SMT-COMP 2025 --- submissions/cvc5.json | 62 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) create mode 100644 submissions/cvc5.json diff --git a/submissions/cvc5.json b/submissions/cvc5.json new file mode 100644 index 00000000..9772e300 --- /dev/null +++ b/submissions/cvc5.json @@ -0,0 +1,62 @@ +{ + "name": "cvc5", + "contributors": [ + "Haniel Barbosa", + "Clark Barrett", + "Hanna Lachnitt", + "Daniel Larraz", + "Abdalrhman Mohamed", + "Mudathir Mohamed", + "José Neto", + "Aina Niemetz", + "Alex Ozdemir", + "Mathias Preiner", + "Andrew Reynolds", + "Hans-Jörg Schurr", + "Cesare Tinelli", + "Amalee Wilson", + "Yoni Zohar" + ], + "contacts": [ + "Hans-Jörg Schurr ", + "Daniel Larraz ", + "Clark Barrett " + ], + "archive": { + "url": "https://homepage.cs.uiowa.edu/~hschrr/smtcomp2025/cvc5-default.zip", + "h": { + "sha256": "736c9e6cf74c5767a4061ba57ea88020202a5aa8018c473a9603bcf3a0368ff2" + } + }, + "website": "https://cvc5.github.io/", + "system_description": "https://homepage.cs.uiowa.edu/~hschrr/smtcomp2025/cvc5.pdf", + "command": [ "bin/starexec_run_sq" ], + "solver_type": "Standalone", + "participations": [ + { + "tracks": [ "SingleQuery" ], + "logics": ".*" + }, + { + "tracks": [ "UnsatCore" ], + "logics": ".*", + "command": [ "bin/starexec_run_uc" ] + }, + { + "tracks": [ "ModelValidation" ], + "logics": ".*", + "command": [ "bin/starexec_run_mv" ] + }, + { + "tracks": [ "Incremental" ], + "logics": ".*", + "archive": { + "url": "https://homepage.cs.uiowa.edu/~hschrr/smtcomp2025/cvc5-inc.zip", + "h": { + "sha256": "19285b411762267ab5270d8b4d103c0bca02816c43016e6ab971d80017ca6dec" + } + }, + "command": [ "bin/smtcomp_run_incremental" ] + } + ] +} From 025abe9f17047ae8b5915e01d9868aded7e657ca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hans-J=C3=B6rg?= Date: Fri, 13 Jun 2025 16:10:36 -0500 Subject: [PATCH 2/3] Add seed --- submissions/cvc5.json | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/submissions/cvc5.json b/submissions/cvc5.json index 9772e300..c3e6e559 100644 --- a/submissions/cvc5.json +++ b/submissions/cvc5.json @@ -58,5 +58,6 @@ }, "command": [ "bin/smtcomp_run_incremental" ] } - ] + ], +"seed": 8465677983 } From c2ac16e2bf227d3bf5b11ea8db6b8abaa1289579 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hans-J=C3=B6rg?= Date: Fri, 27 Jun 2025 21:07:15 -0500 Subject: [PATCH 3/3] Link to Zenodo files --- submissions/cvc5.json | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/submissions/cvc5.json b/submissions/cvc5.json index c3e6e559..bb3f1719 100644 --- a/submissions/cvc5.json +++ b/submissions/cvc5.json @@ -23,13 +23,13 @@ "Clark Barrett " ], "archive": { - "url": "https://homepage.cs.uiowa.edu/~hschrr/smtcomp2025/cvc5-default.zip", + "url": "https://zenodo.org/records/15760304/files/cvc5-default.zip", "h": { - "sha256": "736c9e6cf74c5767a4061ba57ea88020202a5aa8018c473a9603bcf3a0368ff2" + "sha256": "627082d4c9b70d74787fbb8f78214fd4bc20924de1be294f658df4ea2e20c63f" } }, "website": "https://cvc5.github.io/", - "system_description": "https://homepage.cs.uiowa.edu/~hschrr/smtcomp2025/cvc5.pdf", + "system_description": "https://zenodo.org/records/15760304/files/cvc5.pdf", "command": [ "bin/starexec_run_sq" ], "solver_type": "Standalone", "participations": [ @@ -51,9 +51,9 @@ "tracks": [ "Incremental" ], "logics": ".*", "archive": { - "url": "https://homepage.cs.uiowa.edu/~hschrr/smtcomp2025/cvc5-inc.zip", + "url": "https://zenodo.org/records/15760304/files/cvc5-inc.zip", "h": { - "sha256": "19285b411762267ab5270d8b4d103c0bca02816c43016e6ab971d80017ca6dec" + "sha256": "e5c29e6ae5a6193e06812f62c7eeb574f64939dd3ff61f08ae2ac87e6296fc48" } }, "command": [ "bin/smtcomp_run_incremental" ]