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).
Key | Value |
programName | sv-benchmarks/c/termination-restricted-15/a.10_true-termination.c |
programSHA | 8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b |
witnessName | results-verified/2ls.2018-12-04_2244.logfiles/sv-comp19_prop-termination.a.10_true-termination.c.files/witness.graphml |
witnessSHA | 15406c1707244a13cea6a9a5e658edb242e130bd3c5656a2e48ef2a6e7146680 |
Key | Value |
architecture | 64bit |
creationtime | 2018-12-05T19:22 CET (sv-comp) |
producer | 2LS |
programfile | ../../sv-benchmarks/c/termination-restricted-15/a.10_true-termination.c |
programhash | 8d0216d6bf8bf4f618f739d27f28d08a28da9c3b |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(F end) ) |
witness-file | witnessFileByHash/15406c1707244a13cea6a9a5e658edb242e130bd3c5656a2e48ef2a6e7146680.graphml |
witness-sha256 | 15406c1707244a13cea6a9a5e658edb242e130bd3c5656a2e48ef2a6e7146680 |
witness-size | 8004 |
witness-type | correctness_witness |
Found 28 witnesses for program sv-benchmarks/c/termination-restricted-15/a.10_true-termination.c, 8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9c1550f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T07:21:01Z | ||
edcafeb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:42:40+01:00 | ||
2a341e8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2023-12-20T03:38 CET (comp) | ||
35a98a1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 7 | 2023-12-02T18:48:12Z | ||
df786ef | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 7 | 2023-12-02T22:07:01Z | ||
37a33c9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-20T03:41:15+01:00 | 2a341e8 | |
6a1dcc5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-19T14:56:57+01:00 | b4c9e38 | |
8797de8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-19T04:34:43+01:00 | dfe390a | |
99458db | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-17T06:26:32+01:00 | cc8c99e | |
61c97a1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-04T11:39:09+01:00 | 35a98a1 | |
2f6e0af | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-04T01:21:51+01:00 | 117e93d | |
df56799 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-03T18:29:59+01:00 | edcafeb | |
5118912 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-03T10:00:44+01:00 | 9c1550f | |
4066764 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-03T05:47:42+01:00 | df786ef | |
a978035 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-01T00:10:18+01:00 | 4d395f7 | |
f217fb0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T11:28:34+01:00 | e7ad9ab | |
e7ad9ab | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T06:53:56+01:00 | ||
bb07843 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-29T08:19:00+01:00 | 4770c40 | |
117e93d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 5 | 2023-12-03T21:57:30+01:00 | ||
cc8c99e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 5 | 2023-12-17T01:55:15+01:00 | ||
dfe390a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2023-12-18T18:31:36+01:00 | ||
4770c40 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 7 | 2023-11-29T02:19:54Z | ||
4d395f7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | 2LS | 8 | 2023-11-30T09:38:10+01:00 | ||
f3ed128 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 8 | 2023-11-30T23:10:39+01:00 | ||
d5620ad | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: c10c49fc-8028-4ad2-a04d-dd3cf5dae6c5 creation_time: '2023-12-02T23:07:01+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_1c4ca286-9e40-4ebf-8021-da0ce770908e/sv-benchmarks/c/termination-restricted-15/a.10.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_1c4ca286-9e40-4ebf-8021-da0ce770908e/sv-benchmarks/c/termination-restricted-15/a.10.c : 8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_1c4ca286-9e40-4ebf-8021-da0ce770908e/sv-benchmarks/c/termination-restricted-15/a.10.c file_hash: 8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b line: 11 column: 0 function: main value: ((((x <= 2147483647) && (0 <= (x + 2147483648))) && (y < 2147483648)) && (0 <= (y + 2147483648))) format: c_expression | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T05:45:44+01:00 | ||
abe9792 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 965c7139-d018-41a4-afdd-c285c816a5c8 creation_time: '2023-11-29T03:19:54+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ec3a2998-698c-40d9-bcb1-841c2267713e/sv-benchmarks/c/termination-restricted-15/a.10.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ec3a2998-698c-40d9-bcb1-841c2267713e/sv-benchmarks/c/termination-restricted-15/a.10.c : 8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ec3a2998-698c-40d9-bcb1-841c2267713e/sv-benchmarks/c/termination-restricted-15/a.10.c file_hash: 8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b line: 11 column: 0 function: main value: ((((x <= 2147483647) && (0 <= (x + 2147483648))) && (y < 2147483648)) && (0 <= (y + 2147483648))) format: c_expression | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-29T07:47:02+01:00 | ||
673ec1c | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 7bcf3840-0cce-4269-a4ac-5091b6d559cb creation_time: '2023-12-02T19:48:12+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ac32177d-1ed2-41dc-9dba-76ce68cb93fd/sv-benchmarks/c/termination-restricted-15/a.10.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ac32177d-1ed2-41dc-9dba-76ce68cb93fd/sv-benchmarks/c/termination-restricted-15/a.10.c : 8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ac32177d-1ed2-41dc-9dba-76ce68cb93fd/sv-benchmarks/c/termination-restricted-15/a.10.c file_hash: 8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b line: 11 column: 0 function: main value: ((((x <= 2147483647) && (0 <= (x + 2147483648))) && (y < 2147483648)) && (0 <= (y + 2147483648))) format: c_expression | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-04T11:56:04+01:00 | ||
9742000 | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: 33f234fd-5234-47fb-a3f4-267dde7eebfc creation_time: 2023-12-01T01:31:13Z producer: name: Goblint version: tags/svcomp24-0-gc2e9465a7 command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--sets'' ''ana.specification'' ''../../sv-benchmarks/c/properties/no-overflow.prp'' ''--sets'' ''exp.architecture'' ''64bit'' ''../../sv-benchmarks/c/termination-restricted-15/a.10.c''' task: input_files: - ../../sv-benchmarks/c/termination-restricted-15/a.10.c input_file_hashes: ../../sv-benchmarks/c/termination-restricted-15/a.10.c: 8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/a.10.c file_hash: 8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b line: 11 column: 11 function: main value: 0 == c format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/a.10.c file_hash: 8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b line: 11 column: 11 function: main value: c == 0 format: c_expression | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-01T04:58:45+01:00 |
Found 24 witnesses for program sv-benchmarks/c/termination-restricted-15/a.10_true-termination.c, 8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e35dfc6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T13:25:23Z | ||
5b48f0b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-10T22:17:29+01:00 | ||
2a341e8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2022-12-12T11:02 CET (comp) | ||
dcad55f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 7 | 2022-12-14T06:54:46Z | ||
7259290 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 7 | 2022-12-15T01:09:32Z | ||
efaa10e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T11:32:12+01:00 | 2a341e8 | |
1a9c6b7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T10:51:35+01:00 | dcad55f | |
5b51c07 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T07:31:21+01:00 | bac1967 | |
c0f1e6c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T06:23:20+01:00 | 7259290 | |
2e61723 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T02:33:15+01:00 | 8023193 | |
c986950 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T00:07:46+01:00 | 45be4e2 | |
229441f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T22:51:17+01:00 | 5b48f0b | |
df79e85 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T18:04:59+01:00 | 5ebfc51 | |
fd3d5ce | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T17:47:23+01:00 | e35dfc6 | |
65c66e7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T11:05:52+01:00 | 784622d | |
ce745ef | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T00:45:50+01:00 | dd5a80b | |
6e185c4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-27T23:12:07+01:00 | 9ba620b | |
784622d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2022-12-10T11:55:02+01:00 | ||
8023193 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 5 | 2022-12-12T01:11:50+01:00 | ||
dd5a80b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 5 | 2022-12-25T13:39:12+01:00 | ||
5ebfc51 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2022-12-09T17:39:13+01:00 | ||
bac1967 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 7 | 2022-12-13T17:17:40Z | ||
9ba620b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | 2LS | 8 | 2022-12-07T23:05:38+01:00 | ||
b940627 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 8 | 2022-12-07T23:03:36+01:00 |
Found 1 witnesses for program sv-benchmarks/c/termination-restricted-15/a.10_true-termination.c, 8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d10823f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 8 | 2021-12-05T22:35:50+01:00 |
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/a.10_true-termination.c, 8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/a.10_true-termination.c, 8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/a.10_true-termination.c, 8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 2 witnesses for program sv-benchmarks/c/termination-restricted-15/a.10_true-termination.c, 8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
0dbdaaf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 6 | 2017-12-01T18:29 CET (sv-comp) | ||
fbacd7b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 8 | 2017-12-01T12:04 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/a.10_true-termination.c, 8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/8289502743fb6ee3e9387ca4db850e54d4ebfec650d98779b674c3406acaae1b.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |