From 27cc5d0b0da6e48a2f7549e26744c75f0def786d Mon Sep 17 00:00:00 2001 From: konstantin-korovin <36406221+konstantin-korovin@users.noreply.github.com> Date: Fri, 13 Jun 2025 19:41:58 +0100 Subject: [PATCH 01/12] Create iProver iProver v3.9.3 initial submission --- submissions/iprover | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 submissions/iprover diff --git a/submissions/iprover b/submissions/iprover new file mode 100644 index 00000000..014e8096 --- /dev/null +++ b/submissions/iprover @@ -0,0 +1,29 @@ +{ + "name": "iProver v3.9.3", + "contributors": [ + { "name": "Konstantin Korovin", "website": "https://korovin.gitlab.io/" } + ], + "contacts": ["Konstantin Korovin "], + "archive": { + "url": "https://zenodo.org/records/15659520", + "h": { "sha256": "0a839572e490ee2028d9dae00a15dd3c7700d73a143f3aa42e2f811cc92b63e5" } + }, + "website": "https://gitlab.com/korovin/iprover", + "system_description": "http://www.cs.man.ac.uk/~korovink/iprover-smt-comp-2024.pdf", + "command": ["cd bin; iprover_smtcomp.sh"], + + "solver_type": "wrapped", + "participations": [ + { "tracks": ["SingleQuery"], + "divisions" :["Arith","Equality","Equality+LinearArith","Equality+NonLinearArith"], + + "logics": ["ALIA, ANIA, AUFDTLIA, AUFDTLIRA, AUFDTNIRA, AUFLIA, AUFLIRA, AUFNIA, AUFNIRA, LIA, LRA, NIA, NRA, UF, UFDT, UFDTLIA, UFDTLIRA, UFDTNIA, UFDTNIRA, UFIDL, UFLIA, UFLRA, UFNIA, UFNIRA"] }, + + { "tracks": ["Parallel"], + "divisions" :["Arith","Equality","Equality+LinearArith","Equality+NonLinearArith"], + + "logics": ["ALIA, ANIA, AUFDTLIA, AUFDTLIRA, AUFDTNIRA, AUFLIA, AUFLIRA, AUFNIA, AUFNIRA, LIA, LRA, NIA, NRA, UF, UFDT, UFDTLIA, UFDTLIRA, UFDTNIA, UFDTNIRA, UFIDL, UFLIA, UFLRA, UFNIA, UFNIRA"]} + + ] +} + From 958a93ed287c92b27348361187448031881344ee Mon Sep 17 00:00:00 2001 From: konstantin-korovin <36406221+konstantin-korovin@users.noreply.github.com> Date: Fri, 13 Jun 2025 19:48:50 +0100 Subject: [PATCH 02/12] Update iProver --- submissions/iprover | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/submissions/iprover b/submissions/iprover index 014e8096..61c6a9bd 100644 --- a/submissions/iprover +++ b/submissions/iprover @@ -11,19 +11,13 @@ "website": "https://gitlab.com/korovin/iprover", "system_description": "http://www.cs.man.ac.uk/~korovink/iprover-smt-comp-2024.pdf", "command": ["cd bin; iprover_smtcomp.sh"], - "solver_type": "wrapped", "participations": [ { "tracks": ["SingleQuery"], "divisions" :["Arith","Equality","Equality+LinearArith","Equality+NonLinearArith"], - "logics": ["ALIA, ANIA, AUFDTLIA, AUFDTLIRA, AUFDTNIRA, AUFLIA, AUFLIRA, AUFNIA, AUFNIRA, LIA, LRA, NIA, NRA, UF, UFDT, UFDTLIA, UFDTLIRA, UFDTNIA, UFDTNIRA, UFIDL, UFLIA, UFLRA, UFNIA, UFNIRA"] }, - { "tracks": ["Parallel"], "divisions" :["Arith","Equality","Equality+LinearArith","Equality+NonLinearArith"], - - "logics": ["ALIA, ANIA, AUFDTLIA, AUFDTLIRA, AUFDTNIRA, AUFLIA, AUFLIRA, AUFNIA, AUFNIRA, LIA, LRA, NIA, NRA, UF, UFDT, UFDTLIA, UFDTLIRA, UFDTNIA, UFDTNIRA, UFIDL, UFLIA, UFLRA, UFNIA, UFNIRA"]} - + "logics": ["ALIA, ANIA, AUFDTLIA, AUFDTLIRA, AUFDTNIRA, AUFLIA, AUFLIRA, AUFNIA, AUFNIRA, LIA, LRA, NIA, NRA, UF, UFDT, UFDTLIA, UFDTLIRA, UFDTNIA, UFDTNIRA, UFIDL, UFLIA, UFLRA, UFNIA, UFNIRA"]} ] } - From 69694312a1a62feeab48115d860aa98ccaf9f852 Mon Sep 17 00:00:00 2001 From: konstantin-korovin <36406221+konstantin-korovin@users.noreply.github.com> Date: Fri, 13 Jun 2025 19:58:19 +0100 Subject: [PATCH 03/12] Update iProver --- submissions/iprover | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/submissions/iprover b/submissions/iprover index 61c6a9bd..5fd6a690 100644 --- a/submissions/iprover +++ b/submissions/iprover @@ -1,12 +1,12 @@ { "name": "iProver v3.9.3", - "contributors": [ + "contributors": [ { "name": "Konstantin Korovin", "website": "https://korovin.gitlab.io/" } ], "contacts": ["Konstantin Korovin "], "archive": { "url": "https://zenodo.org/records/15659520", - "h": { "sha256": "0a839572e490ee2028d9dae00a15dd3c7700d73a143f3aa42e2f811cc92b63e5" } + "h": { "sha256": "0a839572e490ee2028d9dae00a15dd3c7700d73a143f3aa42e2f811cc92b63e5"} }, "website": "https://gitlab.com/korovin/iprover", "system_description": "http://www.cs.man.ac.uk/~korovink/iprover-smt-comp-2024.pdf", @@ -18,6 +18,6 @@ "logics": ["ALIA, ANIA, AUFDTLIA, AUFDTLIRA, AUFDTNIRA, AUFLIA, AUFLIRA, AUFNIA, AUFNIRA, LIA, LRA, NIA, NRA, UF, UFDT, UFDTLIA, UFDTLIRA, UFDTNIA, UFDTNIRA, UFIDL, UFLIA, UFLRA, UFNIA, UFNIRA"] }, { "tracks": ["Parallel"], "divisions" :["Arith","Equality","Equality+LinearArith","Equality+NonLinearArith"], - "logics": ["ALIA, ANIA, AUFDTLIA, AUFDTLIRA, AUFDTNIRA, AUFLIA, AUFLIRA, AUFNIA, AUFNIRA, LIA, LRA, NIA, NRA, UF, UFDT, UFDTLIA, UFDTLIRA, UFDTNIA, UFDTNIRA, UFIDL, UFLIA, UFLRA, UFNIA, UFNIRA"]} + "logics": ["ALIA, ANIA, AUFDTLIA, AUFDTLIRA, AUFDTNIRA, AUFLIA, AUFLIRA, AUFNIA, AUFNIRA, LIA, LRA, NIA, NRA, UF, UFDT, UFDTLIA, UFDTLIRA, UFDTNIA, UFDTNIRA, UFIDL, UFLIA, UFLRA, UFNIA, UFNIRA"]} ] } From 32b4b023fdd85cf29f0c012649450992cd3153c4 Mon Sep 17 00:00:00 2001 From: konstantin-korovin <36406221+konstantin-korovin@users.noreply.github.com> Date: Mon, 16 Jun 2025 15:55:59 +0100 Subject: [PATCH 04/12] Rename iprover to iprover.json --- submissions/{iprover => iprover.json} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename submissions/{iprover => iprover.json} (100%) diff --git a/submissions/iprover b/submissions/iprover.json similarity index 100% rename from submissions/iprover rename to submissions/iprover.json From 7d84b6b274eac87c113e80606989d01d24e1ba3b Mon Sep 17 00:00:00 2001 From: konstantin-korovin <36406221+konstantin-korovin@users.noreply.github.com> Date: Mon, 16 Jun 2025 16:10:13 +0100 Subject: [PATCH 05/12] Update iprover.json removed quotes in logics --- submissions/iprover.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/submissions/iprover.json b/submissions/iprover.json index 5fd6a690..13be4ee0 100644 --- a/submissions/iprover.json +++ b/submissions/iprover.json @@ -15,9 +15,9 @@ "participations": [ { "tracks": ["SingleQuery"], "divisions" :["Arith","Equality","Equality+LinearArith","Equality+NonLinearArith"], - "logics": ["ALIA, ANIA, AUFDTLIA, AUFDTLIRA, AUFDTNIRA, AUFLIA, AUFLIRA, AUFNIA, AUFNIRA, LIA, LRA, NIA, NRA, UF, UFDT, UFDTLIA, UFDTLIRA, UFDTNIA, UFDTNIRA, UFIDL, UFLIA, UFLRA, UFNIA, UFNIRA"] }, + "logics": [ALIA,ANIA,AUFDTLIA,AUFDTLIRA,AUFDTNIRA,AUFLIA,AUFLIRA,AUFNIA,AUFNIRA,LIA,LRA,NIA,NRA,UF,UFDT,UFDTLIA,UFDTLIRA,UFDTNIA,UFDTNIRA,UFIDL,UFLIA,UFLRA,UFNIA,UFNIRA]}, { "tracks": ["Parallel"], "divisions" :["Arith","Equality","Equality+LinearArith","Equality+NonLinearArith"], - "logics": ["ALIA, ANIA, AUFDTLIA, AUFDTLIRA, AUFDTNIRA, AUFLIA, AUFLIRA, AUFNIA, AUFNIRA, LIA, LRA, NIA, NRA, UF, UFDT, UFDTLIA, UFDTLIRA, UFDTNIA, UFDTNIRA, UFIDL, UFLIA, UFLRA, UFNIA, UFNIRA"]} + "logics": [ALIA,ANIA,AUFDTLIA,AUFDTLIRA,AUFDTNIRA,AUFLIA,AUFLIRA,AUFNIA,AUFNIRA,LIA,LRA,NIA,NRA,UF,UFDT,UFDTLIA,UFDTLIRA,UFDTNIA,UFDTNIRA,UFIDL,UFLIA,UFLRA,UFNIA,UFNIRA]} ] } From ae57d0c0730a5bc7d01027f06ec7464e101f8596 Mon Sep 17 00:00:00 2001 From: konstantin-korovin <36406221+konstantin-korovin@users.noreply.github.com> Date: Mon, 16 Jun 2025 16:19:07 +0100 Subject: [PATCH 06/12] Update iprover.json after JSONLint validation --- submissions/iprover.json | 51 ++++++++++++++++++++++++++++++++-------- 1 file changed, 41 insertions(+), 10 deletions(-) diff --git a/submissions/iprover.json b/submissions/iprover.json index 13be4ee0..eafff9f1 100644 --- a/submissions/iprover.json +++ b/submissions/iprover.json @@ -1,23 +1,54 @@ { "name": "iProver v3.9.3", "contributors": [ - { "name": "Konstantin Korovin", "website": "https://korovin.gitlab.io/" } + { + "name": "Konstantin Korovin", + "website": "https://korovin.gitlab.io/" + } + ], + "contacts": [ + "Konstantin Korovin " ], - "contacts": ["Konstantin Korovin "], "archive": { "url": "https://zenodo.org/records/15659520", - "h": { "sha256": "0a839572e490ee2028d9dae00a15dd3c7700d73a143f3aa42e2f811cc92b63e5"} + "h": { + "sha256": "0a839572e490ee2028d9dae00a15dd3c7700d73a143f3aa42e2f811cc92b63e5" + } }, "website": "https://gitlab.com/korovin/iprover", "system_description": "http://www.cs.man.ac.uk/~korovink/iprover-smt-comp-2024.pdf", - "command": ["cd bin; iprover_smtcomp.sh"], + "command": [ + "cd bin; iprover_smtcomp.sh" + ], "solver_type": "wrapped", "participations": [ - { "tracks": ["SingleQuery"], - "divisions" :["Arith","Equality","Equality+LinearArith","Equality+NonLinearArith"], - "logics": [ALIA,ANIA,AUFDTLIA,AUFDTLIRA,AUFDTNIRA,AUFLIA,AUFLIRA,AUFNIA,AUFNIRA,LIA,LRA,NIA,NRA,UF,UFDT,UFDTLIA,UFDTLIRA,UFDTNIA,UFDTNIRA,UFIDL,UFLIA,UFLRA,UFNIA,UFNIRA]}, - { "tracks": ["Parallel"], - "divisions" :["Arith","Equality","Equality+LinearArith","Equality+NonLinearArith"], - "logics": [ALIA,ANIA,AUFDTLIA,AUFDTLIRA,AUFDTNIRA,AUFLIA,AUFLIRA,AUFNIA,AUFNIRA,LIA,LRA,NIA,NRA,UF,UFDT,UFDTLIA,UFDTLIRA,UFDTNIA,UFDTNIRA,UFIDL,UFLIA,UFLRA,UFNIA,UFNIRA]} + { + "tracks": [ + "SingleQuery" + ], + "divisions": [ + "Arith", + "Equality", + "Equality+LinearArith", + "Equality+NonLinearArith" + ], + "logics": [ + "ALIA, ANIA, AUFDTLIA, AUFDTLIRA, AUFDTNIRA, AUFLIA, AUFLIRA, AUFNIA, AUFNIRA, LIA, LRA, NIA, NRA, UF, UFDT, UFDTLIA, UFDTLIRA, UFDTNIA, UFDTNIRA, UFIDL, UFLIA, UFLRA, UFNIA, UFNIRA" + ] + }, + { + "tracks": [ + "Parallel" + ], + "divisions": [ + "Arith", + "Equality", + "Equality+LinearArith", + "Equality+NonLinearArith" + ], + "logics": [ + "ALIA, ANIA, AUFDTLIA, AUFDTLIRA, AUFDTNIRA, AUFLIA, AUFLIRA, AUFNIA, AUFNIRA, LIA, LRA, NIA, NRA, UF, UFDT, UFDTLIA, UFDTLIRA, UFDTNIA, UFDTNIRA, UFIDL, UFLIA, UFLRA, UFNIA, UFNIRA" + ] + } ] } From dd84cd2cbc0eda6f119e93aa552e839d2b18cae4 Mon Sep 17 00:00:00 2001 From: konstantin-korovin <36406221+konstantin-korovin@users.noreply.github.com> Date: Mon, 16 Jun 2025 16:35:02 +0100 Subject: [PATCH 07/12] Update iprover.json added quotes --- submissions/iprover.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/submissions/iprover.json b/submissions/iprover.json index eafff9f1..d2bdb58b 100644 --- a/submissions/iprover.json +++ b/submissions/iprover.json @@ -33,7 +33,7 @@ "Equality+NonLinearArith" ], "logics": [ - "ALIA, ANIA, AUFDTLIA, AUFDTLIRA, AUFDTNIRA, AUFLIA, AUFLIRA, AUFNIA, AUFNIRA, LIA, LRA, NIA, NRA, UF, UFDT, UFDTLIA, UFDTLIRA, UFDTNIA, UFDTNIRA, UFIDL, UFLIA, UFLRA, UFNIA, UFNIRA" + "ALIA", "ANIA", "AUFDTLIA", "AUFDTLIRA", "AUFDTNIRA", "AUFLIA", "AUFLIRA", "AUFNIA", "AUFNIRA", "LIA", "LRA", "NIA", "NRA", "UF", "UFDT", "UFDTLIA", "UFDTLIRA", "UFDTNIA", "UFDTNIRA", "UFIDL", "UFLIA", "UFLRA", "UFNIA", "UFNIRA" ] }, { @@ -47,7 +47,7 @@ "Equality+NonLinearArith" ], "logics": [ - "ALIA, ANIA, AUFDTLIA, AUFDTLIRA, AUFDTNIRA, AUFLIA, AUFLIRA, AUFNIA, AUFNIRA, LIA, LRA, NIA, NRA, UF, UFDT, UFDTLIA, UFDTLIRA, UFDTNIA, UFDTNIRA, UFIDL, UFLIA, UFLRA, UFNIA, UFNIRA" + "ALIA", "ANIA", "AUFDTLIA", "AUFDTLIRA", "AUFDTNIRA", "AUFLIA", "AUFLIRA", "AUFNIA", "AUFNIRA", "LIA", "LRA", "NIA", "NRA", "UF", "UFDT", "UFDTLIA", "UFDTLIRA", "UFDTNIA", "UFDTNIRA", "UFIDL", "UFLIA", "UFLRA", "UFNIA", "UFNIRA" ] } ] From 66a22202cb7972eb8a5815c0b5594b4979619eb5 Mon Sep 17 00:00:00 2001 From: konstantin-korovin <36406221+konstantin-korovin@users.noreply.github.com> Date: Mon, 16 Jun 2025 16:39:34 +0100 Subject: [PATCH 08/12] Update iprover.json added seed --- submissions/iprover.json | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/submissions/iprover.json b/submissions/iprover.json index d2bdb58b..9c008654 100644 --- a/submissions/iprover.json +++ b/submissions/iprover.json @@ -50,5 +50,6 @@ "ALIA", "ANIA", "AUFDTLIA", "AUFDTLIRA", "AUFDTNIRA", "AUFLIA", "AUFLIRA", "AUFNIA", "AUFNIRA", "LIA", "LRA", "NIA", "NRA", "UF", "UFDT", "UFDTLIA", "UFDTLIRA", "UFDTNIA", "UFDTNIRA", "UFIDL", "UFLIA", "UFLRA", "UFNIA", "UFNIRA" ] } - ] + ], + "seed": 139 } From 0131de45b4d0779a6b30bf05abcb85b218a8bc3a Mon Sep 17 00:00:00 2001 From: konstantin-korovin <36406221+konstantin-korovin@users.noreply.github.com> Date: Mon, 16 Jun 2025 16:49:57 +0100 Subject: [PATCH 09/12] Update iprover.json updated url --- submissions/iprover.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submissions/iprover.json b/submissions/iprover.json index 9c008654..e6f7bdd5 100644 --- a/submissions/iprover.json +++ b/submissions/iprover.json @@ -10,7 +10,7 @@ "Konstantin Korovin " ], "archive": { - "url": "https://zenodo.org/records/15659520", + "url": "https://zenodo.org/records/15659520/files/iprover_v3.9.3_smt_init_2025.zip?download=1", "h": { "sha256": "0a839572e490ee2028d9dae00a15dd3c7700d73a143f3aa42e2f811cc92b63e5" } From 522be14d51f1ee5d71af1db8c3d9f0fc443e48d5 Mon Sep 17 00:00:00 2001 From: konstantin-korovin <36406221+konstantin-korovin@users.noreply.github.com> Date: Mon, 16 Jun 2025 17:15:14 +0100 Subject: [PATCH 10/12] Update iprover.json updated "command" --- submissions/iprover.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submissions/iprover.json b/submissions/iprover.json index e6f7bdd5..8c427147 100644 --- a/submissions/iprover.json +++ b/submissions/iprover.json @@ -18,7 +18,7 @@ "website": "https://gitlab.com/korovin/iprover", "system_description": "http://www.cs.man.ac.uk/~korovink/iprover-smt-comp-2024.pdf", "command": [ - "cd bin; iprover_smtcomp.sh" + "cd bin; ./iprover_smtcomp.sh" ], "solver_type": "wrapped", "participations": [ From 7357f8e59bfc97028056caf52e3a33a54685dc0d Mon Sep 17 00:00:00 2001 From: konstantin-korovin <36406221+konstantin-korovin@users.noreply.github.com> Date: Mon, 16 Jun 2025 17:20:47 +0100 Subject: [PATCH 11/12] Update iprover.json updated "command" --- submissions/iprover.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submissions/iprover.json b/submissions/iprover.json index 8c427147..78a614cb 100644 --- a/submissions/iprover.json +++ b/submissions/iprover.json @@ -18,7 +18,7 @@ "website": "https://gitlab.com/korovin/iprover", "system_description": "http://www.cs.man.ac.uk/~korovink/iprover-smt-comp-2024.pdf", "command": [ - "cd bin; ./iprover_smtcomp.sh" + "bin/iprover_smtcomp.sh" ], "solver_type": "wrapped", "participations": [ From f84a566848a264c70eee0ae26fb72e3a3af62939 Mon Sep 17 00:00:00 2001 From: konstantin-korovin <36406221+konstantin-korovin@users.noreply.github.com> Date: Mon, 16 Jun 2025 22:47:32 +0100 Subject: [PATCH 12/12] Update iprover.json updated system description link --- submissions/iprover.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submissions/iprover.json b/submissions/iprover.json index 78a614cb..508b12ff 100644 --- a/submissions/iprover.json +++ b/submissions/iprover.json @@ -16,7 +16,7 @@ } }, "website": "https://gitlab.com/korovin/iprover", - "system_description": "http://www.cs.man.ac.uk/~korovink/iprover-smt-comp-2024.pdf", + "system_description": "http://www.cs.man.ac.uk/~korovink/iprover-smt-comp-2025.pdf", "command": [ "bin/iprover_smtcomp.sh" ],