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/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c
programSHA 626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898
witnessName results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-termination.CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c.files/witness.graphml
witnessSHA 68d9a87ba1ab8f4a46286c123c72a70b5df69a359155f55b211764c3e0b4272c

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-05T14:55:14.110679
producer DepthK v3.0
programfile /tmp/vcloud-vcloud-master/worker/working_dir_eee6f398-611f-4ddc-afd6-5b86b34bb828/sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c
programhash 7e9d7ee8b64b2fe79b2fb3806ae1ecb1089e2e41
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/68d9a87ba1ab8f4a46286c123c72a70b5df69a359155f55b211764c3e0b4272c.graphml
witness-sha256 68d9a87ba1ab8f4a46286c123c72a70b5df69a359155f55b211764c3e0b4272c
witness-size 3514
witness-type correctness_witness

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

Trying to find witnesses for program (626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898, sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c).

Found 32 witnesses for program sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c, 626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3e3bd18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T08:07:21Z
Download 3416ec9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:40:39+01:00
Download ecd0a85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:37 CET (comp)
Download 051fa6e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 9 2023-12-02T14:46:36Z
Download a1e1ce5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T12:06:31Z
Download a4f06f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 9 2023-12-03T02:01:11Z
Download c187a49 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 20 2023-12-01T01:27:20Z
Download 43dcc57 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-20T03:41:16+01:00 Download ecd0a85
Download 548efda Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-19T15:15:11+01:00 Download fc0d334
Download 8bf1e18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-19T04:12:29+01:00 Download 1e376e6
Download 19fbfcc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-17T06:08:42+01:00 Download 4ca290b
Download 36721f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T11:39:00+01:00 Download 051fa6e
Download 8c44f14 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T01:31:43+01:00 Download ced06a9
Download c8e0902 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T18:31:05+01:00 Download 3416ec9
Download 4f4e60c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T10:01:26+01:00 Download 3e3bd18
Download 4310c60 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T05:51:35+01:00 Download a4f06f1
Download 9bd265f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-01T03:35:54+01:00 Download c187a49
Download 726dacc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T23:47:07+01:00 Download 7cffe3d
Download e91c064 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T13:06:46+01:00 Download 7b9dbaf
Download 7b9dbaf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T06:07:27+01:00
Download bf4ceb5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-29T18:10:43+01:00 Download a1e1ce5
Download f7b70af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-29T07:55:32+01:00 Download edb2253
Download ced06a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 5 2023-12-03T18:07:05+01:00
Download 4ca290b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2023-12-17T04:31:02+01:00
Download 1e376e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2023-12-19T00:20:49+01:00
Download edb2253 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 9 2023-11-28T19:23:18Z
Download 7cffe3d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 9 2023-11-30T22:59:05+01:00
Download 49275e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2023-11-30T20:42:50+01:00
Download 1a008d4 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 5514363f-bd18-4cac-8372-b56e1c01be07 creation_time: '2023-12-03T03:01:11+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_8786a0df-7dde-4d94-bdcd-5e784cb50648/sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_8786a0df-7dde-4d94-bdcd-5e784cb50648/sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1.c : 626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898 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_8786a0df-7dde-4d94-bdcd-5e784cb50648/sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1.c file_hash: 626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898 line: 18 column: 0 function: main value: ((x <= 2147483647) && (y <= 2147483647)) format: c_expression correctness_witness CPAchecker 2.3 6 2023-12-03T05:39:36+01:00
Download 27cbb0d Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 0f8fb69a-ca27-4188-9292-2ae6cd7d3b83 creation_time: '2023-11-28T20:23:18+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f63722d8-8214-42d5-8ec9-7dbd39aadb35/sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f63722d8-8214-42d5-8ec9-7dbd39aadb35/sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1.c : 626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898 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_f63722d8-8214-42d5-8ec9-7dbd39aadb35/sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1.c file_hash: 626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898 line: 18 column: 0 function: main value: ((x <= 2147483647) && (y <= 2147483647)) format: c_expression correctness_witness CPAchecker 2.3 6 2023-11-29T07:49:51+01:00
Download a3b9ac2 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 0cb36fbf-80dd-4f62-966d-1630c1f4160b creation_time: '2023-12-02T15:46:36+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a74bd41a-e7f1-4c17-8c3f-4b2ec128a80b/sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a74bd41a-e7f1-4c17-8c3f-4b2ec128a80b/sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1.c : 626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898 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_a74bd41a-e7f1-4c17-8c3f-4b2ec128a80b/sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1.c file_hash: 626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898 line: 18 column: 0 function: main value: ((x <= 2147483647) && (y <= 2147483647)) format: c_expression correctness_witness CPAchecker 2.3 6 2023-12-04T11:56:42+01:00
Download 802d7f3 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: 41e726ba-1d0b-455c-b34a-8b0b8d736bf6 creation_time: 2023-12-01T01:27:20Z 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/CookSeeZuleger-TACAS2013-Fig1.c''' task: input_files: - ../../sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1.c input_file_hashes: ../../sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1.c: 626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: [] correctness_witness CPAchecker 2.3 6 2023-12-01T04:19:56+01:00

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

Trying to find witnesses for program (626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898, sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c).

Found 28 witnesses for program sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c, 626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5d607f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T10:00:19Z
Download c2304c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T22:01:58+01:00
Download ecd0a85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T11:00 CET (comp)
Download bcde728 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 8 2022-12-14T11:00:58Z
Download 856dfe3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T10:55:02Z
Download e0baf88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 8 2022-12-15T02:24:04Z
Download 36f4031 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp23-0-g4f5dcf38f) 30 2022-12-10T09:12:12Z
Download 6e26d69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T11:32:14+01:00 Download ecd0a85
Download 484e38c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T10:51:21+01:00 Download bcde728
Download 443e310 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T07:35:33+01:00 Download 182f22e
Download d16bbb6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T06:32:59+01:00 Download e0baf88
Download f72a67b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T03:54:03+01:00 Download 856dfe3
Download 4bf4d03 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T02:34:23+01:00 Download 296cfc6
Download a90d948 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T00:06:34+01:00 Download 2c5303b
Download ad43d94 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T22:51:52+01:00 Download c2304c0
Download 1872427 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T22:40:31+01:00 Download 36f4031
Download cdc7d4f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T18:22:21+01:00 Download d14b883
Download da49d56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T17:44:25+01:00 Download 5d607f3
Download c561313 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T11:23:31+01:00 Download 9c355ed
Download 9b1f9a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T01:00:01+01:00 Download 873b5e0
Download c7de443 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-27T23:00:01+01:00 Download edc4cdc
Download 9c355ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2022-12-10T18:03:07+01:00
Download 296cfc6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 5 2022-12-11T21:24:28+01:00
Download 873b5e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2022-12-25T13:27:29+01:00
Download d14b883 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2022-12-10T00:24:38+01:00
Download 182f22e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 8 2022-12-13T21:32:46Z
Download edc4cdc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 9 2022-12-07T21:18:33+01:00
Download 835b9b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2022-12-07T22:46:46+01:00

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

Trying to find witnesses for program (626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898, sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c).

Found 23 witnesses for program sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c, 626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f6aac1a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2021-12-06T13:40:26+01:00
Download 9e8d2b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.2.8 3 2021-12-13T22:40:22Z
Download 9da1b48 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 8 2021-12-10T04:07:52Z
Download f9ede9e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 8 2021-12-10T13:33:35Z
Download b1a3c3a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp22-0-ge852ac510) 9 2021-12-07T21:01:00Z
Download 0068227 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-14T00:13:18+01:00 Download 9e8d2b2
Download 5a324da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-10T21:16:19+01:00 Download 8c9cf52
Download 640c60f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-10T17:28:10+01:00 Download f9ede9e
Download 6d48bf5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-10T08:35:01+01:00 Download 9da1b48
Download 0122644 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-09T15:37:52+01:00 Download 2be3cbf
Download 3bae717 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-08T21:45:12+01:00 Download 7349569
Download 40ea8cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-07T23:31:54+01:00 Download b1a3c3a
Download 5ddeb4a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-07T02:55:59+01:00 Download 7c0f127
Download e4b7784 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-06T14:48:51+01:00 Download f6aac1a
Download b368cac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-06T01:14:49+01:00 Download 9179679
Download 81cc5c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-05T20:00:11+01:00 Download a784b7c
Download a784b7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-05T14:32:41+01:00
Download 8c9cf52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2021-12-10T17:16:58+01:00
Download 7349569 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 5 2021-12-08T19:54:35+01:00
Download 2be3cbf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 5 2021-12-09T10:23:59+01:00
Download 7c0f127 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 8 2021-12-06T17:39:00Z
Download 9179679 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 9 2021-12-05T22:48:17+01:00
Download 30ef8d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2021-12-06T00:43:17+01:00

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

Trying to find witnesses for program (626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898, sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c).

Found 12 witnesses for program sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c, 626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 79e2c7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.2.1 3 2020-12-06T23:47:45
Download ce3d76b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (svcomp21-0-g82e03b87) 9 2020-12-07T10:05:24
Download fb46840 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-09T22:04:33+01:00 Download a1cbcab
Download 5d3b2c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-09T21:38:47+01:00 Download 72c2e4a
Download 4e5122a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-09T02:15:01+01:00 Download 7110239
Download 6132a56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-08T07:44:31+01:00 Download 6e22b40
Download d92137d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-07T21:12:16+01:00 Download ce3d76b
Download 3541837 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-07T00:08:42+01:00 Download 79e2c7c
Download f974def Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-06T16:57:54+01:00 Download ff5c7fa
Download 0586ff2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-06T13:12:58+01:00 Download 0af9638
Download 0af9638 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-05T13:56:43+01:00
Download 6e22b40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 5 2020-12-08T05:16:11+01:00

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

Trying to find witnesses for program (626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898, sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c).

Found 2 witnesses for program sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c, 626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 41f684e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 5 2019-11-29T21:25:55+01:00
Download 395b720 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 5 2019-12-01T05:10:37+01:00

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

Trying to find witnesses for program (626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898, sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c).

Found 3 witnesses for program sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c, 626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download be41c09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness SMACK 1.9.3 3 2018-12-08T07:22:48
Download 576c59e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-07T09:41:22+01:00
Download 0554fff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-05T19:54:23+01:00

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

Trying to find witnesses for program (626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898, sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c).

Found 9 witnesses for program sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c, 626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6d96bd5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 8 2017-12-03T07:44Z
Download f84eb8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 8 2017-12-03T10:27Z
Download 40c2dda Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T17:32:19.276399
Download 0507833 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 3.1 6 2017-12-01T14:31 CET (sv-comp)
Download 525b932 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T11:04:54+01:00
Download b77fda9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 8 2017-12-03T10:38Z
Download b56ef58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 9 2017-12-01T10:22 CET (sv-comp)
Download c9011d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 6 2017-12-01T19:26 CET (sv-comp)
Download 73fefd5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2017-12-01T12:11 CET (sv-comp)

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

Trying to find witnesses for program (626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898, sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c, 626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/626f3da6fd18561761a79d5d72b6e4952ec90284e3abc32807b89f761ebfb898.json

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