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/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c
programSHA f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
witnessName results-verified/map2check.2018-12-06_1220.logfiles/sv-comp19_prop-memsafety.ArraysOfVariableLength4_true-valid-memsafety_true-termination.c.files/witness.graphml
witnessSHA c9bca6e7ff808032bc0e90941fd3fa0cfb37e5e131365aee2719844949455784

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/c9bca6e7ff808032bc0e90941fd3fa0cfb37e5e131365aee2719844949455784.json

Key Value
architecture 32bit
creationtime 2018-12-06T12:50 CET (sv-comp)
error-specification-length Key 'specification' longer than 100 characters.
producer Map2Check
programfile /tmp/vcloud-vcloud-master/worker/working_dir_58d4f932-1730-4742-8e7b-4d2129815858/bin-2019/map2check/../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c
programhash 97fe3d28a1849ecc88958d9d302f4fb4c5dbb992
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) )
witness-file witnessFileByHash/c9bca6e7ff808032bc0e90941fd3fa0cfb37e5e131365aee2719844949455784.graphml
witness-sha256 c9bca6e7ff808032bc0e90941fd3fa0cfb37e5e131365aee2719844949455784
witness-size 2216
witness-type correctness_witness

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

Trying to find witnesses for program (f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df, sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c).

Found 55 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c, f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fe59110 Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2023-12-18T10:41:18+01:00
Download 4fe86eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2023-11-29T19:23:07Z
Download 9c0b659 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 7 2023-11-30T08:03:17+01:00
Download ee521a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 7 2023-12-03T22:18:00+01:00
Download 520ff52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 10 2023-12-18T01:35:40+01:00
Download ec695e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-05T12:35:07Z
Download 1886ebd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-04T13:18:14Z
Download 54d7ab5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-01T21:06:39Z
Download b651ee6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 7.4.0 incr 3 2023-12-01T13:58:28Z
Download 08bdd98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 7 2023-12-19T01:13:36+01:00
Download 01b69bc 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 13 2023-12-02T14:13:32Z
Download 6e5d4e6 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 PredatorHP 4 2023-11-30T08:24:56Z
Download dce0358 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-29T15:27:25Z
Download 217ce36 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 CBMC 738 2023-12-17T17:32:07+01:00
Download ce08af3 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 13 2023-11-29T06:10:30Z
Download 330b486 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 8 2023-12-17T21:50:50+01:00 Download 4efda52
Download c0048af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:40:30+01:00
Download aaedb50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.4.0 3 2023-12-03T06:40:50Z
Download 3e3f079 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:37 CET (comp)
Download cf20f4d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 13 2023-12-02T12:32:20Z
Download 9e23193 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2023-12-17T04:04:21Z
Download b9228fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2023-11-29T19:49:37Z
Download ab2bc58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2023-12-19T21:19:03
Download 02a6e56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T14:03:22Z
Download 57955c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 7.4.0 kind 3 2023-12-01T16:57:17Z
Download 5a061ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-20T02:16:38+01:00 Download ab2bc58
Download 10fa91f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-17T06:24:06+01:00 Download 9e23193
Download e1c083f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-05T14:20:44+01:00 Download b1c3f30
Download 4dea057 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-04T16:29:28+01:00 Download cbbe10c
Download 9bcbe44 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-04T11:30:35+01:00 Download cf20f4d
Download b07b019 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-03T18:35:36+01:00 Download c0048af
Download 52d3242 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-03T09:54:01+01:00 Download aaedb50
Download 32667f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-01T22:47:08+01:00 Download 5d55f59
Download 35b66e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-01T18:11:44+01:00 Download 57955c4
Download f01acad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-30T05:34:43+01:00
Download af4f7da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-30T02:43:09+01:00 Download b9228fe
Download 8703ef2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-29T18:21:16+01:00 Download 02a6e56
Download 3a407c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-29T07:56:06+01:00 Download 3372908
Download 56d86da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 8 2023-12-04T00:04:46+01:00
Download a441f14 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 8 2023-12-18T17:47:44+01:00
Download 4efda52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 725 2023-12-17T15:46:59+01:00
Download b1c3f30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-05T10:31:07Z
Download cbbe10c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-04T14:52:31Z
Download 5d55f59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-01T19:50:58Z
Download 3372908 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 14 2023-11-29T03:00:39Z
Download 88b7de6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.4.0 3 2023-12-01T14:18:57Z
Download 6c28908 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2023-11-29T21:43:40Z
Download ba85deb Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2023-12-19T22:03:43
Download 514d11a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 725 2023-12-17T08:59:11+01:00
Download 1d11e6f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-05T08:56:56Z
Download cd10ff6 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-04T09:45:16Z
Download f12541e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-01T21:08:48Z
Download ab3bd88 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: f927e826-4cd2-4f6a-97e5-ba55fc83f675 creation_time: '2023-11-29T04:00:39+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_836b4165-b4a3-45ec-807c-75d7bad9e6b4/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_836b4165-b4a3-45ec-807c-75d7bad9e6b4/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c : f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 32bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_836b4165-b4a3-45ec-807c-75d7bad9e6b4/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df line: 25 column: 0 function: main value: ((i <= 2147483646) && (0 <= (i + 2147483648))) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_836b4165-b4a3-45ec-807c-75d7bad9e6b4/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df line: 28 column: 0 function: main value: ((i <= 2147483644) && (0 <= (i + 2147483648))) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_836b4165-b4a3-45ec-807c-75d7bad9e6b4/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df line: 15 column: 0 function: foo value: (((((((i % 4294967296) <= 31) && (32 == size)) && (0 <= (i + 2147483648))) && (i == 0)) && (i <= 2147483645)) || ((((((i % 4294967296) <= 31) && (0 <= (i + 2147483648))) && (size <= 32)) && (1 <= i)) && (i <= 2147483645))) format: c_expression correctness_witness CPAchecker 2.3 10 2023-11-29T07:49:01+01:00
Download a7a7506 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 4ad5c713-554c-4e45-a69b-e98bd1fbdfa9 creation_time: '2023-12-02T13:32:20+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7697a523-fb04-425e-87d3-0cbde9b52736/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7697a523-fb04-425e-87d3-0cbde9b52736/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c : f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 32bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7697a523-fb04-425e-87d3-0cbde9b52736/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df line: 25 column: 0 function: main value: ((0 <= i) && (i <= 2147483647)) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7697a523-fb04-425e-87d3-0cbde9b52736/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df line: 28 column: 0 function: main value: ((0 <= i) && (i <= 2147483645)) format: c_expression correctness_witness CPAchecker 2.3 9 2023-12-04T12:03:29+01:00
Download e673554 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: d2312ea7-1808-4581-9c5e-b259eadc6e5f creation_time: 2023-12-01T01:58: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'' ''32bit'' ''../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c''' task: input_files: - ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c input_file_hashes: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df data_model: ILP32 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df line: 15 column: 8 function: foo value: 32 == size format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df line: 15 column: 8 function: foo value: size == 32 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df line: 15 column: 8 function: foo value: (((((((((((((((((((((((((((12 <= i && (-44LL + (long long )i) + (long long )size >= 0LL) && (20LL + (long long )i) - (long long )size >= 0LL) && (((i <= 31 && (-1LL - (long long )i) + (long long )size >= 0LL) && (63LL - (long long )i) - (long long )size >= 0LL) || ((i <= 32 && (0LL - (long long )i) + (long long )size >= 0LL) && (64LL - (long long )i) - (long long )size >= 0LL))) || (((((-43LL + (long long )i) + (long long )size >= 0LL && (-21LL - (long long )i) + (long long )size >= 0LL) && (21LL + (long long )i) - (long long )size >= 0LL) && (43LL - (long long )i) - (long long )size >= 0LL) && i == 11)) || (((((-43LL + (long long )i) + (long long )size >= 0LL && (-21LL - (long long )i) + (long long )size >= 0LL) && (21LL + (long long )i) - (long long )size >= 0LL) && (43LL - (long long )i) - (long long )size >= 0LL) && i == 11)) || (((((-42LL + (long long )i) + (long long )size >= 0LL && (-22LL - (long long )i) + (long long )size >= 0LL) && (22LL + (long long )i) - (long long )size >= 0LL) && (42LL - (long long )i) - (long long )size >= 0LL) && i == 10)) || (((((-42LL + (long long )i) + (long long )size >= 0LL && (-22LL - (long long )i) + (long long )size >= 0LL) && (22LL + (long long )i) - (long long )size >= 0LL) && (42LL - (long long )i) - (long long )size >= 0LL) && i == 10)) || (((((-41LL + (long long )i) + (long long )size >= 0LL && (-23LL - (long long )i) + (long long )size >= 0LL) && (23LL + (long long )i) - (long long )size >= 0LL) && (41LL - (long long )i) - (long long )size >= 0LL) && i == 9)) || (((((-41LL + (long long )i) + (long long )size >= 0LL && (-23LL - (long long )i) + (long long )size >= 0LL) && (23LL + (long long )i) - (long long )size >= 0LL) && (41LL - (long long )i) - (long long )size >= 0LL) && i == 9)) || (((((-40LL + (long long )i) + (long long )size >= 0LL && (-24LL - (long long )i) + (long long )size >= 0LL) && (24LL + (long long )i) - (long long )size >= 0LL) && (40LL - (long long )i) - (long long )size >= 0LL) && i == 8)) || (((((-40LL + (long long )i) + (long long )size >= 0LL && (-24LL - (long long )i) + (long long )size >= 0LL) && (24LL + (long long )i) - (long long )size >= 0LL) && (40LL - (long long )i) - (long long )size >= 0LL) && i == 8)) || (((((-39LL + (long long )i) + (long long )size >= 0LL && (-25LL - (long long )i) + (long long )size >= 0LL) && (25LL + (long long )i) - (long long )size >= 0LL) && (39LL - (long long )i) - (long long )size >= 0LL) && i == 7)) || (((((-39LL + (long long )i) + (long long )size >= 0LL && (-25LL - (long long )i) + (long long )size >= 0LL) && (25LL + (long long )i) - (long long )size >= 0LL) && (39LL - (long long )i) - (long long )size >= 0LL) && i == 7)) || (((((-38LL + (long long )i) + (long long )size >= 0LL && (-26LL - (long long )i) + (long long )size >= 0LL) && (26LL + (long long )i) - (long long )size >= 0LL) && (38LL - (long long )i) - (long long )size >= 0LL) && i == 6)) || (((((-38LL + (long long )i) + (long long )size >= 0LL && (-26LL - (long long )i) + (long long )size >= 0LL) && (26LL + (long long )i) - (long long )size >= 0LL) && (38LL - (long long )i) - (long long )size >= 0LL) && i == 6)) || (((((-37LL + (long long )i) + (long long )size >= 0LL && (-27LL - (long long )i) + (long long )size >= 0LL) && (27LL + (long long )i) - (long long )size >= 0LL) && (37LL - (long long )i) - (long long )size >= 0LL) && i == 5)) || (((((-37LL + (long long )i) + (long long )size >= 0LL && (-27LL - (long long )i) + (long long )size >= 0LL) && (27LL + (long long )i) - (long long )size >= 0LL) && (37LL - (long long )i) - (long long )size >= 0LL) && i == 5)) || (((((-36LL + (long long )i) + (long long )size >= 0LL && (-28LL - (long long )i) + (long long )size >= 0LL) && (28LL + (long long )i) - (long long )size >= 0LL) && (36LL - (long long )i) - (long long )size >= 0LL) && i == 4)) || (((((-36LL + (long long )i) + (long long )size >= 0LL && (-28LL - (long long )i) + (long long )size >= 0LL) && (28LL + (long long )i) - (long long )size >= 0LL) && (36LL - (long long )i) - (long long )size >= 0LL) && i == 4)) || (((((-35LL + (long long )i) + (long long )size >= 0LL && (-29LL - (long long )i) + (long long )size >= 0LL) && (29LL + (long long )i) - (long long )size >= 0LL) && (35LL - (long long )i) - (long long )size >= 0LL) && i == 3)) || (((((-35LL + (long long )i) + (long long )size >= 0LL && (-29LL - (long long )i) + (long long )size >= 0LL) && (29LL + (long long )i) - (long long )size >= 0LL) && (35LL - (long long )i) - (long long )size >= 0LL) && i == 3)) || (((((-34LL + (long long )i) + (long long )size >= 0LL && (-30LL - (long long )i) + (long long )size >= 0LL) && (30LL + (long long )i) - (long long )size >= 0LL) && (34LL - (long long )i) - (long long )size >= 0LL) && i == 2)) || (((((-34LL + (long long )i) + (long long )size >= 0LL && (-30LL - (long long )i) + (long long )size >= 0LL) && (30LL + (long long )i) - (long long )size >= 0LL) && (34LL - (long long )i) - (long long )size >= 0LL) && i == 2)) || (((((-33LL + (long long )i) + (long long )size >= 0LL && (-31LL - (long long )i) + (long long )size >= 0LL) && (31LL + (long long )i) - (long long )size >= 0LL) && (33LL - (long long )i) - (long long )size >= 0LL) && i == 1)) || (((((-33LL + (long long )i) + (long long )size >= 0LL && (-31LL - (long long )i) + (long long )size >= 0LL) && (31LL + (long long )i) - (long long )size >= 0LL) && (33LL - (long long )i) - (long long )size >= 0LL) && i == 1)) || ((((((-32LL + (long long )i) + (long long )size >= 0LL && (-32LL - (long long )i) + (long long )size >= 0LL) && (32LL + (long long )i) - (long long )size >= 0LL) && (32LL - (long long )i) - (long long )size >= 0LL) && 0 == i) && i == 0)) || ((((((-32LL + (long long )i) + (long long )size >= 0LL && (-32LL - (long long )i) + (long long )size >= 0LL) && (32LL + (long long )i) - (long long )size >= 0LL) && (32LL - (long long )i) - (long long )size >= 0LL) && 0 == i) && i == 0)) || ((((2147483616LL + (long long )i) + (long long )size >= 0LL && (2147483615LL - (long long )i) + (long long )size >= 0LL) && (2147483680LL + (long long )i) - (long long )size >= 0LL) && (2147483679LL - (long long )i) - (long long )size >= 0LL) format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4.c file_hash: f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df line: 28 column: 5 function: main value: (((((((((((((((((((((((((((((((((((((((((((((((((((i == 7 || i == 21) || i == 6) || i == 20) || i == 6) || i == 20) || i == 5) || i == 19) || i == 5) || i == 19) || i == 4) || i == 18) || i == 4) || i == 18) || i == 3) || i == 17) || i == 3) || i == 17) || i == 2) || i == 16) || i == 2) || i == 16) || i == 1) || i == 15) || i == 1) || i == 15) || (0 == i && i == 0)) || i == 14) || (0 == i && i == 0)) || i == 14) || 8 <= i) || i == 13) || i == 13) || i == 12) || i == 12) || i == 11) || 25 <= i) || i == 11) || (25 <= i && i != 1)) || i == 10) || i == 24) || i == 10) || i == 24) || i == 9) || i == 23) || i == 9) || i == 23) || i == 8) || i == 22) || i == 8) || i == 22) || i == 7) || i == 21 format: c_expression correctness_witness CPAchecker 2.3 19 2023-12-01T04:45:12+01:00

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

Trying to find witnesses for program (f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df, sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c).

Found 45 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c, f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0edf89e Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2022-12-09T06:37:04+01:00
Download 6097c36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2022-12-12T14:55:09Z
Download 8e6d6fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 7 2022-12-10T14:51:24+01:00
Download 508b873 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 7 2022-12-12T01:54:56+01:00
Download 01e7c4b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 10 2022-12-09T02:55:12+01:00
Download de42eac Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2022-12-08T17:25:44Z
Download 005ce1e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 7.0.0 incr 3 2022-12-18T23:13:31Z
Download 16fbe37 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 6.8.0 incr 3 2022-12-25T10:17:43Z
Download 80c646a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 7 2022-12-10T03:06:26+01:00
Download f89c718 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 12 2022-12-14T12:30:38Z
Download b8adef2 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-11T09:19:52Z
Download 56c20c1 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 CBMC 738 2022-12-08T11:43:26+01:00
Download 18e6c25 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 12 2022-12-13T13:51:15Z
Download 9b5377b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 8 2023-01-28T04:00:30+01:00 Download 26d4730
Download 41f5966 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T21:59:48+01:00
Download 924182a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.4.0 3 2022-12-09T11:00:24Z
Download 3e3f079 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T11:01 CET (comp)
Download c6da006 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 13 2022-12-14T07:33:14Z
Download acf6f8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2022-12-25T10:34:27Z
Download 45cf419 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2022-12-12T12:27:16Z
Download 30f8cbf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2022-12-11T17:42:25
Download 59c063e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T10:55:57Z
Download 986fb06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 7.0.0 kind 3 2022-12-18T18:23:52Z
Download 3f4fb99 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 6.8.0 kind 3 2022-12-25T10:34:27Z
Download 822ed56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T10:51:26+01:00 Download c6da006
Download a15751a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 10 2023-01-29T07:40:19+01:00 Download d56c34a
Download 53ea7bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T05:21:28+01:00 Download 45cf419
Download 70da0bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T04:48:58+01:00 Download 30f8cbf
Download fcbb613 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T22:53:43+01:00 Download 41f5966
Download bd0619c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T17:38:45+01:00 Download 924182a
Download ea1fd5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T15:02:28+01:00 Download 986fb06
Download 4b02a06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T00:31:06+01:00 Download 3f4fb99
Download 7193de8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-27T23:43:46+01:00 Download 1f13984
Download c2939d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2022-12-10T19:57:25+01:00
Download d15c81c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 8 2022-12-12T02:48:25+01:00
Download d5f1296 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 8 2022-12-10T04:36:17+01:00
Download 26d4730 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 725 2022-12-08T04:58:58+01:00
Download 1f13984 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2022-12-08T15:06:46Z
Download d56c34a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 13 2022-12-13T14:20:38Z
Download 3f4791f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2022-12-25T10:19:43Z
Download 9e23e99 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.0.0 3 2022-12-18T22:54:42Z
Download 6b27a80 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2022-12-12T10:50:03Z
Download 2bfe11d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2022-12-11T16:49:36
Download b53c04d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 725 2022-12-08T03:16:09+01:00
Download 65359b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2022-12-08T14:28:35Z

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

Trying to find witnesses for program (f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df, sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c).

Found 16 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c, f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 9c04e47 Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2021-12-07T08:04:28+01:00
Download 4e2faf5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2021-12-07T17:04:59Z
Download 812d5e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 7 2021-12-05T15:27:30+01:00
Download 5314b2b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 7 2021-12-08T20:32:00+01:00
Download 3a50ff4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 7 2021-12-09T10:51:34+01:00
Download 4416398 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 10 2021-12-07T02:30:06+01:00
Download d47eabd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 6.8.0 incr 3 2021-12-08T03:45:54Z
Download b567782 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 12 2021-12-10T06:05:33Z
Download a8d2083 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 CBMC 738 2021-12-06T09:29:07+01:00
Download 44aadde 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 12 2021-12-06T22:54:22Z
Download 4f07c61 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness SESL 2 2021-12-06T11:54:55+01:00
Download 6e1274a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2021-12-08T09:37:21Z
Download ff16b15 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness VERIFUZZ 3 2021-12-11T10:46:25Z
Download 3456117 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2021-12-07T15:34:52Z
Download b00a907 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2021-12-09T07:20:52
Download 7e14882 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 725 2021-12-06T06:42:52+01:00

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

Trying to find witnesses for program (f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df, sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c).

Found 8 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c, f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a0a6c50 Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2020-12-06T18:30:10+01:00
Download 231e188 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 2 2020-12-11T18:56:31
Download a3c9be4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 2 2020-12-08T15:25:59
Download 57e6bcb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0 7 2020-12-05T14:31:18+01:00
Download e1f70f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 7 2020-12-08T02:11:38+01:00
Download 1c6d74b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-11T14:39:44
Download 67b8e19 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-08T18:47:12
Download 71bfa58 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2020-12-08T09:38:29

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

Trying to find witnesses for program (f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df, sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c).

Found 3 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c, f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 91ffeaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 7 2019-11-30T11:04:04+01:00
Download 7b30e3a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 7 2019-12-01T02:23:33+01:00
Download f759504 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:22 CET (comp)

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

Trying to find witnesses for program (f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df, sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c).

Found 5 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c, f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c584fc3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2018-12-08T00:27 CET (sv-comp)
Download e3bddb2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-05T09:48:23+01:00
Download 0ba100e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 8 2018-12-06T21:45:10+01:00
Download dc84801 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T20:19 CET (sv-comp)
Download 5dce3d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T08:00 CET (sv-comp)

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

Trying to find witnesses for program (f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df, sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c).

Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c, f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 594d7e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2017-12-02T23:54 CET (sv-comp)
Download 6eb35a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T11:41:46.829647
Download 8628189 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-01T23:31:37.050062
Download 62ed6ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T08:34:31+01:00
Download 7c972ed 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 9 2017-12-03T06:53Z
Download a386552 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 Map2Check 4 2017-12-01T23:35 CET (sv-comp)
Download 2f05e0c 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 CBMC 838 2017-12-01T08:30 CET (sv-comp)
Download cf549f0 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 9 2017-12-03T03:59Z
Download 38a60fd 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 17 2017-12-01T08:23 CET (sv-comp)
Download c6adaab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T22:37:21.502806
Download b5f627d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T10:43:44.535682
Download a7d628f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 272 2017-12-01T19:54 CET (sv-comp)
Download a01e759 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 823 2017-12-01T13:26 CET (sv-comp)
Download 2dce131 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 16 2017-12-01T12:04 CET (sv-comp)

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

Trying to find witnesses for program (f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df, sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c, f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f3d22aeda2fb15b9dd79854281ee0f5e475c0f7ee1551b76594f45703ddc81df.json

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