From dcb74d564a07da7e0d33364ab100cdbdbfdfb4cb Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Wed, 15 May 2024 22:02:46 +0200 Subject: [PATCH 1/5] Create smtinterpol for 2025 --- submissions/smtinterpol.json | 44 ++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) create mode 100644 submissions/smtinterpol.json diff --git a/submissions/smtinterpol.json b/submissions/smtinterpol.json new file mode 100644 index 00000000..8a083638 --- /dev/null +++ b/submissions/smtinterpol.json @@ -0,0 +1,44 @@ +{ + "name": "SMTInterpol", + "contributors": [ + "Max Barth", "Leon Cacace", + "Jürgen Christ", "Daniel Dietsch", "Leonard Fichtner", + "Joanna Greulich", "Elisabeth Henkel", "Matthias Heizmann", + "Jochen Hoenicke", "Moritz Mohr", "Alexander Nutz", + "Markus Pomrehn", "Pascal Raiola", "Tanja Schindler" + ], + "contacts": [ + "Jochen Hoenicke " + ], + "archive": { + "url": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/smtcomp/smtinterpol-2.5-1399-g79018412.tar.gz", + "h": { "sha256": "5ce2002583a7035629ff98fc60df75bef1d14110b702ccdb721baa3c62d250b7" } + }, + "website": "https://ultimate.informatik.uni-freiburg.de/smtinterpol", + "system_description": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/sysdesc2025.pdf", + "command": ["smtinterpol"], + "solver_type": "Standalone", + "seed": "2030142482", + "participations": [ + { + "tracks": ["SingleQuery"], + "logics": "(QF_)?(AX?)?(UF)?(BV)?(DT)?([IR]DL|[NL][IR]*A)?", + "command": ["smtinterpol"] + }, + { + "tracks": ["Incremental"], + "logics": "(QF_)?(AX?)?(UF)?(BV)?(DT)?([IR]DL|[NL][IR]*A)?", + "command": ["smtinterpol"] + }, + { + "tracks": ["ModelValidation"], + "logics": "(QF_)(AX?)?(UF)?(BV)?(DT)?([IR]DL|[NL][IR]*A)?", + "command": ["smtinterpol"] + }, + { + "tracks": ["UnsatCore"], + "logics": "(QF_)?(AX?)?(UF)?(BV)?(DT)?([IR]DL|[NL][IR]*A)?", + "command": ["smtinterpol"] + } + ] +} From 9c86c2816c21e93cec74592c60ae9573c1ff3965 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Tue, 10 Jun 2025 17:55:56 +0200 Subject: [PATCH 2/5] Updated solver to support all logics --- submissions/smtinterpol.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/submissions/smtinterpol.json b/submissions/smtinterpol.json index 8a083638..769392ca 100644 --- a/submissions/smtinterpol.json +++ b/submissions/smtinterpol.json @@ -11,8 +11,8 @@ "Jochen Hoenicke " ], "archive": { - "url": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/smtcomp/smtinterpol-2.5-1399-g79018412.tar.gz", - "h": { "sha256": "5ce2002583a7035629ff98fc60df75bef1d14110b702ccdb721baa3c62d250b7" } + "url": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/smtcomp/smtinterpol-2.5-1400-g2599b60f.tar.gz", + "h": { "sha256": "a73c77c1bbaf9b8d6cd31bdf933df3b6fba02cbb3a6da0eef62649d281a08f6d" } }, "website": "https://ultimate.informatik.uni-freiburg.de/smtinterpol", "system_description": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/sysdesc2025.pdf", From 80ef4ab0825b21c7a33897bab366a462ac6c0217 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Thu, 26 Jun 2025 22:42:17 +0200 Subject: [PATCH 3/5] Upated version --- submissions/smtinterpol.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/submissions/smtinterpol.json b/submissions/smtinterpol.json index 769392ca..ed368cdc 100644 --- a/submissions/smtinterpol.json +++ b/submissions/smtinterpol.json @@ -11,8 +11,8 @@ "Jochen Hoenicke " ], "archive": { - "url": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/smtcomp/smtinterpol-2.5-1400-g2599b60f.tar.gz", - "h": { "sha256": "a73c77c1bbaf9b8d6cd31bdf933df3b6fba02cbb3a6da0eef62649d281a08f6d" } + "url": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/smtcomp/smtinterpol-2.5-1405-gae7e68ef.tar.gz", + "h": { "sha256": "193ba2a7c2c67e950de57e520414fdbee3c08daa51374e4f8a7aa8857a43805a" } }, "website": "https://ultimate.informatik.uni-freiburg.de/smtinterpol", "system_description": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/sysdesc2025.pdf", From e4e0ac6461595c0c1b6d52ad4a1de06c78db738a Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Fri, 27 Jun 2025 19:18:16 +0200 Subject: [PATCH 4/5] Clean rebuild using docker --- submissions/smtinterpol.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submissions/smtinterpol.json b/submissions/smtinterpol.json index ed368cdc..043fb0f9 100644 --- a/submissions/smtinterpol.json +++ b/submissions/smtinterpol.json @@ -12,7 +12,7 @@ ], "archive": { "url": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/smtcomp/smtinterpol-2.5-1405-gae7e68ef.tar.gz", - "h": { "sha256": "193ba2a7c2c67e950de57e520414fdbee3c08daa51374e4f8a7aa8857a43805a" } + "h": { "sha256": "41a3ce3d38417a807865a389df3b8466492d584070c21888ac2732d8470d601c" } }, "website": "https://ultimate.informatik.uni-freiburg.de/smtinterpol", "system_description": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/sysdesc2025.pdf", From 715450480b9a86743ec5f15444f37b1571377087 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Wed, 2 Jul 2025 10:10:01 +0200 Subject: [PATCH 5/5] Updated URL to point to zenodo --- submissions/smtinterpol.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submissions/smtinterpol.json b/submissions/smtinterpol.json index 043fb0f9..04200e9b 100644 --- a/submissions/smtinterpol.json +++ b/submissions/smtinterpol.json @@ -11,7 +11,7 @@ "Jochen Hoenicke " ], "archive": { - "url": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/smtcomp/smtinterpol-2.5-1405-gae7e68ef.tar.gz", + "url": "https://zenodo.org/records/15756957/files/smtinterpol-2.5-1405-gae7e68ef.tar.gz?download=1", "h": { "sha256": "41a3ce3d38417a807865a389df3b8466492d584070c21888ac2732d8470d601c" } }, "website": "https://ultimate.informatik.uni-freiburg.de/smtinterpol",