Witness Inspection

A description of this web service can be found in the CAV paper "Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses" (more material).

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

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

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

Found 37 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i, ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ac2f26a Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T09:31:36+01:00
Download af7ce46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2023-12-17T01:58:49Z
Download 1298973 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 7 2023-12-18T12:01:46+01:00 Download ac2f26a
Download 9ae49da Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 7 2023-11-30T09:09:11+01:00
Download 59aa699 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 7 2023-12-03T20:37:23+01:00
Download 940465f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 13 2023-12-18T01:44:18+01:00
Download 9ea6a92 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 19 2023-11-29T01:17:04Z
Download 60c9173 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0 7 2023-12-19T10:37:30+01:00
Download d7f9a85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 7 2023-12-19T01:19:19+01:00
Download ddc10cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:57:12+01:00
Download 0d50766 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.4.0 3 2023-12-03T08:02:36Z
Download 969ddd4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 17 2023-12-02T14:40:21Z
Download cc386da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2023-12-17T01:58:42Z
Download da0f498 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2023-11-29T19:28:53Z
Download 67ba7a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T09:22:08Z
Download 805fa67 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 17 2023-12-02T19:52:19Z
Download 0056e90 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 7 2023-12-19T14:54:04+01:00 Download f36a167
Download 0c7465e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 7 2023-12-19T02:59:47+01:00 Download 738290a
Download 47df936 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 7 2023-12-17T06:08:44+01:00 Download cc386da
Download bbc3f3d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 7 2023-12-04T11:30:43+01:00 Download 969ddd4
Download 57c5fbb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 7 2023-12-04T02:12:32+01:00 Download 17dd34a
Download 3b22ead Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 7 2023-12-03T18:33:16+01:00 Download ddc10cb
Download 7001795 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 7 2023-12-03T09:54:22+01:00 Download 0d50766
Download b2b27ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 7 2023-12-03T05:49:26+01:00 Download 805fa67
Download 7826dc0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 7 2023-11-30T11:37:26+01:00 Download 57f7d25
Download 57f7d25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 7 2023-11-30T06:41:20+01:00
Download 333da15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 7 2023-11-30T02:30:09+01:00 Download da0f498
Download c377879 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 7 2023-11-29T18:25:55+01:00 Download 67ba7a5
Download 5c0604c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 7 2023-11-29T08:02:44+01:00 Download ad07e7a
Download 17dd34a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 7 2023-12-03T21:54:02+01:00
Download f36a167 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 7 2023-12-19T12:12:31+01:00
Download 738290a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 7 2023-12-18T20:49:10+01:00
Download ad07e7a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 17 2023-11-29T03:25:19Z
Download 216a25b Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: f7a1ad6b-9cd6-4990-a928-5e1c41ca0e96 creation_time: '2023-11-29T04:25:19+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_dfaa01d4-cf61-4214-a1dc-c2d0aa683211/sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca-2.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_dfaa01d4-cf61-4214-a1dc-c2d0aa683211/sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca-2.i : ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] correctness_witness CPAchecker 2.3 8 2023-11-29T07:47:09+01:00
Download 04fcf89 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: e2b761ae-c080-4499-a149-3468d668d394 creation_time: '2023-12-02T20:52:19+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5da0c7f4-f4c9-4ce4-aebb-6c46cf072f09/sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca-2.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5da0c7f4-f4c9-4ce4-aebb-6c46cf072f09/sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca-2.i : ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] correctness_witness CPAchecker 2.3 8 2023-12-03T05:35:45+01:00
Download 1a79577 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 1841af8d-4851-4589-8319-4bd7b8a99d7b creation_time: '2023-12-02T15:40:21+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_1edc6e2c-0959-4049-840b-5b2f28d7bd2d/sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca-2.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_1edc6e2c-0959-4049-840b-5b2f28d7bd2d/sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca-2.i : ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] correctness_witness CPAchecker 2.3 8 2023-12-04T12:01:27+01:00
Download b008b27 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: 55f78097-b1e4-4704-a5d2-5259b1761eef creation_time: 2023-12-01T01:38:52Z producer: name: Goblint version: tags/svcomp24-0-gc2e9465a7 command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--sets'' ''ana.specification'' ''../../sv-benchmarks/c/properties/no-overflow.prp'' ''--sets'' ''exp.architecture'' ''64bit'' ''../../sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca-2.i''' task: input_files: - ../../sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca-2.i input_file_hashes: ../../sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca-2.i: ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca-2.i file_hash: ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746 line: 557 column: 11 function: cstpncpy value: (n != 18446744073709551615UL && (((n != 18446744073709551614UL && (((n != 18446744073709551613UL && (((n != 18446744073709551612UL && (((n != 18446744073709551611UL && (((n != 18446744073709551610UL && (((n <= 2147483640UL && n != 18446744073709551609UL) || ((1UL <= n && n <= 2147483641UL) && n != 0UL)) || n <= 2147483641UL)) || ((1UL <= n && n <= 2147483642UL) && n != 0UL)) || n <= 2147483642UL)) || ((1UL <= n && n <= 2147483643UL) && n != 0UL)) || n <= 2147483643UL)) || ((1UL <= n && n <= 2147483644UL) && n != 0UL)) || n <= 2147483644UL)) || ((1UL <= n && n <= 2147483645UL) && n != 0UL)) || n <= 2147483645UL)) || ((1UL <= n && n <= 2147483646UL) && n != 0UL)) || n <= 2147483646UL)) || ((1UL <= n && n <= 2147483647UL) && n != 0UL) format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca-2.i file_hash: ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746 line: 555 column: 8 function: cstpncpy value: 1UL <= n format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca-2.i file_hash: ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746 line: 555 column: 8 function: cstpncpy value: n <= 2147483647UL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca-2.i file_hash: ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746 line: 555 column: 8 function: cstpncpy value: n != 0UL format: c_expression correctness_witness CPAchecker 2.3 11 2023-12-01T04:35:16+01:00

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

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

Found 33 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i, ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 43b5a42 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T05:13:52+01:00
Download c259925 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Symbiotic 3 2022-12-25T12:06:01Z
Download cd2b794 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 7 2023-01-28T14:18:06+01:00 Download 43b5a42
Download 88330e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 7 2022-12-10T15:59:48+01:00
Download cde2ac8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 7 2022-12-12T02:38:02+01:00
Download b3137cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0 7 2022-12-11T02:05:45+01:00
Download 708c645 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 7 2022-12-09T18:12:37+01:00
Download bfe5cd8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-38892M 13 2022-12-09T03:14:06+01:00
Download a8cd393 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 18 2022-12-13T16:20:23Z
Download b87e10b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T21:59:13+01:00
Download ec67ff6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.4.0 3 2022-12-09T12:54:12Z
Download 5adfbc6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 16 2022-12-14T14:35:29Z
Download 0fab770 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2022-12-25T12:35:45Z
Download ce793ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2022-12-12T13:43:00Z
Download f3d6e85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T09:24:21Z
Download bbac80f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 16 2022-12-14T19:49:09Z
Download 23d75cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 7 2023-01-29T11:06:21+01:00 Download 5adfbc6
Download 54ee6cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 7 2023-01-29T07:16:09+01:00 Download e5732d5
Download 8c3f897 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 7 2023-01-29T06:24:52+01:00 Download bbac80f
Download dd9e2ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 7 2023-01-29T05:31:12+01:00 Download ce793ab
Download 7c0698a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 7 2023-01-29T03:46:23+01:00 Download f3d6e85
Download 5ee6243 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 7 2023-01-29T02:49:22+01:00 Download 4dbaafc
Download c1276f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 7 2023-01-29T00:07:03+01:00 Download 47954d7
Download fa4131e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 7 2023-01-28T22:50:45+01:00 Download b87e10b
Download f367004 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 7 2023-01-28T19:00:27+01:00 Download 2cdd821
Download a9ccf43 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 7 2023-01-28T17:38:04+01:00 Download ec67ff6
Download 319a24c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 7 2023-01-28T11:26:49+01:00 Download bb61950
Download 6da782b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 7 2023-01-28T01:01:07+01:00 Download 0fab770
Download bb61950 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 7 2022-12-10T20:09:26+01:00
Download 4dbaafc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 7 2022-12-11T23:31:35+01:00
Download 47954d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 7 2022-12-11T04:03:30+01:00
Download 2cdd821 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 7 2022-12-10T01:47:48+01:00
Download e5732d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 16 2022-12-13T14:32:31Z

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

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

Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i, ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 93d9671 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2021-12-10T18:42:28

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

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

Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i, ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0d24544 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-11T15:34:34
Download b52b915 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-09T00:39:21

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

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

Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i, ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746.json

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

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

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

Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i, ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746.json

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

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

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

Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i, ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746.json

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

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

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

Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/openbsd_cstpncpy-alloca_true-termination.c.i, ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/ddb0eb207fb72f46b2f9a0f11e334a77be9b4b455314fd1b26a90347e4178746.json

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