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/Singapore_v2_false-no-overflow.c
programSHA edb354cbb0643ca3195c80cb1e14d607e93ee809850be073054e985bb1bf4462
witnessName results-verified/cbmc.2018-12-04_2248.logfiles/sv-comp19_prop-nooverflow.Singapore_v2_false-no-overflow.c.files/witness.graphml
witnessSHA f8eb5b9a986ba6075cf46012ffbba55302238d3e4d46ec97dd03b1d1156ec156

Information about the Witness from Competition Database

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

Key Value
architecture 64bit
creationtime 2018-12-05T18:32 CET (sv-comp)
producer CBMC
programfile ../../sv-benchmarks/c/termination-crafted/Singapore_v2_false-no-overflow.c
programhash 64dec40380a4996c8a1a20fecf77593fe0e4519c
sourcecodelang C
specification CHECK( init(main()), LTL(G ! overflow) )
witness-file witnessFileByHash/f8eb5b9a986ba6075cf46012ffbba55302238d3e4d46ec97dd03b1d1156ec156.graphml
witness-sha256 f8eb5b9a986ba6075cf46012ffbba55302238d3e4d46ec97dd03b1d1156ec156
witness-size 4562
witness-type violation_witness

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6f0cd7d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness crux-llvm-0.5.0.99 4 2023-12-18T05:02:56+01:00
Download 3e0ee58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness VeriOover 2 2023-12-20T03:37 CET (comp)
Download ce25205 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Taipan 5 2023-12-02T18:56:37Z
Download 6abe0ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 3 2023-11-29T21:26:03Z
Download ab694d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2023-12-19T19:54:56
Download f1ad943 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Kojak 5 2023-12-03T03:53:00Z
Download e6ff33d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 7.4.0 kind 4 2023-12-01T10:14:33Z
Download e2b90b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 9 2023-12-20T03:41:27+01:00 Download 3e0ee58
Download bd4127d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 6 2023-12-20T02:40:36+01:00 Download ab694d9
Download 33c8640 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 7 2023-12-19T15:33:19+01:00 Download e2ccaad
Download 96ae914 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 6 2023-12-19T05:27:38+01:00 Download 3ed417c
Download ae84d86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 12 2023-12-18T06:11:24+01:00 Download 6f0cd7d
Download e3a52ce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 6 2023-12-17T22:07:39+01:00 Download fb85c5b
Download 3f30dd9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 6 2023-12-05T14:40:42+01:00 Download b938f1a
Download 4e8a90f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 6 2023-12-04T16:44:15+01:00 Download d869931
Download e0ddcfb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 6 2023-12-04T12:12:04+01:00 Download ce25205
Download 92a5cba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 6 2023-12-04T02:26:38+01:00 Download dc633da
Download cdd6f0d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 6 2023-12-03T18:31:18+01:00 Download aa572c4
Download 9351271 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 6 2023-12-03T06:18:55+01:00 Download f1ad943
Download 2719ff1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 6 2023-12-01T18:27:38+01:00 Download e6ff33d
Download ca024c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 7 2023-12-01T00:29:13+01:00 Download 30ee62b
Download a96f004 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 6 2023-11-30T13:42:49+01:00 Download 5269087
Download 5269087 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 6 2023-11-30T06:48:18+01:00
Download f2ce0b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 6 2023-11-30T03:03:09+01:00 Download 6abe0ad
Download c772126 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 6 2023-11-29T08:33:38+01:00 Download e4b09a2
Download dc633da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 6 2023-12-03T23:40:29+01:00
Download 3ed417c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2023-12-18T23:34:34+01:00
Download fb85c5b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CBMC 4 2023-12-17T17:56:22+01:00
Download b938f1a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Bubaak 3 2023-12-05T12:36:34Z
Download d869931 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Bubaak 3 2023-12-04T13:10:49Z
Download e4b09a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Automizer 5 2023-11-29T02:02:31Z
Download 30ee62b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness 2LS 4 2023-11-30T09:38:09+01:00
Download aa572c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:40:45+01:00
Download 880a9a8 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: cc1818fe-5451-46fc-9de5-8bbeaa1de625 creation_time: 2023-12-01T02:09:05Z 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/Singapore_v2.c''' task: input_files: - ../../sv-benchmarks/c/termination-crafted/Singapore_v2.c input_file_hashes: ../../sv-benchmarks/c/termination-crafted/Singapore_v2.c: edb354cbb0643ca3195c80cb1e14d607e93ee809850be073054e985bb1bf4462 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/Singapore_v2.c file_hash: edb354cbb0643ca3195c80cb1e14d607e93ee809850be073054e985bb1bf4462 line: 17 column: 15 function: main value: ((-3LL + (long long )x) - (long long )y >= 0LL && ((((-2147483646 <= x && ((((((((y <= 2147483635 || y <= 2147483636) || y <= 2147483637) || y <= 2147483638) || y <= 2147483639) || y <= 2147483640) || y <= 2147483641) || y <= 2147483642) || y <= 2147483643)) || (-2147483645 <= x && y <= 2147483644)) || ((-2147483647 <= y && -2147483644 <= x) && y <= 2147483645)) || ((-2147483646 <= y && -2147483643 <= x) && y <= 2147483646))) || ((-2147483645 <= x && -2147483645 <= y) && (-2LL + (long long )x) + (long long )y >= 0LL) format: c_expression violation_witness CPAchecker 2.3 8 2023-12-01T04:06:04+01:00
Download c1169c8 Inspect Inspect
Validate
- content: - segment: - waypoint: action: follow constraint: format: C value: \result == 1 location: column: 31 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_9a33bd5f-f44a-4b25-b6da-b391ffd31af6/sv-benchmarks/c/termination-crafted/Singapore_v2.c line: 14 type: function_return - segment: - waypoint: action: follow constraint: format: C value: \result == 2147483647 location: column: 31 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_9a33bd5f-f44a-4b25-b6da-b391ffd31af6/sv-benchmarks/c/termination-crafted/Singapore_v2.c line: 15 type: function_return - segment: - waypoint: action: follow location: column: 9 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_9a33bd5f-f44a-4b25-b6da-b391ffd31af6/sv-benchmarks/c/termination-crafted/Singapore_v2.c line: 16 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T21:26:03Z' format_version: '0.1' producer: name: symbiotic task: data_model: LP64 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_9a33bd5f-f44a-4b25-b6da-b391ffd31af6/sv-benchmarks/c/termination-crafted/Singapore_v2.c : edb354cbb0643ca3195c80cb1e14d607e93ee809850be073054e985bb1bf4462 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_9a33bd5f-f44a-4b25-b6da-b391ffd31af6/sv-benchmarks/c/termination-crafted/Singapore_v2.c language: C specification: CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 8 2023-11-30T02:57:37+01:00

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3130d73 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness verifuzz 3 2022-12-15T07:51:53+01:00
Download 67d2950 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness crux-llvm-0.5.0.99 4 2022-12-09T04:46:10+01:00
Download 3e0ee58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness VeriOover 2 2022-12-12T11:01 CET (comp)
Download f95787a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Taipan 5 2022-12-14T09:46:43Z
Download ab0f2f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 3 2022-12-12T15:14:03Z
Download 3b05d20 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2022-12-11T14:04:35
Download 65b2e3f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Kojak 5 2022-12-15T02:39:43Z
Download 5538752 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 7.0.0 kind 4 2022-12-18T16:42:49Z
Download 86428c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 6.8.0 kind 4 2022-12-25T12:10:33Z
Download 59bdf75 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 9 2023-01-29T11:32:33+01:00 Download 3e0ee58
Download 3a3c018 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 6 2023-01-29T10:45:45+01:00 Download f95787a
Download b7da701 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 6 2023-01-29T06:52:55+01:00 Download 666a7d0
Download d5bdf85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 6 2023-01-29T06:38:48+01:00 Download 65b2e3f
Download 5705804 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 6 2023-01-29T05:58:43+01:00 Download ab0f2f7
Download d750154 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 6 2023-01-29T04:30:47+01:00 Download 3b05d20
Download 55daf8b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 6 2023-01-29T01:32:31+01:00 Download e23dda9
Download 0a771c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 7 2023-01-29T00:51:33+01:00 Download 52ba61c
Download 81663b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 6 2023-01-28T22:53:17+01:00 Download 246234e
Download fb2e9ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 6 2023-01-28T21:04:59+01:00 Download 2f1edc1
Download dd0e652 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 6 2023-01-28T15:45:20+01:00 Download 5538752
Download cc9bb0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 6 2023-01-28T08:56:39+01:00 Download 8707733
Download 080751e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 12 2023-01-28T08:32:14+01:00 Download 67d2950
Download 91d0f7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 6 2023-01-28T04:23:16+01:00 Download 83c8ddc
Download 1ea6242 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 6 2023-01-28T02:23:53+01:00 Download 86428c3
Download f8a2541 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 7 2023-01-27T23:39:25+01:00 Download 5473f51
Download 8707733 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 6 2022-12-10T19:20:58+01:00
Download e23dda9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 6 2022-12-12T00:29:56+01:00
Download 2f1edc1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2022-12-09T23:10:46+01:00
Download 83c8ddc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CBMC 4 2022-12-08T08:07:23+01:00
Download 2f5e036 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Bubaak 3 2022-12-08T14:44:20Z
Download 666a7d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Automizer 5 2022-12-13T20:56:32Z
Download 5473f51 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness 2LS 4 2022-12-08T00:55:36+01:00
Download 246234e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T22:18:14+01:00
Download 87d1215 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T00:29:03+01:00 Download 2f5e036

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 81c5b3e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness verifuzz 3 2021-12-11T09:35:10+01:00
Download 8c5ad8a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness crux-llvm-0.5.0.99 4 2021-12-07T06:30:08+01:00
Download dcb28f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Taipan 5 2021-12-10T00:10:16Z
Download 1e500b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 3 2021-12-07T12:57:34Z
Download af0af6a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2021-12-09T05:12:03
Download 9184862 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Kojak 5 2021-12-10T08:42:25Z
Download 8c272e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 6.8.0 kind 4 2021-12-08T05:42:09Z
Download 18e4c31 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 6 2021-12-10T21:25:30+01:00 Download 0766d2f
Download 4581258 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 6 2021-12-10T17:27:24+01:00 Download 9184862
Download e99f890 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 6 2021-12-10T08:33:58+01:00 Download dcb28f9
Download 54be75a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 6 2021-12-09T16:02:28+01:00 Download f9df117
Download 8e8c7a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 6 2021-12-09T10:14:47+01:00 Download af0af6a
Download 3da2f06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 6 2021-12-08T21:09:57+01:00 Download a49b06f
Download 793058a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 6 2021-12-08T13:47:52+01:00 Download 8c272e7
Download 697e344 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 6 2021-12-07T19:12:19+01:00 Download 1e500b8
Download f72d8eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 12 2021-12-07T08:14:37+01:00 Download 8c5ad8a
Download 53f3299 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 6 2021-12-07T02:35:10+01:00 Download e1d59ac
Download 9f9416e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 6 2021-12-06T01:24:48+01:00 Download 5f57893
Download eff0e8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 6 2021-12-05T20:40:57+01:00 Download fdfcf7e
Download fdfcf7e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 6 2021-12-05T16:41:56+01:00
Download a49b06f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 6 2021-12-08T18:31:01+01:00
Download f9df117 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 6 2021-12-09T13:46:37+01:00
Download 15ab7d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CBMC 5 2021-12-06T03:33:47+01:00
Download e1d59ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Automizer 5 2021-12-06T20:02:11Z
Download 5f57893 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness 2LS 4 2021-12-05T20:57:54+01:00
Download f1b231b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2021-12-06T13:41:13+01:00
Download ae98c11 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-06T11:48:58+01:00 Download 15ab7d3

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 38c04ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.1 3 2020-12-06T23:34:44
Download 14597ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 3 2020-12-11T15:21:55
Download 2e43a61 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 2 2020-12-08T20:26:50
Download 833c480 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2020-12-08T10:27:42
Download 23eb056 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 6 2020-12-12T01:40:57+01:00 Download 14597ff
Download 4877057 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 6 2020-12-09T22:13:04+01:00 Download 1de9180
Download ca035d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 6 2020-12-09T21:20:41+01:00 Download 99ca895
Download 9d1877b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 6 2020-12-09T04:11:35+01:00 Download 2e43a61
Download dcd0e17 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 6 2020-12-09T02:14:23+01:00 Download e2c531c
Download 13b6dbe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 6 2020-12-08T13:21:51+01:00 Download 833c480
Download a30797d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 6 2020-12-08T06:36:19+01:00 Download 5cdd4e6
Download 7d6de63 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 6 2020-12-07T16:20:47+01:00 Download 976a838
Download b2c6717 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 6 2020-12-07T00:14:10+01:00 Download 38c04ab
Download 281ecde Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 7 2020-12-06T19:14:50+01:00 Download f4172d6
Download dd4ba87 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 6 2020-12-06T18:02:28+01:00 Download 8395291
Download baa90c5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 7 2020-12-06T10:31:17+01:00 Download f4172d6
Download 1690d74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 6 2020-12-05T18:11:38+01:00 Download 8395291
Download 8395291 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 6 2020-12-05T15:17:21+01:00
Download 5cdd4e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 6 2020-12-08T03:51:41+01:00
Download f373af9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) unknown_witness Goblint (svcomp21-0-g82e03b87) 3 2020-12-07T10:25:10
Download a29c0e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-06T18:27:54+01:00 Download d220a6a
Download 82350da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-06T07:42:35+01:00 Download d220a6a

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 862fa99 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 1 2019-12-01 03:21:26
Download 76a6bde Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2019-12-04T00:26 CET (comp)
Download e702c24 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-11T22:00:33+01:00 Download 3c5aea9
Download bbe74b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-11T21:42:10+01:00 Download 4925c5d
Download 50de1a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-11T21:09:33+01:00 Download 862fa99
Download d3f2899 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-11T20:54:25+01:00 Download 3f4f8b9
Download 9fbac3e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-11T20:44:42+01:00 Download 0f95d2a
Download 74aae5d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-08T00:26:15+01:00 Download 3e5e504
Download 5d1d13f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-07T21:12:48+01:00 Download 8225892
Download feb259b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-05T19:34:31+01:00 Download d455d8d
Download f726132 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-04T02:58:13+01:00 Download 76a6bde
Download 1e1794b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 5 2019-12-03T08:09:50+01:00 Download db73dd3
Download db73dd3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.9 4 2019-11-30T02:30:49+01:00
Download 3c5aea9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 4 2019-11-30T23:26:30+01:00
Download 39f0bd9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 4 2019-12-05T20:21:22+01:00 Download cdd2c57

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download eeb63ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 2 2018-12-08T00:53 CET (sv-comp)
Download a100027 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness SMACK 1.9.3 4 2018-12-08T16:05:08
Download ca2d81c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Pinaka 4 2018-12-07T07:53 CET (sv-comp)
Download 5736c0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 4 2018-12-07T06:33:59+01:00
Download 099ccef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:53:09+01:00 Download 5bfc6b0
Download 1247419 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:38:28+01:00 Download 45fe09f
Download f39bca1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T20:21:47+01:00 Download 711421d
Download ba5dfee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-09T18:20:47+01:00 Download 0d4d65d
Download 37af9c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T23:42:32+01:00 Download eeb63ff
Download 525836d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T22:10:50+01:00 Download a100027
Download cc5e8db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T09:05:33+01:00 Download 5736c0f
Download 49a8a2b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-08T05:03:17+01:00 Download 78d8e88
Download 5084d6a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-07T17:45:16+01:00 Download ca2d81c
Download 7d6cc98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:48:50+01:00 Download 1e534eb
Download 9474411 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:41:59+01:00 Download 9fd2cd7
Download 01fadbb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 5 2018-12-06T09:11:15+01:00 Download aa0ecf6
Download 1e534eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.7-svn 29852 4 2018-12-06T07:32:20+01:00
Download f4600c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T09:15:37+01:00 Download f8eb5b9

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c2d75a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Taipan 4 2017-12-03T07:43Z
Download 83c7ef4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 2 2017-12-03T04:21 CET (sv-comp)
Download a88d41d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Map2Check 3 2017-12-02T01:24 CET (sv-comp)
Download 3a992f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Kojak 4 2017-12-03T10:19Z
Download afc8385 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 4.6.0 kind 4 2017-12-02T17:32:26.866226
Download 064990e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 4.6.0 incr 4 2017-12-02T06:08:40.512504
Download 3532045 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness ESBMC 3.1 4 2017-12-01T13:59 CET (sv-comp)
Download dbd8338 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T11:53:00+01:00 56a1463
Download 057a5aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T11:52:11+01:00 c2dbb2e
Download 264fbfb 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 05a70ed
Download f2d1ea0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-03T05:13:04+01:00 ff709ad
Download 2924ded Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T20:09:43+01:00 491e44f
Download c15d667 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-02T08:12:31+01:00 276cca4
Download fe34828 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T12:02:34+01:00 63bf699
Download 785216f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 5 2017-12-01T11:19:09+01:00 e387a9b
Download 4a54cd8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T11:00:01+01:00
Download a0eef3e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CBMC 5 2017-12-01T12:06 CET (sv-comp)
Download f49f500 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Automizer 4 2017-12-03T10:21Z
Download 09ad297 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness 2LS 4 2017-12-01T10:43 CET (sv-comp)
Download de40123 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T12:31:54+01:00 4a14c00

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

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

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

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