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

View and Validate the Witness

Input Given to this Service about the Witness (URL Query)

Key Value
programName sv-benchmarks/c/termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c
programSHA 4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75
witnessName results-verified/cbmc-path.2018-12-04_2245.logfiles/sv-comp19_prop-termination.java_Sequence_true-termination_true-no-overflow.c.files/witness.graphml
witnessSHA e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855.json

Key Value
creationtime 2018-12-05T13:03 CET (sv-comp)
error-programhash Key 'programhash' not present.
error-specification-exists Key 'specification' not present.
error-xmlparsing File produces XML parsing error.
witness-file witnessFileByHash/e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855.graphml
witness-sha256 e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855
witness-size 0

The following keys are missing in the witness XML file: witness-type, sourcecodelang, producer, specification, programfile, programhash, architecture.

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

Trying to find witnesses for program (4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75, sv-benchmarks/c/termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c).

Found 48 witnesses for program sv-benchmarks/c/termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c, 4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download ef7c039 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T06:54:44Z
Download 98b90de Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.3 7 2023-12-17T21:52:22+01:00 Download 357f63f
Download 0a79bd5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T18:01:11+01:00
Download 66b897f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:37 CET (comp)
Download 9b28984 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 15 2023-12-02T13:37:28Z
Download d830a2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2023-12-17T01:17:00Z
Download 1280674 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2023-11-29T22:35:35Z
Download 5c49928 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2023-12-19T19:33:46
Download 1c29ca2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T16:00:28Z
Download a2045da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 16 2023-12-01T01:43:52Z
Download d3136ad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 7.4.0 kind 3 2023-12-01T03:18:59Z
Download c18364a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 675 2023-12-20T03:55:45+01:00 Download 66b897f
Download d217570 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 655 2023-12-20T02:46:40+01:00 Download 5c49928
Download 9ac1fb4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-19T15:27:11+01:00 Download b39d472
Download 4702e6b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 632 2023-12-17T06:32:47+01:00 Download d830a2d
Download 519afc5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 607 2023-12-05T14:35:00+01:00 Download b9affc8
Download 9f0c8d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 644 2023-12-04T16:42:38+01:00 Download 0ec3140
Download bdb10b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-04T11:49:51+01:00 Download 9b28984
Download 0843d38 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-12-03T18:46:44+01:00 Download 0a79bd5
Download 387f992 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 134 2023-12-03T10:02:40+01:00 Download ef7c039
Download 0c11791 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 655 2023-12-01T23:01:37+01:00 Download b27d484
Download 26363cd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 616 2023-12-01T18:08:20+01:00 Download d3136ad
Download 39cf28b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 23 2023-12-01T03:53:55+01:00 Download a2045da
Download 5024092 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 566 2023-12-01T00:00:37+01:00 Download 949a677
Download 15ce1e9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 675 2023-11-30T07:15:31+01:00
Download 7a3a324 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 632 2023-11-30T02:58:57+01:00 Download 1280674
Download b77fac7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 594 2023-11-29T18:39:53+01:00 Download 1c29ca2
Download af4c9f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 5 2023-11-29T07:56:17+01:00 Download c763461
Download b1194cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 679 2023-12-03T22:05:33+01:00
Download 575f400 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 348 2023-12-19T01:50:58+01:00
Download 357f63f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 71 2023-12-17T16:52:46+01:00
Download b9affc8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-05T12:34:39Z
Download 0ec3140 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-04T13:49:23Z
Download b27d484 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-01T19:38:58Z
Download c763461 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 15 2023-11-28T23:08:50Z
Download 949a677 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 11 2023-11-30T22:33:20+01:00
Download 87d493b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.4.0 3 2023-12-01T10:31:20Z
Download ce25120 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2023-11-29T20:58:06Z
Download 4a2b0d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2023-12-19T19:10:35
Download 51aea1d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 3 2023-12-01T02:02:57Z
Download 67b18e0 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 71 2023-12-17T08:44:06+01:00
Download 97d8036 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-05T08:48:33Z
Download 7c93a16 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-04T13:49:10Z
Download 1850492 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2023-12-01T20:26:06Z
Download 85dfb36 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2023-11-30T21:58:55+01:00
Download aa4af8b Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: b5d6cab3-c9a6-47d6-8c4d-ef86d6802762 creation_time: '2023-12-02T14:37:28+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_27a3aaf3-64e8-4ea2-b7a3-5c2889cf8a85/sv-benchmarks/c/termination-restricted-15/java_Sequence.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_27a3aaf3-64e8-4ea2-b7a3-5c2889cf8a85/sv-benchmarks/c/termination-restricted-15/java_Sequence.c : 4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75 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_27a3aaf3-64e8-4ea2-b7a3-5c2889cf8a85/sv-benchmarks/c/termination-restricted-15/java_Sequence.c file_hash: 4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75 line: 10 column: 0 function: main value: (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((c <= 76) && (76 <= i)) && (0 <= c)) || (((c <= 89) && (89 <= i)) && (0 <= c))) || (((0 <= c) && (99 <= i)) && (c <= 2147483556))) || (((57 <= i) && (0 <= c)) && (c <= 57))) || (((c <= 14) && (0 <= c)) && (14 == i))) || (((c <= 56) && (0 <= c)) && (56 <= i))) || (((c <= 25) && (0 <= c)) && (25 <= i))) || (((i == 12) && (0 <= c)) && (c <= 12))) || (((88 <= i) && (0 <= c)) && (c <= 88))) || (((0 <= c) && (41 <= i)) && (c <= 41))) || (((0 <= c) && (c <= 73)) && (73 <= i))) || (((91 <= i) && (0 <= c)) && (c <= 91))) || (((83 <= i) && (0 <= c)) && (c <= 83))) || (((0 <= c) && (34 <= i)) && (c <= 34))) || (((c <= 43) && (43 <= i)) && (0 <= c))) || (((0 <= c) && (16 == i)) && (c <= 16))) || (((c <= 61) && (0 <= c)) && (61 <= i))) || (((9 == i) && (0 <= c)) && (c <= 9))) || (((c <= 38) && (0 <= c)) && (38 <= i))) || (((c <= 42) && (42 <= i)) && (0 <= c))) || (((90 <= i) && (0 <= c)) && (c <= 90))) || (((47 <= i) && (c <= 47)) && (0 <= c))) || (((c <= 19) && (0 <= c)) && (19 == i))) || (((72 <= i) && (c <= 72)) && (0 <= c))) || (((49 <= i) && (0 <= c)) && (c <= 49))) || (((98 <= i) && (0 <= c)) && (c <= 2147483555))) || (((35 <= i) && (c <= 35)) && (0 <= c))) || (((c <= 45) && (0 <= c)) && (45 <= i))) || (((0 <= c) && (7 == i)) && (c <= 7))) || (((c <= 87) && (87 <= i)) && (0 <= c))) || (((i == 8) && (0 <= c)) && (c <= 8))) || (((0 <= c) && (26 <= i)) && (c <= 26))) || (((44 <= i) && (0 <= c)) && (c <= 44))) || (((c <= 1) && (i == 1)) && (0 <= c))) || (((0 <= c) && (94 <= i)) && (c <= 94))) || (((79 <= i) && (c <= 79)) && (0 <= c))) || (((i == 17) && (0 <= c)) && (c <= 17))) || (((c <= 4) && (i == 4)) && (0 <= c))) || (((c <= 50) && (0 <= c)) && (50 <= i))) || (((52 <= i) && (c <= 52)) && (0 <= c))) || (((58 <= i) && (0 <= c)) && (c <= 58))) || (((0 <= c) && (i == 13)) && (c <= 13))) || (((c <= 66) && (66 <= i)) && (0 <= c))) || (((c <= 24) && (0 <= c)) && (24 <= i))) || (((84 <= i) && (0 <= c)) && (c <= 84))) || (((21 == i) && (c <= 21)) && (0 <= c))) || (((36 <= i) && (c <= 36)) && (0 <= c))) || (((0 <= c) && (78 <= i)) && (c <= 78))) || (((c <= 92) && (92 <= i)) && (0 <= c))) || (((28 <= i) && (c <= 28)) && (0 <= c))) || (((c <= 5) && (5 == i)) && (0 <= c))) || (((c <= 22) && (0 <= c)) && (22 == i))) || (((c <= 62) && (0 <= c)) && (62 <= i))) || (((23 <= i) && (0 <= c)) && (c <= 23))) || (((c <= 63) && (0 <= c)) && (63 <= i))) || (((c <= 51) && (51 <= i)) && (0 <= c))) || (((64 <= i) && (c <= 64)) && (0 <= c))) || (((93 <= i) && (0 <= c)) && (c <= 93))) || (((97 <= i) && (c <= 2147483554)) && (0 <= c))) || (((c <= 65) && (0 <= c)) && (65 <= i))) || (((c <= 10) && (0 <= c)) && (i == 10))) || (((i == 11) && (0 <= c)) && (c <= 11))) || (((59 <= i) && (0 <= c)) && (c <= 59))) || (((c <= 53) && (53 <= i)) && (0 <= c))) || (((c <= 2147483557) && (0 <= c)) && (100 <= i))) || (((2 == i) && (0 <= c)) && (c <= 2))) || (((c <= 69) && (0 <= c)) && (69 <= i))) || (((0 <= c) && (74 <= i)) && (c <= 74))) || (((c <= 2147483552) && (0 <= c)) && (95 <= i))) || (((c <= 68) && (0 <= c)) && (68 <= i))) || (((0 <= c) && (67 <= i)) && (c <= 67))) || (((c <= 54) && (0 <= c)) && (54 <= i))) || (((0 <= c) && (c <= 81)) && (81 <= i))) || (((0 <= c) && (85 <= i)) && (c <= 85))) || (((0 <= c) && (c <= 2147483553)) && (96 <= i))) || (((i == 15) && (c <= 15)) && (0 <= c))) || (((29 <= i) && (0 <= c)) && (c <= 29))) || (((c <= 33) && (0 <= c)) && (33 <= i))) || (((82 <= i) && (0 <= c)) && (c <= 82))) || (((48 <= i) && (c <= 48)) && (0 <= c))) || (((55 <= i) && (c <= 55)) && (0 <= c))) || (((0 <= c) && (c <= 71)) && (71 <= i))) || (((0 <= c) && (c <= 32)) && (32 <= i))) || (((c <= 60) && (60 <= i)) && (0 <= c))) || (((0 <= c) && (c <= 31)) && (31 <= i))) || (((c <= 70) && (0 <= c)) && (70 <= i))) || ((c == 0) && (i == 0))) || (((86 <= i) && (c <= 86)) && (0 <= c))) || (((0 <= c) && (c <= 6)) && (6 == i))) || (((40 <= i) && (0 <= c)) && (c <= 40))) || (((0 <= c) && (c <= 18)) && (i == 18))) || (((c <= 80) && (0 <= c)) && (80 <= i))) || (((0 <= c) && (c <= 77)) && (77 <= i))) || (((30 <= i) && (0 <= c)) && (c <= 30))) || (((3 == i) && (0 <= c)) && (c <= 3))) || (((37 <= i) && (c <= 37)) && (0 <= c))) || (((c <= 39) && (0 <= c)) && (39 <= i))) || (((i == 20) && (0 <= c)) && (c <= 20))) || (((c <= 27) && (27 <= i)) && (0 <= c))) || (((0 <= c) && (c <= 75)) && (75 <= i))) || (((0 <= c) && (46 <= i)) && (c <= 46))) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_27a3aaf3-64e8-4ea2-b7a3-5c2889cf8a85/sv-benchmarks/c/termination-restricted-15/java_Sequence.c file_hash: 4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75 line: 15 column: 0 function: main value: ((((((((((c <= 2147483561) && (17 <= j)) && (0 <= c)) && (100 <= i)) || ((((23 <= j) && (0 <= c)) && (100 <= i)) && (c <= 2147483563))) || ((((0 <= c) && (c <= 2147483559)) && (100 <= i)) && (11 <= j))) || ((((20 <= j) && (0 <= c)) && (100 <= i)) && (c <= 2147483562))) || ((((14 <= j) && (0 <= c)) && (c <= 2147483560)) && (100 <= i))) || ((((c <= 2147483557) && (5 <= j)) && (0 <= c)) && (100 <= i))) || ((((8 <= j) && (0 <= c)) && (c <= 2147483558)) && (100 <= i))) format: c_expression correctness_witness CPAchecker 2.3 517 2023-12-04T12:16:19+01:00
Download 361dc2d Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: b3e21584-4740-443e-89e8-7786ceb029a1 creation_time: '2023-11-29T00:08:51+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_172067b8-e0b2-468f-9b04-3bff09175dce/sv-benchmarks/c/termination-restricted-15/java_Sequence.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_172067b8-e0b2-468f-9b04-3bff09175dce/sv-benchmarks/c/termination-restricted-15/java_Sequence.c : 4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75 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_172067b8-e0b2-468f-9b04-3bff09175dce/sv-benchmarks/c/termination-restricted-15/java_Sequence.c file_hash: 4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75 line: 10 column: 0 function: main value: (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((c <= 76) && (76 <= i)) && (0 <= c)) || (((c <= 89) && (89 <= i)) && (0 <= c))) || (((0 <= c) && (99 <= i)) && (c <= 2147483556))) || (((57 <= i) && (0 <= c)) && (c <= 57))) || (((c <= 14) && (0 <= c)) && (14 == i))) || (((c <= 56) && (0 <= c)) && (56 <= i))) || (((c <= 25) && (0 <= c)) && (25 <= i))) || (((i == 12) && (0 <= c)) && (c <= 12))) || (((88 <= i) && (0 <= c)) && (c <= 88))) || (((0 <= c) && (41 <= i)) && (c <= 41))) || (((0 <= c) && (c <= 73)) && (73 <= i))) || (((91 <= i) && (0 <= c)) && (c <= 91))) || (((83 <= i) && (0 <= c)) && (c <= 83))) || (((0 <= c) && (34 <= i)) && (c <= 34))) || (((c <= 43) && (43 <= i)) && (0 <= c))) || (((0 <= c) && (16 == i)) && (c <= 16))) || (((c <= 61) && (0 <= c)) && (61 <= i))) || (((9 == i) && (0 <= c)) && (c <= 9))) || (((c <= 38) && (0 <= c)) && (38 <= i))) || (((c <= 42) && (42 <= i)) && (0 <= c))) || (((90 <= i) && (0 <= c)) && (c <= 90))) || (((47 <= i) && (c <= 47)) && (0 <= c))) || (((c <= 19) && (0 <= c)) && (19 == i))) || (((72 <= i) && (c <= 72)) && (0 <= c))) || (((49 <= i) && (0 <= c)) && (c <= 49))) || (((98 <= i) && (0 <= c)) && (c <= 2147483555))) || (((35 <= i) && (c <= 35)) && (0 <= c))) || (((c <= 45) && (0 <= c)) && (45 <= i))) || (((0 <= c) && (7 == i)) && (c <= 7))) || (((c <= 87) && (87 <= i)) && (0 <= c))) || (((i == 8) && (0 <= c)) && (c <= 8))) || (((0 <= c) && (26 <= i)) && (c <= 26))) || (((44 <= i) && (0 <= c)) && (c <= 44))) || (((c <= 1) && (i == 1)) && (0 <= c))) || (((0 <= c) && (94 <= i)) && (c <= 94))) || (((79 <= i) && (c <= 79)) && (0 <= c))) || (((i == 17) && (0 <= c)) && (c <= 17))) || (((c <= 4) && (i == 4)) && (0 <= c))) || (((c <= 50) && (0 <= c)) && (50 <= i))) || (((52 <= i) && (c <= 52)) && (0 <= c))) || (((58 <= i) && (0 <= c)) && (c <= 58))) || (((0 <= c) && (i == 13)) && (c <= 13))) || (((c <= 66) && (66 <= i)) && (0 <= c))) || (((c <= 24) && (0 <= c)) && (24 <= i))) || (((84 <= i) && (0 <= c)) && (c <= 84))) || (((21 == i) && (c <= 21)) && (0 <= c))) || (((36 <= i) && (c <= 36)) && (0 <= c))) || (((0 <= c) && (78 <= i)) && (c <= 78))) || (((c <= 92) && (92 <= i)) && (0 <= c))) || (((28 <= i) && (c <= 28)) && (0 <= c))) || (((c <= 5) && (5 == i)) && (0 <= c))) || (((c <= 22) && (0 <= c)) && (22 == i))) || (((c <= 62) && (0 <= c)) && (62 <= i))) || (((23 <= i) && (0 <= c)) && (c <= 23))) || (((c <= 63) && (0 <= c)) && (63 <= i))) || (((c <= 51) && (51 <= i)) && (0 <= c))) || (((64 <= i) && (c <= 64)) && (0 <= c))) || (((93 <= i) && (0 <= c)) && (c <= 93))) || (((97 <= i) && (c <= 2147483554)) && (0 <= c))) || (((c <= 65) && (0 <= c)) && (65 <= i))) || (((c <= 10) && (0 <= c)) && (i == 10))) || (((i == 11) && (0 <= c)) && (c <= 11))) || (((59 <= i) && (0 <= c)) && (c <= 59))) || (((c <= 53) && (53 <= i)) && (0 <= c))) || (((c <= 2147483557) && (0 <= c)) && (100 <= i))) || (((2 == i) && (0 <= c)) && (c <= 2))) || (((c <= 69) && (0 <= c)) && (69 <= i))) || (((0 <= c) && (74 <= i)) && (c <= 74))) || (((c <= 2147483552) && (0 <= c)) && (95 <= i))) || (((c <= 68) && (0 <= c)) && (68 <= i))) || (((0 <= c) && (67 <= i)) && (c <= 67))) || (((c <= 54) && (0 <= c)) && (54 <= i))) || (((0 <= c) && (c <= 81)) && (81 <= i))) || (((0 <= c) && (85 <= i)) && (c <= 85))) || (((0 <= c) && (c <= 2147483553)) && (96 <= i))) || (((i == 15) && (c <= 15)) && (0 <= c))) || (((29 <= i) && (0 <= c)) && (c <= 29))) || (((c <= 33) && (0 <= c)) && (33 <= i))) || (((82 <= i) && (0 <= c)) && (c <= 82))) || (((48 <= i) && (c <= 48)) && (0 <= c))) || (((55 <= i) && (c <= 55)) && (0 <= c))) || (((0 <= c) && (c <= 71)) && (71 <= i))) || (((0 <= c) && (c <= 32)) && (32 <= i))) || (((c <= 60) && (60 <= i)) && (0 <= c))) || (((0 <= c) && (c <= 31)) && (31 <= i))) || (((c <= 70) && (0 <= c)) && (70 <= i))) || ((c == 0) && (i == 0))) || (((86 <= i) && (c <= 86)) && (0 <= c))) || (((0 <= c) && (c <= 6)) && (6 == i))) || (((40 <= i) && (0 <= c)) && (c <= 40))) || (((0 <= c) && (c <= 18)) && (i == 18))) || (((c <= 80) && (0 <= c)) && (80 <= i))) || (((0 <= c) && (c <= 77)) && (77 <= i))) || (((30 <= i) && (0 <= c)) && (c <= 30))) || (((3 == i) && (0 <= c)) && (c <= 3))) || (((37 <= i) && (c <= 37)) && (0 <= c))) || (((c <= 39) && (0 <= c)) && (39 <= i))) || (((i == 20) && (0 <= c)) && (c <= 20))) || (((c <= 27) && (27 <= i)) && (0 <= c))) || (((0 <= c) && (c <= 75)) && (75 <= i))) || (((0 <= c) && (46 <= i)) && (c <= 46))) format: c_expression - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_172067b8-e0b2-468f-9b04-3bff09175dce/sv-benchmarks/c/termination-restricted-15/java_Sequence.c file_hash: 4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75 line: 15 column: 0 function: main value: ((((((((((c <= 2147483561) && (17 <= j)) && (0 <= c)) && (100 <= i)) || ((((23 <= j) && (0 <= c)) && (100 <= i)) && (c <= 2147483563))) || ((((0 <= c) && (c <= 2147483559)) && (100 <= i)) && (11 <= j))) || ((((20 <= j) && (0 <= c)) && (100 <= i)) && (c <= 2147483562))) || ((((14 <= j) && (0 <= c)) && (c <= 2147483560)) && (100 <= i))) || ((((c <= 2147483557) && (5 <= j)) && (0 <= c)) && (100 <= i))) || ((((8 <= j) && (0 <= c)) && (c <= 2147483558)) && (100 <= i))) format: c_expression correctness_witness CPAchecker 2.3 664 2023-11-29T08:00:35+01:00
Download e61c296 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: 54be8fd6-59bf-41fa-bee5-162682d7f625 creation_time: 2023-12-01T01:43:52Z 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/java_Sequence.c''' task: input_files: - ../../sv-benchmarks/c/termination-restricted-15/java_Sequence.c input_file_hashes: ../../sv-benchmarks/c/termination-restricted-15/java_Sequence.c: 4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75 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/java_Sequence.c file_hash: 4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75 line: 15 column: 11 function: main value: i == 100 format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/java_Sequence.c file_hash: 4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75 line: 15 column: 11 function: main value: (((((((((((((((((((-201LL + (long long )c) + (long long )i >= 0LL && (-109LL + (long long )c) + (long long )j >= 0LL) && (-108LL + (long long )i) + (long long )j >= 0LL) && (1LL - (long long )c) + (long long )i >= 0LL) && (92LL - (long long )i) + (long long )j >= 0LL) && (93LL - (long long )c) + (long long )j >= 0LL) && (-93LL + (long long )c) - (long long )j >= 0LL) && (-92LL + (long long )i) - (long long )j >= 0LL) && (-1LL + (long long )c) - (long long )i >= 0LL) && (108LL - (long long )i) - (long long )j >= 0LL) && (109LL - (long long )c) - (long long )j >= 0LL) && (201LL - (long long )c) - (long long )i >= 0LL) && j == 8) && c == 101) || (((((((((((((((12 <= c && c <= 100) && (-200LL + (long long )c) + (long long )i >= 0LL) && (-105LL + (long long )i) + (long long )j >= 0LL) && (-105LL + (long long )c) + (long long )j >= 0LL) && (0LL - (long long )c) + (long long )i >= 0LL) && (95LL - (long long )i) + (long long )j >= 0LL) && (95LL - (long long )c) + (long long )j >= 0LL) && (-95LL + (long long )i) - (long long )j >= 0LL) && (-95LL + (long long )c) - (long long )j >= 0LL) && (105LL - (long long )i) - (long long )j >= 0LL) && (105LL - (long long )c) - (long long )j >= 0LL) && (200LL - (long long )c) - (long long )i >= 0LL) && (long long )c - (long long )i >= 0LL) && 5 == j) && j == 5)) || ((((((((((((((-206LL + (long long )c) + (long long )i >= 0LL && (-129LL + (long long )c) + (long long )j >= 0LL) && (-123LL + (long long )i) + (long long )j >= 0LL) && (6LL - (long long )c) + (long long )i >= 0LL) && (77LL - (long long )i) + (long long )j >= 0LL) && (83LL - (long long )c) + (long long )j >= 0LL) && (-83LL + (long long )c) - (long long )j >= 0LL) && (-77LL + (long long )i) - (long long )j >= 0LL) && (-6LL + (long long )c) - (long long )i >= 0LL) && (123LL - (long long )i) - (long long )j >= 0LL) && (129LL - (long long )c) - (long long )j >= 0LL) && (206LL - (long long )c) - (long long )i >= 0LL) && j == 23) && c == 106)) || ((((((((((((((-205LL + (long long )c) + (long long )i >= 0LL && (-125LL + (long long )c) + (long long )j >= 0LL) && (-120LL + (long long )i) + (long long )j >= 0LL) && (5LL - (long long )c) + (long long )i >= 0LL) && (80LL - (long long )i) + (long long )j >= 0LL) && (85LL - (long long )c) + (long long )j >= 0LL) && (-85LL + (long long )c) - (long long )j >= 0LL) && (-80LL + (long long )i) - (long long )j >= 0LL) && (-5LL + (long long )c) - (long long )i >= 0LL) && (120LL - (long long )i) - (long long )j >= 0LL) && (125LL - (long long )c) - (long long )j >= 0LL) && (205LL - (long long )c) - (long long )i >= 0LL) && j == 20) && c == 105)) || ((((((((((((((-204LL + (long long )c) + (long long )i >= 0LL && (-121LL + (long long )c) + (long long )j >= 0LL) && (-117LL + (long long )i) + (long long )j >= 0LL) && (4LL - (long long )c) + (long long )i >= 0LL) && (83LL - (long long )i) + (long long )j >= 0LL) && (87LL - (long long )c) + (long long )j >= 0LL) && (-87LL + (long long )c) - (long long )j >= 0LL) && (-83LL + (long long )i) - (long long )j >= 0LL) && (-4LL + (long long )c) - (long long )i >= 0LL) && (117LL - (long long )i) - (long long )j >= 0LL) && (121LL - (long long )c) - (long long )j >= 0LL) && (204LL - (long long )c) - (long long )i >= 0LL) && j == 17) && c == 104)) || ((((((((((((((-203LL + (long long )c) + (long long )i >= 0LL && (-117LL + (long long )c) + (long long )j >= 0LL) && (-114LL + (long long )i) + (long long )j >= 0LL) && (3LL - (long long )c) + (long long )i >= 0LL) && (86LL - (long long )i) + (long long )j >= 0LL) && (89LL - (long long )c) + (long long )j >= 0LL) && (-89LL + (long long )c) - (long long )j >= 0LL) && (-86LL + (long long )i) - (long long )j >= 0LL) && (-3LL + (long long )c) - (long long )i >= 0LL) && (114LL - (long long )i) - (long long )j >= 0LL) && (117LL - (long long )c) - (long long )j >= 0LL) && (203LL - (long long )c) - (long long )i >= 0LL) && j == 14) && c == 103)) || ((((((((((((((-202LL + (long long )c) + (long long )i >= 0LL && (-113LL + (long long )c) + (long long )j >= 0LL) && (-111LL + (long long )i) + (long long )j >= 0LL) && (2LL - (long long )c) + (long long )i >= 0LL) && (89LL - (long long )i) + (long long )j >= 0LL) && (91LL - (long long )c) + (long long )j >= 0LL) && (-91LL + (long long )c) - (long long )j >= 0LL) && (-89LL + (long long )i) - (long long )j >= 0LL) && (-2LL + (long long )c) - (long long )i >= 0LL) && (111LL - (long long )i) - (long long )j >= 0LL) && (113LL - (long long )c) - (long long )j >= 0LL) && (202LL - (long long )c) - (long long )i >= 0LL) && j == 11) && c == 102) format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/java_Sequence.c file_hash: 4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75 line: 10 column: 11 function: main value: (0LL - (long long )c) + (long long )i >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/java_Sequence.c file_hash: 4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75 line: 10 column: 11 function: main value: (long long )c - (long long )i >= 0LL format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-restricted-15/java_Sequence.c file_hash: 4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75 line: 10 column: 11 function: main value: ((((((((((((((((((((((((12 <= i && 12 <= c) && i <= 100) && c <= 100) && (-24LL + (long long )c) + (long long )i >= 0LL) && (2147483636LL + (long long )i) + (long long )j >= 0LL) && (2147483636LL + (long long )c) + (long long )j >= 0LL) && (2147483748LL - (long long )i) + (long long )j >= 0LL) && (2147483748LL - (long long )c) + (long long )j >= 0LL) && (2147483635LL + (long long )i) - (long long )j >= 0LL) && (2147483635LL + (long long )c) - (long long )j >= 0LL) && (200LL - (long long )c) - (long long )i >= 0LL) && (2147483747LL - (long long )i) - (long long )j >= 0LL) && (2147483747LL - (long long )c) - (long long )j >= 0LL) || ((((((((((((-22LL + (long long )c) + (long long )i >= 0LL && (2147483637LL + (long long )i) + (long long )j >= 0LL) && (2147483637LL + (long long )c) + (long long )j >= 0LL) && (2147483659LL - (long long )i) + (long long )j >= 0LL) && (2147483659LL - (long long )c) + (long long )j >= 0LL) && (2147483636LL + (long long )i) - (long long )j >= 0LL) && (2147483636LL + (long long )c) - (long long )j >= 0LL) && (22LL - (long long )c) - (long long )i >= 0LL) && (2147483658LL - (long long )i) - (long long )j >= 0LL) && (2147483658LL - (long long )c) - (long long )j >= 0LL) && i == 11) && c == 11)) || ((((((((((((-20LL + (long long )c) + (long long )i >= 0LL && (2147483638LL + (long long )i) + (long long )j >= 0LL) && (2147483638LL + (long long )c) + (long long )j >= 0LL) && (2147483658LL - (long long )i) + (long long )j >= 0LL) && (2147483658LL - (long long )c) + (long long )j >= 0LL) && (2147483637LL + (long long )i) - (long long )j >= 0LL) && (2147483637LL + (long long )c) - (long long )j >= 0LL) && (20LL - (long long )c) - (long long )i >= 0LL) && (2147483657LL - (long long )i) - (long long )j >= 0LL) && (2147483657LL - (long long )c) - (long long )j >= 0LL) && i == 10) && c == 10)) || ((((((((((((-18LL + (long long )c) + (long long )i >= 0LL && (2147483639LL + (long long )i) + (long long )j >= 0LL) && (2147483639LL + (long long )c) + (long long )j >= 0LL) && (2147483657LL - (long long )i) + (long long )j >= 0LL) && (2147483657LL - (long long )c) + (long long )j >= 0LL) && (2147483638LL + (long long )i) - (long long )j >= 0LL) && (2147483638LL + (long long )c) - (long long )j >= 0LL) && (18LL - (long long )c) - (long long )i >= 0LL) && (2147483656LL - (long long )i) - (long long )j >= 0LL) && (2147483656LL - (long long )c) - (long long )j >= 0LL) && i == 9) && c == 9)) || ((((((((((((-16LL + (long long )c) + (long long )i >= 0LL && (2147483640LL + (long long )i) + (long long )j >= 0LL) && (2147483640LL + (long long )c) + (long long )j >= 0LL) && (2147483656LL - (long long )i) + (long long )j >= 0LL) && (2147483656LL - (long long )c) + (long long )j >= 0LL) && (2147483639LL + (long long )i) - (long long )j >= 0LL) && (2147483639LL + (long long )c) - (long long )j >= 0LL) && (16LL - (long long )c) - (long long )i >= 0LL) && (2147483655LL - (long long )i) - (long long )j >= 0LL) && (2147483655LL - (long long )c) - (long long )j >= 0LL) && i == 8) && c == 8)) || ((((((((((((-14LL + (long long )c) + (long long )i >= 0LL && (2147483641LL + (long long )i) + (long long )j >= 0LL) && (2147483641LL + (long long )c) + (long long )j >= 0LL) && (2147483655LL - (long long )i) + (long long )j >= 0LL) && (2147483655LL - (long long )c) + (long long )j >= 0LL) && (2147483640LL + (long long )i) - (long long )j >= 0LL) && (2147483640LL + (long long )c) - (long long )j >= 0LL) && (14LL - (long long )c) - (long long )i >= 0LL) && (2147483654LL - (long long )i) - (long long )j >= 0LL) && (2147483654LL - (long long )c) - (long long )j >= 0LL) && i == 7) && c == 7)) || ((((((((((((-12LL + (long long )c) + (long long )i >= 0LL && (2147483642LL + (long long )i) + (long long )j >= 0LL) && (2147483642LL + (long long )c) + (long long )j >= 0LL) && (2147483654LL - (long long )i) + (long long )j >= 0LL) && (2147483654LL - (long long )c) + (long long )j >= 0LL) && (2147483641LL + (long long )i) - (long long )j >= 0LL) && (2147483641LL + (long long )c) - (long long )j >= 0LL) && (12LL - (long long )c) - (long long )i >= 0LL) && (2147483653LL - (long long )i) - (long long )j >= 0LL) && (2147483653LL - (long long )c) - (long long )j >= 0LL) && i == 6) && c == 6)) || ((((((((((((-10LL + (long long )c) + (long long )i >= 0LL && (2147483643LL + (long long )i) + (long long )j >= 0LL) && (2147483643LL + (long long )c) + (long long )j >= 0LL) && (2147483653LL - (long long )i) + (long long )j >= 0LL) && (2147483653LL - (long long )c) + (long long )j >= 0LL) && (2147483642LL + (long long )i) - (long long )j >= 0LL) && (2147483642LL + (long long )c) - (long long )j >= 0LL) && (10LL - (long long )c) - (long long )i >= 0LL) && (2147483652LL - (long long )i) - (long long )j >= 0LL) && (2147483652LL - (long long )c) - (long long )j >= 0LL) && i == 5) && c == 5)) || ((((((((((((-8LL + (long long )c) + (long long )i >= 0LL && (2147483644LL + (long long )i) + (long long )j >= 0LL) && (2147483644LL + (long long )c) + (long long )j >= 0LL) && (2147483652LL - (long long )i) + (long long )j >= 0LL) && (2147483652LL - (long long )c) + (long long )j >= 0LL) && (2147483643LL + (long long )i) - (long long )j >= 0LL) && (2147483643LL + (long long )c) - (long long )j >= 0LL) && (8LL - (long long )c) - (long long )i >= 0LL) && (2147483651LL - (long long )i) - (long long )j >= 0LL) && (2147483651LL - (long long )c) - (long long )j >= 0LL) && i == 4) && c == 4)) || ((((((((((((-6LL + (long long )c) + (long long )i >= 0LL && (2147483645LL + (long long )i) + (long long )j >= 0LL) && (2147483645LL + (long long )c) + (long long )j >= 0LL) && (2147483651LL - (long long )i) + (long long )j >= 0LL) && (2147483651LL - (long long )c) + (long long )j >= 0LL) && (2147483644LL + (long long )i) - (long long )j >= 0LL) && (2147483644LL + (long long )c) - (long long )j >= 0LL) && (6LL - (long long )c) - (long long )i >= 0LL) && (2147483650LL - (long long )i) - (long long )j >= 0LL) && (2147483650LL - (long long )c) - (long long )j >= 0LL) && i == 3) && c == 3)) || ((((((((((((-4LL + (long long )c) + (long long )i >= 0LL && (2147483646LL + (long long )i) + (long long )j >= 0LL) && (2147483646LL + (long long )c) + (long long )j >= 0LL) && (2147483650LL - (long long )i) + (long long )j >= 0LL) && (2147483650LL - (long long )c) + (long long )j >= 0LL) && (2147483645LL + (long long )i) - (long long )j >= 0LL) && (2147483645LL + (long long )c) - (long long )j >= 0LL) && (4LL - (long long )c) - (long long )i >= 0LL) && (2147483649LL - (long long )i) - (long long )j >= 0LL) && (2147483649LL - (long long )c) - (long long )j >= 0LL) && i == 2) && c == 2)) || ((((((((((((-2LL + (long long )c) + (long long )i >= 0LL && (2147483647LL + (long long )i) + (long long )j >= 0LL) && (2147483647LL + (long long )c) + (long long )j >= 0LL) && (2147483649LL - (long long )i) + (long long )j >= 0LL) && (2147483649LL - (long long )c) + (long long )j >= 0LL) && (2147483646LL + (long long )i) - (long long )j >= 0LL) && (2147483646LL + (long long )c) - (long long )j >= 0LL) && (2LL - (long long )c) - (long long )i >= 0LL) && (2147483648LL - (long long )i) - (long long )j >= 0LL) && (2147483648LL - (long long )c) - (long long )j >= 0LL) && i == 1) && c == 1)) || (((((((((((((((2147483648LL + (long long )i) + (long long )j >= 0LL && (2147483648LL + (long long )c) + (long long )j >= 0LL) && (2147483648LL - (long long )i) + (long long )j >= 0LL) && (2147483648LL - (long long )c) + (long long )j >= 0LL) && (long long )c + (long long )i >= 0LL) && (2147483647LL + (long long )i) - (long long )j >= 0LL) && (2147483647LL + (long long )c) - (long long )j >= 0LL) && (0LL - (long long )c) - (long long )i >= 0LL) && (2147483647LL - (long long )i) - (long long )j >= 0LL) && (2147483647LL - (long long )c) - (long long )j >= 0LL) && 0 == i) && 0 == c) && i == 0) && i == c) && c == 0) format: c_expression correctness_witness CPAchecker 2.3 626 2023-12-01T04:33:25+01:00

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

Trying to find witnesses for program (4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75, sv-benchmarks/c/termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c).

Found 40 witnesses for program sv-benchmarks/c/termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c, 4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8ba1ba1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T12:08:39Z
Download e0ce8ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 4 2023-01-29T07:26:34+01:00 Download 37cdb26
Download bf748d1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 2 2023-01-28T22:42:42+01:00 Download df5040a
Download e10a69e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness CPAchecker 2.2 7 2023-01-28T03:55:33+01:00 Download dcc91c2
Download 3926052 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T22:11:44+01:00
Download 66b897f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T11:01 CET (comp)
Download ee0c81b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 15 2022-12-14T04:16:54Z
Download 1512c0b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2022-12-25T08:14:54Z
Download 327a59a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2022-12-12T12:50:24Z
Download 717d4f9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Pinaka 3 2022-12-11T15:25:14
Download 935f63e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T09:03:26Z
Download df5040a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp23-0-g4f5dcf38f) 50 2022-12-10T09:31:40Z
Download 89b6c6f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 7.0.0 kind 3 2022-12-18T16:14:34Z
Download f02bb7e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 6.8.0 kind 3 2022-12-25T08:14:54Z
Download 63d973d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 674 2023-01-29T11:46:53+01:00 Download 66b897f
Download 9159642 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T10:56:38+01:00 Download ee0c81b
Download a0674dc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 658 2023-01-29T05:34:11+01:00 Download 327a59a
Download 7da72d0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T05:04:32+01:00 Download 717d4f9
Download 90f18ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 629 2023-01-29T04:02:30+01:00 Download 935f63e
Download 3665efa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 5 2023-01-29T00:20:54+01:00 Download 9573797
Download 300c645 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 45 2023-01-28T23:05:22+01:00 Download 3926052
Download 0afc917 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 130 2023-01-28T17:45:24+01:00 Download 8ba1ba1
Download 69a5828 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 632 2023-01-28T15:10:40+01:00 Download 89b6c6f
Download 02f1376 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 632 2023-01-28T01:00:35+01:00 Download f02bb7e
Download e384b00 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 658 2023-01-27T23:58:56+01:00 Download 001924b
Download 35e1dcd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 607 2023-01-27T23:22:56+01:00 Download 239914c
Download 158f59f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 679 2022-12-10T21:56:37+01:00
Download 9dea4f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 679 2022-12-11T20:54:16+01:00
Download 286977f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 679 2022-12-10T01:32:19+01:00
Download dcc91c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 71 2022-12-08T11:43:53+01:00
Download 001924b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2022-12-08T18:47:21Z
Download 37cdb26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 15 2022-12-13T19:50:12Z
Download 239914c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 11 2022-12-08T01:34:54+01:00
Download ddba6b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2022-12-25T09:45:26Z
Download 5af7c3f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 7.0.0 3 2022-12-18T23:53:52Z
Download d3eccb7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2022-12-12T17:54:42Z
Download c75a68d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2022-12-11T15:46:06
Download 4cc98f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 71 2022-12-08T12:18:44+01:00
Download be4fcb8 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Bubaak 3 2022-12-08T16:38:18Z
Download f7ffe06 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2022-12-07T23:26:10+01:00

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

Trying to find witnesses for program (4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75, sv-benchmarks/c/termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c).

Found 5 witnesses for program sv-benchmarks/c/termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c, 4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 45922d9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(reach_error())) ) correctness_witness ESBMC 6.8.0 3 2021-12-08T11:43:01Z
Download e5f1cc4 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 3 2021-12-07T14:12:56Z
Download f754c65 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2021-12-09T05:25:14
Download 3edb248 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 71 2021-12-06T10:18:56+01:00
Download 9dd58e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2021-12-05T23:16:16+01:00

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

Trying to find witnesses for program (4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75, sv-benchmarks/c/termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c).

Found 3 witnesses for program sv-benchmarks/c/termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c, 4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download beaa84e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-11T18:51:43
Download a796aa4 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 2 2020-12-09T01:04:37
Download 448912c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2020-12-08T08:08:52

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

Trying to find witnesses for program (4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75, sv-benchmarks/c/termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c).

Found 1 witnesses for program sv-benchmarks/c/termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c, 4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 9f8f36f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2019-12-04T00:16 CET (comp)

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

Trying to find witnesses for program (4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75, sv-benchmarks/c/termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c).

Found 2 witnesses for program sv-benchmarks/c/termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c, 4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 28b5264 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-08T19:28 CET (sv-comp)
Download 881fc0e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Pinaka 3 2018-12-07T01:12 CET (sv-comp)

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

Trying to find witnesses for program (4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75, sv-benchmarks/c/termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c).

Found 5 witnesses for program sv-benchmarks/c/termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c, 4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b431e91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-03T01:34:27.456550
Download 1dbc42e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T08:46:03.501672
Download 5fc42c1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 6 2017-12-01T17:23 CET (sv-comp)
Download 9e053a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 78 2017-12-01T13:56 CET (sv-comp)
Download 5ef4ce9 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 9 2017-12-01T15:43 CET (sv-comp)

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

Trying to find witnesses for program (4c7fd2dfb73ccf40686976b843bd7f2e1f45b17323a2ffa706fb90cccb1bab75, sv-benchmarks/c/termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c).

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

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