From e4d19aad37b78de418d9180f623e0f24ec2ed189 Mon Sep 17 00:00:00 2001 From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com> Date: Wed, 27 May 2026 21:31:27 -0700 Subject: [PATCH 1/4] init --- submissions/yices2.json | 190 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 190 insertions(+) create mode 100644 submissions/yices2.json diff --git a/submissions/yices2.json b/submissions/yices2.json new file mode 100644 index 000000000..ff37b4ed1 --- /dev/null +++ b/submissions/yices2.json @@ -0,0 +1,190 @@ +{ + "name": "Yices2", + "contributors": [ + "Bruno Dutertre", + "Aman Goel", + "Stéphane Graham-Lengrand", + "Thomas Hader", + "Ahmed Irfan", + "Dejan Jovanovic", + "Enrico Lipparini", + "Ian A Mason", + "Karthik Nukala", + "Harald Ruess" + ], + "contacts": [ + "Ahmed Irfan ", + "Stéphane Graham-Lengrand " + ], + "archive": { + "url": "https://ahmed-irfan.github.io/smtcomp/yices2-smtcomp-2026.zip" + }, + "website": "https://yices.csl.sri.com", + "system_description": "https://ahmed-irfan.github.io/smtcomp/yices2-smtcomp-2026.pdf", + "solver_type": "Standalone", + "participations": [ + { + "tracks": ["SingleQuery"], + "logics": ["QF_ABV", + "QF_ALIA", + "QF_ANIA", + "QF_AUFBV", + "QF_AUFBVLIA", + "QF_AUFBVNIA", + "QF_AUFLIA", + "QF_AUFNIA", + "QF_AX", + "QF_BVLRA", + "QF_IDL", + "QF_LIA", + "QF_LIRA", + "QF_LRA", + "QF_NIRA", + "QF_NRA", + "QF_RDL", + "QF_UF", + "QF_UFBV", + "QF_UFBVLIA", + "QF_UFIDL", + "QF_UFLIA", + "QF_UFLRA", + "QF_UFNIA", + "QF_UFNRA", + "UF"], + "command": ["./yices_smt2"] + }, + { + "tracks": ["SingleQuery"], + "logics": ["QF_BV"], + "command": ["./yices_smt2", "--delegate=kissat"] + }, + { + "tracks": ["SingleQuery"], + "logics": ["QF_NIA"], + "command": ["./yices_smt2", "--mcsat-l2o"] + }, + { + "tracks": ["Incremental"], + "logics": ["QF_ABV", + "QF_ALIA", + "QF_ANIA", + "QF_AUFBV", + "QF_AUFBVLIA", + "QF_AUFBVNIA", + "QF_AUFLIA", + "QF_AUFNIA", + "QF_AX", + "QF_BV", + "QF_BVLRA", + "QF_IDL", + "QF_LIA", + "QF_LIRA", + "QF_LRA", + "QF_NIA", + "QF_NIRA", + "QF_NRA", + "QF_RDL", + "QF_UF", + "QF_UFBV", + "QF_UFBVLIA", + "QF_UFIDL", + "QF_UFLIA", + "QF_UFLRA", + "QF_UFNIA", + "QF_UFNRA"], + "command": ["./yices_smt2", "--incremental"] + }, + { + "tracks": ["UnsatCore"], + "logics": ["QF_ABV", + "QF_ALIA", + "QF_ANIA", + "QF_AUFBV", + "QF_AUFBVLIA", + "QF_AUFBVNIA", + "QF_AUFLIA", + "QF_AUFNIA", + "QF_AX", + "QF_BV", + "QF_BVLRA", + "QF_IDL", + "QF_LIA", + "QF_LIRA", + "QF_LRA", + "QF_NIA", + "QF_NIRA", + "QF_NRA", + "QF_RDL", + "QF_UF", + "QF_UFBV", + "QF_UFBVLIA", + "QF_UFIDL", + "QF_UFLIA", + "QF_UFLRA", + "QF_UFNIA", + "QF_UFNRA"], + "command": ["./yices_smt2"] + }, + { + "tracks": ["ModelValidation"], + "logics": ["QF_BV", + "QF_BVLRA", + "QF_IDL", + "QF_LIA", + "QF_LIRA", + "QF_LRA", + "QF_NIRA", + "QF_NRA", + "QF_RDL", + "QF_UF", + "QF_UFBV", + "QF_UFBVLIA", + "QF_UFIDL", + "QF_UFLIA", + "QF_UFLRA", + "QF_UFNIA", + "QF_UFNRA"], + "command": ["./yices_smt2"] + }, + { + "tracks": ["ModelValidation"], + "logics": ["QF_NIA"], + "command": ["./yices_smt2", "--mcsat-l2o"] + }, + { + "tracks": ["Parallel"], + "logics": ["QF_NIA"], + "command": ["./yices2_parallel.py", "--yices", "./yices_smt2", "-n", "64", "--mcsat-l2o"] + }, + { + "tracks": ["Parallel"], + "logics": ["QF_ABV", + "QF_ALIA", + "QF_ANIA", + "QF_AUFBV", + "QF_AUFBVLIA", + "QF_AUFBVNIA", + "QF_AUFLIA", + "QF_AUFNIA", + "QF_AX", + "QF_BVLRA", + "QF_IDL", + "QF_LIA", + "QF_LIRA", + "QF_LRA", + "QF_NIRA", + "QF_NRA", + "QF_RDL", + "QF_UF", + "QF_UFBV", + "QF_UFBVLIA", + "QF_UFIDL", + "QF_UFLIA", + "QF_UFLRA", + "QF_UFNIA", + "QF_UFNRA"], + "command": ["./yices2_parallel.py", "--yices", "./yices_smt2", "-n", "64"] + } + ], + "seed": 37 +} From 61bafe47ff35c1738aafcfcb5324fe2329c2d9e7 Mon Sep 17 00:00:00 2001 From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com> Date: Mon, 8 Jun 2026 22:06:39 -0700 Subject: [PATCH 2/4] update yices2 submission --- submissions/yices2.json | 39 +++++++++++++++++---------------------- 1 file changed, 17 insertions(+), 22 deletions(-) diff --git a/submissions/yices2.json b/submissions/yices2.json index ff37b4ed1..dcc1ac0bc 100644 --- a/submissions/yices2.json +++ b/submissions/yices2.json @@ -56,13 +56,18 @@ { "tracks": ["SingleQuery"], "logics": ["QF_BV"], - "command": ["./yices_smt2", "--delegate=kissat"] + "command": ["./yices_smt2", "--delegate=cadical"] }, { "tracks": ["SingleQuery"], "logics": ["QF_NIA"], "command": ["./yices_smt2", "--mcsat-l2o"] }, + { + "tracks": ["Incremental"], + "logics": ["QF_BV"], + "command": ["./yices_smt2", "--incremental", "--delegate=cadical"] + }, { "tracks": ["Incremental"], "logics": ["QF_ABV", @@ -74,7 +79,6 @@ "QF_AUFLIA", "QF_AUFNIA", "QF_AX", - "QF_BV", "QF_BVLRA", "QF_IDL", "QF_LIA", @@ -127,7 +131,16 @@ }, { "tracks": ["ModelValidation"], - "logics": ["QF_BV", + "logics": ["QF_ABV", + "QF_ALIA", + "QF_ANIA", + "QF_AUFBV", + "QF_AUFBVLIA", + "QF_AUFBVNIA", + "QF_AUFLIA", + "QF_AUFNIA", + "QF_AX", + "QF_BV", "QF_BVLRA", "QF_IDL", "QF_LIA", @@ -158,29 +171,11 @@ }, { "tracks": ["Parallel"], - "logics": ["QF_ABV", - "QF_ALIA", - "QF_ANIA", - "QF_AUFBV", - "QF_AUFBVLIA", + "logics": ["QF_ANIA", "QF_AUFBVNIA", - "QF_AUFLIA", "QF_AUFNIA", - "QF_AX", - "QF_BVLRA", - "QF_IDL", - "QF_LIA", - "QF_LIRA", - "QF_LRA", "QF_NIRA", "QF_NRA", - "QF_RDL", - "QF_UF", - "QF_UFBV", - "QF_UFBVLIA", - "QF_UFIDL", - "QF_UFLIA", - "QF_UFLRA", "QF_UFNIA", "QF_UFNRA"], "command": ["./yices2_parallel.py", "--yices", "./yices_smt2", "-n", "64"] From 79dd7d6f3da8dc88689c132b2cc6e556a1415001 Mon Sep 17 00:00:00 2001 From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com> Date: Thu, 11 Jun 2026 02:00:46 -0700 Subject: [PATCH 3/4] update link --- submissions/yices2.json | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/submissions/yices2.json b/submissions/yices2.json index dcc1ac0bc..738f4dad5 100644 --- a/submissions/yices2.json +++ b/submissions/yices2.json @@ -17,7 +17,7 @@ "Stéphane Graham-Lengrand " ], "archive": { - "url": "https://ahmed-irfan.github.io/smtcomp/yices2-smtcomp-2026.zip" + "url": "https://zenodo.org/records/20639538/files/yices2-smtcomp-2026.zip?download=1" }, "website": "https://yices.csl.sri.com", "system_description": "https://ahmed-irfan.github.io/smtcomp/yices2-smtcomp-2026.pdf", @@ -181,5 +181,6 @@ "command": ["./yices2_parallel.py", "--yices", "./yices_smt2", "-n", "64"] } ], - "seed": 37 + "seed": 37, + "final": true } From 34cd4ac531787efd9a77a95008d1d2e5a0a867a6 Mon Sep 17 00:00:00 2001 From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com> Date: Thu, 11 Jun 2026 03:40:54 -0700 Subject: [PATCH 4/4] update link + add hash --- submissions/yices2.json | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/submissions/yices2.json b/submissions/yices2.json index 738f4dad5..9feb4472e 100644 --- a/submissions/yices2.json +++ b/submissions/yices2.json @@ -17,7 +17,8 @@ "Stéphane Graham-Lengrand " ], "archive": { - "url": "https://zenodo.org/records/20639538/files/yices2-smtcomp-2026.zip?download=1" + "url": "https://zenodo.org/records/20639538/files/yices2-smtcomp-2026.zip", + "h": { "sha256": "0d9ee518d59613d28172a85a7f056e829255e1b1b1e15ee5d2e02f4f392e4777" } }, "website": "https://yices.csl.sri.com", "system_description": "https://ahmed-irfan.github.io/smtcomp/yices2-smtcomp-2026.pdf",