Witness Inspection

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).

This link does not point to a witness, but below is a list of witnesses for the same program.

Available Results for the Program from Witness Store SV-COMP '24

Trying to find witnesses for program (f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4, sv-benchmarks/c/termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c).

Found 30 witnesses for program sv-benchmarks/c/termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c, f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download fddc202 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T06:57:47Z
Download 52152f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:37 CET (comp)
Download d8de408 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 7 2023-12-02T14:12:50Z
Download 22f3998 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T13:36:32Z
Download f158a77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 7 2023-12-02T19:54:20Z
Download 9017196 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 34 2023-12-01T02:08:00Z
Download 58ac3e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-20T03:41:15+01:00 Download 52152f8
Download 93984bd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-19T15:01:56+01:00 Download 248d1bc
Download fb302f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-19T04:46:55+01:00 Download a261ab5
Download 734c56a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-17T06:08:43+01:00 Download 835a00c
Download be79786 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-04T11:23:58+01:00 Download d8de408
Download 3be8b5e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-04T01:34:46+01:00 Download 2995ff2
Download bb31f19 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-03T09:58:52+01:00 Download fddc202
Download a87e60f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-03T06:01:20+01:00 Download f158a77
Download 344bd11 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-12-01T03:41:50+01:00 Download 9017196
Download e2703d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-11-30T23:46:22+01:00 Download c0853b2
Download 950bf16 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-11-30T11:43:28+01:00 Download a54ee4b
Download a54ee4b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-11-30T07:50:18+01:00
Download 02da858 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-11-29T18:12:16+01:00 Download 22f3998
Download 5537a8e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 6 2023-11-29T08:00:09+01:00 Download b8260c0
Download 2995ff2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 6 2023-12-03T22:12:52+01:00
Download 835a00c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 6 2023-12-17T05:25:43+01:00
Download a261ab5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2023-12-19T02:16:31+01:00
Download b8260c0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 7 2023-11-29T02:27:40Z
Download c0853b2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 8 2023-11-30T22:40:14+01:00
Download 2a38088 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 8 2023-11-30T22:33:11+01:00
Download 54d39e4 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: d07010de-681d-498f-a221-eb26e71ae2d6 creation_time: '2023-12-02T15:12:50+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0389c280-7f22-4904-8788-e49b440fb4c1/sv-benchmarks/c/termination-restricted-15/c.01_assume.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0389c280-7f22-4904-8788-e49b440fb4c1/sv-benchmarks/c/termination-restricted-15/c.01_assume.c : f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4 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_0389c280-7f22-4904-8788-e49b440fb4c1/sv-benchmarks/c/termination-restricted-15/c.01_assume.c file_hash: f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4 line: 9 column: 0 function: main value: (x < 2147483648) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0389c280-7f22-4904-8788-e49b440fb4c1/sv-benchmarks/c/termination-restricted-15/c.01_assume.c file_hash: f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4 line: 11 column: 0 function: main value: (((0 <= x) && (1 <= y)) && (x <= 2147483647)) format: c_expression correctness_witness CPAchecker 2.3 7 2023-12-04T11:58:04+01:00
Download b5c7b85 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 87a58b84-e332-4c1f-a78c-8be5d263d598 creation_time: '2023-12-02T20:54:20+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_baa94111-e93f-47a1-9271-395563cc9ca2/sv-benchmarks/c/termination-restricted-15/c.01_assume.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_baa94111-e93f-47a1-9271-395563cc9ca2/sv-benchmarks/c/termination-restricted-15/c.01_assume.c : f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4 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_baa94111-e93f-47a1-9271-395563cc9ca2/sv-benchmarks/c/termination-restricted-15/c.01_assume.c file_hash: f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4 line: 9 column: 0 function: main value: (x <= 2147483647) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_baa94111-e93f-47a1-9271-395563cc9ca2/sv-benchmarks/c/termination-restricted-15/c.01_assume.c file_hash: f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4 line: 11 column: 0 function: main value: ((0 <= x) && (x <= 2147483647)) format: c_expression correctness_witness CPAchecker 2.3 7 2023-12-03T05:40:41+01:00
Download 4c58e2d Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 4db2f7f1-281b-4620-90d2-5e767825db12 creation_time: '2023-11-29T03:27:40+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ae8b5cca-a70b-4865-a50b-499bc79fbcd4/sv-benchmarks/c/termination-restricted-15/c.01_assume.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ae8b5cca-a70b-4865-a50b-499bc79fbcd4/sv-benchmarks/c/termination-restricted-15/c.01_assume.c : f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4 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_ae8b5cca-a70b-4865-a50b-499bc79fbcd4/sv-benchmarks/c/termination-restricted-15/c.01_assume.c file_hash: f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4 line: 9 column: 0 function: main value: (x < 2147483648) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ae8b5cca-a70b-4865-a50b-499bc79fbcd4/sv-benchmarks/c/termination-restricted-15/c.01_assume.c file_hash: f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4 line: 11 column: 0 function: main value: (((0 <= x) && (1 <= y)) && (x <= 2147483647)) format: c_expression correctness_witness CPAchecker 2.3 7 2023-11-29T07:43:15+01:00
Download 0da4286 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: 2a7731f0-eb08-4be2-b486-7b40bec80529 creation_time: 2023-12-01T02:08: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-restricted-15/c.01_assume.c''' task: input_files: - ../../sv-benchmarks/c/termination-restricted-15/c.01_assume.c input_file_hashes: ../../sv-benchmarks/c/termination-restricted-15/c.01_assume.c: f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4 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/c.01_assume.c file_hash: f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4 line: 11 column: 15 function: main value: ((((((((((x != 0 && ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((y == 1024 && (((1025 <= x && (-2049LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) || ((513 <= x && (-1537LL + (long long )x) + (long long )y >= 0LL) && (511LL + (long long )x) - (long long )y >= 0LL))) || (((2097153 <= x && (-4194305LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 2097152)) || (((2097153 <= x && (-4194305LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 2097152)) || (((1048577 <= x && (-3145729LL + (long long )x) + (long long )y >= 0LL) && (1048575LL + (long long )x) - (long long )y >= 0LL) && y == 2097152)) || (((513 <= x && (-1025LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 512)) || (((513 <= x && (-1025LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 512)) || (((257 <= x && (-769LL + (long long )x) + (long long )y >= 0LL) && (255LL + (long long )x) - (long long )y >= 0LL) && y == 512)) || (((1048577 <= x && (-2097153LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 1048576)) || (((1048577 <= x && (-2097153LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 1048576)) || (((524289 <= x && (-1572865LL + (long long )x) + (long long )y >= 0LL) && (524287LL + (long long )x) - (long long )y >= 0LL) && y == 1048576)) || (((257 <= x && (-513LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 256)) || (((257 <= x && (-513LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 256)) || (((129 <= x && (-385LL + (long long )x) + (long long )y >= 0LL) && (127LL + (long long )x) - (long long )y >= 0LL) && y == 256)) || (((524289 <= x && (-1048577LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 524288)) || (((524289 <= x && (-1048577LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 524288)) || (((262145 <= x && (-786433LL + (long long )x) + (long long )y >= 0LL) && (262143LL + (long long )x) - (long long )y >= 0LL) && y == 524288)) || (((129 <= x && (-257LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 128)) || (((129 <= x && (-257LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 128)) || (((65 <= x && (-193LL + (long long )x) + (long long )y >= 0LL) && (63LL + (long long )x) - (long long )y >= 0LL) && y == 128)) || (((262145 <= x && (-524289LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 262144)) || (((262145 <= x && (-524289LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 262144)) || (((131073 <= x && (-393217LL + (long long )x) + (long long )y >= 0LL) && (131071LL + (long long )x) - (long long )y >= 0LL) && y == 262144)) || (((65 <= x && (-129LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 64)) || (((65 <= x && (-129LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 64)) || (((33 <= x && (-97LL + (long long )x) + (long long )y >= 0LL) && (31LL + (long long )x) - (long long )y >= 0LL) && y == 64)) || (((131073 <= x && (-262145LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 131072)) || (((131073 <= x && (-262145LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 131072)) || (((65537 <= x && (-196609LL + (long long )x) + (long long )y >= 0LL) && (65535LL + (long long )x) - (long long )y >= 0LL) && y == 131072)) || (((33 <= x && (-65LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 32)) || (((33 <= x && (-65LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 32)) || (((17 <= x && (-49LL + (long long )x) + (long long )y >= 0LL) && (15LL + (long long )x) - (long long )y >= 0LL) && y == 32)) || (((65537 <= x && (-131073LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 65536)) || (((65537 <= x && (-131073LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 65536)) || (((32769 <= x && (-98305LL + (long long )x) + (long long )y >= 0LL) && (32767LL + (long long )x) - (long long )y >= 0LL) && y == 65536)) || (((17 <= x && (-33LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 16)) || (((17 <= x && (-33LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 16)) || (((9 <= x && (-25LL + (long long )x) + (long long )y >= 0LL) && (7LL + (long long )x) - (long long )y >= 0LL) && y == 16)) || (((32769 <= x && (-65537LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 32768)) || (((32769 <= x && (-65537LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 32768)) || (((16385 <= x && (-49153LL + (long long )x) + (long long )y >= 0LL) && (16383LL + (long long )x) - (long long )y >= 0LL) && y == 32768)) || (((9 <= x && (-17LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 8)) || (((9 <= x && (-17LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 8)) || (((5 <= x && (-13LL + (long long )x) + (long long )y >= 0LL) && (3LL + (long long )x) - (long long )y >= 0LL) && y == 8)) || (((16385 <= x && (-32769LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 16384)) || (((16385 <= x && (-32769LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 16384)) || (((8193 <= x && (-24577LL + (long long )x) + (long long )y >= 0LL) && (8191LL + (long long )x) - (long long )y >= 0LL) && y == 16384)) || (((5 <= x && (-9LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 4)) || (((5 <= x && (-9LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 4)) || ((((((33554432 <= y && 33554433 <= x) && y <= 2147483646) && (-67108865LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y % 33554432 == 0) && y != 0)) || (((3 <= x && (-7LL + (long long )x) + (long long )y >= 0LL) && (1LL + (long long )x) - (long long )y >= 0LL) && y == 4)) || (((((33554432 <= y && 33554433 <= x) && y <= 2147483646) && (-67108865LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y % 33554432 == 0)) || (((((16777217 <= x && 33554432 <= y) && y <= 2147483646) && (-50331649LL + (long long )x) + (long long )y >= 0LL) && (1073741822LL + (long long )x) - (long long )y >= 0LL) && y % 33554432 == 0)) || (((8193 <= x && (-16385LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 8192)) || (((8193 <= x && (-16385LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 8192)) || (((4097 <= x && (-12289LL + (long long )x) + (long long )y >= 0LL) && (4095LL + (long long )x) - (long long )y >= 0LL) && y == 8192)) || (((3 <= x && (-5LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 2)) || (((3 <= x && (-5LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 2)) || (((2 <= x && (-4LL + (long long )x) + (long long )y >= 0LL) && (long long )x - (long long )y >= 0LL) && y == 2)) || (((16777217 <= x && (-33554433LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 16777216)) || (((16777217 <= x && (-33554433LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 16777216)) || (((8388609 <= x && (-25165825LL + (long long )x) + (long long )y >= 0LL) && (8388607LL + (long long )x) - (long long )y >= 0LL) && y == 16777216)) || (((4097 <= x && (-8193LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 4096)) || (((4097 <= x && (-8193LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 4096)) || (((2049 <= x && (-6145LL + (long long )x) + (long long )y >= 0LL) && (2047LL + (long long )x) - (long long )y >= 0LL) && y == 4096)) || ((((2 <= x && (-3LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && 1 == y) && y == 1)) || ((((2 <= x && (-3LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && 1 == y) && y == 1))) || ((((0 <= x && (-1LL + (long long )x) + (long long )y >= 0LL) && (1LL + (long long )x) - (long long )y >= 0LL) && 1 == y) && y == 1)) || ((((8388609 <= x && (-16777217LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 8388608) && x != 0)) || ((((8388609 <= x && (-16777217LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 8388608) && x != 0)) || ((((4194305 <= x && (-12582913LL + (long long )x) + (long long )y >= 0LL) && (4194303LL + (long long )x) - (long long )y >= 0LL) && y == 8388608) && x != 0)) || ((((2049 <= x && (-4097LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 2048) && x != 0)) || ((((2049 <= x && (-4097LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 2048) && x != 0)) || ((((1025 <= x && (-3073LL + (long long )x) + (long long )y >= 0LL) && (1023LL + (long long )x) - (long long )y >= 0LL) && y == 2048) && x != 0)) || ((((4194305 <= x && (-8388609LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 4194304) && x != 0)) || ((((4194305 <= x && (-8388609LL + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )x) - (long long )y >= 0LL) && y == 4194304) && x != 0)) || ((((2097153 <= x && (-6291457LL + (long long )x) + (long long )y >= 0LL) && (2097151LL + (long long )x) - (long long )y >= 0LL) && y == 4194304) && x != 0) format: c_expression correctness_witness CPAchecker 2.3 21 2023-12-01T04:04:25+01:00

Available Results for the Program from Witness Store SV-COMP '23

Trying to find witnesses for program (f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4, sv-benchmarks/c/termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c).

Found 28 witnesses for program sv-benchmarks/c/termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c, f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7521b52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T08:56:50Z
Download de4e965 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T22:09:15+01:00
Download 52152f8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T10:59 CET (comp)
Download 832fffa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 7 2022-12-14T09:28:41Z
Download 4cecc16 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T11:38:08Z
Download 522b11d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 7 2022-12-14T23:21:47Z
Download 191368d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp23-0-g4f5dcf38f) 66 2022-12-10T07:14:19Z
Download 0755212 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-29T11:32:11+01:00 Download 52152f8
Download 8c5c410 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-29T10:51:24+01:00 Download 832fffa
Download 896eaca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-29T07:16:52+01:00 Download 664d53b
Download c836d0c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-29T06:30:43+01:00 Download 522b11d
Download 653ba51 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-29T03:46:41+01:00 Download 4cecc16
Download 2e495cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-29T03:10:58+01:00 Download 02341b1
Download df096af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-29T00:13:59+01:00 Download be518a0
Download 616ddb2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-28T22:52:22+01:00 Download de4e965
Download 628c970 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-28T22:27:40+01:00 Download 191368d
Download 3744051 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-28T18:43:16+01:00 Download 951b5bc
Download a5e6b89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-28T17:46:07+01:00 Download 7521b52
Download f3dcc61 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-28T12:24:03+01:00 Download fd36108
Download 5e15782 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-28T00:45:31+01:00 Download bf58222
Download 7d4c0cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2023-01-27T23:03:44+01:00 Download 34bff8c
Download fd36108 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 6 2022-12-10T15:41:37+01:00
Download 02341b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 6 2022-12-11T22:59:05+01:00
Download bf58222 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 6 2022-12-25T13:12:36+01:00
Download 951b5bc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 6 2022-12-09T18:10:31+01:00
Download 664d53b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 7 2022-12-13T11:18:37Z
Download 34bff8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 8 2022-12-07T23:50:15+01:00
Download 7464c6b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 8 2022-12-07T22:04:43+01:00

Available Results for the Program from Witness Store SV-COMP '22

Trying to find witnesses for program (f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4, sv-benchmarks/c/termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c).

Found 1 witnesses for program sv-benchmarks/c/termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c, f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 63ed1d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 8 2021-12-06T00:32:55+01:00

Available Results for the Program from Witness Store SV-COMP '21

Trying to find witnesses for program (f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4, sv-benchmarks/c/termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c, f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '20

Trying to find witnesses for program (f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4, sv-benchmarks/c/termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c, f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '19

Trying to find witnesses for program (f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4, sv-benchmarks/c/termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c, f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '18

Trying to find witnesses for program (f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4, sv-benchmarks/c/termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c).

Found 2 witnesses for program sv-benchmarks/c/termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c, f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d066ae5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 6 2017-12-01T18:04 CET (sv-comp)
Download cb5e2ef Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 8 2017-12-01T16:21 CET (sv-comp)

Available Results for the Program from Witness Store SV-COMP '17

Trying to find witnesses for program (f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4, sv-benchmarks/c/termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c, f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f716f85b4674adf32c5382ff55713973e95460ac3d0ffe3bfad3cafce9960ed4.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness