From 79efed8c707216d71b6e20b968dce710c199223c Mon Sep 17 00:00:00 2001 From: Hans-Joerg Schurr Date: Mon, 27 May 2024 14:42:42 -0500 Subject: [PATCH 1/5] Add cvc5 preliminary version --- submissions/cvc5.json | 70 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 70 insertions(+) create mode 100644 submissions/cvc5.json diff --git a/submissions/cvc5.json b/submissions/cvc5.json new file mode 100644 index 00000000..593c0375 --- /dev/null +++ b/submissions/cvc5.json @@ -0,0 +1,70 @@ +{ + "name": "cvc5", + "contributors": [ + "Leni Aniva", + "Haniel Barbosa", + "Clark Barrett", + "Hanna Lachnitt", + "Daniel Larraz", + "Abdalrhman Mohamed", + "Mudathir Mohamed", + "Aina Niemetz", + "Alex Ozdemir", + "Mathias Preiner", + "Andrew Reynolds", + "Hans-Jörg Schurr", + "Cesare Tinelli", + "Amalee Wilson", + "Yoni Zohar" + ], + "contacts": [ + "Hans-Jörg Schurr ", + "Amalee Wilson ", + "Clark Barrett " + ], + "archive": { + "url": "https://homepage.divms.uiowa.edu/~hschrr/smtcomp2024/cvc5-default.zip", + "h": { + "sha256": "4e8b6f6aaa8a22afec427633e66d1880f9f106efca4aa35d143cd97f90f2b3bb" + } + }, + "website": "https://cvc5.github.io/", + "system_description": "https://homepage.divms.uiowa.edu/~hschrr/smtcomp2024/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.divms.uiowa.edu/~hschrr/smtcomp2024/cvc5-inc.zip", + "h": { + "sha256": "25d7fb5461a5b4b96e75145d95700085db81f3b0f6c7af556b47a2aaf1fbcd96" + } + }, + "command": [ "bin/starexec_run_default" ] + }, + { + "tracks": [ "Cloud" ], + "logics": ".*" + }, + { + "tracks": [ "Parallel" ], + "logics": ".*" + } + ] +} From 8d3ba8a1ce67ef727dd75f67ae4867f2e81cab61 Mon Sep 17 00:00:00 2001 From: Hans-Joerg Schurr Date: Tue, 28 May 2024 10:49:27 -0500 Subject: [PATCH 2/5] Remove cvc5 from parallel track --- submissions/cvc5.json | 4 ---- 1 file changed, 4 deletions(-) diff --git a/submissions/cvc5.json b/submissions/cvc5.json index 593c0375..3c757e48 100644 --- a/submissions/cvc5.json +++ b/submissions/cvc5.json @@ -61,10 +61,6 @@ { "tracks": [ "Cloud" ], "logics": ".*" - }, - { - "tracks": [ "Parallel" ], - "logics": ".*" } ] } From 6f9e1ab34f0c24684fc08d703fd45adff75e60d9 Mon Sep 17 00:00:00 2001 From: Hans-Joerg Schurr Date: Fri, 31 May 2024 15:38:10 -0500 Subject: [PATCH 3/5] Fix command for incremental track --- submissions/cvc5.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submissions/cvc5.json b/submissions/cvc5.json index 3c757e48..e913ed09 100644 --- a/submissions/cvc5.json +++ b/submissions/cvc5.json @@ -56,7 +56,7 @@ "sha256": "25d7fb5461a5b4b96e75145d95700085db81f3b0f6c7af556b47a2aaf1fbcd96" } }, - "command": [ "bin/starexec_run_default" ] + "command": [ "bin/smtcomp_run_incremental" ] }, { "tracks": [ "Cloud" ], From 6f3be7e01cf4b6e3bd3fda1afc4d5bc92f0222ae Mon Sep 17 00:00:00 2001 From: Hans-Joerg Schurr Date: Wed, 5 Jun 2024 14:04:43 -0500 Subject: [PATCH 4/5] Remove cvc5 from the cloud track --- submissions/cvc5.json | 4 ---- 1 file changed, 4 deletions(-) diff --git a/submissions/cvc5.json b/submissions/cvc5.json index e913ed09..82d85b2d 100644 --- a/submissions/cvc5.json +++ b/submissions/cvc5.json @@ -57,10 +57,6 @@ } }, "command": [ "bin/smtcomp_run_incremental" ] - }, - { - "tracks": [ "Cloud" ], - "logics": ".*" } ] } From 269c1f8f67583e6ece61c3a1c147a03af01355e5 Mon Sep 17 00:00:00 2001 From: Hans-Joerg Schurr Date: Thu, 13 Jun 2024 18:48:37 -0500 Subject: [PATCH 5/5] Use Zenodo release --- submissions/cvc5.json | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/submissions/cvc5.json b/submissions/cvc5.json index 82d85b2d..576dfad3 100644 --- a/submissions/cvc5.json +++ b/submissions/cvc5.json @@ -23,13 +23,13 @@ "Clark Barrett " ], "archive": { - "url": "https://homepage.divms.uiowa.edu/~hschrr/smtcomp2024/cvc5-default.zip", + "url": "https://zenodo.org/records/11581520/files/cvc5-default.zip", "h": { "sha256": "4e8b6f6aaa8a22afec427633e66d1880f9f106efca4aa35d143cd97f90f2b3bb" } }, "website": "https://cvc5.github.io/", - "system_description": "https://homepage.divms.uiowa.edu/~hschrr/smtcomp2024/cvc5.pdf", + "system_description": "https://zenodo.org/records/11581520/files/cvc5.pdf", "command": [ "bin/starexec_run_sq" ], "solver_type": "Standalone", "participations": [ @@ -51,7 +51,7 @@ "tracks": [ "Incremental" ], "logics": ".*", "archive": { - "url": "https://homepage.divms.uiowa.edu/~hschrr/smtcomp2024/cvc5-inc.zip", + "url": "https://zenodo.org/records/11581520/files/cvc5-inc.zip", "h": { "sha256": "25d7fb5461a5b4b96e75145d95700085db81f3b0f6c7af556b47a2aaf1fbcd96" }