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/Benghazi_nondet_false-no-overflow.c
programSHA b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d
witnessName results-verified/depthk.2017-12-01_1307.logfiles/sv-comp18.Benghazi_nondet_false-no-overflow.c.files/witness.graphml
witnessSHA 260309a5fa30e3ec7229dd10211483221c4307256d5681a875391df6327bee0c

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/260309a5fa30e3ec7229dd10211483221c4307256d5681a875391df6327bee0c.json

Key Value
architecture 32bit
creationtime 2017-12-01T13:26 CET (sv-comp)
memoryModel precise
producer ESBMC 3.1
program-sha256 b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d
programfile /tmp/vcloud-vcloud-master/worker/working_dir_57f21b67-91dd-4c9b-a373-5508b77fd830/sv-benchmarks/c/termination-crafted/Benghazi_nondet_false-no-overflow.c
programhash 4b00a880f08a57cdde8634a0eb6e47259ec0173f
sourcecodelang C
specification CHECK( init(main()), LTL(G ! overflow) )
witness-file witnessFileByHash/260309a5fa30e3ec7229dd10211483221c4307256d5681a875391df6327bee0c.graphml
witness-sha256 260309a5fa30e3ec7229dd10211483221c4307256d5681a875391df6327bee0c
witness-size 4716
witness-type violation_witness

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

Trying to find witnesses for program (b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d, sv-benchmarks/c/termination-crafted/Benghazi_nondet_false-no-overflow.c).

