diff --git a/submissions/smts-32.json b/submissions/smts-32.json new file mode 100644 index 00000000..08867c9e --- /dev/null +++ b/submissions/smts-32.json @@ -0,0 +1,37 @@ +{ + "name": "SMTS (32 cores)", + "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://zenodo.org/records/16024075/files/smts.tar.bz2" + , + "h": { "sha256": "2d8b45c2458493d45f632f9657a735d90957667caf7eb980b17b9b832b8bcc24" } + }, + "command": ["./SMTS/server/smts.py", "-l", "-p", "-o", "32", "-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/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": 89, + "competitive": false, + "final": true +} diff --git a/submissions/smts-64.json b/submissions/smts-64.json new file mode 100644 index 00000000..52223da8 --- /dev/null +++ b/submissions/smts-64.json @@ -0,0 +1,37 @@ +{ + "name": "SMTS (64 cores)", + "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://zenodo.org/records/16024075/files/smts.tar.bz2" + , + "h": { "sha256": "2d8b45c2458493d45f632f9657a735d90957667caf7eb980b17b9b832b8bcc24" } + }, + "command": ["./SMTS/server/smts.py", "-l", "-p", "-o", "64", "-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/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": 89, + "competitive": false, + "final": true +} diff --git a/submissions/smts.json b/submissions/smts.json index b3ccb33f..b973f5bc 100644 --- a/submissions/smts.json +++ b/submissions/smts.json @@ -11,11 +11,11 @@ "Tomáš Kolárik " ], "archive": { - "url": "https://zenodo.org/records/15756050/files/smts.tar.bz2" + "url": "https://zenodo.org/records/16024075/files/smts.tar.bz2" , - "h": { "sha256": "9de09b0fd757b904ef0c0e8bc515bdf1a9a615e3b140279bd41783c24638e2b8" } + "h": { "sha256": "2d8b45c2458493d45f632f9657a735d90957667caf7eb980b17b9b832b8bcc24" } }, - "command": ["./SMTS/server/smts.py", "-l", "-p", "-pt", "2", "-nt", "30", "-o", "128", "-fp"], + "command": ["./SMTS/server/smts.py", "-l", "-p", "-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/abstract-2025.pdf", "solver_type": "Standalone",