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

View and Validate the Witness

Input Given to this Service about the Witness (URL Query)

Key Value
programName sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c
programSHA 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539
witnessName results-verified/utaipan.2017-12-03_0843.logfiles/sv-comp18.Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c.files/witness.graphml
witnessSHA 9fa282310ee1d6898f5618eef4fc9f156c26a9c693328f25da94bcdde8c19294

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/9fa282310ee1d6898f5618eef4fc9f156c26a9c693328f25da94bcdde8c19294.json

Key Value
architecture 64bit
creationtime 2017-12-03T07:44Z
producer Taipan
program-sha256 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539
programfile /tmp/vcloud-vcloud-master/worker/working_dir_4bdda5f0-da0e-41b4-85bc-971ef84dc9ba/sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c
programhash 282a32bc5fb3d70423f87a450340f7a26ab0f093
sourcecodelang C
specification CHECK( init(main()), LTL(G ! overflow) )
witness-file witnessFileByHash/9fa282310ee1d6898f5618eef4fc9f156c26a9c693328f25da94bcdde8c19294.graphml
witness-sha256 9fa282310ee1d6898f5618eef4fc9f156c26a9c693328f25da94bcdde8c19294
witness-size 8638
witness-type correctness_witness

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

Trying to find witnesses for program (302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539, sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 40 witnesses for program sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c, 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e2ee727 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T09:05:55+01:00
Download 2486804 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2023-12-17T03:56:52Z
Download 128c33c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2023-11-29T20:58:12Z
Download 9e942b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 36 2023-12-18T12:03:39+01:00 Download e2ee727
Download 3c2f0aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 7 2023-11-30T07:52:48+01:00
Download 0f104d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 7 2023-12-03T20:56:38+01:00
Download 2b3c1bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 8 2023-12-18T01:34:32+01:00
Download 1e73494 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 11 2023-12-02T18:50:01Z
Download 954f265 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T06:37:28Z
Download 0c7db53 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 33 2023-12-01T00:58:03Z
Download bac500f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Automizer 11 2023-11-29T03:14:16Z
Download d1670c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness 2LS 16 2023-11-30T21:03:45+01:00
Download 51eea33 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 7 2023-12-18T17:10:59+01:00
Download d1f8920 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.4.0 3 2023-12-03T07:59:04Z
Download a1a9755 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:37 CET (comp)
Download 8df8a8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 12 2023-12-02T12:33:03Z
Download e3c53b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T12:20:03Z
Download c39679c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 34 2023-12-01T01:15:23Z
Download 38eab2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-20T03:41:10+01:00 Download a1a9755
Download 8255968 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-19T14:35:05+01:00 Download 076d4db
Download c451509 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-19T04:06:24+01:00 Download 8348044
Download 9116217 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-17T06:09:18+01:00 Download 6aa10fe
Download 4be1fbd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-04T11:44:05+01:00 Download 8df8a8e
Download e637915 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-04T01:16:35+01:00 Download 6de5520
Download e991cb0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-03T09:54:39+01:00 Download d1f8920
Download 564d706 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-01T03:44:53+01:00 Download c39679c
Download a29aeb9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-11-30T23:46:17+01:00 Download 559bb7c
Download 9d026b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-11-30T11:59:19+01:00 Download ea7883f
Download ea7883f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-11-30T05:25:25+01:00
Download 962171c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-11-29T18:26:08+01:00 Download e3c53b4
Download 11620d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-11-29T08:19:50+01:00 Download 49a6b66
Download 6de5520 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 6 2023-12-03T22:33:57+01:00
Download 6aa10fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 6 2023-12-17T03:35:28+01:00
Download 8348044 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2023-12-18T18:10:08+01:00
Download 49a6b66 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 12 2023-11-29T01:48:14Z
Download 559bb7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 13 2023-11-30T22:36:58+01:00
Download 187b568 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 13 2023-11-30T21:47:28+01:00
Download 6247dc4 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: e5b30cb7-0726-4d61-88ad-4129131aad76 creation_time: '2023-11-29T02:48:14+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7acad84b-79a5-4732-8cbc-5232c6fdf22b/sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex-2.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7acad84b-79a5-4732-8cbc-5232c6fdf22b/sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex-2.c : 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539 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_7acad84b-79a5-4732-8cbc-5232c6fdf22b/sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex-2.c file_hash: 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539 line: 15 column: 0 function: main value: ((0 < i) || (i == 0)) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7acad84b-79a5-4732-8cbc-5232c6fdf22b/sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex-2.c file_hash: 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539 line: 22 column: 0 function: main value: (((0 <= k) && (x <= (2147483647 + k))) && (k <= 1047)) format: c_expression correctness_witness CPAchecker 2.3 8 2023-11-29T07:49:17+01:00
Download ab5c446 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 7fed7fd3-6dd0-47d6-92f5-8d76a9711362 creation_time: '2023-12-02T13:33:03+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_208e41b4-6b19-4cbe-9767-7b90369fb34b/sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex-2.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_208e41b4-6b19-4cbe-9767-7b90369fb34b/sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex-2.c : 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539 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_208e41b4-6b19-4cbe-9767-7b90369fb34b/sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex-2.c file_hash: 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539 line: 15 column: 0 function: main value: ((((0 <= (k + 2147483648)) && (1 <= i)) && (k <= 2147483647)) || (((0 <= (k + 2147483648)) && (i == 0)) && (k <= 2147483647))) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_208e41b4-6b19-4cbe-9767-7b90369fb34b/sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex-2.c file_hash: 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539 line: 22 column: 0 function: main value: ((((0 <= k) && (x <= 2147483647)) && (k <= 1047)) && (0 <= (x + 2147483648))) format: c_expression correctness_witness CPAchecker 2.3 8 2023-12-04T11:57:44+01:00
Download 6c15dba Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: b0e9de7c-3d16-4791-b3a8-7cd07bba1c3b creation_time: 2023-12-01T01:15:23Z 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-crafted/Arrays03-ValueRestictsIndex-2.c''' task: input_files: - ../../sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex-2.c input_file_hashes: ../../sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex-2.c: 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex-2.c file_hash: 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539 line: 22 column: 9 function: main value: 0 <= k format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex-2.c file_hash: 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539 line: 22 column: 9 function: main value: k <= 1047 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex-2.c file_hash: 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539 line: 22 column: 9 function: main value: (-1048LL + (long long )i) + (long long )k >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex-2.c file_hash: 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539 line: 22 column: 9 function: main value: (1048LL - (long long )i) + (long long )k >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex-2.c file_hash: 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539 line: 22 column: 9 function: main value: (-1LL + (long long )i) - (long long )k >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex-2.c file_hash: 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539 line: 22 column: 9 function: main value: (2095LL - (long long )i) - (long long )k >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex-2.c file_hash: 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539 line: 22 column: 9 function: main value: i == 1048 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex-2.c file_hash: 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539 line: 15 column: 6 function: main value: ((((((((((((8 <= i && i <= 1048) && (2147483640LL + (long long )i) + (long long )x >= 0LL) && (2147484696LL - (long long )i) + (long long )x >= 0LL) && (2147483639LL + (long long )i) - (long long )x >= 0LL) && (2147484695LL - (long long )i) - (long long )x >= 0LL) || (((((2147483641LL + (long long )i) + (long long )x >= 0LL && (2147483655LL - (long long )i) + (long long )x >= 0LL) && (2147483640LL + (long long )i) - (long long )x >= 0LL) && (2147483654LL - (long long )i) - (long long )x >= 0LL) && i == 7)) || (((((2147483642LL + (long long )i) + (long long )x >= 0LL && (2147483654LL - (long long )i) + (long long )x >= 0LL) && (2147483641LL + (long long )i) - (long long )x >= 0LL) && (2147483653LL - (long long )i) - (long long )x >= 0LL) && i == 6)) || (((((2147483643LL + (long long )i) + (long long )x >= 0LL && (2147483653LL - (long long )i) + (long long )x >= 0LL) && (2147483642LL + (long long )i) - (long long )x >= 0LL) && (2147483652LL - (long long )i) - (long long )x >= 0LL) && i == 5)) || (((((2147483644LL + (long long )i) + (long long )x >= 0LL && (2147483652LL - (long long )i) + (long long )x >= 0LL) && (2147483643LL + (long long )i) - (long long )x >= 0LL) && (2147483651LL - (long long )i) - (long long )x >= 0LL) && i == 4)) || (((((2147483645LL + (long long )i) + (long long )x >= 0LL && (2147483651LL - (long long )i) + (long long )x >= 0LL) && (2147483644LL + (long long )i) - (long long )x >= 0LL) && (2147483650LL - (long long )i) - (long long )x >= 0LL) && i == 3)) || (((((2147483646LL + (long long )i) + (long long )x >= 0LL && (2147483650LL - (long long )i) + (long long )x >= 0LL) && (2147483645LL + (long long )i) - (long long )x >= 0LL) && (2147483649LL - (long long )i) - (long long )x >= 0LL) && i == 2)) || (((((2147483647LL + (long long )i) + (long long )x >= 0LL && (2147483649LL - (long long )i) + (long long )x >= 0LL) && (2147483646LL + (long long )i) - (long long )x >= 0LL) && (2147483648LL - (long long )i) - (long long )x >= 0LL) && i == 1)) || ((((((2147483648LL + (long long )i) + (long long )x >= 0LL && (2147483648LL - (long long )i) + (long long )x >= 0LL) && (2147483647LL + (long long )i) - (long long )x >= 0LL) && (2147483647LL - (long long )i) - (long long )x >= 0LL) && 0 == i) && i == 0) format: c_expression correctness_witness CPAchecker 2.3 13 2023-12-01T05:08:52+01:00

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

Trying to find witnesses for program (302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539, sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 36 witnesses for program sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c, 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3e215be Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T06:55:47+01:00
Download bceb002 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2022-12-25T12:20:10Z
Download a71c900 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2022-12-12T16:05:50Z
Download 24307c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 36 2023-01-28T14:14:35+01:00 Download 3e215be
Download d3bce21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 7 2022-12-10T21:12:40+01:00
Download 1a2ec0d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 7 2022-12-11T23:08:25+01:00
Download f407be6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 7 2022-12-10T04:01:11+01:00
Download 46129f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 8 2022-12-09T03:22:03+01:00
Download 190ff4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 10 2022-12-14T11:41:15Z
Download 4e251b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T11:04:18Z
Download f97c0cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Automizer 10 2022-12-13T17:19:34Z
Download 7bf47de Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness 2LS 16 2022-12-07T21:44:18+01:00
Download 724e119 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.4.0 3 2022-12-09T10:49:55Z
Download a1a9755 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T11:01 CET (comp)
Download 569cae5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 12 2022-12-14T12:31:08Z
Download 8b8337b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T11:46:30Z
Download 1459652 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp23-0-g4f5dcf38f) 79 2022-12-10T07:50:01Z
Download 3fba8fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-29T11:32:15+01:00 Download a1a9755
Download 69676a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-29T11:07:44+01:00 Download 569cae5
Download 79f4092 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-29T07:20:25+01:00 Download 6397d6a
Download ee93a87 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-29T03:49:02+01:00 Download 8b8337b
Download eb0217c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-29T02:35:30+01:00 Download 3ba8545
Download 490bd0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-29T00:06:32+01:00 Download 6803ff3
Download e034122 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-28T22:38:49+01:00 Download 1459652
Download a3640da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-28T18:19:52+01:00 Download 58607fe
Download 3cb6c43 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-28T17:38:12+01:00 Download 724e119
Download cebf5d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-28T11:07:18+01:00 Download 95799a6
Download b317936 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-28T00:31:06+01:00 Download 23f303a
Download 12fda35 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-27T23:00:47+01:00 Download 98a3cf7
Download 95799a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2022-12-10T19:55:24+01:00
Download 3ba8545 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 6 2022-12-12T00:07:06+01:00
Download 23f303a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 6 2022-12-25T13:29:31+01:00
Download 58607fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2022-12-10T01:19:41+01:00
Download 6397d6a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 11 2022-12-13T09:56:25Z
Download 98a3cf7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 13 2022-12-07T22:07:55+01:00
Download ed251fb Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 13 2022-12-08T00:37:53+01:00

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

Trying to find witnesses for program (302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539, sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 26 witnesses for program sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c, 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ca09af3 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2021-12-07T09:28:58+01:00
Download 65b011b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2021-12-07T12:23:24Z
Download 1470415 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 7 2021-12-05T15:58:40+01:00
Download e540bfa Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 7 2021-12-08T20:32:13+01:00
Download 97592c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 7 2021-12-09T13:34:56+01:00
Download d5f485c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 8 2021-12-07T02:06:18+01:00
Download c44b0e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 10 2021-12-10T00:10:21Z
Download 78a45fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Automizer 10 2021-12-07T00:40:39Z
Download ab8d9db Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness 2LS 15 2021-12-05T22:51:32+01:00
Download 9c64dd0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.2.8 3 2021-12-13T20:21:19Z
Download e24318a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 12 2021-12-10T02:50:05Z
Download 5d01f86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 6 2021-12-14T00:23:41+01:00 Download 9c64dd0
Download 52c2d1f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 6 2021-12-10T21:00:56+01:00 Download 3e007bd
Download 3f9aaf5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 6 2021-12-10T08:38:48+01:00 Download e24318a
Download 857fb11 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 6 2021-12-09T15:39:37+01:00 Download 8d00c2d
Download 1fe03f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 6 2021-12-08T22:16:07+01:00 Download f281b13
Download d23eead Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 6 2021-12-07T02:52:08+01:00 Download 6d2f63d
Download 8cf1166 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 6 2021-12-06T01:17:46+01:00 Download 7765a96
Download 7eba633 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 6 2021-12-05T20:24:12+01:00 Download 8786434
Download 8786434 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 6 2021-12-05T16:13:42+01:00
Download 3e007bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 6 2021-12-10T19:22:00+01:00
Download f281b13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 6 2021-12-08T20:02:12+01:00
Download 8d00c2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 6 2021-12-09T13:49:25+01:00
Download 6d2f63d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 11 2021-12-06T20:05:09Z
Download 7765a96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 13 2021-12-05T19:43:11+01:00
Download 50b6a17 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 12 2021-12-06T00:34:21+01:00

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

Trying to find witnesses for program (302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539, sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 12 witnesses for program sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c, 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4efdf86 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2020-12-06T18:43:20+01:00
Download 5a603aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 7 2020-12-07T22:43:21+01:00
Download dbf14d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0 7 2020-12-05T15:52:16+01:00
Download d44f5b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.1 3 2020-12-06T23:46:24
Download 175e52b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) unknown_witness Goblint (svcomp21-0-g82e03b87) 3 2020-12-07T17:18:21
Download 254f57f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 6 2020-12-09T21:21:52+01:00 Download 353b026
Download 9fa4b2b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 6 2020-12-09T02:14:58+01:00 Download 758392a
Download be7314c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 6 2020-12-08T06:22:27+01:00 Download 652760d
Download 109c57d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 6 2020-12-06T16:59:33+01:00 Download a9732b0
Download 54ebe09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 6 2020-12-06T13:47:41+01:00 Download ee58026
Download ee58026 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 6 2020-12-05T17:21:00+01:00
Download 652760d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 6 2020-12-08T05:20:15+01:00

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

Trying to find witnesses for program (302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539, sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 4 witnesses for program sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c, 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8395cc3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 7 2019-11-29T23:31:49+01:00
Download 13fe4f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 7 2019-12-01T18:24:54+01:00
Download cc3084f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 757 2019-11-30T11:26:51+01:00
Download 71b2987 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 757 2019-12-01T12:08:56+01:00

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

Trying to find witnesses for program (302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539, sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 2 witnesses for program sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c, 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b6980de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 873 2018-12-07T04:13:18+01:00
Download fc63732 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 873 2018-12-05T13:27:31+01:00

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

Trying to find witnesses for program (302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539, sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 8 witnesses for program sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c, 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 9fa2823 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 9 2017-12-03T07:44Z
Download df65d26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 9 2017-12-03T10:34Z
Download 30d80e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T18:44:08.471175
Download 068237b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 3.1 7 2017-12-01T13:20 CET (sv-comp)
Download b5e5732 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 8 2017-12-03T10:17Z
Download 45b8b78 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 12 2017-12-01T10:49 CET (sv-comp)
Download 961168f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 7 2017-12-01T15:56 CET (sv-comp)
Download 0c51132 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 12 2017-12-01T15:18 CET (sv-comp)

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

Trying to find witnesses for program (302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539, sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c, 302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/302c18c494f9017ecbb07643194b1d54ba0a6bba467355d4f775638dea57e539.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness