A description of this web service can be found in the CAV paper "Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses" (more material).
Found 26 witnesses for program sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca_true-termination.c.i, ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
82a5b8c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-12-04T01:19:05+01:00 | 507169c | |
7b672cc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-11-30T12:02:08+01:00 | 769c46d | |
bfccbf7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.1 | 4 | 2023-12-17T03:43:06+01:00 | ||
0801e0e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.0 | 4 | 2023-12-19T12:01:55+01:00 | ||
44ec720 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 4 | 2023-12-18T20:35:43+01:00 | ||
c3b8a9b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:22:14+01:00 | ||
c80f4c7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T08:06:22Z | ||
5a93caa | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 15 | 2023-12-02T17:19:55Z | ||
a5a08c6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2023-11-29T09:51:41Z | ||
a28f511 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 25 | 2023-12-01T01:16:02Z | ||
1f991c8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-19T15:34:13+01:00 | 0801e0e | |
6f19ed2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-19T05:26:36+01:00 | 44ec720 | |
e4ebdcb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-17T06:38:08+01:00 | bfccbf7 | |
8d3ecc9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-04T11:38:25+01:00 | 5a93caa | |
e9c85bd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-03T18:31:06+01:00 | c3b8a9b | |
75538ac | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-03T09:54:38+01:00 | c80f4c7 | |
d707b26 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-01T03:42:06+01:00 | a28f511 | |
769c46d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-30T08:14:45+01:00 | ||
41bacbe | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-29T18:11:49+01:00 | a5a08c6 | |
4eda49d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-29T08:07:17+01:00 | 4634e0d | |
507169c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 7 | 2023-12-03T21:09:39+01:00 | ||
4634e0d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 15 | 2023-11-28T23:31:16Z | ||
cb833e9 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 3 | 2023-12-01T01:12:52Z | ||
0757701 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: a50f1aca-0277-4112-95b7-8fb6d91ffdb4 creation_time: '2023-12-02T18:19:55+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7c84cb03-fdef-4967-9ba4-502124e92a54/sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7c84cb03-fdef-4967-9ba4-502124e92a54/sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i : ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7c84cb03-fdef-4967-9ba4-502124e92a54/sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i file_hash: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d line: 550 column: 0 function: SelectionSort value: ((((i == 0) && (array_size <= 2147483647)) && (1 <= array_size)) || ((((array_size <= 2147483647) && (0 <= (j + 2147483648))) && (1 <= i)) && (1 <= array_size))) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7c84cb03-fdef-4967-9ba4-502124e92a54/sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i file_hash: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d line: 554 column: 0 function: SelectionSort value: (((((array_size <= 2147483647) && ((i + 2) <= array_size)) && (0 <= (j + 2147483648))) && (1 <= i)) || ((((i == 0) && (array_size <= 2147483647)) && (1 <= j)) && (2 <= array_size))) format: c_expression | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-04T11:59:55+01:00 | ||
96a6434 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 2094a042-e363-495e-811a-a5e72c9f8a09 creation_time: '2023-11-29T00:31:16+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11763872-a760-4b7f-810a-bc766de6bb73/sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11763872-a760-4b7f-810a-bc766de6bb73/sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i : ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11763872-a760-4b7f-810a-bc766de6bb73/sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i file_hash: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d line: 550 column: 0 function: SelectionSort value: (((((((array_size <= 2147483647) && (array_size <= 2147483647)) && (0 <= (j + 2147483648))) && (1 <= i)) && (1 <= array_size)) && (1 <= array_size)) || (((((i == 0) && (array_size <= 2147483647)) && (array_size <= 2147483647)) && (1 <= array_size)) && (1 <= array_size))) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11763872-a760-4b7f-810a-bc766de6bb73/sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i file_hash: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d line: 554 column: 0 function: SelectionSort value: ((((((((i == 0) && (array_size <= 2147483647)) && (array_size <= 2147483647)) && ((i + 2) <= array_size)) && (1 <= j)) && (1 <= array_size)) && (1 <= array_size)) || (((((((array_size <= 2147483647) && (array_size <= 2147483647)) && ((i + 2) <= array_size)) && (0 <= (j + 2147483648))) && (1 <= i)) && (1 <= array_size)) && (1 <= array_size))) format: c_expression | correctness_witness | CPAchecker 2.3 | 10 | 2023-11-29T07:49:19+01:00 | ||
dd639ff | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: 9a906ecd-01e7-4fce-b1b9-edaadd554843 creation_time: 2023-12-01T01:16:02Z producer: name: Goblint version: tags/svcomp24-0-gc2e9465a7 command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--sets'' ''ana.specification'' ''../../sv-benchmarks/c/properties/no-overflow.prp'' ''--sets'' ''exp.architecture'' ''64bit'' ''../../sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i''' task: input_files: - ../../sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i input_file_hashes: ../../sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i file_hash: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d line: 550 column: 8 function: SelectionSort value: array_size != 0 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i file_hash: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d line: 550 column: 8 function: SelectionSort value: (0 <= i && ((((((((((((((0 <= min && 2 <= array_size) && 2 <= j) && i <= 2147483645) && (-4LL + (long long )array_size) + (long long )j >= 0LL) && (-2LL + (long long )array_size) + (long long )i >= 0LL) && (-2LL + (long long )i) + (long long )j >= 0LL) && (-2LL - (long long )i) + (long long )j >= 0LL) && (0LL - (long long )array_size) + (long long )j >= 0LL) && (-2LL + (long long )array_size) - (long long )i >= 0LL) && (long long )array_size - (long long )j >= 0LL) && array_size != 1) && j != 0) && j != 1) || (((((((1 <= array_size && i <= 2147483646) && (-1LL + (long long )array_size) + (long long )i >= 0LL) && (2147483647LL + (long long )array_size) + (long long )j >= 0LL) && (2147483648LL + (long long )i) + (long long )j >= 0LL) && (2147483648LL - (long long )i) + (long long )j >= 0LL) && (-1LL + (long long )array_size) - (long long )i >= 0LL) && (2147483646LL + (long long )array_size) - (long long )j >= 0LL))) || ((((((((((((((((((1 <= array_size && (2147483647LL + (long long )array_size) + (long long )i >= 0LL) && (2147483647LL + (long long )array_size) + (long long )j >= 0LL) && (2147483647LL + (long long )array_size) + (long long )temp >= 0LL) && (4294967296LL + (long long )i) + (long long )j >= 0LL) && (4294967296LL + (long long )i) + (long long )temp >= 0LL) && (4294967296LL + (long long )j) + (long long )temp >= 0LL) && (4294967295LL - (long long )i) + (long long )j >= 0LL) && (4294967295LL - (long long )i) + (long long )temp >= 0LL) && (4294967295LL - (long long )j) + (long long )temp >= 0LL) && (2147483646LL + (long long )array_size) - (long long )i >= 0LL) && (2147483646LL + (long long )array_size) - (long long )j >= 0LL) && (2147483646LL + (long long )array_size) - (long long )temp >= 0LL) && (4294967295LL + (long long )i) - (long long )j >= 0LL) && (4294967295LL + (long long )i) - (long long )temp >= 0LL) && (4294967295LL + (long long )j) - (long long )temp >= 0LL) && (4294967294LL - (long long )i) - (long long )j >= 0LL) && (4294967294LL - (long long )i) - (long long )temp >= 0LL) && (4294967294LL - (long long )j) - (long long )temp >= 0LL) format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i file_hash: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d line: 554 column: 12 function: SelectionSort value: 0 <= i format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i file_hash: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d line: 554 column: 12 function: SelectionSort value: 0 <= min format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i file_hash: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d line: 554 column: 12 function: SelectionSort value: i <= 2147483645 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i file_hash: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d line: 554 column: 12 function: SelectionSort value: array_size != 0 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i file_hash: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d line: 554 column: 12 function: SelectionSort value: array_size != 1 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca-2.i file_hash: ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d line: 554 column: 12 function: SelectionSort value: ((((((min <= 2147483646 && ((j != 1 && (((j != 2 && (((j != 3 && (((j != 4 && (((j != 5 && (((j != 6 && (((j != 7 && (((j != 8 && (((j != 9 && (((((((11 <= j && (-11LL + (long long )i) + (long long )j >= 0LL) && (-11LL - (long long )i) + (long long )j >= 0LL) && (11LL + (long long )i) - (long long )j >= 0LL) && j != 10) && (((((((12 <= array_size && j <= 2147483646) && (-23LL + (long long )array_size) + (long long )j >= 0LL) && (-12LL + (long long )array_size) + (long long )i >= 0LL) && (-12LL + (long long )array_size) - (long long )i >= 0LL) && (-1LL + (long long )array_size) - (long long )j >= 0LL) && j != 0) || ((((11 <= array_size && (-22LL + (long long )array_size) + (long long )j >= 0LL) && (-11LL + (long long )array_size) + (long long )i >= 0LL) && (-11LL + (long long )array_size) - (long long )i >= 0LL) && (long long )array_size - (long long )j >= 0LL))) || ((((((((((10 <= j && 11 <= array_size) && j <= 2147483646) && (-21LL + (long long )array_size) + (long long )j >= 0LL) && (-11LL + (long long )array_size) + (long long )i >= 0LL) && (-10LL + (long long )i) + (long long )j >= 0LL) && (-10LL - (long long )i) + (long long )j >= 0LL) && (-11LL + (long long )array_size) - (long long )i >= 0LL) && (-1LL + (long long )array_size) - (long long )j >= 0LL) && (10LL + (long long )i) - (long long )j >= 0LL) && j != 0)) || ((((((((10 <= array_size && 10 <= j) && (-20LL + (long long )array_size) + (long long )j >= 0LL) && (-10LL + (long long )array_size) + (long long )i >= 0LL) && (-10LL + (long long )i) + (long long )j >= 0LL) && (-10LL - (long long )i) + (long long )j >= 0LL) && (-10LL + (long long )array_size) - (long long )i >= 0LL) && (10LL + (long long )i) - (long long )j >= 0LL) && (long long )array_size - (long long )j >= 0LL))) || ((((((((((9 <= j && 10 <= array_size) && j <= 2147483646) && (-19LL + (long long )array_size) + (long long )j >= 0LL) && (-10LL + (long long )array_size) + (long long )i >= 0LL) && (-9LL + (long long )i) + (long long )j >= 0LL) && (-9LL - (long long )i) + (long long )j >= 0LL) && (-10LL + (long long )array_size) - (long long )i >= 0LL) && (-1LL + (long long )array_size) - (long long )j >= 0LL) && (9LL + (long long )i) - (long long )j >= 0LL) && j != 0)) || ((((((((9 <= array_size && 9 <= j) && (-18LL + (long long )array_size) + (long long )j >= 0LL) && (-9LL + (long long )array_size) + (long long )i >= 0LL) && (-9LL + (long long )i) + (long long )j >= 0LL) && (-9LL - (long long )i) + (long long )j >= 0LL) && (-9LL + (long long )array_size) - (long long )i >= 0LL) && (9LL + (long long )i) - (long long )j >= 0LL) && (long long )array_size - (long long )j >= 0LL))) || ((((((((((8 <= j && 9 <= array_size) && j <= 2147483646) && (-17LL + (long long )array_size) + (long long )j >= 0LL) && (-9LL + (long long )array_size) + (long long )i >= 0LL) && (-8LL + (long long )i) + (long long )j >= 0LL) && (-8LL - (long long )i) + (long long )j >= 0LL) && (-9LL + (long long )array_size) - (long long )i >= 0LL) && (-1LL + (long long )array_size) - (long long )j >= 0LL) && (8LL + (long long )i) - (long long )j >= 0LL) && j != 0)) || ((((((((8 <= array_size && 8 <= j) && (-16LL + (long long )array_size) + (long long )j >= 0LL) && (-8LL + (long long )array_size) + (long long )i >= 0LL) && (-8LL + (long long )i) + (long long )j >= 0LL) && (-8LL - (long long )i) + (long long )j >= 0LL) && (-8LL + (long long )array_size) - (long long )i >= 0LL) && (8LL + (long long )i) - (long long )j >= 0LL) && (long long )array_size - (long long )j >= 0LL))) || ((((((((((7 <= j && 8 <= array_size) && j <= 2147483646) && (-15LL + (long long )array_size) + (long long )j >= 0LL) && (-8LL + (long long )array_size) + (long long )i >= 0LL) && (-7LL + (long long )i) + (long long )j >= 0LL) && (-7LL - (long long )i) + (long long )j >= 0LL) && (-8LL + (long long )array_size) - (long long )i >= 0LL) && (-1LL + (long long )array_size) - (long long )j >= 0LL) && (7LL + (long long )i) - (long long )j >= 0LL) && j != 0)) || ((((((((7 <= array_size && 7 <= j) && (-14LL + (long long )array_size) + (long long )j >= 0LL) && (-7LL + (long long )array_size) + (long long )i >= 0LL) && (-7LL + (long long )i) + (long long )j >= 0LL) && (-7LL - (long long )i) + (long long )j >= 0LL) && (-7LL + (long long )array_size) - (long long )i >= 0LL) && (7LL + (long long )i) - (long long )j >= 0LL) && (long long )array_size - (long long )j >= 0LL))) || ((((((((((6 <= j && 7 <= array_size) && j <= 2147483646) && (-13LL + (long long )array_size) + (long long )j >= 0LL) && (-7LL + (long long )array_size) + (long long )i >= 0LL) && (-6LL + (long long )i) + (long long )j >= 0LL) && (-6LL - (long long )i) + (long long )j >= 0LL) && (-7LL + (long long )array_size) - (long long )i >= 0LL) && (-1LL + (long long )array_size) - (long long )j >= 0LL) && (6LL + (long long )i) - (long long )j >= 0LL) && j != 0)) || ((((((((6 <= array_size && 6 <= j) && (-12LL + (long long )array_size) + (long long )j >= 0LL) && (-6LL + (long long )array_size) + (long long )i >= 0LL) && (-6LL + (long long )i) + (long long )j >= 0LL) && (-6LL - (long long )i) + (long long )j >= 0LL) && (-6LL + (long long )array_size) - (long long )i >= 0LL) && (6LL + (long long )i) - (long long )j >= 0LL) && (long long )array_size - (long long )j >= 0LL))) || ((((((((((5 <= j && 6 <= array_size) && j <= 2147483646) && (-11LL + (long long )array_size) + (long long )j >= 0LL) && (-6LL + (long long )array_size) + (long long )i >= 0LL) && (-5LL + (long long )i) + (long long )j >= 0LL) && (-5LL - (long long )i) + (long long )j >= 0LL) && (-6LL + (long long )array_size) - (long long )i >= 0LL) && (-1LL + (long long )array_size) - (long long )j >= 0LL) && (5LL + (long long )i) - (long long )j >= 0LL) && j != 0)) || ((((((((5 <= array_size && 5 <= j) && (-10LL + (long long )array_size) + (long long )j >= 0LL) && (-5LL + (long long )array_size) + (long long )i >= 0LL) && (-5LL + (long long )i) + (long long )j >= 0LL) && (-5LL - (long long )i) + (long long )j >= 0LL) && (-5LL + (long long )array_size) - (long long )i >= 0LL) && (5LL + (long long )i) - (long long )j >= 0LL) && (long long )array_size - (long long )j >= 0LL))) || ((((((((((4 <= j && 5 <= array_size) && j <= 2147483646) && (-9LL + (long long )array_size) + (long long )j >= 0LL) && (-5LL + (long long )array_size) + (long long )i >= 0LL) && (-4LL + (long long )i) + (long long )j >= 0LL) && (-4LL - (long long )i) + (long long )j >= 0LL) && (-5LL + (long long )array_size) - (long long )i >= 0LL) && (-1LL + (long long )array_size) - (long long )j >= 0LL) && (4LL + (long long )i) - (long long )j >= 0LL) && j != 0)) || ((((((((4 <= array_size && 4 <= j) && (-8LL + (long long )array_size) + (long long )j >= 0LL) && (-4LL + (long long )array_size) + (long long )i >= 0LL) && (-4LL + (long long )i) + (long long )j >= 0LL) && (-4LL - (long long )i) + (long long )j >= 0LL) && (-4LL + (long long )array_size) - (long long )i >= 0LL) && (4LL + (long long )i) - (long long )j >= 0LL) && (long long )array_size - (long long )j >= 0LL))) || ((((((((((3 <= j && 4 <= array_size) && j <= 2147483646) && (-7LL + (long long )array_size) + (long long )j >= 0LL) && (-4LL + (long long )array_size) + (long long )i >= 0LL) && (-3LL + (long long )i) + (long long )j >= 0LL) && (-3LL - (long long )i) + (long long )j >= 0LL) && (-4LL + (long long )array_size) - (long long )i >= 0LL) && (-1LL + (long long )array_size) - (long long )j >= 0LL) && (3LL + (long long )i) - (long long )j >= 0LL) && j != 0)) || ((((((((3 <= array_size && 3 <= j) && (-6LL + (long long )array_size) + (long long )j >= 0LL) && (-3LL + (long long )array_size) + (long long )i >= 0LL) && (-3LL + (long long )i) + (long long )j >= 0LL) && (-3LL - (long long )i) + (long long )j >= 0LL) && (-3LL + (long long )array_size) - (long long )i >= 0LL) && (3LL + (long long )i) - (long long )j >= 0LL) && (long long )array_size - (long long )j >= 0LL))) || ((((((((((2 <= j && 3 <= array_size) && j <= 2147483646) && (-5LL + (long long )array_size) + (long long )j >= 0LL) && (-3LL + (long long )array_size) + (long long )i >= 0LL) && (-2LL + (long long )i) + (long long )j >= 0LL) && (-2LL - (long long )i) + (long long )j >= 0LL) && (-3LL + (long long )array_size) - (long long )i >= 0LL) && (-1LL + (long long )array_size) - (long long )j >= 0LL) && (2LL + (long long )i) - (long long )j >= 0LL) && j != 0)) || ((((((((2 <= array_size && 2 <= j) && (-4LL + (long long )array_size) + (long long )j >= 0LL) && (-2LL + (long long )array_size) + (long long )i >= 0LL) && (-2LL + (long long )i) + (long long )j >= 0LL) && (-2LL - (long long )i) + (long long )j >= 0LL) && (-2LL + (long long )array_size) - (long long )i >= 0LL) && (2LL + (long long )i) - (long long )j >= 0LL) && (long long )array_size - (long long )j >= 0LL))) || ((((((((((1 <= j && 2 <= array_size) && j <= 2147483646) && (-3LL + (long long )array_size) + (long long )j >= 0LL) && (-2LL + (long long )array_size) + (long long )i >= 0LL) && (-1LL + (long long )i) + (long long )j >= 0LL) && (-1LL - (long long )i) + (long long )j >= 0LL) && (-2LL + (long long )array_size) - (long long )i >= 0LL) && (-1LL + (long long )array_size) - (long long )j >= 0LL) && (1LL + (long long )i) - (long long )j >= 0LL) && j != 0))) || (((((((((((1 <= j && 2 <= array_size) && j <= 2147483646) && min <= 2147483645) && (-3LL + (long long )array_size) + (long long )j >= 0LL) && (-2LL + (long long )array_size) + (long long )i >= 0LL) && (-1LL + (long long )i) + (long long )j >= 0LL) && (-1LL - (long long )i) + (long long )j >= 0LL) && (-2LL + (long long )array_size) - (long long )i >= 0LL) && (-1LL + (long long )array_size) - (long long )j >= 0LL) && (1LL + (long long )i) - (long long )j >= 0LL) && i == min)) || ((((((((((((13 <= j && 14 <= array_size) && j <= 2147483646) && (-27LL + (long long )array_size) + (long long )j >= 0LL) && (-14LL + (long long )array_size) + (long long )i >= 0LL) && (-13LL + (long long )i) + (long long )j >= 0LL) && (-13LL - (long long )i) + (long long )j >= 0LL) && (-14LL + (long long )array_size) - (long long )i >= 0LL) && (-1LL + (long long )array_size) - (long long )j >= 0LL) && j != 0) && j != 1) && j != 2) && j != 3)) || ((((((((2 <= array_size && min <= 2147483645) && (-2LL + (long long )array_size) + (long long )i >= 0LL) && (2147483646LL + (long long )array_size) + (long long )j >= 0LL) && (2147483648LL + (long long )i) + (long long )j >= 0LL) && (2147483648LL - (long long )i) + (long long )j >= 0LL) && (-2LL + (long long )array_size) - (long long )i >= 0LL) && (2147483646LL + (long long )array_size) - (long long )j >= 0LL) && i == min)) || ((((((((((13 <= array_size && 13 <= j) && (-26LL + (long long )array_size) + (long long )j >= 0LL) && (-13LL + (long long )array_size) + (long long )i >= 0LL) && (-13LL + (long long )i) + (long long )j >= 0LL) && (-13LL - (long long )i) + (long long )j >= 0LL) && (-13LL + (long long )array_size) - (long long )i >= 0LL) && (long long )array_size - (long long )j >= 0LL) && j != 1) && j != 2) && j != 3)) || ((((((((((((((((((((((12 <= j && 13 <= array_size) && j <= 2147483646) && min <= 2147483646) && (-25LL + (long long )array_size) + (long long )j >= 0LL) && (-13LL + (long long )array_size) + (long long )i >= 0LL) && (-12LL + (long long )i) + (long long )j >= 0LL) && (-12LL - (long long )i) + (long long )j >= 0LL) && (-13LL + (long long )array_size) - (long long )i >= 0LL) && (-1LL + (long long )array_size) - (long long )j >= 0LL) && (12LL + (long long )i) - (long long )j >= 0LL) && j != 0) && j != 1) && j != 2) && j != 3) && j != 4) && j != 5) && j != 6) && j != 7) && j != 8) && j != 9) && j != 10) && j != 11)) || ((((((((((((((((((((12 <= array_size && 12 <= j) && min <= 2147483646) && (-24LL + (long long )array_size) + (long long )j >= 0LL) && (-12LL + (long long )array_size) + (long long )i >= 0LL) && (-12LL + (long long )i) + (long long )j >= 0LL) && (-12LL - (long long )i) + (long long )j >= 0LL) && (-12LL + (long long )array_size) - (long long )i >= 0LL) && (12LL + (long long )i) - (long long )j >= 0LL) && (long long )array_size - (long long )j >= 0LL) && j != 1) && j != 2) && j != 3) && j != 4) && j != 5) && j != 6) && j != 7) && j != 8) && j != 9) && j != 10) && j != 11) format: c_expression | correctness_witness | CPAchecker 2.3 | 30 | 2023-12-01T05:12:53+01:00 |
Found 22 witnesses for program sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca_true-termination.c.i, ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
77e9e1e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-29T02:47:54+01:00 | be1f2f5 | |
95328cc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T10:54:27+01:00 | 4d4ea81 | |
b661269 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.1 | 4 | 2022-12-25T09:30:53+01:00 | ||
b32c53d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.0 | 4 | 2022-12-11T04:22:54+01:00 | ||
b9c5efd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 4 | 2022-12-09T21:05:04+01:00 | ||
623baa3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-11T01:54:46+01:00 | ||
9691b62 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T12:54:31Z | ||
2dc499e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 14 | 2022-12-14T07:31:22Z | ||
3d3e7bd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2022-12-11T11:03:44Z | ||
bae0a36 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp23-0-g4f5dcf38f) | 87 | 2022-12-10T07:31:56Z | ||
8310d1e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T11:12:04+01:00 | 2dc499e | |
7e69bec | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T07:20:30+01:00 | 52ae568 | |
1cd80fa | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T03:46:41+01:00 | 3d3e7bd | |
f1371a7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T00:53:56+01:00 | b32c53d | |
6668a88 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T22:51:22+01:00 | 623baa3 | |
d3f57d1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T22:36:54+01:00 | bae0a36 | |
45e205f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T21:08:42+01:00 | b9c5efd | |
cf47715 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T17:38:27+01:00 | 9691b62 | |
5c43e11 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T02:21:49+01:00 | b661269 | |
4d4ea81 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2022-12-10T16:04:48+01:00 | ||
be1f2f5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 7 | 2022-12-11T21:54:09+01:00 | ||
52ae568 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 15 | 2022-12-13T10:38:24Z |
Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca_true-termination.c.i, ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3327d70 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T17:25:53 |
Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca_true-termination.c.i, ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e6be4bb | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T23:09:45 | ||
431b25e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-09T01:18:21 |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca_true-termination.c.i, ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca_true-termination.c.i, ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca_true-termination.c.i, ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
07ba7b9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 11 | 2017-12-01T18:36 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca_true-termination.c.i, ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |