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 32 witnesses for program sv-benchmarks/c/termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c, 905898d576dbb9521171e998174a24819933fa88ed72107c9a2c3094e7696cea
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/905898d576dbb9521171e998174a24819933fa88ed72107c9a2c3094e7696cea.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2193c98 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T18:01:31+01:00 | ||
04217e0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T08:08:50Z | ||
d56334a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 16 | 2023-12-02T14:10:01Z | ||
4de2795 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2023-12-17T03:43:57Z | ||
a89541e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T20:04:58Z | ||
56e9d3e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2023-12-20T00:07:47 | ||
4e19e4e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2023-11-29T06:25:20Z | ||
478d19f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 16 | 2023-12-02T22:35:51Z | ||
7e3dc63 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 11 | 2023-12-01T01:04:00Z | ||
f36edf2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-20T02:17:25+01:00 | 56e9d3e | |
ae96e4e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-19T14:43:55+01:00 | 11ef88a | |
b1a03d0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-19T03:30:17+01:00 | 2f1d842 | |
16e422e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-17T06:08:40+01:00 | 4de2795 | |
d404eff | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-04T11:52:47+01:00 | d56334a | |
a8b0644 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-04T01:51:11+01:00 | 3f924c7 | |
3f3f015 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-03T18:29:51+01:00 | 2193c98 | |
653069a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-03T09:54:42+01:00 | 04217e0 | |
1199928 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-03T05:50:29+01:00 | 478d19f | |
f4c1e71 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-01T03:45:55+01:00 | 7e3dc63 | |
689e448 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-30T11:32:11+01:00 | 3c8489e | |
3c8489e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-30T04:57:28+01:00 | ||
8361bda | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-30T02:35:54+01:00 | a89541e | |
b6d12a8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-29T18:26:29+01:00 | 4e19e4e | |
41431c8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-29T08:21:27+01:00 | 3ba0dcc | |
3f924c7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 8 | 2023-12-04T00:32:06+01:00 | ||
11ef88a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 8 | 2023-12-19T12:16:24+01:00 | ||
2f1d842 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 8 | 2023-12-18T21:51:18+01:00 | ||
3ba0dcc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 16 | 2023-11-28T23:01:58Z | ||
bbda2aa | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: ec458603-b594-4a5d-ac0b-cc54cf6b7c8b creation_time: '2023-12-02T23:35:51+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0b653441-e876-4a9d-aafb-468006562481/sv-benchmarks/c/termination-crafted-lit/cstrpbrk.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0b653441-e876-4a9d-aafb-468006562481/sv-benchmarks/c/termination-crafted-lit/cstrpbrk.c : 905898d576dbb9521171e998174a24819933fa88ed72107c9a2c3094e7696cea specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-03T05:42:03+01:00 | ||
16ea4c7 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: a5dac24a-89b4-4d1a-a5f1-fd1f147fe2a4 creation_time: '2023-11-29T00:01:58+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_82799916-696b-480b-b8e5-0899480ae223/sv-benchmarks/c/termination-crafted-lit/cstrpbrk.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_82799916-696b-480b-b8e5-0899480ae223/sv-benchmarks/c/termination-crafted-lit/cstrpbrk.c : 905898d576dbb9521171e998174a24819933fa88ed72107c9a2c3094e7696cea specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 9 | 2023-11-29T07:43:41+01:00 | ||
cac118d | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 027a4889-502a-4d28-a179-ad01fdb05e20 creation_time: '2023-12-02T15:10:01+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f39a9ec4-7202-46a4-a3f0-8a5c8b59982f/sv-benchmarks/c/termination-crafted-lit/cstrpbrk.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f39a9ec4-7202-46a4-a3f0-8a5c8b59982f/sv-benchmarks/c/termination-crafted-lit/cstrpbrk.c : 905898d576dbb9521171e998174a24819933fa88ed72107c9a2c3094e7696cea specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-04T11:58:41+01:00 | ||
38b7f13 | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: 2b5e889c-1da2-498d-bc25-902689e91991 creation_time: 2023-12-01T01:04:00Z 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/cstrpbrk.c''' task: input_files: - ../../sv-benchmarks/c/termination-crafted-lit/cstrpbrk.c input_file_hashes: ../../sv-benchmarks/c/termination-crafted-lit/cstrpbrk.c: 905898d576dbb9521171e998174a24819933fa88ed72107c9a2c3094e7696cea data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: [] | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-01T04:46:57+01:00 |
Found 29 witnesses for program sv-benchmarks/c/termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c, 905898d576dbb9521171e998174a24819933fa88ed72107c9a2c3094e7696cea
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/905898d576dbb9521171e998174a24819933fa88ed72107c9a2c3094e7696cea.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c56fced | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | verifuzz | 2 | 2022-12-15T08:53:43+01:00 | ||
e9cd7ac | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-11T01:46:01+01:00 | ||
f91fc0d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T10:34:46Z | ||
3be76bf | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 15 | 2022-12-14T06:37:19Z | ||
30d02a3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2022-12-25T08:24:04Z | ||
84092f1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T15:09:47Z | ||
7761bd1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2022-12-11T15:43:22 | ||
cb0e79b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2022-12-11T09:10:32Z | ||
6aa03a4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 15 | 2022-12-14T17:51:21Z | ||
7f3aa4f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp23-0-g4f5dcf38f) | 14 | 2022-12-10T07:59:47Z | ||
06ce77b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T11:11:51+01:00 | 3be76bf | |
cb4ccef | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T07:34:50+01:00 | 6dc1f05 | |
e47879b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T06:23:12+01:00 | 6aa03a4 | |
df5767c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T05:19:45+01:00 | 84092f1 | |
973864a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T04:49:43+01:00 | 7761bd1 | |
34bf9e8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T03:45:44+01:00 | cb0e79b | |
c81fb76 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T02:35:09+01:00 | a84b48c | |
881ce95 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-29T00:13:16+01:00 | c8d4263 | |
1676d07 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T22:52:44+01:00 | e9cd7ac | |
c1c2b28 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T22:38:07+01:00 | 7f3aa4f | |
55dd64b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T18:48:34+01:00 | cc9e66b | |
b9e2d20 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T17:38:10+01:00 | f91fc0d | |
c70bc22 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T11:25:31+01:00 | 67b51b5 | |
be188c1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T00:51:28+01:00 | 30d02a3 | |
67b51b5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2022-12-10T20:23:57+01:00 | ||
a84b48c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 8 | 2022-12-11T22:13:48+01:00 | ||
c8d4263 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 8 | 2022-12-11T06:00:06+01:00 | ||
cc9e66b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 8 | 2022-12-10T01:17:12+01:00 | ||
6dc1f05 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 15 | 2022-12-13T11:31:57Z |
Found 25 witnesses for program sv-benchmarks/c/termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c, 905898d576dbb9521171e998174a24819933fa88ed72107c9a2c3094e7696cea
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/905898d576dbb9521171e998174a24819933fa88ed72107c9a2c3094e7696cea.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4667791 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2021-12-06T13:42:21+01:00 | ||
6700336 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.2.8 | 3 | 2021-12-13T19:55:53Z | ||
c824a7c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 15 | 2021-12-10T06:37:37Z | ||
e1ef58f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T18:57:36 | ||
68032a3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2021-12-07T16:22:34Z | ||
f0d810a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2021-12-09T05:10:12 | ||
04b6807 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 15 | 2021-12-10T11:46:48Z | ||
4d4de71 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp22-0-ge852ac510) | 12 | 2021-12-07T21:07:35Z | ||
b9afcc3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 8 | 2021-12-14T00:09:38+01:00 | 6700336 | |
e310929 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 8 | 2021-12-10T20:56:35+01:00 | e1ef58f | |
19d2967 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 8 | 2021-12-10T17:28:45+01:00 | 04b6807 | |
c6d202c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 8 | 2021-12-10T08:37:56+01:00 | c824a7c | |
e93b89a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 8 | 2021-12-09T15:28:38+01:00 | e61e355 | |
e944342 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 8 | 2021-12-09T10:09:10+01:00 | f0d810a | |
8793a90 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 8 | 2021-12-08T21:51:07+01:00 | 7056777 | |
9403bcd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 8 | 2021-12-07T23:27:43+01:00 | 4d4de71 | |
939f197 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 8 | 2021-12-07T18:54:19+01:00 | 68032a3 | |
390d6df | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 8 | 2021-12-07T02:47:28+01:00 | 8a19e38 | |
15dc148 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 8 | 2021-12-06T14:56:22+01:00 | 4667791 | |
19e699b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 8 | 2021-12-05T20:31:24+01:00 | d95a8c8 | |
d95a8c8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 8 | 2021-12-05T17:55:31+01:00 | ||
7056777 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 8 | 2021-12-08T17:35:17+01:00 | ||
e61e355 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 8 | 2021-12-09T13:33:01+01:00 | ||
8a19e38 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 15 | 2021-12-06T19:39:45Z | ||
d6b2afd | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T16:24:12 |
Found 18 witnesses for program sv-benchmarks/c/termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c, 905898d576dbb9521171e998174a24819933fa88ed72107c9a2c3094e7696cea
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/905898d576dbb9521171e998174a24819933fa88ed72107c9a2c3094e7696cea.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
a96879f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.2.1 | 3 | 2020-12-06T23:51:29 | ||
04dc2f7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T22:53:22 | ||
d376fe7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T15:06:55 | ||
c0aef99 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2020-12-08T09:19:14 | ||
a491a55 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (svcomp21-0-g82e03b87) | 12 | 2020-12-07T19:46:37 | ||
262a6db | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 8 | 2020-12-12T01:22:06+01:00 | 04dc2f7 | |
f125032 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 8 | 2020-12-09T21:47:23+01:00 | 28868ab | |
7d32f0c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 8 | 2020-12-09T21:17:49+01:00 | 95e338a | |
0664926 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 8 | 2020-12-09T03:56:13+01:00 | d376fe7 | |
0f26ce5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 8 | 2020-12-09T02:37:29+01:00 | 514389f | |
c964f43 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 8 | 2020-12-08T13:44:52+01:00 | c0aef99 | |
cc6a11c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 8 | 2020-12-08T07:31:05+01:00 | 538d6fd | |
32d7f15 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 8 | 2020-12-07T21:18:24+01:00 | a491a55 | |
a13e323 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 8 | 2020-12-06T14:07:23+01:00 | 10b5522 | |
10b5522 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 8 | 2020-12-05T13:38:40+01:00 | ||
538d6fd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 8 | 2020-12-08T05:34:14+01:00 | ||
2b3ba50 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T18:28:49 | ||
c6ad7be | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T21:43:58 |
Found 2 witnesses for program sv-benchmarks/c/termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c, 905898d576dbb9521171e998174a24819933fa88ed72107c9a2c3094e7696cea
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/905898d576dbb9521171e998174a24819933fa88ed72107c9a2c3094e7696cea.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4bb68c8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.9 | 8 | 2019-11-30T08:47:46+01:00 | ||
f86e937 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 8 | 2019-11-30T21:24:07+01:00 |
Found 4 witnesses for program sv-benchmarks/c/termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c, 905898d576dbb9521171e998174a24819933fa88ed72107c9a2c3094e7696cea
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/905898d576dbb9521171e998174a24819933fa88ed72107c9a2c3094e7696cea.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
81e7879 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T08:13 CET (sv-comp) | ||
29e5322 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T07:53:17 | ||
6d8dce7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 8 | 2018-12-08T00:06:05+01:00 | ||
5435791 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-05T21:14:05+01:00 |
Found 6 witnesses for program sv-benchmarks/c/termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c, 905898d576dbb9521171e998174a24819933fa88ed72107c9a2c3094e7696cea
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/905898d576dbb9521171e998174a24819933fa88ed72107c9a2c3094e7696cea.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
cec23bb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 15 | 2017-12-03T07:44Z | ||
170d492 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 15 | 2017-12-03T10:28Z | ||
7e1399f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T17:28:57.837280 | ||
fc700ff | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-12-01T10:56:43+01:00 | ||
9650df3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 15 | 2017-12-03T10:36Z | ||
6c56e39 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 10 | 2017-12-01T19:58 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c, 905898d576dbb9521171e998174a24819933fa88ed72107c9a2c3094e7696cea
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/905898d576dbb9521171e998174a24819933fa88ed72107c9a2c3094e7696cea.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |