Witness Inspection

A description of this web service can be found in the CAV paper "Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses" (more material).

View and Validate the Witness

Input Given to this Service about the Witness (URL Query)

Key Value
programName sv-benchmarks/c/termination-crafted-lit/genady_true-termination_true-no-overflow.c
programSHA 287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a
witnessName results-verified/depthk.2017-12-01_1515.logfiles/sv-comp18.genady_true-termination_true-no-overflow.c.files/witness.graphml
witnessSHA 7ee482139812fbc4b9b8bb9701711292c9f94150b2c0589a31c90fe14fc933e7

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/7ee482139812fbc4b9b8bb9701711292c9f94150b2c0589a31c90fe14fc933e7.json

Key Value
architecture 32bit
creationtime 2017-12-01T19:09 CET (sv-comp)
memoryModel precise
producer ESBMC 3.1
program-sha256 287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a
programfile /tmp/vcloud-vcloud-master/worker/working_dir_b5f482fe-4d6e-49ff-b14b-b5859adf04a1/sv-benchmarks/c/termination-crafted-lit/genady_true-termination_true-no-overflow.c
programhash 6938b5c805400363799492c040263d9022406929
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/7ee482139812fbc4b9b8bb9701711292c9f94150b2c0589a31c90fe14fc933e7.graphml
witness-sha256 7ee482139812fbc4b9b8bb9701711292c9f94150b2c0589a31c90fe14fc933e7
witness-size 4836
witness-type correctness_witness

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

Trying to find witnesses for program (287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a, sv-benchmarks/c/termination-crafted-lit/genady_true-termination_true-no-overflow.c).

