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 (cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe, sv-benchmarks/c/termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c).

Found 24 witnesses for program sv-benchmarks/c/termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c, cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b871e96 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T07:38:05Z
Download 725f21a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:38:01+01:00
Download 245e7bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:37 CET (comp)
Download af1a252 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 6 2023-12-02T18:23:48Z
Download 38387c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-20T03:41:15+01:00 Download 245e7bf
Download 5dbc36e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-19T04:36:24+01:00 Download 8bcc979
Download e336718 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-17T06:24:24+01:00 Download f91a382
Download 5d200bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-04T11:23:41+01:00 Download af1a252
Download 33d63ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-04T01:32:24+01:00 Download 924188e
Download 5cc6092 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-03T18:31:42+01:00 Download 725f21a
Download 933a74d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-03T09:57:22+01:00 Download b871e96
Download 7dd005d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-30T23:48:25+01:00 Download 84eff33
Download a168054 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-30T11:44:09+01:00 Download a7296d5
Download a7296d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-30T07:13:22+01:00
Download 2615bc4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-29T08:22:46+01:00 Download 6d8d2c3
Download 924188e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 4 2023-12-03T20:59:39+01:00
Download f91a382 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2023-12-17T02:28:51+01:00
Download 8bcc979 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 4 2023-12-18T22:19:01+01:00
Download 6d8d2c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 6 2023-11-28T22:56:08Z
Download 84eff33 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 10 2023-11-30T22:02:26+01:00
Download 4182527 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 3 2023-12-01T01:12:38Z
Download 6e5090d Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 93799272-4cdc-4c68-a717-f4a55b80685f creation_time: '2023-12-02T19:23:48+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2c9cbaea-4340-4e89-aba0-5adb6e11e3a6/sv-benchmarks/c/termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_2c9cbaea-4340-4e89-aba0-5adb6e11e3a6/sv-benchmarks/c/termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction.c : cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe 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_2c9cbaea-4340-4e89-aba0-5adb6e11e3a6/sv-benchmarks/c/termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction.c file_hash: cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe line: 18 column: 0 function: main value: ((((y <= 2147483646) && (((2 * y) + x) <= 2147483650)) && (1 < y)) || (((x <= 2147483647) && (0 <= (x + 2147483648))) && (y == 1))) format: c_expression correctness_witness CPAchecker 2.3 5 2023-12-04T11:54:28+01:00
Download 9b12cd1 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 412ef393-dd20-4578-bc74-78b6dec570b8 creation_time: '2023-11-28T23:56:08+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5b2679d6-060e-4e1d-9552-f8552b6d3056/sv-benchmarks/c/termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5b2679d6-060e-4e1d-9552-f8552b6d3056/sv-benchmarks/c/termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction.c : cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe 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_5b2679d6-060e-4e1d-9552-f8552b6d3056/sv-benchmarks/c/termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction.c file_hash: cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe line: 18 column: 0 function: main value: (((x <= 2147483647) && (y == 1)) || (((y <= 2147483646) && (((2 * y) + x) <= 2147483650)) && (2 <= y))) format: c_expression correctness_witness CPAchecker 2.3 5 2023-11-29T07:48:34+01:00
Download 9dd3359 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: 9a59d062-b8ea-4258-a6e5-ffbf13135c46 creation_time: 2023-12-01T00:56:08Z 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/BrockschmidtCookFuhs-CAV2013-Introduction.c''' task: input_files: - ../../sv-benchmarks/c/termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction.c input_file_hashes: ../../sv-benchmarks/c/termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction.c: cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe 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/BrockschmidtCookFuhs-CAV2013-Introduction.c file_hash: cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe line: 18 column: 11 function: main value: ((-2LL + (long long )x) + (long long )y >= 0LL && (((((((((((((-2147483646 <= x && 13 <= y) && x <= 2147483569) || ((((((((((((((-10 <= x && x <= 2147483581) && (22LL + (long long )x) - (long long )y >= 0LL) && y == 12) && x != -66) && x != -65) && x != -63) && x != -60) && x != -56) && x != -51) && x != -45) && x != -38) && x != -30) && x != -21) && x != -11)) || (((((((((((((-9 <= x && x <= 2147483592) && (20LL + (long long )x) - (long long )y >= 0LL) && y == 11) && x != -55) && x != -54) && x != -52) && x != -49) && x != -45) && x != -40) && x != -34) && x != -27) && x != -19) && x != -10)) || ((((((((((((-8 <= x && x <= 2147483602) && (18LL + (long long )x) - (long long )y >= 0LL) && y == 10) && x != -45) && x != -44) && x != -42) && x != -39) && x != -35) && x != -30) && x != -24) && x != -17) && x != -9)) || (((((((((((-7 <= x && x <= 2147483611) && (16LL + (long long )x) - (long long )y >= 0LL) && y == 9) && x != -36) && x != -35) && x != -33) && x != -30) && x != -26) && x != -21) && x != -15) && x != -8)) || ((((((((((-6 <= x && x <= 2147483619) && (14LL + (long long )x) - (long long )y >= 0LL) && y == 8) && x != -28) && x != -27) && x != -25) && x != -22) && x != -18) && x != -13) && x != -7)) || (((((((((-5 <= x && x <= 2147483626) && (12LL + (long long )x) - (long long )y >= 0LL) && y == 7) && x != -21) && x != -20) && x != -18) && x != -15) && x != -11) && x != -6)) || ((((((((-4 <= x && x <= 2147483632) && (10LL + (long long )x) - (long long )y >= 0LL) && y == 6) && x != -15) && x != -14) && x != -12) && x != -9) && x != -5)) || (((((((-3 <= x && x <= 2147483637) && (8LL + (long long )x) - (long long )y >= 0LL) && y == 5) && x != -10) && x != -9) && x != -7) && x != -4)) || ((((((-2 <= x && x <= 2147483641) && (6LL + (long long )x) - (long long )y >= 0LL) && y == 4) && x != -6) && x != -5) && x != -3)) || (((((-1 <= x && x <= 2147483644) && (4LL + (long long )x) - (long long )y >= 0LL) && y == 3) && x != -3) && x != -2)) || ((((0 <= x && x <= 2147483646) && (2LL + (long long )x) - (long long )y >= 0LL) && y == 2) && x != -1))) || (1 == y && y == 1) format: c_expression correctness_witness CPAchecker 2.3 9 2023-12-01T04:13:39+01:00

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

Trying to find witnesses for program (cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe, sv-benchmarks/c/termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c).

Found 21 witnesses for program sv-benchmarks/c/termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c, cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download c15952a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T12:40:43Z
Download def73a5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T22:12:10+01:00
Download 245e7bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T11:01 CET (comp)
Download ed6b61d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 6 2022-12-14T06:31:55Z
Download 3f5b7d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T11:32:12+01:00 Download 245e7bf
Download 104764e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T10:51:24+01:00 Download ed6b61d
Download 968bfc1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T07:32:05+01:00 Download 38d6425
Download 15d5233 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T02:59:00+01:00 Download 53d2467
Download 9b20dd9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T22:51:47+01:00 Download def73a5
Download db06041 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T18:11:05+01:00 Download 7f9d43b
Download 1f13288 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T17:46:31+01:00 Download c15952a
Download 6f9def4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T11:04:21+01:00 Download 41bc633
Download 162567c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T00:57:39+01:00 Download 04ef611
Download 6d4c206 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-27T23:02:45+01:00 Download 525ee06
Download 41bc633 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2022-12-10T21:11:48+01:00
Download 53d2467 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 4 2022-12-11T21:48:59+01:00
Download 04ef611 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2022-12-25T11:14:03+01:00
Download 7f9d43b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 4 2022-12-10T00:03:49+01:00
Download 38d6425 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 6 2022-12-13T18:52:32Z
Download 525ee06 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 10 2022-12-08T00:15:24+01:00
Download dd75f19 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2022-12-08T19:10:59Z

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

Trying to find witnesses for program (cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe, sv-benchmarks/c/termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c).

Found 16 witnesses for program sv-benchmarks/c/termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c, cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 68d041f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2021-12-06T13:40:37+01:00
Download 7360aa3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.2.8 3 2021-12-13T21:34:48Z
Download c2271f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 6 2021-12-10T02:00:04Z
Download 54eaf30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-14T00:24:28+01:00 Download 7360aa3
Download b5f9110 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-10T20:57:47+01:00 Download 5172300
Download 9b305f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-10T08:47:40+01:00 Download c2271f3
Download a4d6d6a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-09T15:33:50+01:00 Download 434710a
Download cb5a789 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-08T21:27:14+01:00 Download 8b89ac9
Download 95015cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-07T03:06:29+01:00 Download ba92ff4
Download 9ff06ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-06T15:01:04+01:00 Download 68d041f
Download 458f0c4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-05T20:01:09+01:00 Download 728a96a
Download 728a96a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-05T16:10:49+01:00
Download 5172300 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2021-12-10T20:05:26+01:00
Download 8b89ac9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 4 2021-12-08T18:31:26+01:00
Download 434710a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 4 2021-12-09T13:45:29+01:00
Download ba92ff4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 6 2021-12-06T22:52:58Z

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

Trying to find witnesses for program (cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe, sv-benchmarks/c/termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c).

Found 8 witnesses for program sv-benchmarks/c/termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c, cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ad195ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.1 3 2020-12-06T23:35:44
Download b0edd3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) unknown_witness Goblint (svcomp21-0-g82e03b87) 3 2020-12-07T17:39:39
Download 9e132fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-09T21:33:53+01:00 Download a3b5816
Download 53bd09f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-09T02:16:24+01:00 Download e1b02a0
Download 225fb88 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-08T07:36:03+01:00 Download 673fce2
Download b13f4e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-06T13:38:45+01:00 Download 5a9767b
Download 5a9767b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-05T16:09:00+01:00
Download 673fce2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 4 2020-12-07T23:25:09+01:00

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

Trying to find witnesses for program (cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe, sv-benchmarks/c/termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c).

Found 2 witnesses for program sv-benchmarks/c/termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c, cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 62c6931 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 576 2019-11-30T07:46:58+01:00
Download 66902ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 576 2019-12-01T00:28:36+01:00

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

Trying to find witnesses for program (cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe, sv-benchmarks/c/termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c).

Found 3 witnesses for program sv-benchmarks/c/termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c, cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 31f929b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness SMACK 1.9.3 3 2018-12-08T01:07:28
Download 0c2440a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 658 2018-12-07T23:29:29+01:00
Download 5bbcd6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 658 2018-12-05T11:21:54+01:00

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

Trying to find witnesses for program (cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe, sv-benchmarks/c/termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c).

Found 4 witnesses for program sv-benchmarks/c/termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c, cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fcc6309 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 6 2017-12-03T07:43Z
Download 671e28e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 7 2017-12-03T10:24Z
Download 39fddcf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 6 2017-12-03T10:23Z
Download 5a9669f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 5 2017-12-01T19:36 CET (sv-comp)

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

Trying to find witnesses for program (cf5951cf7c939342bb5d014c8a7a12e4f95042e50c8d2f477b21d0a3234d49fe, sv-benchmarks/c/termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c).

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

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