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 (ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc, sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i).

Found 36 witnesses for program sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i, ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8f35d16 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2023-12-18T09:18:09+01:00
Download 90e6360 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 6 2023-12-18T12:05:03+01:00 Download 8f35d16
Download 692648f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.3 5 2023-11-30T08:14:47+01:00
Download ce6b67d Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 6 2023-12-03T23:35:22+01:00
Download 364734c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2023-12-18T18:23:14+01:00
Download 972e1dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 10 2023-12-02T12:07:32Z
Download 3d7d195 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:37Z
Download 1dcf434 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:11:14Z
Download 9e5958d 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 Kojak 13 2023-12-02T20:30:58Z
Download 41fafea Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 29 2023-11-30T22:37:35Z
Download 1d6d480 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 2023-11-29T00:56:59Z
Download a4a92c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:41:24+01:00
Download 31a1ba2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.4.0 3 2023-12-03T07:34:07Z
Download 31854c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 9 2023-12-02T12:55:53Z
Download 5e630a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T11:48:24Z
Download 49c8d72 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 9 2023-12-03T00:18:00Z
Download ba64bee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-19T15:09:48+01:00 Download 7b5d7a4
Download 0e54b1f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-19T04:20:36+01:00 Download e431567
Download 30ccb88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-17T06:16:50+01:00 Download 1fd351b
Download 11728c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T11:49:14+01:00 Download 31854c3
Download e37c83f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T02:02:18+01:00 Download 9d147f7
Download 2be7e92 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T18:29:42+01:00 Download a4a92c4
Download 960c3fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T09:54:32+01:00 Download 31a1ba2
Download 2103e03 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T06:05:28+01:00 Download 49c8d72
Download ae80952 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T11:50:55+01:00 Download bafb422
Download bafb422 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T07:30:19+01:00
Download 4e8d2a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-29T18:26:50+01:00 Download 5e630a0
Download 40789ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-29T08:07:19+01:00 Download ddb36d1
Download 9d147f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 5 2023-12-03T22:09:50+01:00
Download 1fd351b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2023-12-17T03:45:54+01:00
Download e431567 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2023-12-18T18:40:56+01:00
Download ddb36d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 9 2023-11-29T01:11:56Z
Download add3e0d Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 6d672be7-36fc-44f9-8005-9e328792b166 creation_time: '2023-11-29T02:11:56+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ba09afab-848d-475b-80b5-f0a31b48de7f/sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ba09afab-848d-475b-80b5-f0a31b48de7f/sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca.i : ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] correctness_witness CPAchecker 2.3 6 2023-11-29T07:44:13+01:00
Download f52fdaa Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 4550f7b1-056b-4f69-be88-500f516c3d04 creation_time: 2023-12-03T01:18+01:00 producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_049b0fbb-b619-473d-8f4f-8885cd81b7d5/sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_049b0fbb-b619-473d-8f4f-8885cd81b7d5/sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca.i : ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] correctness_witness CPAchecker 2.3 6 2023-12-03T05:46:10+01:00
Download 170b79c Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 01ea014f-c5fc-4090-8de3-1d58dc1d630b creation_time: '2023-12-02T13:55:53+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_57f527c3-9934-400c-abba-3ff7945c92f1/sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_57f527c3-9934-400c-abba-3ff7945c92f1/sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca.i : ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] correctness_witness CPAchecker 2.3 6 2023-12-04T12:02:46+01:00
Download 9e6cd54 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: 987877d3-5518-4ee9-a5e2-8d52373530e1 creation_time: 2023-12-01T01:49:17Z 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/HarrisLalNoriRajamani-2010SAS-Fig3-alloca.i''' task: input_files: - ../../sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca.i input_file_hashes: ../../sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca.i: ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: [] correctness_witness CPAchecker 2.3 6 2023-12-01T04:27:29+01:00

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

Trying to find witnesses for program (ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc, sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i).

Found 31 witnesses for program sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i, ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 47dc9d1 Inspect Inspect
Validate
valid-memsafety violation_witness DIVINE 4 2 2022-12-09T06:47:21+01:00
Download a5ca0b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 6 2023-01-28T14:22:14+01:00 Download 47dc9d1
Download 61945df Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2 5 2022-12-10T21:42:12+01:00
Download c48a08b Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 6 2022-12-12T00:18:34+01:00
Download bb50dc3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Taipan 10 2022-12-14T07:25:24Z
Download 50b0458 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-11T08:53:42Z
Download 4b6befe 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 Kojak 12 2022-12-14T23:38:16Z
Download 7417c79 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness Automizer 10 2022-12-13T14:54:02Z
Download a7f3712 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2022-12-09T17:34:03+01:00
Download ae8bd1b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T22:03:54+01:00
Download f73f6d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.4.0 3 2022-12-09T13:07:38Z
Download f7454ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 9 2022-12-14T13:11:02Z
Download 5da6a76 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T09:23:10Z
Download 845996b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 9 2022-12-14T17:07:11Z
Download fafe921 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T11:06:04+01:00 Download f7454ed
Download 66d09a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T07:17:10+01:00 Download 658c042
Download c441748 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T06:23:30+01:00 Download 845996b
Download 7517817 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T03:52:19+01:00 Download 5da6a76
Download 1bcc368 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T02:47:55+01:00 Download 54cfb69
Download 85b0136 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T00:07:05+01:00 Download 980719f
Download 5034f1e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T22:52:36+01:00 Download ae8bd1b
Download e685d26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T18:33:14+01:00 Download a936990
Download ed57a42 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T17:38:39+01:00 Download f73f6d2
Download 1825a94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T11:55:40+01:00 Download 547d818
Download c5c4a57 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T00:30:43+01:00 Download 91ac5f1
Download 547d818 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2022-12-10T17:38:28+01:00
Download 54cfb69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 5 2022-12-12T00:01:11+01:00
Download 91ac5f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2022-12-25T12:41:57+01:00
Download a936990 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2022-12-10T00:10:59+01:00
Download 658c042 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 9 2022-12-13T11:21:28Z
Download 0bdabea Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2022-12-08T16:20:26Z

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

Trying to find witnesses for program (ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc, sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i).

Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i, ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc.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 '21

Trying to find witnesses for program (ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc, sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i).

Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i, ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc.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 '20

Trying to find witnesses for program (ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc, sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i).

Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i, ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc.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 (ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc, sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i).

Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i, ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc.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 (ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc, sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i).

Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i, ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3cdb007 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 6 2017-12-01T18:37 CET (sv-comp)
Download c39cd40 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 15 2017-12-01T15:00 CET (sv-comp)

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

Trying to find witnesses for program (ec52b50984ce4a37adbf31241337a0752ee4ecf2eb9496b3e3fee60fba9a59cc, sv-benchmarks/c/termination-memory-alloca/HarrisLalNoriRajamani-2010SAS-Fig3-alloca_true-termination.c.i).

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

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