From 956b7aaf0aab0434d56f26a934f5f5bd8a10cc21 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Kol=C3=A1rik?= Date: Thu, 12 Jun 2025 11:09:09 +0200 Subject: [PATCH 1/4] SMTS submission 2026 --- submissions/smts.json | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 submissions/smts.json diff --git a/submissions/smts.json b/submissions/smts.json new file mode 100644 index 000000000..b8452b5cf --- /dev/null +++ b/submissions/smts.json @@ -0,0 +1,34 @@ +{ + "name": "SMTS", + "contributors": [ + { "name": "Tomáš Kolárik", "website": "https://github.com/Tomaqa" } + , + { "name": "Antti E. J. Hyvärinen", "website": "https://github.com/aehyvari" } + , + { "name": "Seyedmasoud Asadzadeh", "website": "https://masoudasadzade.github.io" } + ], + "contacts": [ + "Tomáš Kolárik " + ], + "archive": { + "url": "https://github.com/usi-verification-and-security/SMTS/archive/refs/tags/tacas26-artifact.tar.gz" + }, + "command": ["./SMTS-tacas26-artifact/server/smts.py", "-l", "-p", "-nt", "32", "-o", "128", "-fp"], + "website": "https://github.com/usi-verification-and-security/SMTS", + "system_description": "https://github.com/usi-verification-and-security/opensmt-doc/blob/master/smt-comp/smts-abstract-2026.pdf", + "solver_type": "Standalone", + "participations": [ + { + "tracks": ["Parallel"], + "logics": [ + "QF_UF", "QF_AX", + "QF_IDL", "QF_RDL", "QF_LIA", "QF_LRA", + "QF_UFIDL", "QF_UFLIA", "QF_UFLRA", + "QF_ALIA", + "QF_AUFLIA" + ] + } + ], + "seed": 6789, + "final": false +} From 62d825aadd1f5966e0b395116650fbb5f65024fd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Kol=C3=A1rik?= Date: Wed, 10 Jun 2026 12:01:45 +0200 Subject: [PATCH 2/4] SMTS submission 2026: changed to derived solver --- submissions/smts-base.json | 33 +++++++++++++++++++++++++++++++++ submissions/smts.json | 4 ++-- 2 files changed, 35 insertions(+), 2 deletions(-) create mode 100644 submissions/smts-base.json diff --git a/submissions/smts-base.json b/submissions/smts-base.json new file mode 100644 index 000000000..7cd0c757e --- /dev/null +++ b/submissions/smts-base.json @@ -0,0 +1,33 @@ +{ + "name": "OpenSMT-SMTS-base", + "contributors": [ + { "name": "Tomáš Kolárik", "website": "https://github.com/Tomaqa" } + , + { "name": "Martin Blicha", "website": "https://github.com/blishko" } + ], + "contacts": [ + "Tomáš Kolárik " + ], + "archive": { + "url": "https://github.com/usi-verification-and-security/opensmt/releases/download/v2.9.1/opensmt-x64-linux-static.tar.bz2" + }, + "command": ["./opensmt"], + "website": "https://github.com/usi-verification-and-security/opensmt", + "system_description": "https://github.com/usi-verification-and-security/opensmt-doc/blob/master/smt-comp/abstract-2025.pdf", + "solver_type": "Standalone", + "participations": [ + { + "tracks": ["Parallel"], + "logics": [ + "QF_UF", "QF_AX", + "QF_IDL", "QF_RDL", "QF_LIA", "QF_LRA", + "QF_UFIDL", "QF_UFLIA", "QF_UFLRA", + "QF_ALIA", + "QF_AUFLIA" + ] + } + ], + "seed": 67893, + "competitive": false, + "final": false +} diff --git a/submissions/smts.json b/submissions/smts.json index b8452b5cf..efa12c4a5 100644 --- a/submissions/smts.json +++ b/submissions/smts.json @@ -1,5 +1,5 @@ { - "name": "SMTS", + "name": "OpenSMT-SMTS", "contributors": [ { "name": "Tomáš Kolárik", "website": "https://github.com/Tomaqa" } , @@ -16,7 +16,7 @@ "command": ["./SMTS-tacas26-artifact/server/smts.py", "-l", "-p", "-nt", "32", "-o", "128", "-fp"], "website": "https://github.com/usi-verification-and-security/SMTS", "system_description": "https://github.com/usi-verification-and-security/opensmt-doc/blob/master/smt-comp/smts-abstract-2026.pdf", - "solver_type": "Standalone", + "solver_type": "derived", "participations": [ { "tracks": ["Parallel"], From 665b5ded2f1c96dc0e8d2df9ced8e0b62bed7b6c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Kol=C3=A1rik?= Date: Wed, 10 Jun 2026 12:53:11 +0200 Subject: [PATCH 3/4] SMTS submission 2026: upd. the broken archive --- submissions/smts.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/submissions/smts.json b/submissions/smts.json index efa12c4a5..66d52280b 100644 --- a/submissions/smts.json +++ b/submissions/smts.json @@ -11,9 +11,9 @@ "Tomáš Kolárik " ], "archive": { - "url": "https://github.com/usi-verification-and-security/SMTS/archive/refs/tags/tacas26-artifact.tar.gz" + "url": "https://github.com/usi-verification-and-security/SMTS/raw/refs/heads/data/data/smtcomp/smtcomp26-smts.tar.bz2" }, - "command": ["./SMTS-tacas26-artifact/server/smts.py", "-l", "-p", "-nt", "32", "-o", "128", "-fp"], + "command": ["./SMTS/server/smts.py", "-l", "-p", "-nt", "32", "-o", "128", "-fp"], "website": "https://github.com/usi-verification-and-security/SMTS", "system_description": "https://github.com/usi-verification-and-security/opensmt-doc/blob/master/smt-comp/smts-abstract-2026.pdf", "solver_type": "derived", From 833fe0c12d7b9d3803eb104c377e3869b370837b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Kol=C3=A1rik?= Date: Wed, 10 Jun 2026 13:19:11 +0200 Subject: [PATCH 4/4] SMTS submission 2026: final --- submissions/smts-base.json | 6 ++++-- submissions/smts.json | 6 ++++-- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/submissions/smts-base.json b/submissions/smts-base.json index 7cd0c757e..ba63737f6 100644 --- a/submissions/smts-base.json +++ b/submissions/smts-base.json @@ -9,7 +9,9 @@ "Tomáš Kolárik " ], "archive": { - "url": "https://github.com/usi-verification-and-security/opensmt/releases/download/v2.9.1/opensmt-x64-linux-static.tar.bz2" + "url": "https://zenodo.org/records/20625983/files/opensmt-smts-base.tar.bz2" + , + "h": { "sha256": "4c1e2e08031524a1c4baf3085ef18d986b2103c7575bdb79ce5a47855da4383d" } }, "command": ["./opensmt"], "website": "https://github.com/usi-verification-and-security/opensmt", @@ -29,5 +31,5 @@ ], "seed": 67893, "competitive": false, - "final": false + "final": true } diff --git a/submissions/smts.json b/submissions/smts.json index 66d52280b..b297fa2d1 100644 --- a/submissions/smts.json +++ b/submissions/smts.json @@ -11,7 +11,9 @@ "Tomáš Kolárik " ], "archive": { - "url": "https://github.com/usi-verification-and-security/SMTS/raw/refs/heads/data/data/smtcomp/smtcomp26-smts.tar.bz2" + "url": "https://zenodo.org/records/20625983/files/opensmt-smts.tar.bz2" + , + "h": { "sha256": "8ccfa04fca0f603c0f3aea0500c73c02b1a3397a070b9f8d21ad604074ae9b11" } }, "command": ["./SMTS/server/smts.py", "-l", "-p", "-nt", "32", "-o", "128", "-fp"], "website": "https://github.com/usi-verification-and-security/SMTS", @@ -30,5 +32,5 @@ } ], "seed": 6789, - "final": false + "final": true }