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/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c
programSHA 6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822
witnessName results-verified/uautomizer.2018-12-08_0742.logfiles/sv-comp19_prop-nooverflow.Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c.files/witness.graphml
witnessSHA e3998a4b4264d28bb814fdba8f4f6939b505baa32044c32a499243662a9ebb63

Information about the Witness from Competition Database

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

Key Value
architecture 64bit
creationtime 2018-12-09T09:11Z
producer Automizer
programfile /tmp/vcloud-vcloud-master/worker/working_dir_4acbd57e-cfe6-4df4-aa15-2e5da31ec926/sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c
programhash a03b979f45aa8ba48949293cad74f586aed4b0e9
sourcecodelang C
specification CHECK( init(main()), LTL(G ! overflow) )
witness-file witnessFileByHash/e3998a4b4264d28bb814fdba8f4f6939b505baa32044c32a499243662a9ebb63.graphml
witness-sha256 e3998a4b4264d28bb814fdba8f4f6939b505baa32044c32a499243662a9ebb63
witness-size 4242
witness-type correctness_witness

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

Trying to find witnesses for program (6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822, sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c).

Found 45 witnesses for program sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c, 6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6c834f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T07:27:56Z
Download f923b8f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness VeriOover 2 2023-12-20T03:37 CET (comp)
Download 9fbd648 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:49:00+01:00
Download aed39ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness crux-llvm-0.5.0.99 3 2023-12-18T05:10:17+01:00
Download 18a5e76 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 4 2023-12-02T14:38:02Z
Download 3b0967f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2023-12-17T04:24:39Z
Download b550466 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2023-11-29T20:45:53Z
Download 17efaca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T15:25:43Z
Download 9b376a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 4 2023-12-03T00:08:42Z
Download ade180c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 21 2023-12-01T01:58:26Z
Download ab01d6d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-20T03:41:30+01:00 Download f923b8f
Download 537a179 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-19T14:29:01+01:00 Download 71a3662
Download 59d63e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-19T05:00:27+01:00 Download 13b1fcb
Download 1ac624f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-18T06:17:56+01:00 Download aed39ca
Download 772242a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-17T06:08:42+01:00 Download 3b0967f
Download 73225e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-05T14:23:34+01:00 Download 7d3f2e5
Download 352cbd2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-04T16:28:16+01:00 Download c95ea63
Download 0e70f0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-04T11:32:28+01:00 Download 18a5e76
Download 3907cfc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-04T01:20:36+01:00 Download b39da1e
Download 786b24f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-03T18:30:01+01:00 Download 9fbd648
Download c084f5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-03T09:58:30+01:00 Download 6c834f8
Download 016eca7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-03T05:50:59+01:00 Download 9b376a6
Download fc7f8c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-01T22:45:33+01:00 Download 728d518
Download 2aebb37 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-01T03:42:34+01:00 Download ade180c
Download 866048d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-30T23:46:04+01:00 Download b952297
Download 98db89a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-30T11:35:47+01:00 Download cd1b2cf
Download cd1b2cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-30T05:36:53+01:00
Download abfb370 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-30T02:46:46+01:00 Download b550466
Download e733645 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-29T18:34:34+01:00 Download 17efaca
Download c7af366 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-29T08:03:10+01:00 Download 98a6685
Download b39da1e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 4 2023-12-03T22:52:46+01:00
Download 13b1fcb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 4 2023-12-18T20:58:28+01:00
Download 7d3f2e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 2 2023-12-05T11:05:32Z
Download c95ea63 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 2 2023-12-04T12:23:17Z
Download 728d518 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-01T20:07:18Z
Download 98a6685 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 4 2023-11-29T05:02:55Z
Download b952297 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 6 2023-11-30T23:22:06+01:00
Download 29f6ef5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.3 6 2023-11-30T09:03:15+01:00
Download e24bcac Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 6 2023-12-03T23:21:02+01:00
Download f8c7c75 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.1 6 2023-12-17T04:36:24+01:00
Download 1dc4f56 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2023-12-18T19:43:16+01:00
Download 0061c66 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 65ac4216-f031-44aa-8076-0e2723fca3d0 creation_time: '2023-12-03T01:08:42+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3d147474-46ed-4ff7-a6fd-baa8252cfbe5/sv-benchmarks/c/termination-crafted/Cairo_step2-3.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3d147474-46ed-4ff7-a6fd-baa8252cfbe5/sv-benchmarks/c/termination-crafted/Cairo_step2-3.c : 6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] correctness_witness CPAchecker 2.3 5 2023-12-03T05:40:47+01:00
Download 3d3b723 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 4fe14cfe-bde1-4831-91e5-119b32dcacdf creation_time: '2023-11-29T06:02:55+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_414fbe73-f09c-40cf-8172-81e976ffe29b/sv-benchmarks/c/termination-crafted/Cairo_step2-3.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_414fbe73-f09c-40cf-8172-81e976ffe29b/sv-benchmarks/c/termination-crafted/Cairo_step2-3.c : 6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] correctness_witness CPAchecker 2.3 5 2023-11-29T07:44:18+01:00
Download 3360b7a Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 08f0db85-515a-42f3-8f16-24a1e94818d0 creation_time: '2023-12-02T15:38:02+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e5cbb4b6-41c3-4699-aff5-cebfa4e0e1df/sv-benchmarks/c/termination-crafted/Cairo_step2-3.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e5cbb4b6-41c3-4699-aff5-cebfa4e0e1df/sv-benchmarks/c/termination-crafted/Cairo_step2-3.c : 6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] correctness_witness CPAchecker 2.3 5 2023-12-04T11:54:11+01:00
Download ee698a6 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: 051267a5-089c-47be-b200-9aaf497f67f6 creation_time: 2023-12-01T01:58:26Z 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/Cairo_step2-3.c''' task: input_files: - ../../sv-benchmarks/c/termination-crafted/Cairo_step2-3.c input_file_hashes: ../../sv-benchmarks/c/termination-crafted/Cairo_step2-3.c: 6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/Cairo_step2-3.c file_hash: 6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822 line: 16 column: 12 function: main value: (x != 4294967294U || (1U <= x && x != 0U)) || (((((((((((((((((x != 4294967260U && x != 4294967262U) && x != 4294967264U) && x != 4294967266U) && x != 4294967268U) && x != 4294967270U) && x != 4294967272U) && x != 4294967274U) && x != 4294967276U) && x != 4294967278U) && x != 4294967280U) && x != 4294967282U) && x != 4294967284U) && x != 4294967286U) && x != 4294967288U) && x != 4294967290U) && x != 4294967292U) && x != 4294967294U) format: c_expression correctness_witness CPAchecker 2.3 6 2023-12-01T05:38:18+01:00

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

Trying to find witnesses for program (6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822, sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c).

Found 35 witnesses for program sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c, 6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5e9bad4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T13:55:47Z
Download f923b8f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness VeriOover 2 2022-12-12T11:00 CET (comp)
Download a59d858 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-11T01:44:29+01:00
Download a4f2640 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness crux-llvm-0.5.0.99 3 2022-12-09T05:06:56+01:00
Download 84d74db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 4 2022-12-14T02:13:27Z
Download a8e589a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2022-12-25T09:51:36Z
Download f256488 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2022-12-12T16:37:35Z
Download 6f88075 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T09:50:43Z
Download eb85c0e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 4 2022-12-14T22:59:00Z
Download 18806da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp23-0-g4f5dcf38f) 46 2022-12-10T08:15:30Z
Download 049ae59 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T11:32:31+01:00 Download f923b8f
Download b99cd41 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T11:06:33+01:00 Download 84d74db
Download 45538e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T07:16:55+01:00 Download a816a5f
Download 3004d4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T06:28:26+01:00 Download eb85c0e
Download d02a8db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T05:29:21+01:00 Download f256488
Download 0de134d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T03:55:05+01:00 Download 6f88075
Download 664a9ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T02:35:39+01:00 Download 0bdf6e8
Download 54272a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T00:06:24+01:00 Download fb2e7d8
Download 82662d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T22:51:24+01:00 Download a59d858
Download 39abad4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T22:28:00+01:00 Download 18806da
Download 1696cbb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T17:58:56+01:00 Download 5814f97
Download e3fe76a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T17:46:04+01:00 Download 5e9bad4
Download d26f9a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T11:07:40+01:00 Download 988acae
Download c51852c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T08:21:15+01:00 Download a4f2640
Download c37f8b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T00:31:09+01:00 Download a8e589a
Download 0ee621c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-27T23:00:13+01:00 Download 31d8664
Download 988acae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2022-12-10T17:14:58+01:00
Download 0bdf6e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 4 2022-12-12T01:55:46+01:00
Download 5814f97 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 4 2022-12-09T23:10:06+01:00
Download a816a5f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 4 2022-12-13T19:42:50Z
Download 31d8664 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 6 2022-12-07T23:46:10+01:00
Download 046b243 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.2 6 2022-12-10T19:25:35+01:00
Download 1471302 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 6 2022-12-12T01:20:16+01:00
Download 66fc49c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.1 6 2022-12-25T13:05:03+01:00
Download f8e7af0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2022-12-10T03:35:46+01:00

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

Trying to find witnesses for program (6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822, sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c).

Found 30 witnesses for program sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c, 6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 24519bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.8 3 2021-12-13T21:14:32Z
Download e1b0882 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2021-12-06T13:42:26+01:00
Download 2a62362 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness crux-llvm-0.5.0.99 3 2021-12-07T07:47:21+01:00
Download b4114f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 4 2021-12-10T06:43:31Z
Download 5fe19f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 2 2021-12-10T18:27:56
Download 8a42350 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2021-12-07T13:47:24Z
Download 853f940 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 4 2021-12-10T15:00:02Z
Download b9220b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp22-0-ge852ac510) 6 2021-12-07T17:43:51Z
Download 94a150f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-10T21:21:04+01:00 Download 5fe19f7
Download 053509e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-10T17:28:07+01:00 Download 853f940
Download fa40599 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-10T08:42:09+01:00 Download b4114f0
Download 862a24f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-09T15:36:43+01:00 Download e8aa9c8
Download 095a971 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-08T22:08:36+01:00 Download 604f7be
Download 09b88ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-07T23:24:43+01:00 Download b9220b3
Download 71177aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-07T18:58:12+01:00 Download 8a42350
Download fd9f6f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-07T08:16:42+01:00 Download 2a62362
Download 9e29362 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-07T03:04:50+01:00 Download 27c1366
Download d5aad6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-06T14:57:39+01:00 Download e1b0882
Download 53c6a1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-06T01:17:57+01:00 Download 32d766c
Download 2801242 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-05T20:11:48+01:00 Download 9bd757d
Download 9bd757d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-05T18:46:05+01:00
Download 604f7be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 4 2021-12-08T20:00:46+01:00
Download e8aa9c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 4 2021-12-09T11:41:50+01:00
Download 27c1366 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 4 2021-12-06T23:46:39Z
Download 32d766c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 6 2021-12-05T22:18:42+01:00
Download d44f47c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.1 6 2021-12-05T18:51:10+01:00
Download 7237619 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0 6 2021-12-10T20:17:55+01:00
Download bcdc1cd Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 6 2021-12-08T19:49:35+01:00
Download 632b7fa Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 6 2021-12-09T14:52:28+01:00
Download cbf7865 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness AProVE 5 2021-12-05T11:50:02Z

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

Trying to find witnesses for program (6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822, sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c).

Found 18 witnesses for program sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c, 6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ae9e98c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.2.1 3 2020-12-06T23:50:48
Download 10bb73f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 2 2020-12-11T18:42:13
Download cce98e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 2 2020-12-08T20:11:19
Download 6b48c54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (svcomp21-0-g82e03b87) 6 2020-12-07T16:58:57
Download dd19d71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-12T01:32:54+01:00 Download 10bb73f
Download 7f98479 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-09T21:52:54+01:00 Download 64e5a1f
Download f4507c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-09T21:46:02+01:00 Download 4389300
Download 9592809 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-09T03:56:12+01:00 Download cce98e9
Download 88077dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-09T02:37:19+01:00 Download 33161b5
Download 40cc09b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-08T06:41:40+01:00 Download b290baa
Download be4c939 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-07T21:12:17+01:00 Download 6b48c54
Download 9aedacc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-07T00:14:35+01:00 Download ae9e98c
Download 4271615 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-06T16:59:09+01:00 Download f8ba17d
Download a96fd38 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-06T13:50:30+01:00 Download ef5150f
Download ef5150f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-05T12:30:23+01:00
Download b290baa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 4 2020-12-07T23:22:14+01:00
Download 44a41e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0 6 2020-12-05T14:48:50+01:00
Download 56c9973 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 6 2020-12-08T02:31:43+01:00

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

Trying to find witnesses for program (6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822, sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c).

Found 4 witnesses for program sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c, 6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 9492f0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 4 2019-12-01T00:08:52+01:00
Download 9ba132f Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.9 4 2019-11-30T02:26:53+01:00
Download e5fe5da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 4 2019-11-30T11:07:17+01:00
Download 2426663 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 4 2019-12-01T08:30:35+01:00

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

Trying to find witnesses for program (6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822, sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c).

Found 4 witnesses for program sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c, 6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 77ca8c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2018-12-08T08:09 CET (sv-comp)
Download 638057b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness SMACK 1.9.3 3 2018-12-08T17:36:07
Download 820ec82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 4 2018-12-08T04:05:59+01:00
Download d5d7dad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-05T18:56:54+01:00

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

Trying to find witnesses for program (6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822, sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c, 6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822.json

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

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

Trying to find witnesses for program (6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822, sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c, 6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/6aa101e89b2723d4f5947187ba488e187ab12407b68aa9902fd202aa577ac822.json

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