Found 52 witnesses for program sv-benchmarks/c/termination-crafted-lit/genady_true-termination_true-no-overflow.c, 287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download a1d1fab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T06:52:31Z
Download 7dd79b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 4 2023-12-19T04:20:22+01:00 Download ef70803
Download 9bf44b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 4 2023-12-04T01:53:18+01:00 Download 67e8934
Download ec72e48 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 4 2023-11-30T13:03:11+01:00 Download 15416fc
Download 36052e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:56:08+01:00
Download 2b76597 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:37 CET (comp)
Download d65df16 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 6 2023-12-02T13:04:12Z
Download 794cad2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2023-12-17T02:15:14Z
Download c265a34 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2023-11-29T21:03:28Z
Download 6da5301 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2023-12-19T21:16:48
Download f10378a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T13:26:17Z
Download c28601f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 7 2023-12-02T22:59:42Z
Download d44dadc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 12 2023-12-01T00:56:19Z
Download 66d6cd3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-20T03:41:17+01:00 Download 2b76597
Download 5db5a95 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-20T02:27:56+01:00 Download 6da5301
Download f895717 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-19T14:28:36+01:00 Download 3f7d69a
Download 8b2a6b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-17T06:25:36+01:00 Download 794cad2
Download 2af88a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-05T14:20:47+01:00 Download de92918
Download 5266372 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T16:28:50+01:00 Download b2e7ab7
Download 8a6d71f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T11:43:13+01:00 Download d65df16
Download cefe6cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T18:31:06+01:00 Download 36052e8
Download 4833282 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T09:59:02+01:00 Download a1d1fab
Download 05862b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T05:54:33+01:00 Download c28601f
Download 049a906 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-01T22:45:47+01:00 Download 0b81e7e
Download 7fb746b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-01T03:38:33+01:00 Download d44dadc
Download d20c840 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-01T00:13:02+01:00 Download d7ae716
Download 15416fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T08:32:19+01:00
Download d558ce3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-30T02:32:47+01:00 Download c265a34
Download 7ed2f57 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-29T18:10:37+01:00 Download f10378a
Download b6cb904 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-29T08:17:18+01:00 Download b456a8e
Download 67e8934 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 5 2023-12-03T23:01:04+01:00
Download ef70803 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2023-12-18T18:37:36+01:00
Download aaac496 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 3116 2023-12-17T14:47:34+01:00
Download de92918 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-05T12:54:43Z
Download b2e7ab7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-04T13:16:36Z
Download 0b81e7e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-01T20:57:14Z
Download b456a8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 6 2023-11-28T22:30:36Z
Download d7ae716 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 8 2023-11-30T21:44:05+01:00
Download 8630715 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.4.0 3 2023-12-01T12:35:52Z
Download 1115486 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2023-12-17T03:01:05Z
Download f018f0c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2023-11-29T23:21:41Z
Download ca1c3f2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2023-12-19T21:58:46
Download 490c28e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 3 2023-12-01T01:08:36Z
Download ce60a58 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 3116 2023-12-17T13:41:39+01:00
Download ae7a9a6 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-05T08:00:36Z
Download 98c71ff Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-04T14:50:53Z
Download f3bb752 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-01T21:15:02Z
Download b6971cc Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 7 2023-11-30T21:40:30+01:00
Download 83e79a8 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 69c4e62b-ce1a-4a4f-a1b1-0164418308fe creation_time: '2023-12-02T23:59: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_95664cb4-48e4-4cbe-843b-d3e8fab62f8d/sv-benchmarks/c/termination-crafted-lit/genady.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_95664cb4-48e4-4cbe-843b-d3e8fab62f8d/sv-benchmarks/c/termination-crafted-lit/genady.c : 287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a 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_95664cb4-48e4-4cbe-843b-d3e8fab62f8d/sv-benchmarks/c/termination-crafted-lit/genady.c file_hash: 287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a line: 15 column: 0 function: main value: (((((((((10001 <= (i + j)) && (j <= 4)) && (i <= (9993 + j))) || (((10001 <= (i + j)) && (j <= 3)) && (i <= (9995 + j)))) || ((((10001 <= (i + j)) && (j <= (3 + i))) && (j <= 9996)) && ((i + 1) < j))) || (((10001 <= (i + j)) && (i <= 9995)) && (j <= (i + 1)))) || (((10001 <= (i + j)) && (i <= (j + 9991))) && (j <= 5))) || ((((9997 + j) <= i) && (i < 10000)) && (1 < j))) || ((((j <= 1) && (i <= (9999 + j))) && (1 <= j)) && ((9999 + j) <= i))) format: c_expression correctness_witness CPAchecker 2.3 7 2023-12-03T05:32:43+01:00
Download 336facf Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 53ad6ba4-e888-4a2a-bd11-63adb90a6522 creation_time: '2023-11-28T23:30:36+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d61a8057-aacf-4584-ab7f-cb4790f45964/sv-benchmarks/c/termination-crafted-lit/genady.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d61a8057-aacf-4584-ab7f-cb4790f45964/sv-benchmarks/c/termination-crafted-lit/genady.c : 287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a 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_d61a8057-aacf-4584-ab7f-cb4790f45964/sv-benchmarks/c/termination-crafted-lit/genady.c file_hash: 287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a line: 15 column: 0 function: main value: (((((((j == 1) && (10000 == i)) || ((9996 == i) && (5 == j))) || ((j == 4) && (9997 == i))) || (((10001 <= (i + j)) && (i <= 9995)) && (j <= 9995))) || ((2 == j) && (9999 == i))) || ((9998 == i) && (3 == j))) format: c_expression correctness_witness CPAchecker 2.3 7 2023-11-29T07:44:11+01:00
Download 5451d0d Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 187e1b2b-50f7-40bd-a5cd-fb7cd9c0624c creation_time: '2023-12-02T14:04: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_d66fe149-87dc-4894-8362-f0010dbdc6f3/sv-benchmarks/c/termination-crafted-lit/genady.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d66fe149-87dc-4894-8362-f0010dbdc6f3/sv-benchmarks/c/termination-crafted-lit/genady.c : 287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a 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_d66fe149-87dc-4894-8362-f0010dbdc6f3/sv-benchmarks/c/termination-crafted-lit/genady.c file_hash: 287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a line: 15 column: 0 function: main value: (((j == 1) && (10000 == i)) || (((2 <= j) && (i <= 9999)) && (j <= (i + 1)))) format: c_expression correctness_witness CPAchecker 2.3 7 2023-12-04T11:56:06+01:00
Download 60cc5f1 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: a6a3e1b9-639e-4dfd-82ac-3da386cd26c9 creation_time: 2023-12-01T00:56:19Z producer: name: Goblint version: tags/svcomp24-0-gc2e9465a7 command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--sets'' ''ana.specification'' ''../../sv-benchmarks/c/properties/no-overflow.prp'' ''--sets'' ''exp.architecture'' ''64bit'' ''../../sv-benchmarks/c/termination-crafted-lit/genady.c''' task: input_files: - ../../sv-benchmarks/c/termination-crafted-lit/genady.c input_file_hashes: ../../sv-benchmarks/c/termination-crafted-lit/genady.c: 287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a 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-lit/genady.c file_hash: 287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a line: 15 column: 11 function: main value: (-10001LL + (long long )i) + (long long )j >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/genady.c file_hash: 287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a line: 15 column: 11 function: main value: (10001LL - (long long )i) - (long long )j >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted-lit/genady.c file_hash: 287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a line: 15 column: 11 function: main value: ((((((((((((((((13 <= j && 256 <= i) && i <= 9988) && j <= 65536) && (9975LL - (long long )i) + (long long )j >= 0LL) && (1LL + (long long )i) - (long long )j >= 0LL) || ((((9977LL - (long long )i) + (long long )j >= 0LL && (-9977LL + (long long )i) - (long long )j >= 0LL) && i == 9989) && j == 12)) || ((((9979LL - (long long )i) + (long long )j >= 0LL && (-9979LL + (long long )i) - (long long )j >= 0LL) && i == 9990) && j == 11)) || ((((9981LL - (long long )i) + (long long )j >= 0LL && (-9981LL + (long long )i) - (long long )j >= 0LL) && i == 9991) && j == 10)) || ((((9983LL - (long long )i) + (long long )j >= 0LL && (-9983LL + (long long )i) - (long long )j >= 0LL) && i == 9992) && j == 9)) || ((((9985LL - (long long )i) + (long long )j >= 0LL && (-9985LL + (long long )i) - (long long )j >= 0LL) && i == 9993) && j == 8)) || ((((9987LL - (long long )i) + (long long )j >= 0LL && (-9987LL + (long long )i) - (long long )j >= 0LL) && i == 9994) && j == 7)) || ((((9989LL - (long long )i) + (long long )j >= 0LL && (-9989LL + (long long )i) - (long long )j >= 0LL) && i == 9995) && j == 6)) || ((((9991LL - (long long )i) + (long long )j >= 0LL && (-9991LL + (long long )i) - (long long )j >= 0LL) && i == 9996) && j == 5)) || ((((9993LL - (long long )i) + (long long )j >= 0LL && (-9993LL + (long long )i) - (long long )j >= 0LL) && i == 9997) && j == 4)) || ((((9995LL - (long long )i) + (long long )j >= 0LL && (-9995LL + (long long )i) - (long long )j >= 0LL) && i == 9998) && j == 3)) || ((((9997LL - (long long )i) + (long long )j >= 0LL && (-9997LL + (long long )i) - (long long )j >= 0LL) && i == 9999) && j == 2)) || ((((((9999LL - (long long )i) + (long long )j >= 0LL && (-9999LL + (long long )i) - (long long )j >= 0LL) && 1 == j) && 10000 == i) && i == 10000) && j == 1) format: c_expression correctness_witness CPAchecker 2.3 10 2023-12-01T05:19:54+01:00

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

Trying to find witnesses for program (287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a, sv-benchmarks/c/termination-crafted-lit/genady_true-termination_true-no-overflow.c).

Found 39 witnesses for program sv-benchmarks/c/termination-crafted-lit/genady_true-termination_true-no-overflow.c, 287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fa48e26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T10:38:08Z
Download 949f0d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 4 2023-01-29T02:50:37+01:00 Download 8cef511
Download 44268d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 2 2023-01-28T22:28:44+01:00 Download 1fdd191
Download 23e6514 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 4 2023-01-28T18:43:14+01:00 Download 168f636
Download 5424e1c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 4 2023-01-28T11:27:14+01:00 Download cb026fe
Download cfc8888 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-11T01:56:27+01:00
Download 2b76597 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T10:59 CET (comp)
Download f68387f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 6 2022-12-14T02:18:43Z
Download 66f73a1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2022-12-25T11:17:14Z
Download b658530 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2022-12-12T10:58:24Z
Download 59d47ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2022-12-11T14:42:00
Download b60e075 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 7 2022-12-14T23:33:04Z
Download 1fdd191 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp23-0-g4f5dcf38f) 28 2022-12-10T09:25:08Z
Download f235d09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T11:32:12+01:00 Download 2b76597
Download c697c54 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T10:56:46+01:00 Download f68387f
Download d1d2eb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T07:16:18+01:00 Download 5312f40
Download 82036e2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T06:23:15+01:00 Download b60e075
Download 9a8476a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T05:25:41+01:00 Download b658530
Download 8c70021 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T04:49:56+01:00 Download 59d47ee
Download 82b5702 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T00:08:00+01:00 Download 5d9d404
Download 8226786 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T22:52:11+01:00 Download cfc8888
Download e65bd00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T17:45:53+01:00 Download fa48e26
Download be4772c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-28T01:09:56+01:00 Download 66f73a1
Download 880c877 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-27T23:44:21+01:00 Download 6530d2c
Download e4efbf8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-27T23:06:18+01:00 Download a279a67
Download cb026fe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2022-12-10T19:48:11+01:00
Download 8cef511 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 5 2022-12-12T02:00:10+01:00
Download 168f636 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 5 2022-12-09T16:59:26+01:00
Download 7f1e850 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 3116 2022-12-08T13:01:57+01:00
Download 6530d2c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2022-12-08T19:46:47Z
Download 5312f40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 6 2022-12-13T10:16:03Z
Download a279a67 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 8 2022-12-08T01:35:12+01:00
Download fe650a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.0.0 3 2022-12-19T01:02:20Z
Download 44e0abc Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2022-12-25T09:30:08Z
Download 8341a96 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2022-12-12T12:51:29Z
Download f11cdc9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2022-12-11T14:22:49
Download adcca0d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 3116 2022-12-08T11:14:28+01:00
Download 91ecc96 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2022-12-08T20:37:34Z
Download a882c3b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 7 2022-12-08T00:56:08+01:00

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

Trying to find witnesses for program (287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a, sv-benchmarks/c/termination-crafted-lit/genady_true-termination_true-no-overflow.c).

Found 33 witnesses for program sv-benchmarks/c/termination-crafted-lit/genady_true-termination_true-no-overflow.c, 287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download f2e084b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 4 2021-12-09T15:50:05+01:00 Download 8237ea4
Download f78c753 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 4 2021-12-08T22:05:30+01:00 Download 2d6fc7c
Download 237b68e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 2 2021-12-07T23:31:54+01:00 Download 05c5dde
Download e71dfdd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.1 4 2021-12-05T20:24:09+01:00 Download 4e74f68
Download 17d12af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2021-12-06T13:37:40+01:00
Download 1147348 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.2.8 3 2021-12-13T21:03:41Z
Download de9b01e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 6 2021-12-10T00:55:05Z
Download 3e0b1e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 2 2021-12-10T18:22:15
Download 639921e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2021-12-07T14:56:23Z
Download 708fb74 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2021-12-09T06:53:44
Download a8dcfc0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 7 2021-12-10T12:07:03Z
Download 05c5dde Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp22-0-ge852ac510) 6 2021-12-07T17:42:54Z
Download 7c9cf86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-14T00:12:39+01:00 Download 1147348
Download 8ec4cee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-10T21:02:15+01:00 Download 3e0b1e3
Download f8efce5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-10T17:36:31+01:00 Download a8dcfc0
Download a978cce Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-10T08:54:18+01:00 Download de9b01e
Download c1902b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-09T10:09:51+01:00 Download 708fb74
Download d6d39b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-07T18:55:18+01:00 Download 639921e
Download 00bed0d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-07T03:10:09+01:00 Download e9d4e86
Download 6d7b708 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-06T15:12:47+01:00 Download 17d12af
Download 4c4d779 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-06T01:20:01+01:00 Download 3d9a2dc
Download 4e74f68 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 5 2021-12-05T19:06:50+01:00
Download 2d6fc7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 5 2021-12-08T19:41:34+01:00
Download 8237ea4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 5 2021-12-09T14:49:51+01:00
Download a13f7e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 3116 2021-12-06T06:00:40+01:00
Download e9d4e86 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 7 2021-12-06T23:05:48Z
Download 3d9a2dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 8 2021-12-05T22:21:05+01:00
Download 4f7b131 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2021-12-08T07:02:36Z
Download 876b2d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2021-12-10T16:25:00
Download 3647015 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2021-12-07T09:27:24Z
Download 4a498bf Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2021-12-09T07:17:02
Download 9760a3e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 3116 2021-12-06T07:34:54+01:00
Download 6ab95de Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 7 2021-12-05T20:43:40+01:00

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

Trying to find witnesses for program (287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a, sv-benchmarks/c/termination-crafted-lit/genady_true-termination_true-no-overflow.c).

Found 19 witnesses for program sv-benchmarks/c/termination-crafted-lit/genady_true-termination_true-no-overflow.c, 287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 77e3808 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.1 3 2020-12-06T23:50:34
Download b272ff8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 4 2020-12-08T06:22:08+01:00 Download 033a29e
Download 1bef87a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.0 4 2020-12-06T13:25:59+01:00 Download 834154f
Download 5ad0109 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) unknown_witness Goblint (svcomp21-0-g82e03b87) 3 2020-12-07T17:30:23
Download 50348e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 2 2020-12-11T22:40:11
Download df8647a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 2 2020-12-08T22:46:03
Download 3f07cef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2020-12-08T07:51:27
Download c06c5aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-12T01:27:09+01:00 Download 50348e0
Download 5af4a40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-09T22:08:08+01:00 Download 0f4b4ce
Download 970d69e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-09T21:31:12+01:00 Download e3dcaef
Download 99c672a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-09T03:56:32+01:00 Download df8647a
Download 1119db3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-09T02:17:40+01:00 Download 0a6f476
Download 58dc7f0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-08T13:31:56+01:00 Download 3f07cef
Download d200e6a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-06T16:42:07+01:00 Download 28ad7ad
Download 834154f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 5 2020-12-05T15:30:21+01:00
Download 033a29e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 5 2020-12-08T05:30:57+01:00
Download 0e0ae3b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-11T17:36:34
Download af77e0e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-09T02:37:00
Download 4f4cf84 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2020-12-08T08:00:57

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

Trying to find witnesses for program (287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a, sv-benchmarks/c/termination-crafted-lit/genady_true-termination_true-no-overflow.c).

Found 4 witnesses for program sv-benchmarks/c/termination-crafted-lit/genady_true-termination_true-no-overflow.c, 287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2081b5c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2019-12-03T22:23 CET (comp)
Download 386d580 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 915 2019-11-29T21:30:59+01:00
Download 10b5f53 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 4 2019-12-01T16:47:29+01:00
Download 23e5b1b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-03T23:16 CET (comp)

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

Trying to find witnesses for program (287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a, sv-benchmarks/c/termination-crafted-lit/genady_true-termination_true-no-overflow.c).

Found 6 witnesses for program sv-benchmarks/c/termination-crafted-lit/genady_true-termination_true-no-overflow.c, 287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 29a4f04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2018-12-08T05:03 CET (sv-comp)
Download 2495c46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2018-12-07T04:02 CET (sv-comp)
Download e4b977b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 1046 2018-12-06T13:13:36+01:00
Download 4a3fabd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 1046 2018-12-05T06:54:19+01:00
Download fa76ece Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T00:05 CET (sv-comp)
Download 9e0aeff Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-06T20:30 CET (sv-comp)

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

Trying to find witnesses for program (287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a, sv-benchmarks/c/termination-crafted-lit/genady_true-termination_true-no-overflow.c).

Found 12 witnesses for program sv-benchmarks/c/termination-crafted-lit/genady_true-termination_true-no-overflow.c, 287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ba0af7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 6 2017-12-03T07:43Z
Download 3d782c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2017-12-03T04:38 CET (sv-comp)
Download e1da143 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Map2Check 3 2017-12-02T01:53 CET (sv-comp)
Download 4ba2762 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 8 2017-12-03T10:30Z
Download 576d77e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 7124 2017-12-01T11:41 CET (sv-comp)
Download adc85dd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 6 2017-12-03T10:24Z
Download b5eeb1f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 7 2017-12-01T10:23 CET (sv-comp)
Download 435f809 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T22:18:47.693687
Download 9928eff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T08:49:42.918108
Download 7ee4821 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 5 2017-12-01T19:09 CET (sv-comp)
Download 79b5cf9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 3456 2017-12-01T18:58 CET (sv-comp)
Download 3f73c65 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 7 2017-12-01T14:34 CET (sv-comp)

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

Trying to find witnesses for program (287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a, sv-benchmarks/c/termination-crafted-lit/genady_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted-lit/genady_true-termination_true-no-overflow.c, 287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/287610e8766968d20807fa7cedb2876e161017ade0a329100f16c8240065cc6a.json

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