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 28 witnesses for program sv-benchmarks/c/termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c, d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f9b9995 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T10:56:18+01:00 | ||
b8ae4a6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-12-17T00:52:12Z | ||
1eddf03 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T19:42:47Z | ||
e4d3d55 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T02:38:55+01:00 | ||
1b1e9be | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 6 | 2023-12-03T22:18:54+01:00 | ||
50d108c | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2023-12-18T22:10:32+01:00 | ||
46cebb3 | 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 | 11 | 2023-12-02T17:32:39Z | ||
fa3106e | 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) | 30 | 2023-12-01T01:34:42Z | ||
4777c81 | 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 | 11 | 2023-11-29T05:13:51Z | ||
fd9bbac | 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 | 14 | 2023-11-30T23:21:17+01:00 | ||
a4dd829 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T06:29:49Z | ||
9a2f5f8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2023-12-20T03:38 CET (comp) | ||
7b8c57e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 30 | 2023-12-01T02:09:31Z | ||
ec747f3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-20T03:41:10+01:00 | 9a2f5f8 | |
cc7567b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-19T15:11:24+01:00 | 8678dcc | |
6120fb6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-19T05:09:29+01:00 | cc87841 | |
ae4a4af | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-17T06:24:20+01:00 | 21ff1f4 | |
9e1653c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-04T01:50:05+01:00 | 3d1c610 | |
1739ea4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T09:54:13+01:00 | a4dd829 | |
6f3ee94 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-01T03:36:37+01:00 | 7b8c57e | |
0acdec8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-01T00:04:55+01:00 | 8ff7ad0 | |
a067775 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T12:07:56+01:00 | 8101f70 | |
8101f70 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T07:54:54+01:00 | ||
3d1c610 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 6 | 2023-12-03T21:15:50+01:00 | ||
21ff1f4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 6 | 2023-12-17T04:51:05+01:00 | ||
cc87841 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2023-12-18T20:12:36+01:00 | ||
8ff7ad0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | 2LS | 12 | 2023-11-30T22:32:03+01:00 | ||
104d01f | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: 05fe3eb6-9296-49e3-aa55-72329fb4939d creation_time: 2023-12-01T02:09:31Z 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/LexIndexValue-Array-1.c''' task: input_files: - ../../sv-benchmarks/c/termination-crafted/LexIndexValue-Array-1.c input_file_hashes: ../../sv-benchmarks/c/termination-crafted/LexIndexValue-Array-1.c: d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/LexIndexValue-Array-1.c file_hash: d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff line: 18 column: 8 function: main value: (-1048LL + (long long )i) + (long long )k >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/LexIndexValue-Array-1.c file_hash: d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff line: 18 column: 8 function: main value: (1048LL - (long long )i) + (long long )k >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/LexIndexValue-Array-1.c file_hash: d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff line: 18 column: 8 function: main value: i == 1048 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/LexIndexValue-Array-1.c file_hash: d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff line: 18 column: 8 function: main value: ((((((((0 <= k && (((((((k <= 3 && k <= 65535) && (-1045LL + (long long )i) - (long long )k >= 0LL) && (1051LL - (long long )i) - (long long )k >= 0LL) || (((k <= 2 && k <= 255) && (-1046LL + (long long )i) - (long long )k >= 0LL) && (1050LL - (long long )i) - (long long )k >= 0LL)) || (((k <= 2 && k <= 255) && (-1046LL + (long long )i) - (long long )k >= 0LL) && (1050LL - (long long )i) - (long long )k >= 0LL)) || (((k <= 1 && (-1047LL + (long long )i) - (long long )k >= 0LL) && (1049LL - (long long )i) - (long long )k >= 0LL) && (k == 0 || k == 1))) || (((k <= 1 && (-1047LL + (long long )i) - (long long )k >= 0LL) && (1049LL - (long long )i) - (long long )k >= 0LL) && (k == 0 || k == 1)))) || ((((-1048LL + (long long )i) - (long long )k >= 0LL && (1048LL - (long long )i) - (long long )k >= 0LL) && 0 == k) && k == 0)) || ((((-1048LL + (long long )i) - (long long )k >= 0LL && (1048LL - (long long )i) - (long long )k >= 0LL) && 0 == k) && k == 0)) || (((0 <= k && k <= 1047) && (-1LL + (long long )i) - (long long )k >= 0LL) && (2095LL - (long long )i) - (long long )k >= 0LL)) || (((0 <= k && k <= 1048) && (2096LL - (long long )i) - (long long )k >= 0LL) && (long long )i - (long long )k >= 0LL)) || (((0 <= k && k <= 5) && (-1043LL + (long long )i) - (long long )k >= 0LL) && (1053LL - (long long )i) - (long long )k >= 0LL)) || (((0 <= k && k <= 5) && (-1043LL + (long long )i) - (long long )k >= 0LL) && (1053LL - (long long )i) - (long long )k >= 0LL)) || (((0 <= k && k <= 4) && (-1044LL + (long long )i) - (long long )k >= 0LL) && (1052LL - (long long )i) - (long long )k >= 0LL)) || (((0 <= k && k <= 4) && (-1044LL + (long long )i) - (long long )k >= 0LL) && (1052LL - (long long )i) - (long long )k >= 0LL) format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/LexIndexValue-Array-1.c file_hash: d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff line: 14 column: 6 function: main value: 0 == k format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/LexIndexValue-Array-1.c file_hash: d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff line: 14 column: 6 function: main value: k == 0 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/LexIndexValue-Array-1.c file_hash: d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff line: 14 column: 6 function: main value: ((((((((((((8 <= i && i <= 1048) && (-8LL + (long long )i) + (long long )k >= 0LL) && (1048LL - (long long )i) + (long long )k >= 0LL) && (-8LL + (long long )i) - (long long )k >= 0LL) && (1048LL - (long long )i) - (long long )k >= 0LL) || (((((-7LL + (long long )i) + (long long )k >= 0LL && (7LL - (long long )i) + (long long )k >= 0LL) && (-7LL + (long long )i) - (long long )k >= 0LL) && (7LL - (long long )i) - (long long )k >= 0LL) && i == 7)) || (((((-6LL + (long long )i) + (long long )k >= 0LL && (6LL - (long long )i) + (long long )k >= 0LL) && (-6LL + (long long )i) - (long long )k >= 0LL) && (6LL - (long long )i) - (long long )k >= 0LL) && i == 6)) || (((((-5LL + (long long )i) + (long long )k >= 0LL && (5LL - (long long )i) + (long long )k >= 0LL) && (-5LL + (long long )i) - (long long )k >= 0LL) && (5LL - (long long )i) - (long long )k >= 0LL) && i == 5)) || (((((-4LL + (long long )i) + (long long )k >= 0LL && (4LL - (long long )i) + (long long )k >= 0LL) && (-4LL + (long long )i) - (long long )k >= 0LL) && (4LL - (long long )i) - (long long )k >= 0LL) && i == 4)) || (((((-3LL + (long long )i) + (long long )k >= 0LL && (3LL - (long long )i) + (long long )k >= 0LL) && (-3LL + (long long )i) - (long long )k >= 0LL) && (3LL - (long long )i) - (long long )k >= 0LL) && i == 3)) || (((((-2LL + (long long )i) + (long long )k >= 0LL && (2LL - (long long )i) + (long long )k >= 0LL) && (-2LL + (long long )i) - (long long )k >= 0LL) && (2LL - (long long )i) - (long long )k >= 0LL) && i == 2)) || (((((-1LL + (long long )i) + (long long )k >= 0LL && (1LL - (long long )i) + (long long )k >= 0LL) && (-1LL + (long long )i) - (long long )k >= 0LL) && (1LL - (long long )i) - (long long )k >= 0LL) && i == 1)) || (((((((0LL - (long long )i) + (long long )k >= 0LL && (long long )i + (long long )k >= 0LL) && (0LL - (long long )i) - (long long )k >= 0LL) && (long long )i - (long long )k >= 0LL) && 0 == i) && k == i) && i == 0) format: c_expression | correctness_witness | CPAchecker 2.3 | 14 | 2023-12-01T05:38:57+01:00 |
Found 25 witnesses for program sv-benchmarks/c/termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c, d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
947b2ea | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:48:06+01:00 | ||
118a240 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2022-12-25T10:24:17Z | ||
f68b6c4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 6 | 2022-12-10T17:19:21+01:00 | ||
ab1ca0a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 6 | 2022-12-12T00:54:37+01:00 | ||
748c148 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2022-12-10T00:23:25+01:00 | ||
8b6d3d8 | 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 | 11 | 2022-12-14T15:03:34Z | ||
171361e | 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 | 10 | 2022-12-13T19:03:52Z | ||
e235d86 | 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 | 14 | 2022-12-07T21:36:22+01:00 | ||
99300f3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 2 | 2023-01-28T22:42:29+01:00 | c07073a | |
fbbe451 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T09:59:38Z | ||
9a2f5f8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2022-12-12T10:59 CET (comp) | ||
c07073a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp23-0-g4f5dcf38f) | 61 | 2022-12-10T08:38:14Z | ||
e05fe4e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T11:32:18+01:00 | 9a2f5f8 | |
24d611c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T03:03:10+01:00 | 0cfdf42 | |
31e87b1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T00:07:14+01:00 | bd41467 | |
cb76093 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T19:01:20+01:00 | 7dc3f2c | |
eaf0f5e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T17:38:33+01:00 | fbbe451 | |
d583398 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T10:53:16+01:00 | b9aefe8 | |
50c53f2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T00:46:39+01:00 | 8e57676 | |
4f6292b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-27T23:10:41+01:00 | 95075f2 | |
b9aefe8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2022-12-10T11:52:39+01:00 | ||
0cfdf42 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 6 | 2022-12-11T22:07:35+01:00 | ||
8e57676 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 6 | 2022-12-25T11:22:47+01:00 | ||
7dc3f2c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2022-12-10T01:17:40+01:00 | ||
95075f2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | 2LS | 12 | 2022-12-08T01:20:04+01:00 |
Found 20 witnesses for program sv-benchmarks/c/termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c, d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
fa16963 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T09:26:13+01:00 | ||
130e0db | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2021-12-07T09:30:39Z | ||
a0148ca | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 6 | 2021-12-05T18:34:39+01:00 | ||
8c7c4b0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 6 | 2021-12-08T18:28:20+01:00 | ||
a414cd3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 6 | 2021-12-09T13:09:30+01:00 | ||
ca7d512 | 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 | 11 | 2021-12-09T23:14:24Z | ||
79110a0 | 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 | 10 | 2021-12-06T16:10:44Z | ||
6872721 | 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 | 14 | 2021-12-05T20:44:22+01:00 | ||
8bf990b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | SESL | 2 | 2021-12-06T12:17:37+01:00 | ||
0781ac4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.2.8 | 3 | 2021-12-13T20:23:42Z | ||
aabdb2d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 6 | 2021-12-10T21:06:38+01:00 | cd2bb1a | |
578d2b2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 6 | 2021-12-09T15:42:49+01:00 | 0c99d4c | |
bcfa3d5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 6 | 2021-12-08T22:13:51+01:00 | 9c63158 | |
02e9d3e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 6 | 2021-12-06T01:16:12+01:00 | d9903ab | |
350e024 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 6 | 2021-12-05T20:12:50+01:00 | fc12bc0 | |
fc12bc0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 6 | 2021-12-05T18:03:34+01:00 | ||
cd2bb1a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 6 | 2021-12-10T19:16:36+01:00 | ||
9c63158 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 6 | 2021-12-08T19:38:05+01:00 | ||
0c99d4c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 6 | 2021-12-09T12:09:56+01:00 | ||
d9903ab | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | 2LS | 12 | 2021-12-05T23:43:59+01:00 |
Found 10 witnesses for program sv-benchmarks/c/termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c, d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
54c0513 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T17:52:30+01:00 | ||
d0cef91 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 6 | 2020-12-05T17:15:33+01:00 | ||
2b5288c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 6 | 2020-12-08T05:30:50+01:00 | ||
811ffcd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.2.1 | 3 | 2020-12-06T23:51:14 | ||
6a33b1d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | unknown_witness | Goblint (svcomp21-0-g82e03b87) | 3 | 2020-12-07T17:12:16 | ||
8c3ac83 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 6 | 2020-12-08T07:43:52+01:00 | 7c97fb9 | |
beb36a4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 6 | 2020-12-06T16:43:18+01:00 | 17ff137 | |
78cc1d2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 6 | 2020-12-06T13:43:10+01:00 | d044548 | |
d044548 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 6 | 2020-12-05T16:57:44+01:00 | ||
7c97fb9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 6 | 2020-12-08T04:04:31+01:00 |
Found 4 witnesses for program sv-benchmarks/c/termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c, d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2606f07 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 6 | 2019-11-30T15:00:56+01:00 | ||
f013d3d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 6 | 2019-12-01T02:36:04+01:00 | ||
0a435b8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.9 | 6 | 2019-11-30T04:03:18+01:00 | ||
a40902c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 6 | 2019-11-30T21:10:09+01:00 |
Found 2 witnesses for program sv-benchmarks/c/termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c, d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
147876d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 6 | 2018-12-07T12:26:40+01:00 | ||
eb1d1e9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T00:48:14+01:00 |
Found 4 witnesses for program sv-benchmarks/c/termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c, d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
a55a5ec | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | ESBMC 4.6.0 kind | 3 | 2017-12-02T18:44:03.052416 | ||
5f73e09 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-01T11:10:00+01:00 | ||
8dab248 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | 2LS | 11 | 2017-12-01T10:22 CET (sv-comp) | ||
5d96b0f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 7 | 2017-12-01T19:00 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c, d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/d69e4513fb8989bf305d8f9ce21862e8623f2a3d0c8146e8e7fb7e8c658a7eff.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |