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/b.02_true-termination_true-no-overflow.c |
programSHA | f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29 |
witnessName | results-verified/depthk.2017-12-01_1515.logfiles/sv-comp18.b.02_true-termination_true-no-overflow.c.files/witness.graphml |
witnessSHA | c81b0e1868ba526c0cad100ff9b8d57747f48fcab1baa9f042033cbb68b0c9f8 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-01T20:07 CET (sv-comp) |
memoryModel | precise |
producer | ESBMC 3.1 |
program-sha256 | f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_f0b6da1e-3904-455a-845b-af8b59ad0f5e/sv-benchmarks/c/termination-restricted-15/b.02_true-termination_true-no-overflow.c |
programhash | b51be02cd04e7c7b94c5cc3bb2f6a3db64eee451 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/c81b0e1868ba526c0cad100ff9b8d57747f48fcab1baa9f042033cbb68b0c9f8.graphml |
witness-sha256 | c81b0e1868ba526c0cad100ff9b8d57747f48fcab1baa9f042033cbb68b0c9f8 |
witness-size | 4942 |
witness-type | correctness_witness |
Found 33 witnesses for program sv-benchmarks/c/termination-restricted-15/b.02_true-termination_true-no-overflow.c, f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3465540 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T07:33:42Z | ||
436d977 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:48:06+01:00 | ||
6b0db55 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2023-12-20T03:36 CET (comp) | ||
ec65493 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 7 | 2023-12-02T13:20:30Z | ||
0eb4403 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2023-11-29T08:47:16Z | ||
5ccb0b3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 7 | 2023-12-03T01:23:24Z | ||
af99215 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 15 | 2023-12-01T01:52:12Z | ||
f336230 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-20T03:41:16+01:00 | 6b0db55 | |
91840b3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-19T15:03:51+01:00 | 5fbaad6 | |
a3f97b8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-19T04:41:03+01:00 | 70b3454 | |
6986195 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-17T06:08:40+01:00 | edff047 | |
89734bc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-04T11:41:51+01:00 | ec65493 | |
31e0023 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-04T02:05:53+01:00 | ef08069 | |
8ca68ed | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-03T18:30:04+01:00 | 436d977 | |
c47fb03 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-03T09:59:56+01:00 | 3465540 | |
734bdf9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-03T05:59:46+01:00 | 5ccb0b3 | |
7d540bf | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-01T03:51:46+01:00 | af99215 | |
a73cd36 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-01T00:14:59+01:00 | 66c391f | |
0e06660 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-11-30T11:54:20+01:00 | 5813d3a | |
5813d3a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-11-30T08:46:54+01:00 | ||
807ed00 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-11-29T18:26:04+01:00 | 0eb4403 | |
b56d758 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-11-29T08:04:12+01:00 | 1caa616 | |
ef08069 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 4 | 2023-12-03T21:50:38+01:00 | ||
edff047 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2023-12-17T02:19:35+01:00 | ||
70b3454 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 4 | 2023-12-18T20:07:25+01:00 | ||
1caa616 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 7 | 2023-11-28T22:35:36Z | ||
66c391f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | 2LS | 8 | 2023-11-30T23:08:04+01:00 | ||
94edcba | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 3 | 2023-12-01T01:15:03Z | ||
2b99cd6 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 7 | 2023-11-30T22:02:36+01:00 | ||
e799c4a | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: d8cea26e-c952-4c87-83b4-cb11ac85aba1 creation_time: '2023-12-02T14:20: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_42fbb2f3-d47a-4aeb-ba8c-125d47a8c938/sv-benchmarks/c/termination-restricted-15/b.02.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_42fbb2f3-d47a-4aeb-ba8c-125d47a8c938/sv-benchmarks/c/termination-restricted-15/b.02.c : f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29 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_42fbb2f3-d47a-4aeb-ba8c-125d47a8c938/sv-benchmarks/c/termination-restricted-15/b.02.c file_hash: f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29 line: 11 column: 0 function: main value: ((x <= 2147483647) && (0 <= (y + 2147483648))) format: c_expression | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-04T12:00:10+01:00 | ||
6c5ab02 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: cbebc4cd-38be-4a8f-86a6-4ac9bac0cc25 creation_time: '2023-12-03T02:23:24+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_99a5317b-2b20-4f45-bf3b-a9e001a27277/sv-benchmarks/c/termination-restricted-15/b.02.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_99a5317b-2b20-4f45-bf3b-a9e001a27277/sv-benchmarks/c/termination-restricted-15/b.02.c : f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29 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_99a5317b-2b20-4f45-bf3b-a9e001a27277/sv-benchmarks/c/termination-restricted-15/b.02.c file_hash: f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29 line: 11 column: 0 function: main value: ((x <= 2147483647) && (0 <= (y + 2147483648))) format: c_expression | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-03T05:30:46+01:00 | ||
c96a9b5 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 567422dd-fd3a-4cde-813a-f1bc36e50734 creation_time: '2023-11-28T23:35:36+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_25ca36d6-aa22-4dda-a6ac-2bb07dde1706/sv-benchmarks/c/termination-restricted-15/b.02.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_25ca36d6-aa22-4dda-a6ac-2bb07dde1706/sv-benchmarks/c/termination-restricted-15/b.02.c : f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29 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_25ca36d6-aa22-4dda-a6ac-2bb07dde1706/sv-benchmarks/c/termination-restricted-15/b.02.c file_hash: f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29 line: 11 column: 0 function: main value: ((x <= 2147483647) && (0 <= (y + 2147483648))) format: c_expression | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-29T07:50:41+01:00 | ||
cb52b08 | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: 4f38c482-a2c3-4936-ae80-cb870e3cae7d creation_time: 2023-12-01T01:52:12Z 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/b.02.c''' task: input_files: - ../../sv-benchmarks/c/termination-restricted-15/b.02.c input_file_hashes: ../../sv-benchmarks/c/termination-restricted-15/b.02.c: f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29 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/b.02.c file_hash: f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29 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/b.02.c file_hash: f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29 line: 11 column: 11 function: main value: c == 0 format: c_expression | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-01T05:35:17+01:00 |
Found 29 witnesses for program sv-benchmarks/c/termination-restricted-15/b.02_true-termination_true-no-overflow.c, f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
011cf78 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T13:26:08Z | ||
9ecaf21 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-10T22:15:03+01:00 | ||
6b0db55 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2022-12-12T11:02 CET (comp) | ||
36e92dc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 7 | 2022-12-14T13:25:35Z | ||
4834af0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2022-12-11T11:58:22Z | ||
c032869 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 7 | 2022-12-14T15:37:52Z | ||
8d6820c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp23-0-g4f5dcf38f) | 30 | 2022-12-10T06:57:56Z | ||
f9f89de | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T11:32:13+01:00 | 6b0db55 | |
73d6600 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T10:51:52+01:00 | 36e92dc | |
ee8923f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T07:18:27+01:00 | ccebb7a | |
5089979 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T06:32:48+01:00 | c032869 | |
037eadb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T03:53:44+01:00 | 4834af0 | |
03b2982 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T02:48:11+01:00 | 31c26e3 | |
333a081 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T00:06:55+01:00 | f373246 | |
0aae4ad | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T22:51:01+01:00 | 9ecaf21 | |
7f75fcc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T22:23:47+01:00 | 8d6820c | |
cbe6c22 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T18:39:47+01:00 | aef1b4a | |
ae99c75 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T17:45:20+01:00 | 011cf78 | |
c766a50 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T11:08:13+01:00 | 082a2a9 | |
64398d1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T00:47:25+01:00 | 9d978d4 | |
665cc65 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-27T23:10:50+01:00 | 1a07496 | |
082a2a9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2022-12-10T17:47:44+01:00 | ||
31c26e3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 4 | 2022-12-12T01:44:03+01:00 | ||
9d978d4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2022-12-25T10:26:24+01:00 | ||
aef1b4a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 4 | 2022-12-10T00:59:09+01:00 | ||
ccebb7a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 7 | 2022-12-13T13:12:02Z | ||
1a07496 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | 2LS | 8 | 2022-12-07T23:32:40+01:00 | ||
8b9ef0c | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2022-12-08T16:32:57Z | ||
ff86ffa | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 7 | 2022-12-07T23:59:44+01:00 |
Found 1 witnesses for program sv-benchmarks/c/termination-restricted-15/b.02_true-termination_true-no-overflow.c, f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f095adb | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 7 | 2021-12-05T19:38:46+01:00 |
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/b.02_true-termination_true-no-overflow.c, f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29.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/b.02_true-termination_true-no-overflow.c, f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29.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/b.02_true-termination_true-no-overflow.c, f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29.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/b.02_true-termination_true-no-overflow.c, f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c81b0e1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 5 | 2017-12-01T20:07 CET (sv-comp) | ||
276b7e9 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 8 | 2017-12-01T12:10 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/b.02_true-termination_true-no-overflow.c, f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f69721f429e2c078896be0dd43d151ac74ff7c2b11c17b221481c5b944f3ea29.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |