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).
Found 30 witnesses for program sv-benchmarks/c/termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c, f94b058015be4fc42a3d40d63b8ed2b8d3be3933ae3f7b0cb4e17bd99a68e898
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/f94b058015be4fc42a3d40d63b8ed2b8d3be3933ae3f7b0cb4e17bd99a68e898.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d8db2e2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:44:18+01:00 | ||
dbf7524 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T07:31:28Z | ||
7603592 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 15 | 2023-12-02T13:08:17Z | ||
92c8c54 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2023-12-17T01:49:22Z | ||
b559608 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T16:55:16Z | ||
9c8be1b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2023-12-19T19:48:29 | ||
efe5ae3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2023-11-29T15:47:55Z | ||
70e830e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 15 | 2023-12-02T20:54:00Z | ||
45f7980 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 11 | 2023-12-01T01:44:51Z | ||
8196978 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-20T02:17:37+01:00 | 9c8be1b | |
b302b17 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-19T03:58:41+01:00 | 05da4ff | |
7a7861e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-17T06:24:41+01:00 | 92c8c54 | |
3c29969 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-04T11:47:11+01:00 | 7603592 | |
03410bb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-04T01:30:25+01:00 | 2b8250f | |
245b1ff | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-03T18:35:20+01:00 | d8db2e2 | |
279724c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-03T09:53:54+01:00 | dbf7524 | |
edfb40d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-03T05:58:53+01:00 | 70e830e | |
0fcd9ee | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-01T03:45:04+01:00 | 45f7980 | |
64b2e69 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-30T12:44:13+01:00 | fee0495 | |
fee0495 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-30T04:39:26+01:00 | ||
52337c9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-30T02:34:24+01:00 | b559608 | |
fe4e08d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-29T18:16:25+01:00 | efe5ae3 | |
d4c214e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-29T08:17:28+01:00 | a27bc9b | |
2b8250f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 7 | 2023-12-03T20:39:47+01:00 | ||
05da4ff | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 7 | 2023-12-19T01:27:22+01:00 | ||
a27bc9b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 15 | 2023-11-29T00:46:09Z | ||
85ea30a | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: a4a6380f-0825-484d-9b70-781e97b41569 creation_time: '2023-11-29T01:46:09+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ecab30cb-23cb-4658-bc80-b1109fa57ec8/sv-benchmarks/c/termination-crafted-lit/cstrcmp.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ecab30cb-23cb-4658-bc80-b1109fa57ec8/sv-benchmarks/c/termination-crafted-lit/cstrcmp.c : f94b058015be4fc42a3d40d63b8ed2b8d3be3933ae3f7b0cb4e17bd99a68e898 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-29T07:50:08+01:00 | ||
4237407 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 77ab69d1-87a1-40c2-83ff-e221359355e4 creation_time: 2023-12-02T21: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_ff3fe1f0-6106-47c3-950b-fe54a313ef30/sv-benchmarks/c/termination-crafted-lit/cstrcmp.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ff3fe1f0-6106-47c3-950b-fe54a313ef30/sv-benchmarks/c/termination-crafted-lit/cstrcmp.c : f94b058015be4fc42a3d40d63b8ed2b8d3be3933ae3f7b0cb4e17bd99a68e898 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-03T05:43:51+01:00 | ||
c05f74b | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 2359ac70-3ed2-4e79-84a1-052725ece8ce creation_time: '2023-12-02T14:08:17+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_65587f6c-231b-4a3f-8b82-3d8e9b1a1c60/sv-benchmarks/c/termination-crafted-lit/cstrcmp.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_65587f6c-231b-4a3f-8b82-3d8e9b1a1c60/sv-benchmarks/c/termination-crafted-lit/cstrcmp.c : f94b058015be4fc42a3d40d63b8ed2b8d3be3933ae3f7b0cb4e17bd99a68e898 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-04T11:57:07+01:00 | ||
c668640 | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: 1d878885-1250-4531-8e83-9be7fc162fe9 creation_time: 2023-12-01T01:44:51Z 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/cstrcmp.c''' task: input_files: - ../../sv-benchmarks/c/termination-crafted-lit/cstrcmp.c input_file_hashes: ../../sv-benchmarks/c/termination-crafted-lit/cstrcmp.c: f94b058015be4fc42a3d40d63b8ed2b8d3be3933ae3f7b0cb4e17bd99a68e898 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: [] | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-01T04:13:20+01:00 |
Found 27 witnesses for program sv-benchmarks/c/termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c, f94b058015be4fc42a3d40d63b8ed2b8d3be3933ae3f7b0cb4e17bd99a68e898
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/f94b058015be4fc42a3d40d63b8ed2b8d3be3933ae3f7b0cb4e17bd99a68e898.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3e4c752 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | verifuzz | 2 | 2022-12-15T09:12:33+01:00 | ||
bfaf311 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-10T22:08:28+01:00 | ||
12f5b48 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T10:20:09Z | ||
5710c23 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 14 | 2022-12-14T14:22:28Z | ||
1e6a50b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2022-12-25T08:44:34Z | ||
ec4a882 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T11:58:32Z | ||
980d2c3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2022-12-11T16:13:12 | ||
67ea04f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2022-12-11T11:30:28Z | ||
3ce2c15 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 14 | 2022-12-14T21:28:59Z | ||
d92daf1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp23-0-g4f5dcf38f) | 15 | 2022-12-10T07:41:49Z | ||
de2e051 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T10:51:53+01:00 | 5710c23 | |
0c84580 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T07:37:55+01:00 | a11b26b | |
5a56365 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T06:29:18+01:00 | 3ce2c15 | |
6c6d4f1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T05:18:33+01:00 | ec4a882 | |
497f826 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T04:47:08+01:00 | 980d2c3 | |
56eb0d7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T03:46:00+01:00 | 67ea04f | |
3abc6ac | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T03:03:58+01:00 | 1941072 | |
513bf6f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T22:53:39+01:00 | bfaf311 | |
46e1cf8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T22:31:35+01:00 | d92daf1 | |
192ec91 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T18:43:22+01:00 | 9a902de | |
35dbffd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T17:38:09+01:00 | 12f5b48 | |
90b2af2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T11:30:10+01:00 | b0317af | |
e4d3790 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T00:31:05+01:00 | 1e6a50b | |
b0317af | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2022-12-10T19:55:14+01:00 | ||
1941072 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 7 | 2022-12-11T23:56:57+01:00 | ||
9a902de | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 7 | 2022-12-10T02:26:15+01:00 | ||
a11b26b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 14 | 2022-12-13T14:04:45Z |
Found 25 witnesses for program sv-benchmarks/c/termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c, f94b058015be4fc42a3d40d63b8ed2b8d3be3933ae3f7b0cb4e17bd99a68e898
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/f94b058015be4fc42a3d40d63b8ed2b8d3be3933ae3f7b0cb4e17bd99a68e898.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f1259be | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2021-12-06T13:42:48+01:00 | ||
8828ec0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.2.8 | 3 | 2021-12-13T21:21:51Z | ||
68d521d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 15 | 2021-12-10T03:28:25Z | ||
29bc412 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T18:32:05 | ||
957fb17 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2021-12-07T15:43:20Z | ||
72ef69d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2021-12-09T06:12:51 | ||
128873b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 15 | 2021-12-10T13:21:30Z | ||
f866d83 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp22-0-ge852ac510) | 13 | 2021-12-07T21:27:38Z | ||
a0477b8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 7 | 2021-12-14T00:10:08+01:00 | 8828ec0 | |
acaa3f2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 7 | 2021-12-10T21:24:28+01:00 | 29bc412 | |
63f50c6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 7 | 2021-12-10T17:28:05+01:00 | 128873b | |
31e7421 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 7 | 2021-12-10T08:48:02+01:00 | 68d521d | |
a4eec94 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 7 | 2021-12-09T15:29:08+01:00 | e736570 | |
a3266c1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 7 | 2021-12-09T10:09:49+01:00 | 72ef69d | |
9980156 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 7 | 2021-12-08T21:30:44+01:00 | 7150ced | |
4ddc229 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 7 | 2021-12-07T23:35:45+01:00 | f866d83 | |
043de05 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 7 | 2021-12-07T18:56:46+01:00 | 957fb17 | |
86c1c0d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 7 | 2021-12-07T02:54:33+01:00 | d0a35f7 | |
58e5593 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 7 | 2021-12-06T15:05:11+01:00 | f1259be | |
897b597 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 7 | 2021-12-05T20:20:10+01:00 | 05892fa | |
05892fa | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 7 | 2021-12-05T19:03:34+01:00 | ||
7150ced | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 7 | 2021-12-08T20:18:04+01:00 | ||
e736570 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 7 | 2021-12-09T14:27:45+01:00 | ||
d0a35f7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 15 | 2021-12-06T20:36:59Z | ||
078fe99 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T19:05:31 |
Found 18 witnesses for program sv-benchmarks/c/termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c, f94b058015be4fc42a3d40d63b8ed2b8d3be3933ae3f7b0cb4e17bd99a68e898
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/f94b058015be4fc42a3d40d63b8ed2b8d3be3933ae3f7b0cb4e17bd99a68e898.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1edfef0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.2.1 | 3 | 2020-12-06T23:35:26 | ||
82837a2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T16:16:28 | ||
c421cfb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T19:41:45 | ||
e3900ce | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2020-12-08T10:11:38 | ||
34e7cf3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (svcomp21-0-g82e03b87) | 14 | 2020-12-07T16:49:14 | ||
5a33340 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 7 | 2020-12-12T01:31:37+01:00 | 82837a2 | |
85d4369 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 7 | 2020-12-09T22:06:53+01:00 | 35e4113 | |
2eea220 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 7 | 2020-12-09T21:06:31+01:00 | 8ebb0af | |
f04cb82 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 7 | 2020-12-09T03:56:12+01:00 | c421cfb | |
23e8914 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 7 | 2020-12-09T01:57:16+01:00 | e4e41a9 | |
876e19e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 7 | 2020-12-08T13:50:21+01:00 | e3900ce | |
7d78d91 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 7 | 2020-12-08T07:46:41+01:00 | d70c3d8 | |
860e721 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 7 | 2020-12-07T21:12:18+01:00 | 34e7cf3 | |
2ebb368 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 7 | 2020-12-06T13:13:02+01:00 | b627b84 | |
b627b84 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 7 | 2020-12-05T16:04:20+01:00 | ||
d70c3d8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 7 | 2020-12-08T02:26:07+01:00 | ||
0972481 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T23:42:20 | ||
2d0c7f5 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-09T00:22:57 |
Found 2 witnesses for program sv-benchmarks/c/termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c, f94b058015be4fc42a3d40d63b8ed2b8d3be3933ae3f7b0cb4e17bd99a68e898
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f94b058015be4fc42a3d40d63b8ed2b8d3be3933ae3f7b0cb4e17bd99a68e898.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
530432f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.9 | 7 | 2019-11-30T10:36:00+01:00 | ||
7d2bfc4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 7 | 2019-12-01T15:50:57+01:00 |
Found 4 witnesses for program sv-benchmarks/c/termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c, f94b058015be4fc42a3d40d63b8ed2b8d3be3933ae3f7b0cb4e17bd99a68e898
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f94b058015be4fc42a3d40d63b8ed2b8d3be3933ae3f7b0cb4e17bd99a68e898.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
00a4515 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T08:11 CET (sv-comp) | ||
2817c79 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T09:50:16 | ||
3e1bc39 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 7 | 2018-12-06T20:09:19+01:00 | ||
943bf3e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T00:11:27+01:00 |
Found 7 witnesses for program sv-benchmarks/c/termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c, f94b058015be4fc42a3d40d63b8ed2b8d3be3933ae3f7b0cb4e17bd99a68e898
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f94b058015be4fc42a3d40d63b8ed2b8d3be3933ae3f7b0cb4e17bd99a68e898.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
b36f697 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 14 | 2017-12-03T07:43Z | ||
fc1dd58 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 14 | 2017-12-03T10:34Z | ||
28fd2b4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T17:42:40.059973 | ||
b035300 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | ESBMC 3.1 | 7 | 2017-12-01T13:10 CET (sv-comp) | ||
8a265d4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-01T11:32:29+01:00 | ||
5afdd2c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 14 | 2017-12-03T10:38Z | ||
69cfc52 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 7 | 2017-12-01T18:41 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c, f94b058015be4fc42a3d40d63b8ed2b8d3be3933ae3f7b0cb4e17bd99a68e898
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f94b058015be4fc42a3d40d63b8ed2b8d3be3933ae3f7b0cb4e17bd99a68e898.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |