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).

This link does not point to a witness, but below is a list of witnesses for the same program.

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

Trying to find witnesses for program (5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371, sv-benchmarks/c/termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 52 witnesses for program sv-benchmarks/c/termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c, 5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ae09976 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T04:20:06Z
Download b3afc84 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T18:02:22+01:00
Download ded494b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness crux-llvm-0.5.0.99 3 2023-12-18T05:10:03+01:00
Download ac3261e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:36 CET (comp)
Download 77611a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 6 2023-12-02T13:32:12Z
Download 3ef0357 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2023-11-29T18:55:11Z
Download 40b59e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2023-12-19T22:08:33
Download bd1b2f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T14:32:24Z
Download 183776a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 6 2023-12-02T23:03:24Z
Download 88abcef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 21 2023-11-30T22:35:26Z
Download b76dd3f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 7.4.0 kind 3 2023-12-01T15:38:32Z
Download e1d506f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-20T03:41:14+01:00 Download ac3261e
Download a3ab423 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-20T02:27:38+01:00 Download 40b59e1
Download 7966b36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-19T14:48:19+01:00 Download b6f6569
Download 6672cfc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-19T02:58:54+01:00 Download 01db93a
Download af75bea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-18T06:17:05+01:00 Download ded494b
Download e5bc31d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-17T21:53:08+01:00 Download 6d95f32
Download 6c79200 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-05T14:22:46+01:00 Download 116be8c
Download a5188e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T16:29:00+01:00 Download b43639a
Download a4c49c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T11:35:26+01:00 Download 77611a6
Download 1634ab5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T01:29:37+01:00 Download 2ff9f4b
Download 8046bfa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T18:31:51+01:00 Download b3afc84
Download 417e27d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T09:57:50+01:00 Download ae09976
Download 2b76da1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T05:56:09+01:00 Download 183776a
Download 0d31d3b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-01T22:47:18+01:00 Download 4bf0993
Download 2958571 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-01T18:12:07+01:00 Download b76dd3f
Download 12c0acb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-01T03:49:32+01:00 Download 88abcef
Download d9007f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-01T00:14:11+01:00 Download a030a0c
Download 6093934 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T11:54:09+01:00 Download 8fec7e0
Download 8fec7e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-30T05:32:08+01:00
Download dd11992 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T02:43:43+01:00 Download 3ef0357
Download 3581bda Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-29T18:32:16+01:00 Download bd1b2f3
Download f000a01 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-29T08:19:56+01:00 Download 82ba234
Download 2ff9f4b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 4 2023-12-03T20:28:04+01:00
Download 01db93a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 4 2023-12-18T21:52:25+01:00
Download 6d95f32 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 5 2023-12-17T18:31:03+01:00
Download 116be8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-05T10:19:32Z
Download b43639a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-04T09:10:56Z
Download 4bf0993 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-01T20:34:10Z
Download 82ba234 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 6 2023-11-28T23:11:14Z
Download a030a0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 8 2023-11-30T22:49:38+01:00
Download 1cdbcd8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.4.0 3 2023-12-01T11:19:38Z
Download 8d52d7a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2023-11-29T19:48:28Z
Download 80ce822 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2023-12-20T00:03:46
Download 8b93348 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 3 2023-12-01T01:38:12Z
Download 0f10730 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 5 2023-12-17T21:10:46+01:00
Download a3dcb54 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-05T07:23:06Z
Download d4d5434 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-04T13:46:02Z
Download 88cb344 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: f2030165-c697-4337-a143-f7adad12080c creation_time: '2023-12-02T14:32:12+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ab09e2a3-7bae-4fe1-9fcf-8d791fb23e8a/sv-benchmarks/c/termination-crafted/Bangalore_v4.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ab09e2a3-7bae-4fe1-9fcf-8d791fb23e8a/sv-benchmarks/c/termination-crafted/Bangalore_v4.c : 5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ab09e2a3-7bae-4fe1-9fcf-8d791fb23e8a/sv-benchmarks/c/termination-crafted/Bangalore_v4.c file_hash: 5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371 line: 17 column: 0 function: main value: ((((x + 1) <= y) && (0 <= (x + 2147483648))) && (y <= 2147483647)) format: c_expression correctness_witness CPAchecker 2.3 6 2023-12-04T12:02:37+01:00
Download 4219ead Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 681ea222-e342-4788-affd-61b1a7fa8a4f creation_time: '2023-12-03T00:03:24+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4942013a-3d79-4009-a699-a4ac163140e2/sv-benchmarks/c/termination-crafted/Bangalore_v4.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4942013a-3d79-4009-a699-a4ac163140e2/sv-benchmarks/c/termination-crafted/Bangalore_v4.c : 5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4942013a-3d79-4009-a699-a4ac163140e2/sv-benchmarks/c/termination-crafted/Bangalore_v4.c file_hash: 5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371 line: 17 column: 0 function: main value: (((x + 1) <= y) && (y <= 2147483647)) format: c_expression correctness_witness CPAchecker 2.3 6 2023-12-03T05:44:55+01:00
Download 074847b Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 13affcd5-ba3d-47a4-aff0-f18c2a358ed3 creation_time: '2023-11-29T00:11:14+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d2246dd6-bef4-4975-9460-2c15aa057f34/sv-benchmarks/c/termination-crafted/Bangalore_v4.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d2246dd6-bef4-4975-9460-2c15aa057f34/sv-benchmarks/c/termination-crafted/Bangalore_v4.c : 5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d2246dd6-bef4-4975-9460-2c15aa057f34/sv-benchmarks/c/termination-crafted/Bangalore_v4.c file_hash: 5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371 line: 17 column: 0 function: main value: (((x + 1) <= y) && (y <= 2147483647)) format: c_expression correctness_witness CPAchecker 2.3 6 2023-11-29T07:51:21+01:00
Download 8f82152 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: fd91d38a-ac84-4d16-8303-5e013fdb5983 creation_time: 2023-11-30T22:35: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/Bangalore_v4.c''' task: input_files: - ../../sv-benchmarks/c/termination-crafted/Bangalore_v4.c input_file_hashes: ../../sv-benchmarks/c/termination-crafted/Bangalore_v4.c: 5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371 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/Bangalore_v4.c file_hash: 5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371 line: 17 column: 12 function: main value: -2147483647 <= y format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/Bangalore_v4.c file_hash: 5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371 line: 17 column: 12 function: main value: (((-2147483647 <= x && (long long )x + (long long )y >= 0LL) && ((((((((((((((((((((((((x <= 2147352575 && (-131072LL - (long long )x) + (long long )y >= 0LL) || (x <= 2147418111 && (-65536LL - (long long )x) + (long long )y >= 0LL)) || (x <= 2147450879 && (-32768LL - (long long )x) + (long long )y >= 0LL)) || (x <= 2147467263 && (-16384LL - (long long )x) + (long long )y >= 0LL)) || (x <= 2147475455 && (-8192LL - (long long )x) + (long long )y >= 0LL)) || (x <= 2147479551 && (-4096LL - (long long )x) + (long long )y >= 0LL)) || (x <= 2147481599 && (-2048LL - (long long )x) + (long long )y >= 0LL)) || (x <= 2147482623 && (-1024LL - (long long )x) + (long long )y >= 0LL)) || (x <= 2147483135 && (-512LL - (long long )x) + (long long )y >= 0LL)) || (x <= 2147483391 && (-256LL - (long long )x) + (long long )y >= 0LL)) || (x <= 2147483519 && (-128LL - (long long )x) + (long long )y >= 0LL)) || (x <= 2113929215 && (-33554432LL - (long long )x) + (long long )y >= 0LL)) || (x <= 2147483583 && (-64LL - (long long )x) + (long long )y >= 0LL)) || (x <= 2130706431 && (-16777216LL - (long long )x) + (long long )y >= 0LL)) || (x <= 2147483615 && (-32LL - (long long )x) + (long long )y >= 0LL)) || (x <= 2139095039 && (-8388608LL - (long long )x) + (long long )y >= 0LL)) || (x <= 2147483631 && (-16LL - (long long )x) + (long long )y >= 0LL)) || (x <= 2143289343 && (-4194304LL - (long long )x) + (long long )y >= 0LL)) || (x <= 2147483639 && (-8LL - (long long )x) + (long long )y >= 0LL)) || (x <= 2145386495 && (-2097152LL - (long long )x) + (long long )y >= 0LL)) || (x <= 2147483643 && (-4LL - (long long )x) + (long long )y >= 0LL)) || (x <= 2146435071 && (-1048576LL - (long long )x) + (long long )y >= 0LL)) || (x <= 2147483645 && (-2LL - (long long )x) + (long long )y >= 0LL)) || (x <= 2146959359 && (-524288LL - (long long )x) + (long long )y >= 0LL))) || (x <= 2147483646 && (-1LL - (long long )x) + (long long )y >= 0LL)) || (((-2147483647 <= x && x <= 2147221503) && (-262144LL - (long long )x) + (long long )y >= 0LL) && (long long )x + (long long )y >= 0LL) format: c_expression correctness_witness CPAchecker 2.3 9 2023-12-01T04:57:00+01:00

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

Trying to find witnesses for program (5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371, sv-benchmarks/c/termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 45 witnesses for program sv-benchmarks/c/termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c, 5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 86058fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T13:07:37Z
Download 4f83ee7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T22:04:31+01:00
Download de4a349 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness crux-llvm-0.5.0.99 3 2022-12-09T05:00:16+01:00
Download ac3261e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T11:00 CET (comp)
Download 8159adb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 6 2022-12-14T06:53:00Z
Download ab8a8cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2022-12-12T13:32:18Z
Download adec360 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2022-12-11T15:41:04
Download 9ea756c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T09:58:49Z
Download 8839c86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 6 2022-12-15T02:14:40Z
Download 50265a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp23-0-g4f5dcf38f) 8 2022-12-10T09:18:56Z
Download 4ea3ea3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 7.0.0 kind 3 2022-12-18T17:28:16Z
Download 3cb4560 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 6.8.0 kind 3 2022-12-25T12:12:34Z
Download 2c4da05 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T11:32:14+01:00 Download ac3261e
Download 62c1057 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T10:52:01+01:00 Download 8159adb
Download 50a9529 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T07:34:57+01:00 Download 6b217be
Download 6a04419 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T06:25:21+01:00 Download 8839c86
Download 4305b71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T05:22:52+01:00 Download ab8a8cb
Download 7949970 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T04:47:46+01:00 Download adec360
Download edb5641 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T03:45:55+01:00 Download 9ea756c
Download 5e8c4ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T02:54:20+01:00 Download e6fb486
Download f883d3f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T00:06:46+01:00 Download 0ae1647
Download fe23eef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T22:51:47+01:00 Download 4f83ee7
Download 4d1441b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T22:27:22+01:00 Download 50265a9
Download a9caeb1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T18:21:25+01:00 Download c756b95
Download 02bf9e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T17:44:29+01:00 Download 86058fe
Download 18914e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T15:02:07+01:00 Download 4ea3ea3
Download fcff9a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T11:32:19+01:00 Download b8eb568
Download 3aa2ba1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T08:27:30+01:00 Download de4a349
Download 68cb69b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T03:59:50+01:00 Download e3f5cdf
Download 87cca1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T01:08:38+01:00 Download 3cb4560
Download 6f1db53 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-27T23:43:23+01:00 Download 886b0eb
Download 9dbd79c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-27T23:05:11+01:00 Download 1872938
Download b8eb568 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2022-12-10T18:35:45+01:00
Download e6fb486 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 4 2022-12-12T00:28:21+01:00
Download c756b95 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 4 2022-12-10T01:46:07+01:00
Download e3f5cdf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 5 2022-12-08T08:46:02+01:00
Download 886b0eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2022-12-08T15:01:49Z
Download 6b217be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 6 2022-12-13T14:28:16Z
Download 1872938 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 8 2022-12-07T22:55:23+01:00
Download 0397dc5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2022-12-25T11:41:13Z
Download 76a89ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.0.0 3 2022-12-19T00:57:02Z
Download fecbe70 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2022-12-12T14:15:51Z
Download a089a24 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2022-12-11T16:14:53
Download 57a675f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 5 2022-12-08T03:23:06+01:00
Download d32a959 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2022-12-08T21:07:06Z

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

Trying to find witnesses for program (5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371, sv-benchmarks/c/termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 33 witnesses for program sv-benchmarks/c/termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c, 5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a4ef57c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2021-12-06T12:19:22+01:00
Download 09b5903 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.2.8 3 2021-12-13T22:33:25Z
Download 5adea2b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness crux-llvm-0.5.0.99 3 2021-12-07T06:27:40+01:00
Download 0cf8084 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 6 2021-12-10T01:38:52Z
Download 99bad42 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2021-12-07T13:39:18Z
Download c224534 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2021-12-09T07:31:42
Download 588c026 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 6 2021-12-10T15:27:10Z
Download ffaf53c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 6.8.0 kind 3 2021-12-08T08:49:33Z
Download 7dec631 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-14T00:24:35+01:00 Download 09b5903
Download 5a72721 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-10T21:06:13+01:00 Download 09105b3
Download d6aea5a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-10T17:28:21+01:00 Download 588c026
Download 384c171 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-10T08:48:47+01:00 Download 0cf8084
Download 187a750 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-09T15:46:30+01:00 Download 39f4f35
Download cc0ab70 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-09T10:09:25+01:00 Download c224534
Download fed4f8f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-08T21:40:33+01:00 Download aff4348
Download 7074383 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-08T13:33:28+01:00 Download ffaf53c
Download c494b0f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-07T19:02:32+01:00 Download 99bad42
Download 4982c5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-07T08:26:55+01:00 Download 5adea2b
Download 11f0552 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-07T02:54:50+01:00 Download e13bcd2
Download 463401d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-06T14:55:16+01:00 Download a4ef57c
Download 43eea87 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-06T11:44:53+01:00 Download dce6c33
Download a4cf64b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-06T01:09:57+01:00 Download fe9004d
Download 59e7b99 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-05T20:04:35+01:00 Download 5a4fc61
Download 5a4fc61 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-05T14:50:15+01:00
Download aff4348 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 4 2021-12-08T19:47:55+01:00
Download 39f4f35 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 4 2021-12-09T11:25:29+01:00
Download dce6c33 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 5 2021-12-06T11:13:25+01:00
Download e13bcd2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 6 2021-12-06T19:52:39Z
Download fe9004d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 8 2021-12-06T00:27:34+01:00
Download 38de435 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2021-12-08T11:25:42Z
Download 96183c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2021-12-07T14:50:26Z
Download 846a8af Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2021-12-09T06:18:26
Download 0333f48 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 5 2021-12-06T05:53:42+01:00

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

Trying to find witnesses for program (5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371, sv-benchmarks/c/termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 21 witnesses for program sv-benchmarks/c/termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c, 5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4b2a42a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.1 3 2020-12-06T23:51:18
Download 00c5a71 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) unknown_witness Goblint (svcomp21-0-g82e03b87) 3 2020-12-07T18:01:31
Download 1d69a8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 2 2020-12-11T16:55:36
Download 4deab47 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 2 2020-12-08T14:01:48
Download ccb17dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2020-12-08T09:47:20
Download 36d8c88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-12T01:28:06+01:00 Download 1d69a8d
Download c974be3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-09T21:49:05+01:00 Download 2c22ad6
Download f7bfd58 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-09T21:46:30+01:00 Download 93f8a3e
Download bafd846 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-09T03:57:33+01:00 Download 4deab47
Download 35f410a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-09T02:30:04+01:00 Download cc7440f
Download 9be7b31 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-08T13:45:26+01:00 Download ccb17dc
Download 2e9b178 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-08T07:26:54+01:00 Download b242cd6
Download cc01953 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-07T16:56:50+01:00 Download 58cfa85
Download f85842e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-06T16:57:45+01:00 Download 16bfe83
Download 17755b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-06T15:18:29+01:00 Download 502d791
Download f2a34b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-06T13:12:47+01:00 Download 51faeab
Download 51faeab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-05T12:14:31+01:00
Download b242cd6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 4 2020-12-07T23:18:15+01:00
Download a618260 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-11T20:08:21
Download 417d917 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-08T17:16:21
Download 7ee541c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2020-12-08T07:42:56

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

Trying to find witnesses for program (5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371, sv-benchmarks/c/termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 6 witnesses for program sv-benchmarks/c/termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c, 5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 47c4381 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-free) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 4 2019-12-01T14:05:12+01:00
Download 6e3f1dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.9 4 2019-11-29T22:55:53+01:00
Download 4bd57ff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2019-12-03T22:35 CET (comp)
Download 476f724 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 4 2019-11-30T02:12:29+01:00
Download 333ce9b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 4 2019-12-01T02:42:34+01:00
Download dca0db0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:16 CET (comp)

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

Trying to find witnesses for program (5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371, sv-benchmarks/c/termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 7 witnesses for program sv-benchmarks/c/termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c, 5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2079488 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2018-12-08T01:26 CET (sv-comp)
Download 6f5cdde Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness SMACK 1.9.3 3 2018-12-08T14:02:24
Download c32d805 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2018-12-07T10:43 CET (sv-comp)
Download cc73f33 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 5 2018-12-06T21:18:11+01:00
Download d81e0db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 5 2018-12-05T12:37:02+01:00
Download 7f2e3b0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T12:51 CET (sv-comp)
Download aae444b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-06T21:12 CET (sv-comp)

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

Trying to find witnesses for program (5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371, sv-benchmarks/c/termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 15 witnesses for program sv-benchmarks/c/termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c, 5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e130d47 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 6 2017-12-03T07:43Z
Download a74398f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2017-12-03T04:21 CET (sv-comp)
Download 3d01514 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Map2Check 3 2017-12-02T01:32 CET (sv-comp)
Download 1487890 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 6 2017-12-03T10:26Z
Download a64d06f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T18:29:46.115146
Download 5df1844 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 4.6.0 incr 3 2017-12-02T06:38:29.716567
Download 6def263 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 3.1 5 2017-12-01T14:23 CET (sv-comp)
Download a95732a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T11:05:00+01:00
Download ed815d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 6 2017-12-01T11:35 CET (sv-comp)
Download afc2f7e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 6 2017-12-03T10:21Z
Download a4ec6eb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 9 2017-12-01T10:35 CET (sv-comp)
Download 7965d16 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T20:07:49.415665
Download cb48bcb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T09:03:04.207346
Download ac7935b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 5 2017-12-01T20:58 CET (sv-comp)
Download 6c8f17e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 5 2017-12-01T13:02 CET (sv-comp)

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

Trying to find witnesses for program (5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371, sv-benchmarks/c/termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c, 5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/5cc55b361d4f01def0eda607149a19c4785fee68e7824d0210bdec8ce7b04371.json

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