Found 35 witnesses for program sv-benchmarks/c/termination-crafted/Benghazi_nondet_false-no-overflow.c, b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8060c79 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness crux-llvm-0.5.0.99 4 2023-12-18T05:23:57+01:00
Download d4cc720 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness VeriOover 2 2023-12-20T03:37 CET (comp)
Download 1bcac4d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Taipan 5 2023-12-02T16:05:20Z
Download af6b065 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 3 2023-11-29T23:19:36Z
Download d1ce837 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2023-12-19T22:26:03
Download 5140d6a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Kojak 5 2023-12-02T20:30:43Z
Download c6fbd74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 7.4.0 kind 4 2023-12-01T11:43:44Z
Download 4df8d12 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 6 2023-12-20T03:41:27+01:00 Download d4cc720
Download 745a918 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-20T02:40:12+01:00 Download d1ce837
Download a9a33f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-19T05:25:50+01:00 Download fcf14ca
Download 99af120 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 8 2023-12-18T06:13:50+01:00 Download 8060c79
Download 1cb6663 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-05T14:40:11+01:00 Download 27fa35e
Download c56b071 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-04T16:45:27+01:00 Download 7132ab0
Download 9d7162e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-04T12:12:29+01:00 Download 1bcac4d
Download edfc3a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-04T02:25:26+01:00 Download f1fa778
Download 78dc02d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-03T18:36:43+01:00 Download b58f3d0
Download f757c18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-03T06:19:14+01:00 Download 5140d6a
Download 9c3e213 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-12-01T18:29:15+01:00 Download c6fbd74
Download 7a6c54e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-11-30T13:44:59+01:00 Download d29f88a
Download d29f88a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-11-30T07:29:55+01:00
Download b89b286 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 5 2023-11-29T08:32:41+01:00 Download c89fdaf
Download f1fa778 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 5 2023-12-03T22:35:50+01:00
Download fcf14ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2023-12-18T22:57:38+01:00
Download bc822f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CBMC 6 2023-12-17T20:31:56+01:00
Download 27fa35e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Bubaak 3 2023-12-05T12:18:34Z
Download 7132ab0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Bubaak 3 2023-12-04T10:00:04Z
Download c89fdaf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Automizer 5 2023-11-29T01:29:06Z
Download 5e2eac7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness 2LS 5 2023-11-30T21:44:39+01:00
Download b58f3d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:20:06+01:00
Download 560f707 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-19T15:33:55+01:00 Download 39bf109
Download ffe3497 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-17T22:08:53+01:00 Download bc822f4
Download 7cb0570 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-01T00:29:20+01:00 Download 5e2eac7
Download 392b13f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-30T03:01:13+01:00 Download af6b065
Download 25e44e5 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: bb71f0ab-912c-45ef-9073-d399ded93f91 creation_time: 2023-12-01T02:03:34Z 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/Benghazi_nondet-1.c''' task: input_files: - ../../sv-benchmarks/c/termination-crafted/Benghazi_nondet-1.c input_file_hashes: ../../sv-benchmarks/c/termination-crafted/Benghazi_nondet-1.c: b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: [] violation_witness CPAchecker 2.3 6 2023-12-01T05:00:00+01:00
Download 175d296 Inspect Inspect
Validate
- content: - segment: - waypoint: action: follow constraint: format: C value: \result == 0 location: column: 31 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d6868a91-b974-4df5-b572-a04565d36699/sv-benchmarks/c/termination-crafted/Benghazi_nondet-1.c line: 14 type: function_return - segment: - waypoint: action: follow constraint: format: C value: \result == 2147483648 location: column: 32 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d6868a91-b974-4df5-b572-a04565d36699/sv-benchmarks/c/termination-crafted/Benghazi_nondet-1.c line: 15 type: function_return - segment: - waypoint: action: follow constraint: format: C value: \result == 0 location: column: 32 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d6868a91-b974-4df5-b572-a04565d36699/sv-benchmarks/c/termination-crafted/Benghazi_nondet-1.c line: 16 type: function_return - segment: - waypoint: action: follow location: column: 3 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d6868a91-b974-4df5-b572-a04565d36699/sv-benchmarks/c/termination-crafted/Benghazi_nondet-1.c line: 18 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T23:19:36Z' format_version: '0.1' producer: name: symbiotic task: data_model: LP64 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d6868a91-b974-4df5-b572-a04565d36699/sv-benchmarks/c/termination-crafted/Benghazi_nondet-1.c : b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d6868a91-b974-4df5-b572-a04565d36699/sv-benchmarks/c/termination-crafted/Benghazi_nondet-1.c language: C specification: CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 7 2023-11-30T02:59:51+01:00

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

Trying to find witnesses for program (b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d, sv-benchmarks/c/termination-crafted/Benghazi_nondet_false-no-overflow.c).

Found 34 witnesses for program sv-benchmarks/c/termination-crafted/Benghazi_nondet_false-no-overflow.c, b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0857601 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness verifuzz 3 2022-12-15T08:04:27+01:00
Download cfe28e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness crux-llvm-0.5.0.99 4 2022-12-09T05:01:47+01:00
Download d4cc720 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness VeriOover 2 2022-12-12T11:01 CET (comp)
Download 4fc5196 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Taipan 5 2022-12-14T15:00:06Z
Download 672a829 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 3 2022-12-12T17:26:19Z
Download 26d0ace Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2022-12-11T14:27:40
Download 27b732a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Kojak 5 2022-12-14T21:21:05Z
Download 51d6c22 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 7.0.0 kind 4 2022-12-18T19:39:43Z
Download dc9dda4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 6.8.0 kind 4 2022-12-25T08:28:25Z
Download 956bbe1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 6 2023-01-29T11:32:31+01:00 Download d4cc720
Download f737e2b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-29T10:43:57+01:00 Download 4fc5196
Download 832153d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-29T06:53:36+01:00 Download b3001d0
Download 2fd6fc0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-29T06:39:01+01:00 Download 27b732a
Download 78d454b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-29T04:30:54+01:00 Download 26d0ace
Download 99ecbf7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-29T01:31:48+01:00 Download 9f5f914
Download 0a007b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-28T22:51:41+01:00 Download e29a7f4
Download be2d41c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-28T21:06:18+01:00 Download 5f947a6
Download 4ad2e9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 6 2023-01-28T15:45:31+01:00 Download 51d6c22
Download 4338ed4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-28T08:55:18+01:00 Download 433ec8e
Download 4e3fd53 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 8 2023-01-28T08:32:26+01:00 Download cfe28e9
Download 16ac00e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2023-01-28T02:23:41+01:00 Download dc9dda4
Download 433ec8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 5 2022-12-10T19:54:37+01:00
Download 9f5f914 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 5 2022-12-11T21:43:49+01:00
Download 5f947a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2022-12-10T04:35:59+01:00
Download 1a6836b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CBMC 6 2022-12-08T10:25:47+01:00
Download 884c8ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Bubaak 3 2022-12-08T21:37:55Z
Download b3001d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Automizer 5 2022-12-13T21:22:53Z
Download 4104b02 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness 2LS 5 2022-12-08T00:24:24+01:00
Download e29a7f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T22:02:03+01:00
Download f4fd1ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T05:57:11+01:00 Download 672a829
Download 106fd0d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T00:53:02+01:00 Download 1bb898a
Download dda37cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T04:24:05+01:00 Download 1a6836b
Download d745f21 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T00:30:16+01:00 Download 884c8ec
Download 0fd739d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-27T23:39:13+01:00 Download 4104b02

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

Trying to find witnesses for program (b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d, sv-benchmarks/c/termination-crafted/Benghazi_nondet_false-no-overflow.c).

Found 27 witnesses for program sv-benchmarks/c/termination-crafted/Benghazi_nondet_false-no-overflow.c, b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d47447c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness verifuzz 3 2021-12-11T08:26:38+01:00
Download d601000 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness crux-llvm-0.5.0.99 4 2021-12-07T07:46:19+01:00
Download 46240f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Taipan 5 2021-12-10T03:18:09Z
Download e16cb8a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 3 2021-12-07T14:56:38Z
Download 9d5b7a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2021-12-09T06:28:59
Download 282dc33 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Kojak 5 2021-12-10T13:19:16Z
Download e1ac9b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 6.8.0 kind 4 2021-12-08T04:33:37Z
Download 09277ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 5 2021-12-10T21:25:17+01:00 Download a6a70fd
Download 73fa445 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 5 2021-12-10T17:27:19+01:00 Download 282dc33
Download fd0194e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 5 2021-12-10T08:33:15+01:00 Download 46240f7
Download 37bec1e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 5 2021-12-09T16:00:39+01:00 Download 65fc551
Download 2a84ec0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 5 2021-12-09T10:15:00+01:00 Download 9d5b7a7
Download b7a290f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 5 2021-12-08T21:06:35+01:00 Download e0c0d13
Download 759bb57 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 5 2021-12-08T13:48:49+01:00 Download e1ac9b2
Download c3a8242 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 8 2021-12-07T08:13:58+01:00 Download d601000
Download f1df019 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 5 2021-12-07T02:37:03+01:00 Download ef20706
Download cac069b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 5 2021-12-05T20:40:57+01:00 Download e435179
Download e435179 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 5 2021-12-05T18:04:59+01:00
Download e0c0d13 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 5 2021-12-08T20:32:29+01:00
Download 65fc551 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 5 2021-12-09T11:58:00+01:00
Download 78df337 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CBMC 5 2021-12-06T05:15:40+01:00
Download ef20706 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Automizer 5 2021-12-06T19:47:47Z
Download 9007b0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness 2LS 5 2021-12-05T22:22:32+01:00
Download 124430a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2021-12-06T13:39:44+01:00
Download b67215b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-07T19:09:48+01:00 Download e16cb8a
Download 3a0fb63 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-06T11:49:06+01:00 Download 78df337
Download d53debd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-06T01:25:34+01:00 Download 9007b0e

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

Trying to find witnesses for program (b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d, sv-benchmarks/c/termination-crafted/Benghazi_nondet_false-no-overflow.c).

Found 22 witnesses for program sv-benchmarks/c/termination-crafted/Benghazi_nondet_false-no-overflow.c, b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6fd4e56 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.1 3 2020-12-06T23:35:44
Download f0ea3ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 3 2020-12-11T17:06:39
Download d684864 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 3 2020-12-08T14:07:36
Download 5093dd0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2020-12-08T08:30:32
Download 25146ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-09T22:02:31+01:00 Download d258560
Download 18de3e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-09T21:41:08+01:00 Download 41dfd29
Download b4b36e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-09T01:54:11+01:00 Download adad805
Download ba5a79c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-08T13:12:51+01:00 Download 5093dd0
Download 4d3a4e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-08T07:57:22+01:00 Download a90ba4f
Download f83edbc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-07T16:44:03+01:00 Download de62076
Download 8969af7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-07T00:14:00+01:00 Download 6fd4e56
Download 2be2599 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-06T18:01:39+01:00 Download 958d527
Download 9492e4c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-05T18:09:58+01:00 Download 958d527
Download 958d527 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 5 2020-12-05T14:18:26+01:00
Download a90ba4f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 5 2020-12-07T23:22:05+01:00
Download e3ddd92 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) unknown_witness Goblint (svcomp21-0-g82e03b87) 3 2020-12-07T18:19:01
Download 04cd312 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-12T01:27:25+01:00 Download f0ea3ed
Download c19103e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-09T04:00:33+01:00 Download d684864
Download 7bf155b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-06T19:25:44+01:00 Download 2ca3206
Download b0b7cfc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-06T18:25:06+01:00 Download 1620f9e
Download d2185be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-06T10:28:54+01:00 Download 2ca3206
Download 2545553 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-06T07:39:38+01:00 Download 1620f9e

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

Trying to find witnesses for program (b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d, sv-benchmarks/c/termination-crafted/Benghazi_nondet_false-no-overflow.c).

Found 15 witnesses for program sv-benchmarks/c/termination-crafted/Benghazi_nondet_false-no-overflow.c, b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3519d5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 1 2019-12-01 21:16:13
Download 6f5a3e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2019-12-03T22:38 CET (comp)
Download 355d517 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-11T21:51:46+01:00 Download 34f98dd
Download e6f31e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-11T21:44:15+01:00 Download 49af556
Download 48f378e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-11T20:54:50+01:00 Download ed9d3f2
Download 22b4016 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 11 2019-12-11T20:44:31+01:00 Download 00ea0da
Download 2bcb5df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-08T00:26:03+01:00 Download 50bc247
Download e994373 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-07T21:18:42+01:00 Download 6a64aaa
Download 5c99058 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-04T02:58:53+01:00 Download 6f5a3e2
Download d69b2af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-03T08:10:36+01:00 Download 8618571
Download 8618571 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-11-30T09:53:37+01:00
Download 49af556 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 5 2019-12-01T07:48:17+01:00
Download cb771e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 4 2019-12-11T21:09:00+01:00 Download 3519d5c
Download ac67b2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 4 2019-12-05T20:21:24+01:00 Download 0cf902a
Download e480bd8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 4 2019-12-05T19:34:29+01:00 Download 7237f05

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

Trying to find witnesses for program (b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d, sv-benchmarks/c/termination-crafted/Benghazi_nondet_false-no-overflow.c).

Found 18 witnesses for program sv-benchmarks/c/termination-crafted/Benghazi_nondet_false-no-overflow.c, b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8439596 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 2 2018-12-08T16:56 CET (sv-comp)
Download 362fd59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness SMACK 1.9.3 4 2018-12-08T10:05:10
Download 7ba6aae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2018-12-07T09:36 CET (sv-comp)
Download e32d99e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-08T02:12:13+01:00
Download 2319994 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:53:08+01:00 Download a00bd4e
Download 54a7bb1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:38:05+01:00 Download 7f7dcdd
Download 668e837 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:18:56+01:00 Download db5d621
Download 83e7e25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-09T18:20:45+01:00 Download 742eaf5
Download de86d3a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T23:43:06+01:00 Download 8439596
Download a517872 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T22:07:58+01:00 Download 362fd59
Download 454a362 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T08:47:53+01:00 Download e32d99e
Download 944257b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T04:59:49+01:00 Download f01cd99
Download fea08f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T17:45:44+01:00 Download 7ba6aae
Download 677d598 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:47:54+01:00 Download aedef86
Download dafb859 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 6 2018-12-06T09:41:41+01:00 Download 7945493
Download aedef86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-05T22:31:27+01:00
Download 6f8859e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:20:05+01:00 Download 90aae5b
Download f6c410f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:17:51+01:00 Download 3297fbc

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

Trying to find witnesses for program (b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d, sv-benchmarks/c/termination-crafted/Benghazi_nondet_false-no-overflow.c).

Found 20 witnesses for program sv-benchmarks/c/termination-crafted/Benghazi_nondet_false-no-overflow.c, b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 89604be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Taipan 5 2017-12-03T07:43Z
Download 58a65d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 2 2017-12-03T04:35 CET (sv-comp)
Download d3de2a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Map2Check 3 2017-12-02T00:58 CET (sv-comp)
Download 55c955a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Kojak 5 2017-12-03T10:24Z
Download 0245518 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T17:57:01.741723
Download 79bbc52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-02T06:09:10.589944
Download 260309a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 3.1 5 2017-12-01T13:26 CET (sv-comp)
Download 478967c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T11:53:01+01:00 c5528a8
Download 109dcc4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T11:52:12+01:00 17e7a6e
Download 21016eb 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 506910e
Download 90e6648 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T05:14:15+01:00 be0356f
Download d0130e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T20:10:01+01:00 4b24899
Download 4c94c5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T08:14:46+01:00 2743456
Download c5f9308 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T12:02:01+01:00 984d92b
Download ab46588 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T11:38:06+01:00
Download 2a5f320 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 6 2017-12-01T11:18:54+01:00 9c437e2
Download 3d2c5d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CBMC 8 2017-12-01T12:11 CET (sv-comp)
Download 74547a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Automizer 5 2017-12-03T10:26Z
Download 2d2d29c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness 2LS 5 2017-12-01T10:23 CET (sv-comp)
Download a985cb6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T12:32:46+01:00 00b74c8

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

Trying to find witnesses for program (b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d, sv-benchmarks/c/termination-crafted/Benghazi_nondet_false-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted/Benghazi_nondet_false-no-overflow.c, b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/b9c1fb96b371ca40c85c8007d14ad3e1270c8fac9b0bc1bc334ba14077a7910d.json

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