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 47 witnesses for program sv-benchmarks/c/termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c, 4006e5bbc9a234a3363872bc2e5100c7378eec16240b7c8c65c17af0dd119109
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/4006e5bbc9a234a3363872bc2e5100c7378eec16240b7c8c65c17af0dd119109.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
b11749c | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T10:13:03+01:00 | ||
f545480 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-11-30T00:22:01Z | ||
38ef2cc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-18T12:06:56+01:00 | b11749c | |
adcc235 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-11-30T08:05:11+01:00 | ||
910db59 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 4 | 2023-12-04T00:31:19+01:00 | ||
5cbc1d7 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Taipan | 8 | 2023-12-02T16:56:01Z | ||
e874665 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | PredatorHP | 4 | 2023-11-30T08:25:18Z | ||
5b34bd1 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2023-11-29T12:06:20Z | ||
94d0c55 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Kojak | 8 | 2023-12-02T23:07:50Z | ||
21fbafd | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 16 | 2023-12-01T00:56:11Z | ||
b6de48b | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Automizer | 8 | 2023-11-28T23:03:39Z | ||
47eba1d | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | 2LS | 11 | 2023-11-30T21:14:44+01:00 | ||
6bb90f5 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 4 | 2023-12-18T22:51:47+01:00 | ||
4ad41bc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T06:40:41Z | ||
910166f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:22:51+01:00 | ||
7bda14b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2023-12-20T03:37 CET (comp) | ||
6e3efc5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 7 | 2023-12-02T15:00:30Z | ||
21f5078 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2023-11-29T14:13:19Z | ||
b9c1012 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 7 | 2023-12-03T03:06:47Z | ||
f593e8e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 16 | 2023-12-01T01:07:01Z | ||
f1226a4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-20T03:41:10+01:00 | 7bda14b | |
c68e22a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-19T14:54:49+01:00 | 90db4a4 | |
82aa82c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-19T02:58:01+01:00 | 400c7a9 | |
ca1f7be | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-17T06:23:31+01:00 | 4a7825b | |
faa7c27 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-04T11:33:26+01:00 | 6e3efc5 | |
d1157c0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-04T01:26:50+01:00 | d665725 | |
807d6f8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-03T18:35:00+01:00 | 910166f | |
c8f43d4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-03T10:00:29+01:00 | 4ad41bc | |
dbdb0b9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-03T05:57:30+01:00 | b9c1012 | |
5595e5f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-01T03:36:59+01:00 | f593e8e | |
8c4b041 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-01T00:10:37+01:00 | f33465a | |
d3ff04c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-11-30T12:24:26+01:00 | 22f1d05 | |
22f1d05 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-11-30T08:59:55+01:00 | ||
4f91819 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-11-29T18:25:47+01:00 | 21f5078 | |
c6965b1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-11-29T08:20:27+01:00 | 0c6d8e9 | |
d665725 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 4 | 2023-12-03T23:08:37+01:00 | ||
4a7825b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2023-12-17T00:06:20+01:00 | ||
400c7a9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 4 | 2023-12-18T23:11:52+01:00 | ||
0c6d8e9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 7 | 2023-11-29T01:52:19Z | ||
f33465a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | 2LS | 9 | 2023-11-30T21:52:09+01:00 | ||
ab20c0e | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Bubaak | 3 | 2023-12-04T13:37:46Z | ||
7ed2e29 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 5 | 2023-11-28T19:34:21Z | ||
9f4e1c6 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 5 | 2023-11-30T22:44:56+01:00 | ||
7c0e94f | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: fbc05132-70d9-4db9-86fc-ad31a949964c creation_time: '2023-12-03T04:06:47+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3f5604c6-e6f9-4996-a6c1-7196ea144b29/sv-benchmarks/c/termination-crafted/Arrays02-EquivalentConstantIndices.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3f5604c6-e6f9-4996-a6c1-7196ea144b29/sv-benchmarks/c/termination-crafted/Arrays02-EquivalentConstantIndices.c : 4006e5bbc9a234a3363872bc2e5100c7378eec16240b7c8c65c17af0dd119109 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-03T05:32:04+01:00 | ||
b7f4bc6 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 9a83f57f-7f6f-41f2-8c98-817aae002428 creation_time: '2023-12-02T16:00:30+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_9b3b4db6-da19-4ab4-b92c-60aa09dbebf7/sv-benchmarks/c/termination-crafted/Arrays02-EquivalentConstantIndices.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_9b3b4db6-da19-4ab4-b92c-60aa09dbebf7/sv-benchmarks/c/termination-crafted/Arrays02-EquivalentConstantIndices.c : 4006e5bbc9a234a3363872bc2e5100c7378eec16240b7c8c65c17af0dd119109 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-04T12:03:17+01:00 | ||
589ec5a | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 0637bea1-ef38-4644-89e2-8ecd8ce995b5 creation_time: '2023-11-29T02:52:19+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_92ba7f3c-c234-4fac-8f41-91b69d3a9b84/sv-benchmarks/c/termination-crafted/Arrays02-EquivalentConstantIndices.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_92ba7f3c-c234-4fac-8f41-91b69d3a9b84/sv-benchmarks/c/termination-crafted/Arrays02-EquivalentConstantIndices.c : 4006e5bbc9a234a3363872bc2e5100c7378eec16240b7c8c65c17af0dd119109 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-29T07:49:30+01:00 | ||
7beef13 | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: 78ba92a8-28b5-4b1f-a916-907fb9842359 creation_time: 2023-12-01T01:07:01Z 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/Arrays02-EquivalentConstantIndices.c''' task: input_files: - ../../sv-benchmarks/c/termination-crafted/Arrays02-EquivalentConstantIndices.c input_file_hashes: ../../sv-benchmarks/c/termination-crafted/Arrays02-EquivalentConstantIndices.c: 4006e5bbc9a234a3363872bc2e5100c7378eec16240b7c8c65c17af0dd119109 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: [] | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-01T05:03:44+01:00 |
Found 40 witnesses for program sv-benchmarks/c/termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c, 4006e5bbc9a234a3363872bc2e5100c7378eec16240b7c8c65c17af0dd119109
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/4006e5bbc9a234a3363872bc2e5100c7378eec16240b7c8c65c17af0dd119109.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
20bda0d | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:54:07+01:00 | ||
cea9399 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T14:19:04+01:00 | 20bda0d | |
0acac63 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 4 | 2022-12-10T21:10:21+01:00 | ||
d8f60e5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 4 | 2022-12-11T22:56:11+01:00 | ||
4d41fee | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Taipan | 7 | 2022-12-14T03:48:44Z | ||
cc40ac2 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2022-12-11T10:23:41Z | ||
86b2abe | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Kojak | 7 | 2022-12-15T00:13:49Z | ||
9b62d7b | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Automizer | 7 | 2022-12-13T13:54:49Z | ||
01e3cf1 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | 2LS | 11 | 2022-12-07T23:21:47+01:00 | ||
994d88e | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 4 | 2022-12-10T02:27:17+01:00 | ||
2c70c94 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T12:51:01Z | ||
404f90a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-11T01:46:41+01:00 | ||
7bda14b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2022-12-12T11:01 CET (comp) | ||
45b0faa | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 6 | 2022-12-14T13:47:31Z | ||
90f7303 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2022-12-11T11:16:15Z | ||
d4e6436 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 6 | 2022-12-14T22:47:42Z | ||
9ce47b6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp23-0-g4f5dcf38f) | 18 | 2022-12-10T09:06:53Z | ||
193fe55 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T11:32:13+01:00 | 7bda14b | |
1c27ade | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T10:59:24+01:00 | 45b0faa | |
2ffb82d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T07:16:17+01:00 | 731159f | |
48e9c0b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T06:23:20+01:00 | d4e6436 | |
6b4b959 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T03:45:55+01:00 | 90f7303 | |
d9493e5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T03:11:05+01:00 | a65cbb2 | |
2703802 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T00:06:20+01:00 | 2d2f26d | |
d04711a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T22:50:23+01:00 | 404f90a | |
11d50ec | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T22:40:05+01:00 | 9ce47b6 | |
28159c4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T18:00:58+01:00 | 1f57006 | |
955a0a7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T17:48:39+01:00 | 2c70c94 | |
9b65ee4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T11:03:21+01:00 | 93f9f23 | |
3eb8b14 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T00:45:17+01:00 | e44b0fd | |
941c31d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-27T23:05:39+01:00 | 028c4d1 | |
93f9f23 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2022-12-10T19:31:41+01:00 | ||
a65cbb2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 4 | 2022-12-12T00:47:24+01:00 | ||
e44b0fd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2022-12-25T13:07:19+01:00 | ||
1f57006 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 4 | 2022-12-09T23:20:12+01:00 | ||
731159f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 6 | 2022-12-13T15:20:26Z | ||
028c4d1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | 2LS | 9 | 2022-12-08T01:39:01+01:00 | ||
e405924 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Bubaak | 3 | 2022-12-08T18:49:37Z | ||
65fc196 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 5 | 2022-12-13T18:39:00Z | ||
5253ead | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 5 | 2022-12-08T00:10:41+01:00 |
Found 32 witnesses for program sv-benchmarks/c/termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c, 4006e5bbc9a234a3363872bc2e5100c7378eec16240b7c8c65c17af0dd119109
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/4006e5bbc9a234a3363872bc2e5100c7378eec16240b7c8c65c17af0dd119109.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3f82dc6 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T08:09:14+01:00 | ||
e0b4ca6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-05T16:24:56+01:00 | ||
42fe105 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 4 | 2021-12-08T17:52:38+01:00 | ||
c89b12f | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Taipan | 7 | 2021-12-09T23:37:05Z | ||
33d3cc5 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Kojak | 7 | 2021-12-10T09:11:21Z | ||
73186d7 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Automizer | 7 | 2021-12-06T18:04:06Z | ||
bce63bf | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | 2LS | 11 | 2021-12-06T00:07:39+01:00 | ||
b3af140 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | SESL | 2 | 2021-12-06T11:51:24+01:00 | ||
527efb8 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 4 | 2021-12-09T10:23:31+01:00 | ||
4f5814b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2021-12-06T13:34:59+01:00 | ||
81950bb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.2.8 | 3 | 2021-12-13T21:42:46Z | ||
b759da4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 6 | 2021-12-09T23:45:28Z | ||
0c80e1f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 6 | 2021-12-10T15:06:24Z | ||
b7fa7b7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-14T00:12:20+01:00 | 81950bb | |
7bff81f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-10T21:16:21+01:00 | 7a6d8b9 | |
d48ec6d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-10T17:31:58+01:00 | 0c80e1f | |
a556da6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-10T08:39:25+01:00 | b759da4 | |
ec199f4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-09T15:45:56+01:00 | 85848ab | |
7c9902b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-08T21:13:41+01:00 | 0ac989e | |
40cf6e5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-07T02:56:28+01:00 | 6e9a4e9 | |
74aaece | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-06T15:01:22+01:00 | 4f5814b | |
fd9174f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-06T01:14:30+01:00 | 344a401 | |
5b8d71f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-05T20:04:03+01:00 | 6a41336 | |
6a41336 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-05T17:08:48+01:00 | ||
7a6d8b9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 4 | 2021-12-10T19:47:05+01:00 | ||
0ac989e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 4 | 2021-12-08T20:20:56+01:00 | ||
85848ab | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 4 | 2021-12-09T10:32:09+01:00 | ||
6e9a4e9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 6 | 2021-12-06T23:13:01Z | ||
344a401 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | 2LS | 8 | 2021-12-06T00:35:37+01:00 | ||
1c67778 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 5 | 2021-12-06T23:45:17Z | ||
41a4cff | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | AProVE | 5 | 2021-12-05T11:29:50Z | ||
956f2b2 | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 5 | 2021-12-05T22:42:43+01:00 |
Found 14 witnesses for program sv-benchmarks/c/termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c, 4006e5bbc9a234a3363872bc2e5100c7378eec16240b7c8c65c17af0dd119109
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/4006e5bbc9a234a3363872bc2e5100c7378eec16240b7c8c65c17af0dd119109.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8ff6193 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T12:30:03+01:00 | ||
6ed2cbb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 4 | 2020-12-05T15:33:30+01:00 | ||
2735a2d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 4 | 2020-12-08T02:15:57+01:00 | ||
7a7834d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | unknown_witness | Goblint (svcomp21-0-g82e03b87) | 3 | 2020-12-07T17:06:49 | ||
462d449 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.2.1 | 3 | 2020-12-06T23:35:15 | ||
f8451e3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 4 | 2020-12-09T21:56:52+01:00 | 138b714 | |
19aae59 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 4 | 2020-12-09T21:33:33+01:00 | 89190ed | |
7a46f23 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 4 | 2020-12-09T01:57:59+01:00 | 0f83049 | |
a9297aa | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 4 | 2020-12-08T06:29:43+01:00 | a327162 | |
6e2a5f7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 4 | 2020-12-07T00:09:22+01:00 | 462d449 | |
2fecb21 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 4 | 2020-12-06T16:46:28+01:00 | e4ea7a9 | |
42bced7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 4 | 2020-12-06T14:20:17+01:00 | 6331d44 | |
6331d44 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 4 | 2020-12-05T12:23:20+01:00 | ||
a327162 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 4 | 2020-12-08T04:49:12+01:00 |
Found 4 witnesses for program sv-benchmarks/c/termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c, 4006e5bbc9a234a3363872bc2e5100c7378eec16240b7c8c65c17af0dd119109
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/4006e5bbc9a234a3363872bc2e5100c7378eec16240b7c8c65c17af0dd119109.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1d820e7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 4 | 2019-11-30T14:37:04+01:00 | ||
79f6af1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 4 | 2019-12-01T00:54:57+01:00 | ||
daf66fa | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.9 | 4 | 2019-11-30T03:09:37+01:00 | ||
b34b64c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 4 | 2019-11-30T23:54:09+01:00 |
Found 3 witnesses for program sv-benchmarks/c/termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c, 4006e5bbc9a234a3363872bc2e5100c7378eec16240b7c8c65c17af0dd119109
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/4006e5bbc9a234a3363872bc2e5100c7378eec16240b7c8c65c17af0dd119109.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
407955f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T05:02:47 | ||
8909cb5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 4 | 2018-12-06T21:18:24+01:00 | ||
c866756 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T01:06:31+01:00 |
Found 10 witnesses for program sv-benchmarks/c/termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c, 4006e5bbc9a234a3363872bc2e5100c7378eec16240b7c8c65c17af0dd119109
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/4006e5bbc9a234a3363872bc2e5100c7378eec16240b7c8c65c17af0dd119109.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
746753f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 5 | 2017-12-03T07:43Z | ||
762bce2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 5 | 2017-12-03T10:18Z | ||
b5732c3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T17:28:59.785737 | ||
01b8543 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | ESBMC 3.1 | 4 | 2017-12-01T13:26 CET (sv-comp) | ||
2e62336 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 4 | 2017-12-01T10:58:20+01:00 | ||
290ce7c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 5 | 2017-12-03T10:19Z | ||
e2ac575 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | 2LS | 7 | 2017-12-01T10:25 CET (sv-comp) | ||
a424f55 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 4 | 2017-12-01T19:57 CET (sv-comp) | ||
b7c2bee | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Automizer | 5 | 2017-12-03T11:14Z | ||
58b9f7c | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | 2LS | 5 | 2017-12-01T16:17 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c, 4006e5bbc9a234a3363872bc2e5100c7378eec16240b7c8c65c17af0dd119109
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/4006e5bbc9a234a3363872bc2e5100c7378eec16240b7c8c65c17af0dd119109.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |