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 (46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633, sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c).

Found 33 witnesses for program sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c, 46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 333c855 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T06:13:05Z
Download a266e41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:21:14+01:00
Download 84f92c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:37 CET (comp)
Download 6353d14 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 8 2023-12-02T13:46:13Z
Download 3f4c1c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T10:46:43Z
Download 5baf1de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 8 2023-12-02T21:24:33Z
Download e26413f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 21 2023-12-01T01:17:58Z
Download 7b8b4b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-20T03:41:12+01:00 Download 84f92c0
Download 4346ee2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-19T15:11:53+01:00 Download f77db60
Download f8d5b66 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-19T04:28:09+01:00 Download f436f5d
Download c1b15c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-17T06:10:48+01:00 Download 9ecd741
Download f0e5cde Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T11:24:23+01:00 Download 6353d14
Download bd509e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T01:46:01+01:00 Download 5a7d799
Download 4c3cae6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T18:33:15+01:00 Download a266e41
Download 37b889d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T09:57:04+01:00 Download 333c855
Download 84716fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T05:52:02+01:00 Download 5baf1de
Download 86c3643 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-01T03:54:23+01:00 Download e26413f
Download 8d0cf5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-01T00:16:34+01:00 Download 142e64e
Download 44f20fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T12:31:22+01:00 Download 184c555
Download 184c555 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T06:53:54+01:00
Download b5c3bfb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-29T18:19:24+01:00 Download 3f4c1c9
Download dce4cca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-29T08:18:51+01:00 Download 32905d2
Download 5a7d799 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 5 2023-12-03T22:05:25+01:00
Download 9ecd741 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2023-12-17T04:45:41+01:00
Download f436f5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2023-12-18T22:42:27+01:00
Download 32905d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 8 2023-11-29T00:33:02Z
Download 142e64e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 9 2023-11-30T23:03:09+01:00
Download 503f296 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 3 2023-12-01T00:56:14Z
Download 0ae9610 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 8 2023-11-30T22:43:32+01:00
Download 715e37c Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: e255d26c-bd50-4b3b-b5f6-ddb08d1f35dd creation_time: '2023-11-29T01:33:02+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4cce4c9f-8312-4be0-916a-bea74776eed6/sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4cce4c9f-8312-4be0-916a-bea74776eed6/sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1.c : 46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4cce4c9f-8312-4be0-916a-bea74776eed6/sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1.c file_hash: 46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633 line: 17 column: 0 function: main value: (((0 <= (y + 2147483648)) && (y <= 2147483647)) && (q <= 2147483647)) format: c_expression correctness_witness CPAchecker 2.3 6 2023-11-29T07:49:25+01:00
Download f3929c5 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 94dc5c24-fa0e-4ac5-913a-7055163ad30d creation_time: '2023-12-02T14:46:13+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_380f0c2c-a3d2-4e60-8ec5-0d03487e47cf/sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_380f0c2c-a3d2-4e60-8ec5-0d03487e47cf/sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1.c : 46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_380f0c2c-a3d2-4e60-8ec5-0d03487e47cf/sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1.c file_hash: 46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633 line: 17 column: 0 function: main value: (((0 <= (y + 2147483648)) && (y <= 2147483647)) && (q <= 2147483647)) format: c_expression correctness_witness CPAchecker 2.3 6 2023-12-04T12:04:15+01:00
Download b796ea5 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 1d93a605-4214-424a-86d6-3a07fb566966 creation_time: '2023-12-02T22:24:33+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ebbf185a-3ebd-43d0-ab97-64b96a7005fb/sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ebbf185a-3ebd-43d0-ab97-64b96a7005fb/sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1.c : 46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ebbf185a-3ebd-43d0-ab97-64b96a7005fb/sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1.c file_hash: 46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633 line: 17 column: 0 function: main value: (((0 <= (y + 2147483648)) && (y <= 2147483647)) && (q <= 2147483647)) format: c_expression correctness_witness CPAchecker 2.3 6 2023-12-03T05:32:55+01:00
Download 22b83cb Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: 1573a942-b3a9-46c4-83ac-f621d7e5e45c creation_time: 2023-12-01T01:17:58Z producer: name: Goblint version: tags/svcomp24-0-gc2e9465a7 command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--sets'' ''ana.specification'' ''../../sv-benchmarks/c/properties/no-overflow.prp'' ''--sets'' ''exp.architecture'' ''64bit'' ''../../sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1.c''' task: input_files: - ../../sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1.c input_file_hashes: ../../sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1.c: 46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: [] correctness_witness CPAchecker 2.3 6 2023-12-01T04:43:20+01:00

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

Trying to find witnesses for program (46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633, sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c).

Found 29 witnesses for program sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c, 46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d4bf7b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T12:27:42Z
Download e623bca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T22:12:11+01:00
Download 84f92c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T11:01 CET (comp)
Download 4548a74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 8 2022-12-14T06:21:08Z
Download 1752a70 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T10:37:11Z
Download 981025b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 8 2022-12-15T01:31:35Z
Download 497fa0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp23-0-g4f5dcf38f) 34 2022-12-10T03:53:06Z
Download 3e6e418 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T11:32:12+01:00 Download 84f92c0
Download 84d059f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T10:59:31+01:00 Download 4548a74
Download 2e35aff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T07:16:20+01:00 Download 7d6d640
Download 945a8cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T06:35:11+01:00 Download 981025b
Download 592439e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T03:46:01+01:00 Download 1752a70
Download 6ebe720 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T02:50:31+01:00 Download a9bb3b4
Download 5f0b6ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T00:07:24+01:00 Download 226d982
Download bb645ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T22:53:40+01:00 Download e623bca
Download e5ed81e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T22:23:48+01:00 Download 497fa0f
Download 35e35e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T18:28:41+01:00 Download 31359d7
Download 24221e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T17:44:23+01:00 Download d4bf7b0
Download 85c20b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T11:43:20+01:00 Download 8815fc9
Download 1f96c8f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T00:45:16+01:00 Download 987a72a
Download 527ffcb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-27T23:03:03+01:00 Download 414cb1f
Download 8815fc9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2022-12-10T11:51:29+01:00
Download a9bb3b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 5 2022-12-12T00:13:41+01:00
Download 987a72a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2022-12-25T13:41:35+01:00
Download 31359d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2022-12-10T03:15:20+01:00
Download 7d6d640 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 8 2022-12-13T16:14:02Z
Download 414cb1f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 9 2022-12-08T00:01:09+01:00
Download a4158e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2022-12-08T16:08:14Z
Download 9a30cb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 8 2022-12-08T02:01:14+01:00

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

Trying to find witnesses for program (46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633, sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c).

Found 23 witnesses for program sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c, 46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ff20855 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2021-12-06T14:18:06+01:00
Download 710f5ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.2.8 3 2021-12-13T21:50:27Z
Download 50b8e5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 8 2021-12-10T04:12:55Z
Download 82a3914 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 8 2021-12-10T09:46:20Z
Download bb7b2f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp22-0-ge852ac510) 7 2021-12-07T17:35:56Z
Download 04be4a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-14T00:24:39+01:00 Download 710f5ee
Download 088cd87 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-10T21:00:08+01:00 Download dda5b60
Download f8b75ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-10T17:38:21+01:00 Download 82a3914
Download 381f556 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-10T08:50:36+01:00 Download 50b8e5d
Download bb67e9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-09T15:34:07+01:00 Download 83c599b
Download 7d4b3fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-08T21:39:03+01:00 Download a4bc7f1
Download bad143d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-07T23:39:13+01:00 Download bb7b2f6
Download 78a4220 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-07T03:00:08+01:00 Download f81bcc0
Download eb1b83b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-06T14:45:09+01:00 Download ff20855
Download 4a34ba9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-06T01:12:08+01:00 Download 1cc1242
Download f013578 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-05T20:00:01+01:00 Download dbacdee
Download dbacdee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-05T18:42:24+01:00
Download dda5b60 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2021-12-10T18:18:42+01:00
Download a4bc7f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 5 2021-12-08T19:40:53+01:00
Download 83c599b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 5 2021-12-09T13:31:42+01:00
Download f81bcc0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 8 2021-12-06T20:48:33Z
Download 1cc1242 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 9 2021-12-05T23:52:31+01:00
Download 61e15c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 8 2021-12-06T00:36:14+01:00

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

Trying to find witnesses for program (46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633, sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c).

Found 12 witnesses for program sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c, 46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6165620 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.2.1 3 2020-12-06T23:34:48
Download 53803fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (svcomp21-0-g82e03b87) 7 2020-12-07T15:19:26
Download 84bfe0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-09T21:51:52+01:00 Download 8a12c50
Download 6146183 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-09T21:46:25+01:00 Download 86e83b1
Download b5ae85d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-09T01:46:51+01:00 Download e9495aa
Download 2c0ebf8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-08T06:20:13+01:00 Download 768a00e
Download 7024b94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-07T21:19:34+01:00 Download 53803fc
Download 4873924 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-07T00:12:44+01:00 Download 6165620
Download d4bed91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-06T16:52:33+01:00 Download d9c59ac
Download 67c47a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-06T13:17:13+01:00 Download 3d29f7d
Download 3d29f7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-05T17:15:49+01:00
Download 768a00e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 5 2020-12-08T04:02:12+01:00

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

Trying to find witnesses for program (46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633, sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c).

Found 2 witnesses for program sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c, 46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5780231 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 5 2019-11-29T15:28:06+01:00
Download e7a6796 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 5 2019-12-01T01:42:25+01:00

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

Trying to find witnesses for program (46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633, sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c).

Found 3 witnesses for program sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c, 46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f0c3131 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness SMACK 1.9.3 3 2018-12-08T03:10:38
Download 954e2c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-07T12:13:38+01:00
Download 7166291 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-05T16:42:55+01:00

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

Trying to find witnesses for program (46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633, sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c).

Found 9 witnesses for program sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c, 46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ad3702c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 8 2017-12-03T07:44Z
Download 3ae3f81 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 8 2017-12-03T10:31Z
Download f8eee50 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T18:41:31.313791
Download 117f048 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 3.1 5 2017-12-01T13:25 CET (sv-comp)
Download 9a578ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T11:38:41+01:00
Download 3c96470 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 8 2017-12-03T10:31Z
Download 4645b6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 8 2017-12-01T10:42 CET (sv-comp)
Download 6ed46f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 5 2017-12-01T16:12 CET (sv-comp)
Download 42f0dc2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 8 2017-12-01T16:43 CET (sv-comp)

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

Trying to find witnesses for program (46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633, sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c, 46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/46249a8081e9ed07db6908cd3a496204be92fe5d3b36976e28b801142a0a3633.json

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