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/ArraysOfVariableLength6_true-valid-memsafety_true-termination.c
programSHA 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1
witnessName results-verified/symbiotic.2018-12-07_2142.logfiles/sv-comp19_prop-memsafety.ArraysOfVariableLength6_true-valid-memsafety_true-termination.c.files/witness.graphml
witnessSHA 5daafc6047d693af5a9e8f2eb301039ce3c2046f1b2ba75ef86bac3a4c3e1c89

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-08T01:47 CET (sv-comp)
producer Symbiotic
program-sha256 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1
programfile /tmp/vcloud-vcloud-master/worker/working_dir_99ab9044-b22b-43d2-b786-a295cd4e6789/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6_true-valid-memsafety_true-termination.c
programhash 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1
sourcecodelang C
specification CHECK( init(main()), LTL(G valid-memtrack) )
witness-file witnessFileByHash/5daafc6047d693af5a9e8f2eb301039ce3c2046f1b2ba75ef86bac3a4c3e1c89.graphml
witness-sha256 5daafc6047d693af5a9e8f2eb301039ce3c2046f1b2ba75ef86bac3a4c3e1c89
witness-size 946
witness-type correctness_witness

This witness was created for this program (cf. table above, 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1).

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4d51509 Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2023-12-18T08:59:54+01:00
Download c6ea5c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2023-11-29T20:09:15Z
Download 5a9834f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 7 2023-11-30T05:38:15+01:00
Download 1b022eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 7 2023-12-03T22:54:27+01:00
Download dd82193 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 11 2023-12-18T01:34:38+01:00
Download 8ad89b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-05T07:29:07Z
Download 7cf027d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-04T12:38:14Z
Download fff2d1b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2023-12-01T19:35:45Z
Download d93fc63 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 7.4.0 incr 3 2023-12-01T12:12:06Z
Download dc948b4 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-02T11:42:46Z
Download 17204e7 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:16Z
Download 29df739 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:45:58Z
Download 387fa42 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 748 2023-12-17T15:38:13+01:00
Download 4417545 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-29T00:12:21Z
Download cde06ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 7 2023-12-19T00:23:33+01:00
Download bea556f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 8 2023-12-17T21:51:48+01:00 Download abe6070
Download 8bf4ca9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:45:25+01:00
Download fbc4065 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.4.0 3 2023-12-03T07:44:28Z
Download ef92c9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:37 CET (comp)
Download b9bc9a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 14 2023-12-02T12:36:59Z
Download 4d2c37f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2023-12-17T00:50:13Z
Download 23529c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2023-11-29T21:39:44Z
Download 43f1aa4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2023-12-19T22:27:30
Download 76bbb7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T14:34:17Z
Download 3ed177e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 7.4.0 kind 3 2023-12-01T14:10:39Z
Download beff01c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-20T02:18:28+01:00 Download 43f1aa4
Download 4d1b0cc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-17T06:09:02+01:00 Download 4d2c37f
Download ec52713 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-05T14:23:09+01:00 Download e7b1099
Download 3b3ea66 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-04T16:29:46+01:00 Download f360ad0
Download 516cb4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-04T11:24:11+01:00 Download b9bc9a7
Download e75a051 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-03T18:32:32+01:00 Download 8bf4ca9
Download b2fc5b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-03T09:54:44+01:00 Download fbc4065
Download 7c06f89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-01T22:44:59+01:00 Download 16af9f4
Download 85c36d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-12-01T18:16:48+01:00 Download 3ed177e
Download 9a428c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-30T08:50:08+01:00
Download 9776a2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-30T02:31:38+01:00 Download 23529c8
Download 6c80ff2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-29T18:11:30+01:00 Download 76bbb7c
Download be91ce6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 8 2023-11-29T08:12:08+01:00 Download 3425181
Download 91bfd43 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 8 2023-12-03T21:38:10+01:00
Download 293347f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 8 2023-12-18T22:08:28+01:00
Download abe6070 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 735 2023-12-17T17:57:30+01:00
Download e7b1099 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-05T09:24:02Z
Download f360ad0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-04T13:39:33Z
Download 16af9f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-01T20:55:59Z
Download 3425181 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 14 2023-11-29T06:09:12Z
Download d032114 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.4.0 3 2023-12-01T13:27:18Z
Download 33c0a88 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2023-11-29T19:57:16Z
Download d871cd8 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2023-12-19T21:52:16
Download d1c196b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 735 2023-12-17T18:37:05+01:00
Download 2eb563f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-05T10:00:06Z
Download 700e11b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-04T13:34:23Z
Download 7717221 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-01T20:45:17Z
Download 056f7fc Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: b0c8dbc8-45f7-45e1-9dde-98f29a344a34 creation_time: '2023-12-02T13:36:59+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_79a6e965-719f-48be-a427-23ceb1c9ae03/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_79a6e965-719f-48be-a427-23ceb1c9ae03/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c : 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1 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_79a6e965-719f-48be-a427-23ceb1c9ae03/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c file_hash: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1 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_79a6e965-719f-48be-a427-23ceb1c9ae03/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c file_hash: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1 line: 29 column: 0 function: main value: ((0 <= i) && (i <= 2147483647)) format: c_expression correctness_witness CPAchecker 2.3 9 2023-12-04T11:58:11+01:00
Download 0c7a954 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 752537b5-bd54-4980-a726-bb7582621bd5 creation_time: '2023-11-29T07:09:12+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6f455c72-2f39-46a3-94f1-c91a9fd86611/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6f455c72-2f39-46a3-94f1-c91a9fd86611/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c : 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1 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_6f455c72-2f39-46a3-94f1-c91a9fd86611/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c file_hash: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1 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_6f455c72-2f39-46a3-94f1-c91a9fd86611/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c file_hash: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1 line: 29 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_6f455c72-2f39-46a3-94f1-c91a9fd86611/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c file_hash: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1 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:45:43+01:00
Download bd9d4af Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: 0388eae5-3a21-4153-b461-5b74cd36526a creation_time: 2023-12-01T01:28:50Z 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/ArraysOfVariableLength6.c''' task: input_files: - ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c input_file_hashes: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1 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/ArraysOfVariableLength6.c file_hash: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1 line: 15 column: 8 function: foo value: 32 == size format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c file_hash: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1 line: 15 column: 8 function: foo value: size == 32 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c file_hash: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1 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/ArraysOfVariableLength6.c file_hash: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1 line: 29 column: 5 function: main value: c == & mask[0] format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c file_hash: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1 line: 29 column: 5 function: main value: c == mask format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength6.c file_hash: 6ef2b56a2f4ebf2e6f7f4ededf8760f087ff726b08e36644d8dcb52a8d087cd1 line: 29 column: 5 function: main value: (((((((((((((((((((((((((((((((((((((((((((((((((((i == 8 || i == 22) || i == 7) || i == 21) || 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) || 6 <= 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 format: c_expression correctness_witness CPAchecker 2.3 19 2023-12-01T04:18:47+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ae09e79 Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2022-12-09T06:33:16+01:00
Download 40d5910 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2022-12-12T15:12:09Z
Download 7e6cd4a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 7 2022-12-10T20:54:39+01:00
Download a38a383 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 7 2022-12-11T22:46:57+01:00
Download c3c248b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 11 2022-12-09T02:28:40+01:00
Download 7ce832f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Bubaak 3 2022-12-08T14:38:54Z
Download 708cd5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 7.0.0 incr 3 2022-12-18T17:19:24Z
Download 4786fcd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 6.8.0 incr 3 2022-12-25T12:13:23Z
Download 09edf5f 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 2022-12-14T14:08:59Z
Download bf7ae26 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:22:17Z
Download 2304873 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 748 2022-12-08T05:12:23+01:00
Download 7593681 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-13T09:58:51Z
Download cb3cb16 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 7 2022-12-09T17:10:32+01:00
Download 5516b3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 8 2023-01-28T03:57:30+01:00 Download 0e3501f
Download a79fb17 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-11T01:50:57+01:00
Download d9eea3a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.4.0 3 2022-12-09T11:44:55Z
Download ef92c9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T11:01 CET (comp)
Download 4cbce35 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 13 2022-12-14T10:30:35Z
Download c7009e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2022-12-25T12:30:42Z
Download d58f289 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2022-12-12T15:16:13Z
Download ccf65ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2022-12-11T14:23:26
Download 1745c38 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T12:35:34Z
Download 2df1c4f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 7.0.0 kind 3 2022-12-18T20:41:24Z
Download da8e45b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 6.8.0 kind 3 2022-12-25T12:30:42Z
Download 889fa35 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T11:07:49+01:00 Download 4cbce35
Download bc1f1a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 10 2023-01-29T07:38:22+01:00 Download 703b00d
Download 6562163 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T05:19:46+01:00 Download d58f289
Download e17e869 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-29T04:48:18+01:00 Download ccf65ac
Download d5ec641 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T22:50:37+01:00 Download a79fb17
Download f89c139 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T17:38:49+01:00 Download d9eea3a
Download 0ea561a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T15:01:33+01:00 Download 2df1c4f
Download 8a60dba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-28T00:45:48+01:00 Download da8e45b
Download 92894ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2023-01-27T23:43:26+01:00 Download 5d4f2c5
Download 7a6a693 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 8 2022-12-10T19:40:28+01:00
Download 35630c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 8 2022-12-11T22:06:09+01:00
Download e2dec0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 8 2022-12-09T23:37:20+01:00
Download 0e3501f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 735 2022-12-08T11:07:39+01:00
Download 5d4f2c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2022-12-08T16:06:07Z
Download 703b00d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 14 2022-12-13T20:15:40Z
Download 0f6ab63 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2022-12-25T10:23:02Z
Download b3ff16e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.0.0 3 2022-12-18T21:45:29Z
Download 0dfb6df Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2022-12-12T11:30:13Z
Download 72701d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2022-12-11T18:04:51
Download c181fcf Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 735 2022-12-08T04:32:00+01:00
Download 2823c29 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2022-12-08T15:45:46Z

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f40ac4c Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2021-12-07T09:22:49+01:00
Download 1d07de4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2021-12-07T16:39:30Z
Download 3248833 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.1 7 2021-12-05T19:20:30+01:00
Download 8c1562c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 7 2021-12-08T19:53:12+01:00
Download 28e4629 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 11 2021-12-07T01:53:02+01:00
Download 0eb4ebd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 6.8.0 incr 3 2021-12-08T09:41:51Z
Download 97a2d49 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 2021-12-10T05:22:44Z
Download 18d8c3f 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 748 2021-12-06T02:41:11+01:00
Download 3831ac4 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-06T18:07:56Z
Download e6de0cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) violation_witness SESL 2 2021-12-06T11:22:48+01:00
Download 9dd8f84 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 7 2021-12-09T11:24:00+01:00
Download 8e6bd9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2021-12-08T06:06:37Z
Download 8ecaba7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness VERIFUZZ 3 2021-12-11T05:25:13Z
Download 55f4772 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2021-12-07T13:24:22Z
Download 5407205 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2021-12-09T08:04:46
Download 42f2e73 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 735 2021-12-06T08:41:39+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download be0be49 Inspect Inspect
Validate
valid-memsafety correctness_witness DIVINE 4 2 2020-12-06T18:21:39+01:00
Download 9d9f72d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 2 2020-12-11T18:06:52
Download c0850e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 2 2020-12-08T14:37:08
Download d465679 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 7 2020-12-07T23:17:06+01:00
Download f6470f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0 7 2020-12-05T13:27:14+01:00
Download ec84eaa Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-11T16:58:20
Download 3a8f0d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-09T00:49:48
Download e7c8eea Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2020-12-08T08:43:23

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 62ef5ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 7 2019-11-30T23:10:32+01:00
Download 482da94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.9 7 2019-11-29T21:28:19+01:00
Download 7e3beb5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T23:14 CET (comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5daafc6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2018-12-08T01:47 CET (sv-comp)
Download 93954a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 8 2018-12-08T04:23:20+01:00
Download 589a76a Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.7-svn 29852 8 2018-12-06T00:26:08+01:00
Download 615b68f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T05:23 CET (sv-comp)
Download 96d2276 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T09:11 CET (sv-comp)

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c585874 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 1 2017-12-03T00:02 CET (sv-comp)
Download f7cb3ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.6.1-svn 26773 8 2017-12-01T08:34:11+01:00
Download 263e66e Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T10:49:32.042699
Download 83ee113 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:34:00.293901
Download 0625297 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-03T07:06Z
Download c4f8f40 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:45 CET (sv-comp)
Download 57c3bac 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 850 2017-12-01T08:24 CET (sv-comp)
Download 6ded29b 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 2017-12-03T03:55Z
Download 24d8506 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 18 2017-12-01T08:20 CET (sv-comp)
Download 27c048b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T20:49:30.771091
Download e6c6abb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T08:09:43.992852
Download 6395c4d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 276 2017-12-01T18:45 CET (sv-comp)
Download 9fcb1d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 835 2017-12-01T15:59 CET (sv-comp)
Download 6bf3138 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 17 2017-12-01T12:50 CET (sv-comp)

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

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

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

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