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/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c
programSHA f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462
witnessName results-verified/esbmc-kind.2017-12-02_1823.logfiles/sv-comp18.LeikeHeizmann-WST2014-Ex6_false-no-overflow.c.files/witness.graphml
witnessSHA 8baf46439f278ac9d728fec689947b61654e301affb5e5f791f34d495fbe7352

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/8baf46439f278ac9d728fec689947b61654e301affb5e5f791f34d495fbe7352.json

Key Value
architecture 64bit
creationtime 2017-12-02T17:53:36.825872
producer ESBMC 4.6.0 kind
program-sha256 f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462
programfile ../../sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c
programhash 947235a588f48ba2205d0e28208675772856b98e
sourcecodelang C
specification CHECK( init(main()), LTL(G ! overflow) )
witness-file witnessFileByHash/8baf46439f278ac9d728fec689947b61654e301affb5e5f791f34d495fbe7352.graphml
witness-sha256 8baf46439f278ac9d728fec689947b61654e301affb5e5f791f34d495fbe7352
witness-size 4007
witness-type violation_witness

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

Trying to find witnesses for program (f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462, sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c).

Found 39 witnesses for program sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c, f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 05ce3a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T06:37:15Z
Download d912cf3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness crux-llvm-0.5.0.99 4 2023-12-18T05:22:14+01:00
Download 8f4d86d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness VeriOover 2 2023-12-20T03:37 CET (comp)
Download 20c9c48 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Taipan 5 2023-12-02T07:28:56Z
Download e2fb0c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 3 2023-11-29T16:59:50Z
Download b5c9046 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2023-12-19T23:02:47
Download a04f22b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Kojak 5 2023-12-02T22:10:51Z
Download 4f6c0e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 7.4.0 kind 4 2023-12-01T13:04:54Z
Download 7ef5176 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 6 2023-12-20T03:41:31+01:00 Download 8f4d86d
Download eff764a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-20T02:40:45+01:00 Download b5c9046
Download 3c85ec8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-19T05:26:14+01:00 Download 9f205d4
Download 2fca28f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 7 2023-12-18T06:07:22+01:00 Download d912cf3
Download 0e49874 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-05T14:38:49+01:00 Download 3c64c4c
Download 098a457 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-04T16:44:06+01:00 Download 870bb57
Download c69f892 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-04T12:13:28+01:00 Download 20c9c48
Download 1e8eaa8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-04T02:27:37+01:00 Download c497f59
Download 5b57c6a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-03T18:33:10+01:00 Download 4e80aeb
Download 2462e59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-03T10:00:01+01:00 Download 05ce3a8
Download 747baac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-03T06:18:27+01:00 Download a04f22b
Download 1988862 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-01T22:46:20+01:00 Download 817bd2f
Download c9304be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-01T18:26:51+01:00 Download 4f6c0e0
Download 6419f15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-01T00:28:07+01:00 Download 07b3b06
Download 34b55ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-11-30T13:44:11+01:00 Download 2372b85
Download 2855ae6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-11-30T03:04:40+01:00 Download e2fb0c5
Download 2372b85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-11-30T02:04:29+01:00
Download b0b1060 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-11-29T08:33:33+01:00 Download 7e8287e
Download c497f59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 5 2023-12-03T21:57:06+01:00
Download 9f205d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2023-12-18T16:54:19+01:00
Download eeed8c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CBMC 5 2023-12-17T15:52:06+01:00
Download 3c64c4c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Bubaak 3 2023-12-05T07:28:19Z
Download 870bb57 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Bubaak 3 2023-12-04T09:18:08Z
Download 7e8287e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Automizer 5 2023-11-28T19:36:47Z
Download 07b3b06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness 2LS 4 2023-11-30T23:23:15+01:00
Download 4e80aeb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:36:35+01:00
Download 82bb1ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-19T15:33:45+01:00 Download 1808133
Download 0587a9d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-17T22:07:59+01:00 Download eeed8c4
Download 817bd2f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-01T20:28:41Z
Download cb46685 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: d5370896-d418-4a81-b927-12ea040d95c7 creation_time: 2023-11-30T22:30:19Z 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-WST2014-Ex6.c''' task: input_files: - ../../sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-WST2014-Ex6.c input_file_hashes: ../../sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-WST2014-Ex6.c: f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: [] violation_witness CPAchecker 2.3 6 2023-12-01T05:35:35+01:00
Download 4f41924 Inspect Inspect
Validate
- content: - segment: - waypoint: action: follow constraint: format: C value: \result == 1073741824 location: column: 28 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_fda4fbe3-a4a5-4dba-888e-cb4cf425529e/sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-WST2014-Ex6.c line: 15 type: function_return - segment: - waypoint: action: follow constraint: format: C value: \result == 1 location: column: 28 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_fda4fbe3-a4a5-4dba-888e-cb4cf425529e/sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-WST2014-Ex6.c line: 16 type: function_return - segment: - waypoint: action: follow location: column: 3 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_fda4fbe3-a4a5-4dba-888e-cb4cf425529e/sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-WST2014-Ex6.c line: 18 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T16:59:50Z' format_version: '0.1' producer: name: symbiotic task: data_model: LP64 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_fda4fbe3-a4a5-4dba-888e-cb4cf425529e/sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-WST2014-Ex6.c : f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_fda4fbe3-a4a5-4dba-888e-cb4cf425529e/sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-WST2014-Ex6.c language: C specification: CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 7 2023-11-30T02:57:41+01:00

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

Trying to find witnesses for program (f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462, sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c).

Found 36 witnesses for program sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c, f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 597bc15 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness verifuzz 3 2022-12-15T10:38:06+01:00
Download a263d5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T10:38:24Z
Download 07197dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness crux-llvm-0.5.0.99 4 2022-12-09T03:39:52+01:00
Download 8f4d86d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness VeriOover 2 2022-12-12T10:59 CET (comp)
Download d767900 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Taipan 5 2022-12-14T06:37:22Z
Download d586036 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 3 2022-12-12T13:44:43Z
Download 4581c9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2022-12-11T13:46:03
Download a19c4fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Kojak 5 2022-12-14T15:35:24Z
Download 2115a7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 7.0.0 kind 4 2022-12-18T19:23:37Z
Download d88f9ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 6.8.0 kind 4 2022-12-25T08:51:22Z
Download 8bdbac8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 6 2023-01-29T11:32:31+01:00 Download 8f4d86d
Download b9d852b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-29T10:43:15+01:00 Download d767900
Download e6be846 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-29T06:53:57+01:00 Download 6909cff
Download ff13ff5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-29T06:38:17+01:00 Download a19c4fd
Download 85eb3e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-29T05:56:10+01:00 Download d586036
Download 17f2d60 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-29T04:31:20+01:00 Download 4581c9f
Download 7e524d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-29T01:32:25+01:00 Download aa30acb
Download 2951b49 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-28T22:51:43+01:00 Download 51954f9
Download 6dcc925 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-28T21:08:09+01:00 Download 66111e5
Download c18bbe3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-28T17:45:26+01:00 Download a263d5c
Download 5d4743b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-28T15:41:58+01:00 Download 2115a7d
Download e717e57 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-28T08:56:18+01:00 Download a5312c7
Download 70a0cfe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 7 2023-01-28T08:36:24+01:00 Download 07197dd
Download 81e09da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-28T02:23:40+01:00 Download d88f9ce
Download 3c07948 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-27T23:39:10+01:00 Download 2e7eeab
Download a5312c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2022-12-10T17:11:44+01:00
Download aa30acb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 5 2022-12-11T21:09:45+01:00
Download 66111e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2022-12-09T23:58:11+01:00
Download eec5ad0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CBMC 5 2022-12-08T05:43:54+01:00
Download 1406a1a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Bubaak 3 2022-12-08T20:23:00Z
Download 6909cff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Automizer 5 2022-12-13T20:45:17Z
Download 2e7eeab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness 2LS 4 2022-12-07T22:52:22+01:00
Download 51954f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T22:01:48+01:00
Download f0abae8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T00:53:05+01:00 Download 151d5c5
Download ab75847 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T04:24:09+01:00 Download eec5ad0
Download 104883c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T00:29:50+01:00 Download 1406a1a

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

Trying to find witnesses for program (f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462, sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c).

Found 29 witnesses for program sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c, f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5aed2fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness verifuzz 3 2021-12-11T10:23:53+01:00
Download c9a2ad4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.8 3 2021-12-13T21:54:23Z
Download 5c9f583 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness crux-llvm-0.5.0.99 4 2021-12-07T06:34:45+01:00
Download 883817b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Taipan 5 2021-12-10T01:55:33Z
Download 46003eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 3 2021-12-07T12:37:26Z
Download aaf8f1b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2021-12-09T07:59:15
Download 4a755a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Kojak 5 2021-12-10T11:10:02Z
Download 953eb85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 6.8.0 kind 4 2021-12-08T04:36:27Z
Download bceff21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 5 2021-12-14T00:08:14+01:00 Download c9a2ad4
Download 9ec62a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 5 2021-12-10T21:29:13+01:00 Download 6b54a0b
Download ee388bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 5 2021-12-10T17:27:01+01:00 Download 4a755a5
Download 0aa0e84 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 5 2021-12-10T08:34:01+01:00 Download 883817b
Download 2656348 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 5 2021-12-09T16:01:52+01:00 Download d319639
Download 8cbe642 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 5 2021-12-09T10:15:01+01:00 Download aaf8f1b
Download d398b98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 5 2021-12-08T21:11:26+01:00 Download 95281f9
Download ea8f303 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 5 2021-12-08T13:49:20+01:00 Download 953eb85
Download 20c7afc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 5 2021-12-07T19:12:41+01:00 Download 46003eb
Download bb8abc8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 7 2021-12-07T08:14:40+01:00 Download 5c9f583
Download 3e6b2e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 5 2021-12-07T02:36:20+01:00 Download 232ae45
Download 7c0b342 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 5 2021-12-06T01:23:39+01:00 Download efa15f7
Download 5880504 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 5 2021-12-05T20:40:30+01:00 Download a025b85
Download a025b85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 5 2021-12-05T15:10:12+01:00
Download 95281f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 5 2021-12-08T19:01:15+01:00
Download d319639 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 5 2021-12-09T14:49:05+01:00
Download 8246453 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CBMC 5 2021-12-06T01:07:43+01:00
Download 232ae45 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Automizer 5 2021-12-07T00:30:18Z
Download efa15f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness 2LS 4 2021-12-05T23:08:25+01:00
Download a672c8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2021-12-06T13:43:36+01:00
Download 53d033d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-06T11:49:11+01:00 Download 8246453

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

Trying to find witnesses for program (f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462, sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c).

Found 22 witnesses for program sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c, f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d77722a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.1 3 2020-12-06T23:46:56
Download bd1f21a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 3 2020-12-11T23:09:44
Download ab34515 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 2 2020-12-08T23:40:04
Download 571487b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2020-12-08T11:19:18
Download 3a53a56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-12T01:31:54+01:00 Download bd1f21a
Download 401d5dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-09T22:13:08+01:00 Download 99a57e6
Download 31914ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-09T21:32:39+01:00 Download 7d490f8
Download 10a9993 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-09T04:01:21+01:00 Download ab34515
Download 898110e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-09T02:12:14+01:00 Download 0866896
Download 911ac3d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-08T13:15:15+01:00 Download 571487b
Download d9a7e4f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-08T07:56:15+01:00 Download c3f285d
Download 472f47f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-07T17:01:06+01:00 Download 088a99d
Download 753c946 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-07T00:16:54+01:00 Download d77722a
Download f9b6a51 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-06T18:02:08+01:00 Download 892823e
Download a06c7c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-05T18:36:04+01:00 Download 892823e
Download 892823e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-05T13:37:20+01:00
Download c3f285d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 5 2020-12-07T22:35:59+01:00
Download ae0c287 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) unknown_witness Goblint (svcomp21-0-g82e03b87) 3 2020-12-07T14:36:26
Download 4052334 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-06T19:15:30+01:00 Download 121e884
Download d3112f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-06T18:26:36+01:00 Download 7c84289
Download 1d7ba1a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-06T10:35:09+01:00 Download 121e884
Download 3b8662d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-06T07:46:30+01:00 Download 7c84289

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

Trying to find witnesses for program (f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462, sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c).

Found 15 witnesses for program sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c, f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 20971e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 1 2019-12-01 05:52:27
Download e834eef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2019-12-04T01:27 CET (comp)
Download 19a0fa6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-11T21:46:34+01:00 Download 057a6ec
Download 248a249 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-11T21:46:02+01:00 Download 6999833
Download 8a3e982 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-11T21:09:01+01:00 Download 20971e7
Download 8857999 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-11T20:54:29+01:00 Download 6569483
Download bd46fb6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-11T20:44:33+01:00 Download 6d3abec
Download 106d9a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-08T00:26:10+01:00 Download 6234524
Download 3f921ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-07T21:18:01+01:00 Download fd67a0c
Download c298ac3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-04T02:58:04+01:00 Download e834eef
Download 6a8d5b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-03T08:02:38+01:00 Download d13fe4d
Download d13fe4d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-11-30T05:17:30+01:00
Download 6999833 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 5 2019-12-01T02:02:22+01:00
Download 9221453 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 4 2019-12-05T20:20:22+01:00 Download d505e31
Download 8248a8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 4 2019-12-05T19:34:01+01:00 Download 9a80bc6

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

Trying to find witnesses for program (f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462, sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c).

Found 18 witnesses for program sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c, f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 13bc96e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 2 2018-12-07T21:50 CET (sv-comp)
Download 54ac9ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness SMACK 1.9.3 4 2018-12-08T03:38:28
Download 9b6caf5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2018-12-07T01:31 CET (sv-comp)
Download 56ee1b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-07T23:26:11+01:00
Download a535a9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:53:16+01:00 Download a25a6a1
Download 6986836 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:39:57+01:00 Download 10d53f8
Download 4df25de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:24:29+01:00 Download b3cbe23
Download bbdc4c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T18:20:43+01:00 Download f27a72f
Download 4085110 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T23:44:47+01:00 Download 13bc96e
Download 5287c1a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T22:09:05+01:00 Download 54ac9ed
Download b6af190 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T09:02:38+01:00 Download 56ee1b2
Download a343198 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T05:04:27+01:00 Download ec760ac
Download 8f4be5a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T17:45:40+01:00 Download 9b6caf5
Download eedd957 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:49:10+01:00 Download 3e2a509
Download 326e9fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:42:14+01:00 Download 4495992
Download 2cd8206 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:14:45+01:00 Download 995656a
Download 3e2a509 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T04:51:00+01:00
Download 33f4332 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:12:34+01:00 Download 01e84c4

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

Trying to find witnesses for program (f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462, sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c).

Found 20 witnesses for program sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c, f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 571e1c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Taipan 5 2017-12-03T07:43Z
Download 05c5b2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 2 2017-12-03T04:20 CET (sv-comp)
Download 5d6e483 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Map2Check 3 2017-12-02T01:57 CET (sv-comp)
Download f82bd98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Kojak 5 2017-12-03T10:30Z
Download 8baf464 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T17:53:36.825872
Download fae94b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-02T05:40:39.006401
Download c1088de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 3.1 4 2017-12-01T13:55 CET (sv-comp)
Download e88a37f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T11:52:56+01:00 d3e6ad0
Download fa92d5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T11:52:08+01:00 52971e8
Download c6a8e90 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T08:58:56+01:00 734f7e3
Download 05e3f83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T05:12:14+01:00 724e2ec
Download e62535e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T20:06:48+01:00 b601504
Download 0477ad2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T08:15:03+01:00 d918928
Download 02799e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T12:02:26+01:00 7959e03
Download 80f9675 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T11:19:00+01:00 8196fc9
Download 177af92 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T11:14:24+01:00
Download 82a3054 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CBMC 5 2017-12-01T12:05 CET (sv-comp)
Download e338acb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Automizer 5 2017-12-03T10:21Z
Download 4f9547d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness 2LS 4 2017-12-01T10:35 CET (sv-comp)
Download 4bde02d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T12:32:43+01:00 644a8aa

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

Trying to find witnesses for program (f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462, sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c, f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f60779531d4ef4e8b10b9b9577dc8311e00cfe5c74bee43d157f8b3f754e1462.json

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