From 5c2aaec2752c0bbf63bf9acaeaedec3d70bb8a44 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Wed, 15 May 2024 22:02:46 +0200 Subject: [PATCH 1/9] Create smtinterpol Draft for the smtinterpol submission. --- submissions/smtinterpol | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 submissions/smtinterpol diff --git a/submissions/smtinterpol b/submissions/smtinterpol new file mode 100644 index 00000000..528f602a --- /dev/null +++ b/submissions/smtinterpol @@ -0,0 +1,40 @@ +{ + "name": "SMTInterpol", + "contributors": [ + "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/smtinterpol-smtcomp2024.tar.gz", + "h": { "sha256": "012345" } + }, + "website": "https://ultimate.informatik.uni-freiburg.de/smtinterpol", + "system_description": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/smtcomp2024.pdf", + "command": ["bin/smtinterpol"], + "solver_type": "Standalone", + "participations": [ + { + "tracks": ["SingleQuery"], + "logics": "(QF_)?(AX?)?(UF)?(DT)?([IR]DL|[NL][IR]*A)?", + "command": ["bin/smtinterpol"] + }, + { + "tracks": ["Incremental"], + "logics": "(QF_)?(AX?)?(UF)?(DT)?([IR]DL|[NL][IR]*A)?", + "command": ["bin/smtinterpol"] + }, + { + "tracks": ["ModelValidation"], + "logics": "(QF_)(AX?)?(UF)?(DT)?([IR]DL|[NL][IR]*A)?", + "command": ["bin/smtinterpol"] + }, + { + "tracks": ["UnsatCore"], + "logics": "(QF_)?(AX?)?(UF)?(DT)?([IR]DL|[NL][IR]*A)?", + "command": ["bin/smtinterpol"] + } + ] +} From 980d0cb3bbc42f1d73e50f47c26dcd9e08b07553 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Wed, 22 May 2024 02:51:22 +0200 Subject: [PATCH 2/9] Updated links --- submissions/smtinterpol | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/submissions/smtinterpol b/submissions/smtinterpol index 528f602a..aeb65eb8 100644 --- a/submissions/smtinterpol +++ b/submissions/smtinterpol @@ -8,11 +8,11 @@ ], "contacts": ["Jochen Hoenicke "], "archive": { - "url": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/smtinterpol-smtcomp2024.tar.gz", - "h": { "sha256": "012345" } + "url": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/smtinterpol-2.5-1325-g08d69897.tar.gz", + "h": { "sha256": "eb1fa7797ee8e95558dcef06013397582d4dc23bf54acc8f6a8f1bb6a2037d83" } }, "website": "https://ultimate.informatik.uni-freiburg.de/smtinterpol", - "system_description": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/smtcomp2024.pdf", + "system_description": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/sysdesc2024.pdf", "command": ["bin/smtinterpol"], "solver_type": "Standalone", "participations": [ From b4c906529ddbbf9c15fcdc564986bb4bab73dcc4 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Wed, 22 May 2024 02:54:33 +0200 Subject: [PATCH 3/9] trim trailing whitespace --- submissions/smtinterpol | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/submissions/smtinterpol b/submissions/smtinterpol index aeb65eb8..0d9e13cc 100644 --- a/submissions/smtinterpol +++ b/submissions/smtinterpol @@ -1,9 +1,9 @@ { "name": "SMTInterpol", "contributors": [ - "Jürgen Christ", "Daniel Dietsch", "Leonard Fichtner", - "Joanna Greulich", "Elisabeth Henkel", "Matthias Heizmann", - "Jochen Hoenicke", "Moritz Mohr", "Alexander Nutz", + "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 "], From 3633c3e7c99c3d22581f049d2e2154c09961b42b Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Sun, 26 May 2024 11:53:26 +0200 Subject: [PATCH 4/9] Add bitvector logics --- submissions/smtinterpol | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/submissions/smtinterpol b/submissions/smtinterpol index 0d9e13cc..e5a06aa2 100644 --- a/submissions/smtinterpol +++ b/submissions/smtinterpol @@ -1,6 +1,7 @@ { "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", @@ -8,8 +9,8 @@ ], "contacts": ["Jochen Hoenicke "], "archive": { - "url": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/smtinterpol-2.5-1325-g08d69897.tar.gz", - "h": { "sha256": "eb1fa7797ee8e95558dcef06013397582d4dc23bf54acc8f6a8f1bb6a2037d83" } + "url": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/smtinterpol-2.5-1335-gfbbd08ff.tar.gz", + "h": { "sha256": "4aa2d05b8ffbd684e9507a846111ac342f443234f08424b01454becd124b0818" } }, "website": "https://ultimate.informatik.uni-freiburg.de/smtinterpol", "system_description": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/sysdesc2024.pdf", @@ -21,11 +22,21 @@ "logics": "(QF_)?(AX?)?(UF)?(DT)?([IR]DL|[NL][IR]*A)?", "command": ["bin/smtinterpol"] }, + { + "tracks": ["SingleQuery"], + "logics": "(QF_)?(AX?)?(UF)?BV(DT)?([IR]DL|[NL][IR]*A)?", + "command": ["bin/smtinterpol-bv"] + }, { "tracks": ["Incremental"], "logics": "(QF_)?(AX?)?(UF)?(DT)?([IR]DL|[NL][IR]*A)?", "command": ["bin/smtinterpol"] }, + { + "tracks": ["Incremental"], + "logics": "(QF_)?(AX?)?(UF)?BV(DT)?([IR]DL|[NL][IR]*A)?", + "command": ["bin/smtinterpol-bv"] + }, { "tracks": ["ModelValidation"], "logics": "(QF_)(AX?)?(UF)?(DT)?([IR]DL|[NL][IR]*A)?", From fef38757e9263dbeb7d7cbebef1603923492e4ad Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Fri, 31 May 2024 11:04:11 +0200 Subject: [PATCH 5/9] Added seed --- submissions/{smtinterpol => smtinterpol.json} | 1 + 1 file changed, 1 insertion(+) rename submissions/{smtinterpol => smtinterpol.json} (98%) diff --git a/submissions/smtinterpol b/submissions/smtinterpol.json similarity index 98% rename from submissions/smtinterpol rename to submissions/smtinterpol.json index e5a06aa2..811634da 100644 --- a/submissions/smtinterpol +++ b/submissions/smtinterpol.json @@ -16,6 +16,7 @@ "system_description": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/sysdesc2024.pdf", "command": ["bin/smtinterpol"], "solver_type": "Standalone", + "seed": "4223469823", "participations": [ { "tracks": ["SingleQuery"], From 74316ec38da4c9e32cc0640a6ada686f42765312 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Fri, 31 May 2024 12:05:35 +0200 Subject: [PATCH 6/9] Updated run script, fixed paths --- submissions/smtinterpol.json | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/submissions/smtinterpol.json b/submissions/smtinterpol.json index 811634da..402378c3 100644 --- a/submissions/smtinterpol.json +++ b/submissions/smtinterpol.json @@ -9,44 +9,44 @@ ], "contacts": ["Jochen Hoenicke "], "archive": { - "url": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/smtinterpol-2.5-1335-gfbbd08ff.tar.gz", - "h": { "sha256": "4aa2d05b8ffbd684e9507a846111ac342f443234f08424b01454becd124b0818" } + "url": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/smtinterpol-2.5-1338-g35b19d44.tar.gz", + "h": { "sha256": "7f860df4c5c1a8f2ff5518a672f5803e3d14e56266fd9ba475189fa25edb3a12" } }, "website": "https://ultimate.informatik.uni-freiburg.de/smtinterpol", "system_description": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/sysdesc2024.pdf", - "command": ["bin/smtinterpol"], + "command": ["smtinterpol"], "solver_type": "Standalone", "seed": "4223469823", "participations": [ { "tracks": ["SingleQuery"], "logics": "(QF_)?(AX?)?(UF)?(DT)?([IR]DL|[NL][IR]*A)?", - "command": ["bin/smtinterpol"] + "command": ["smtinterpol"] }, { "tracks": ["SingleQuery"], "logics": "(QF_)?(AX?)?(UF)?BV(DT)?([IR]DL|[NL][IR]*A)?", - "command": ["bin/smtinterpol-bv"] + "command": ["smtinterpol-bv"] }, { "tracks": ["Incremental"], "logics": "(QF_)?(AX?)?(UF)?(DT)?([IR]DL|[NL][IR]*A)?", - "command": ["bin/smtinterpol"] + "command": ["smtinterpol"] }, { "tracks": ["Incremental"], "logics": "(QF_)?(AX?)?(UF)?BV(DT)?([IR]DL|[NL][IR]*A)?", - "command": ["bin/smtinterpol-bv"] + "command": ["smtinterpol-bv"] }, { "tracks": ["ModelValidation"], "logics": "(QF_)(AX?)?(UF)?(DT)?([IR]DL|[NL][IR]*A)?", - "command": ["bin/smtinterpol"] + "command": ["smtinterpol"] }, { "tracks": ["UnsatCore"], "logics": "(QF_)?(AX?)?(UF)?(DT)?([IR]DL|[NL][IR]*A)?", - "command": ["bin/smtinterpol"] + "command": ["smtinterpol"] } ] } From 479e3151add40646ce05e2dd64f0833d95351bcb Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Sun, 9 Jun 2024 20:32:05 +0200 Subject: [PATCH 7/9] Updated submission - New version uploaded - Added Contact - Added new BV logics to model-validation track --- submissions/smtinterpol.json | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/submissions/smtinterpol.json b/submissions/smtinterpol.json index 402378c3..795df2fc 100644 --- a/submissions/smtinterpol.json +++ b/submissions/smtinterpol.json @@ -7,10 +7,13 @@ "Jochen Hoenicke", "Moritz Mohr", "Alexander Nutz", "Markus Pomrehn", "Pascal Raiola", "Tanja Schindler" ], - "contacts": ["Jochen Hoenicke "], + "contacts": [ + "Max Barth ", + "Jochen Hoenicke " + ], "archive": { - "url": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/smtinterpol-2.5-1338-g35b19d44.tar.gz", - "h": { "sha256": "7f860df4c5c1a8f2ff5518a672f5803e3d14e56266fd9ba475189fa25edb3a12" } + "url": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/smtinterpol-2.5-1373-gde02de5f.tar.gz", + "h": { "sha256": "0aa5ef2d0d44bbd53c5f9123c841fcf300279bd5e492f1eacd8ea4817c141c1b" } }, "website": "https://ultimate.informatik.uni-freiburg.de/smtinterpol", "system_description": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/sysdesc2024.pdf", From 1e431f937851ab719b3727ff215b87a5f7ecc478 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Sun, 9 Jun 2024 20:49:50 +0200 Subject: [PATCH 8/9] Added BV logics to model-validation --- submissions/smtinterpol.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submissions/smtinterpol.json b/submissions/smtinterpol.json index 795df2fc..6f5152cf 100644 --- a/submissions/smtinterpol.json +++ b/submissions/smtinterpol.json @@ -43,7 +43,7 @@ }, { "tracks": ["ModelValidation"], - "logics": "(QF_)(AX?)?(UF)?(DT)?([IR]DL|[NL][IR]*A)?", + "logics": "(QF_)(AX?)?(UF)?(BV)?(DT)?([IR]DL|[NL][IR]*A)?", "command": ["smtinterpol"] }, { From 8d8ccad07cdb91d2fb7bdbf2ab50516dbd21b177 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Thu, 13 Jun 2024 16:55:58 +0200 Subject: [PATCH 9/9] Updated binary --- submissions/smtinterpol.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/submissions/smtinterpol.json b/submissions/smtinterpol.json index 6f5152cf..6ee63061 100644 --- a/submissions/smtinterpol.json +++ b/submissions/smtinterpol.json @@ -12,8 +12,8 @@ "Jochen Hoenicke " ], "archive": { - "url": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/smtinterpol-2.5-1373-gde02de5f.tar.gz", - "h": { "sha256": "0aa5ef2d0d44bbd53c5f9123c841fcf300279bd5e492f1eacd8ea4817c141c1b" } + "url": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/smtinterpol-2.5-1381-g0e9bd0bf.tar.gz", + "h": { "sha256": "3616fff7345b8ef9b12e488d4757bffb487fef3cd118737ede67f22382877c2e" } }, "website": "https://ultimate.informatik.uni-freiburg.de/smtinterpol", "system_description": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/sysdesc2024.pdf",