ef7c039 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T06:54:44Z |
|
98b90de |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.3 |
7 |
2023-12-17T21:52:22+01:00 |
357f63f |
0a79bd5 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T18:01:11+01:00 |
|
66b897f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:37 CET (comp) |
|
9b28984 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
15 |
2023-12-02T13:37:28Z |
|
d830a2d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Symbiotic |
3 |
2023-12-17T01:17:00Z |
|
1280674 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Symbiotic |
3 |
2023-11-29T22:35:35Z |
|
5c49928 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Pinaka |
3 |
2023-12-19T19:33:46 |
|
1c29ca2 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Mopsa (v1.0~pre2) |
3 |
2023-11-29T16:00:28Z |
|
a2045da |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
16 |
2023-12-01T01:43:52Z |
|
d3136ad |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
ESBMC 7.4.0 kind |
3 |
2023-12-01T03:18:59Z |
|
c18364a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
675 |
2023-12-20T03:55:45+01:00 |
66b897f |
d217570 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
655 |
2023-12-20T02:46:40+01:00 |
5c49928 |
9ac1fb4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-19T15:27:11+01:00 |
b39d472 |
4702e6b |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
632 |
2023-12-17T06:32:47+01:00 |
d830a2d |
519afc5 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
607 |
2023-12-05T14:35:00+01:00 |
b9affc8 |
9f0c8d9 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
644 |
2023-12-04T16:42:38+01:00 |
0ec3140 |
bdb10b9 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-04T11:49:51+01:00 |
9b28984 |
0843d38 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-03T18:46:44+01:00 |
0a79bd5 |
387f992 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
134 |
2023-12-03T10:02:40+01:00 |
ef7c039 |
0c11791 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
655 |
2023-12-01T23:01:37+01:00 |
b27d484 |
26363cd |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
616 |
2023-12-01T18:08:20+01:00 |
d3136ad |
39cf28b |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
23 |
2023-12-01T03:53:55+01:00 |
a2045da |
5024092 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
566 |
2023-12-01T00:00:37+01:00 |
949a677 |
15ce1e9 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
675 |
2023-11-30T07:15:31+01:00 |
|
7a3a324 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
632 |
2023-11-30T02:58:57+01:00 |
1280674 |
b77fac7 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
594 |
2023-11-29T18:39:53+01:00 |
1c29ca2 |
af4c9f5 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-11-29T07:56:17+01:00 |
c763461 |
b1194cf |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
679 |
2023-12-03T22:05:33+01:00 |
|
575f400 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
348 |
2023-12-19T01:50:58+01:00 |
|
357f63f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CBMC |
71 |
2023-12-17T16:52:46+01:00 |
|
b9affc8 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Bubaak |
3 |
2023-12-05T12:34:39Z |
|
0ec3140 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Bubaak |
3 |
2023-12-04T13:49:23Z |
|
b27d484 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Bubaak |
3 |
2023-12-01T19:38:58Z |
|
c763461 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
15 |
2023-11-28T23:08:50Z |
|
949a677 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
2LS |
11 |
2023-11-30T22:33:20+01:00 |
|
87d493b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 7.4.0 |
3 |
2023-12-01T10:31:20Z |
|
ce25120 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
3 |
2023-11-29T20:58:06Z |
|
4a2b0d8 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Pinaka |
3 |
2023-12-19T19:10:35 |
|
51aea1d |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
3 |
2023-12-01T02:02:57Z |
|
67b18e0 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
CBMC |
71 |
2023-12-17T08:44:06+01:00 |
|
97d8036 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2023-12-05T08:48:33Z |
|
7c93a16 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2023-12-04T13:49:10Z |
|
1850492 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2023-12-01T20:26:06Z |
|
85dfb36 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
2LS |
9 |
2023-11-30T21:58:55+01:00 |
|
aa4af8b |
Inspect |
|
- 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 |
|
361dc2d |
Inspect |
|
- 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 |
|
e61c296 |
Inspect |
|
- 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 |
|