Witness Inspection

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).

This link does not point to a witness, but below is a list of witnesses for the same program.

Available Results for the Program from Witness Store SV-COMP '24

Trying to find witnesses for program (ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d, sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca_true-termination.c.i).

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
Download 82a5b8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 6 2023-12-04T01:19:05+01:00 Download 507169c
Download 7b672cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 6 2023-11-30T12:02:08+01:00 Download 769c46d
Download bfccbf7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 4 2023-12-17T03:43:06+01:00
Download 0801e0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 4 2023-12-19T12:01:55+01:00
Download 44ec720 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 4 2023-12-18T20:35:43+01:00
Download c3b8a9b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:22:14+01:00
Download c80f4c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.4.0 3 2023-12-03T08:06:22Z
Download 5a93caa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 15 2023-12-02T17:19:55Z
Download a5a08c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T09:51:41Z
Download a28f511 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 25 2023-12-01T01:16:02Z
Download 1f991c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 7 2023-12-19T15:34:13+01:00 Download 0801e0e
Download 6f19ed2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 7 2023-12-19T05:26:36+01:00 Download 44ec720
Download e4ebdcb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 7 2023-12-17T06:38:08+01:00 Download bfccbf7
Download 8d3ecc9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 7 2023-12-04T11:38:25+01:00 Download 5a93caa
Download e9c85bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 7 2023-12-03T18:31:06+01:00 Download c3b8a9b
Download 75538ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 7 2023-12-03T09:54:38+01:00 Download c80f4c7
Download d707b26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 7 2023-12-01T03:42:06+01:00 Download a28f511
Download 769c46d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 7 2023-11-30T08:14:45+01:00
Download 41bacbe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 7 2023-11-29T18:11:49+01:00 Download a5a08c6
Download 4eda49d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 7 2023-11-29T08:07:17+01:00 Download 4634e0d
Download 507169c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 7 2023-12-03T21:09:39+01:00
Download 4634e0d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 15 2023-11-28T23:31:16Z
Download cb833e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 3 2023-12-01T01:12:52Z
Download 0757701 Inspect Inspect
Validate
- 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
Download 96a6434 Inspect Inspect
Validate
- 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
Download dd639ff Inspect Inspect
Validate
- 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

Available Results for the Program from Witness Store SV-COMP '23

Trying to find witnesses for program (ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d, sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca_true-termination.c.i).

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
Download 77e9e1e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-29T02:47:54+01:00 Download be1f2f5
Download 95328cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-28T10:54:27+01:00 Download 4d4ea81
Download b661269 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 4 2022-12-25T09:30:53+01:00
Download b32c53d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 4 2022-12-11T04:22:54+01:00
Download b9c5efd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 4 2022-12-09T21:05:04+01:00
Download 623baa3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-11T01:54:46+01:00
Download 9691b62 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.4.0 3 2022-12-09T12:54:31Z
Download 2dc499e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 14 2022-12-14T07:31:22Z
Download 3d3e7bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T11:03:44Z
Download bae0a36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp23-0-g4f5dcf38f) 87 2022-12-10T07:31:56Z
Download 8310d1e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 7 2023-01-29T11:12:04+01:00 Download 2dc499e
Download 7e69bec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 7 2023-01-29T07:20:30+01:00 Download 52ae568
Download 1cd80fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 7 2023-01-29T03:46:41+01:00 Download 3d3e7bd
Download f1371a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 7 2023-01-29T00:53:56+01:00 Download b32c53d
Download 6668a88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 7 2023-01-28T22:51:22+01:00 Download 623baa3
Download d3f57d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 7 2023-01-28T22:36:54+01:00 Download bae0a36
Download 45e205f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 7 2023-01-28T21:08:42+01:00 Download b9c5efd
Download cf47715 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 7 2023-01-28T17:38:27+01:00 Download 9691b62
Download 5c43e11 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 7 2023-01-28T02:21:49+01:00 Download b661269
Download 4d4ea81 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 7 2022-12-10T16:04:48+01:00
Download be1f2f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 7 2022-12-11T21:54:09+01:00
Download 52ae568 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 15 2022-12-13T10:38:24Z

Available Results for the Program from Witness Store SV-COMP '22

Trying to find witnesses for program (ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d, sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca_true-termination.c.i).

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
Download 3327d70 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2021-12-10T17:25:53

Available Results for the Program from Witness Store SV-COMP '21

Trying to find witnesses for program (ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d, sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca_true-termination.c.i).

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
Download e6be4bb Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-11T23:09:45
Download 431b25e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-09T01:18:21

Available Results for the Program from Witness Store SV-COMP '20

Trying to find witnesses for program (ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d, sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca_true-termination.c.i).

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

Available Results for the Program from Witness Store SV-COMP '19

Trying to find witnesses for program (ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d, sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca_true-termination.c.i).

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

Available Results for the Program from Witness Store SV-COMP '18

Trying to find witnesses for program (ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d, sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca_true-termination.c.i).

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
Download 07ba7b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 11 2017-12-01T18:36 CET (sv-comp)

Available Results for the Program from Witness Store SV-COMP '17

Trying to find witnesses for program (ffc745103ed55cbf924659873c1ffa566d33874f07e41d755dd0e85e8b4a5c0d, sv-benchmarks/c/termination-memory-alloca/selectionsort-alloca_true-termination.c.i).

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