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-restricted-15/AlternKonv_false-termination_true-no-overflow.c
programSHA 9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939
witnessName results-validated/cpa-seq-validate-violation-witnesses-uautomizer.2018-12-09_2030.logfiles/sv-comp19_prop-termination.AlternKonv_false-termination_true-no-overflow.c.files/witness.graphml
witnessSHA 943c7f66a31faf3e2f56e3ccd6cafae087412ae7b1f73ea014ffa1690b07746f

Information about the Witness from Competition Database

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

Key Value
architecture 64bit
creationtime 2018-12-09T20:35:29+01:00
producer CPAchecker 1.7-svn 29852
program-sha256 9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939
programfile ../../sv-benchmarks/c/termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c
programhash 9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939
sourcecodelang C
specification CHECK( init(main()), LTL(F end) )
witness-file witnessFileByHash/943c7f66a31faf3e2f56e3ccd6cafae087412ae7b1f73ea014ffa1690b07746f.graphml
witness-sha256 943c7f66a31faf3e2f56e3ccd6cafae087412ae7b1f73ea014ffa1690b07746f
witness-size 9455
witness-type violation_witness

This witness was created for this program (cf. table above, 9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939).

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

Trying to find witnesses for program (9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939, sv-benchmarks/c/termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c).

Found 40 witnesses for program sv-benchmarks/c/termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c, 9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8a13a80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T04:16:04Z
Download 5bfd138 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:35:07+01:00
Download 7b4f092 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:37 CET (comp)
Download c90b9bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 9 2023-12-02T16:43:53Z
Download 1fa46d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T12:44:01Z
Download 8c26121 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 9 2023-12-02T22:37:54Z
Download 625ee93 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 23 2023-12-01T01:16:37Z
Download e20beca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-20T03:41:13+01:00 Download 7b4f092
Download 92ec0fb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-19T14:52:59+01:00 Download 4063c0c
Download f205001 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-19T05:00:32+01:00 Download aae79ad
Download 1ff1d1d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-17T06:26:54+01:00 Download 1bffc9c
Download 8f520bb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-04T11:24:06+01:00 Download c90b9bf
Download b7d9189 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-04T02:01:14+01:00 Download d85a601
Download a049b7f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-03T18:30:13+01:00 Download 5bfd138
Download dc4cc69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-03T10:01:23+01:00 Download 8a13a80
Download c2b6a24 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-03T05:50:39+01:00 Download 8c26121
Download a5c4fb6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-01T03:42:54+01:00 Download 625ee93
Download 6496f40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-01T00:00:14+01:00 Download b668516
Download 01c37bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-11-30T11:34:39+01:00 Download 9aec2de
Download 9aec2de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-11-30T08:05:28+01:00
Download 67b0ffd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-11-29T18:36:07+01:00 Download 1fa46d3
Download 020b3b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-11-29T08:16:39+01:00 Download 38fa7ec
Download d85a601 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 6 2023-12-03T20:35:48+01:00
Download 1bffc9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 6 2023-12-17T02:44:18+01:00
Download aae79ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2023-12-19T02:16:38+01:00
Download 38fa7ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 9 2023-11-29T05:55:03Z
Download b668516 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 11 2023-11-30T22:03:47+01:00
Download a25b151 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness VERIFUZZ 3 2023-12-01T22:31:47Z
Download 6207b97 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.3 9 2023-11-30T08:57:29+01:00
Download 91ba2b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 9 2023-12-03T22:41:33+01:00
Download 71402c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.1 9 2023-12-17T04:41:05+01:00
Download 0ecbdda Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 9 2023-12-18T18:56:14+01:00
Download f0dd03f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Bubaak 3 2023-12-05T09:45:20Z
Download 83227df Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Bubaak 3 2023-12-04T13:28:24Z
Download 46078e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 7 2023-11-29T04:23:50Z
Download f5239f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 6 2023-11-30T23:23:24+01:00
Download 7440f5c Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: c727639a-2961-4f9b-a80f-928e7d5f040a creation_time: '2023-12-02T23:37:54+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f6178a4c-7187-48d5-a982-2d42a69c3335/sv-benchmarks/c/termination-restricted-15/AlternKonv.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f6178a4c-7187-48d5-a982-2d42a69c3335/sv-benchmarks/c/termination-restricted-15/AlternKonv.c : 9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939 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_f6178a4c-7187-48d5-a982-2d42a69c3335/sv-benchmarks/c/termination-restricted-15/AlternKonv.c file_hash: 9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939 line: 9 column: 0 function: main value: ((i <= 2147483647) && (0 <= (i + 2147483648))) format: c_expression correctness_witness CPAchecker 2.3 8 2023-12-03T05:33:10+01:00
Download 0a1adda Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 36a6b379-4572-44ff-a960-90343eb19479 creation_time: '2023-11-29T06:55:03+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_9fc8ac73-14cd-4f01-adfb-d2885245b270/sv-benchmarks/c/termination-restricted-15/AlternKonv.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_9fc8ac73-14cd-4f01-adfb-d2885245b270/sv-benchmarks/c/termination-restricted-15/AlternKonv.c : 9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939 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_9fc8ac73-14cd-4f01-adfb-d2885245b270/sv-benchmarks/c/termination-restricted-15/AlternKonv.c file_hash: 9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939 line: 9 column: 0 function: main value: ((i <= 2147483647) && (0 <= (i + 2147483648))) format: c_expression correctness_witness CPAchecker 2.3 8 2023-11-29T07:45:10+01:00
Download 09360b0 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 1c04b8fd-b32a-4410-a42f-66db1ac272df creation_time: '2023-12-02T17:43:54+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0b4a7ca5-52f0-4a6c-abb2-dd4b10e0bd03/sv-benchmarks/c/termination-restricted-15/AlternKonv.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0b4a7ca5-52f0-4a6c-abb2-dd4b10e0bd03/sv-benchmarks/c/termination-restricted-15/AlternKonv.c : 9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939 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_0b4a7ca5-52f0-4a6c-abb2-dd4b10e0bd03/sv-benchmarks/c/termination-restricted-15/AlternKonv.c file_hash: 9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939 line: 9 column: 0 function: main value: ((i <= 2147483647) && (0 <= (i + 2147483648))) format: c_expression correctness_witness CPAchecker 2.3 8 2023-12-04T12:03:10+01:00
Download ca39732 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: 5e814271-1154-4fb0-ba79-1100490bdf5b creation_time: 2023-12-01T01:16:37Z 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-restricted-15/AlternKonv.c''' task: input_files: - ../../sv-benchmarks/c/termination-restricted-15/AlternKonv.c input_file_hashes: ../../sv-benchmarks/c/termination-restricted-15/AlternKonv.c: 9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: [] correctness_witness CPAchecker 2.3 7 2023-12-01T04:50:09+01:00

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

Trying to find witnesses for program (9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939, sv-benchmarks/c/termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c).

Found 34 witnesses for program sv-benchmarks/c/termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c, 9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4eb5a76 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T11:52:57Z
Download 888da65 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T22:13:20+01:00
Download 7b4f092 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T11:01 CET (comp)
Download ac29359 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 9 2022-12-14T12:16:56Z
Download ae9aac9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T10:18:14Z
Download 1970ac2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 9 2022-12-14T19:06:22Z
Download 9f0d6a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp23-0-g4f5dcf38f) 35 2022-12-10T09:37:51Z
Download e9d60b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-29T11:32:16+01:00 Download 7b4f092
Download 6e70227 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-29T11:07:33+01:00 Download ac29359
Download 7707359 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-29T07:17:48+01:00 Download 9540304
Download 843be64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-29T06:23:12+01:00 Download 1970ac2
Download a76eaff Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-29T03:49:45+01:00 Download ae9aac9
Download 9176787 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-29T02:33:50+01:00 Download 8ed9b91
Download 4c75d9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-29T00:06:25+01:00 Download 00016fc
Download ee649cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-28T22:53:41+01:00 Download 888da65
Download 3e768c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-28T22:32:56+01:00 Download 9f0d6a0
Download 090aa78 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-28T18:27:43+01:00 Download 49382d5
Download cbbbd34 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-28T17:46:18+01:00 Download 4eb5a76
Download e9da9a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-28T11:54:01+01:00 Download 61af04e
Download 2800bf3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-28T00:47:20+01:00 Download df42a3a
Download 0f8730b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-27T23:26:32+01:00 Download 76b8dd5
Download 61af04e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2022-12-10T18:07:35+01:00
Download 8ed9b91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 6 2022-12-11T23:26:01+01:00
Download df42a3a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 6 2022-12-25T12:07:24+01:00
Download 49382d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2022-12-10T03:25:06+01:00
Download 9540304 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 9 2022-12-13T13:40:55Z
Download 76b8dd5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 11 2022-12-08T01:37:56+01:00
Download c788320 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.2 9 2022-12-10T18:51:18+01:00
Download c916425 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 9 2022-12-11T23:24:34+01:00
Download 27721f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.1 9 2022-12-25T13:24:51+01:00
Download b4dec60 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 9 2022-12-10T03:44:09+01:00
Download 8f0bed2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Bubaak 3 2022-12-08T15:33:25Z
Download 3711924 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 7 2022-12-13T17:53:57Z
Download de6ca3e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 6 2022-12-07T22:30:07+01:00

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

Trying to find witnesses for program (9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939, sv-benchmarks/c/termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c).

Found 7 witnesses for program sv-benchmarks/c/termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c, 9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 1324e55 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.1 9 2021-12-05T17:00:34+01:00
Download d0c8257 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0 9 2021-12-10T20:20:08+01:00
Download a8fe5a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 9 2021-12-08T19:18:28+01:00
Download 4712ac7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 9 2021-12-09T13:15:46+01:00
Download e3b7a42 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 7 2021-12-06T22:25:31Z
Download fd60f6a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness AProVE 6 2021-12-05T11:31:26Z
Download 47bda39 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 6 2021-12-05T23:50:32+01:00

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

Trying to find witnesses for program (9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939, sv-benchmarks/c/termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c).

Found 2 witnesses for program sv-benchmarks/c/termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c, 9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 69348e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0 9 2020-12-05T16:32:54+01:00
Download 614d5b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 9 2020-12-08T05:22:28+01:00

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

Trying to find witnesses for program (9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939, sv-benchmarks/c/termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c).

Found 2 witnesses for program sv-benchmarks/c/termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c, 9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d66005c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 9 2019-11-30T09:34:37+01:00
Download 1193527 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 9 2019-11-30T23:23:59+01:00

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

Trying to find witnesses for program (9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939, sv-benchmarks/c/termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c).

Found 4 witnesses for program sv-benchmarks/c/termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c, 9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fc3a072 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 9 2018-12-07T20:40:43+01:00
Download 943c7f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-09T20:35:29+01:00
Download 5b06663 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-05T23:35:21+01:00
Download f34088b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 9 2018-12-05T09:27:26+01:00

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

Trying to find witnesses for program (9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939, sv-benchmarks/c/termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c).

Found 4 witnesses for program sv-benchmarks/c/termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c, 9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6102ea2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 7 2017-12-01T19:51 CET (sv-comp)
Download b365253 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 9 2017-12-01T14:12:16+01:00
Download 7fa9a37 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 7 2017-12-03T11:17Z
Download 8d729d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 7 2017-12-01T14:38 CET (sv-comp)

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

Trying to find witnesses for program (9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939, sv-benchmarks/c/termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c, 9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/9816d5cc9e8c1fba9291af90498afaa319416e5c56fa3cf3ce8da9d63d3e9939.json

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