2f8f5be |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T07:14:37Z |
|
800e749 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T17:51:55+01:00 |
|
5a85b36 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:36 CET (comp) |
|
a9d5a99 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
6 |
2023-12-02T16:23:03Z |
|
85b8d89 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Symbiotic |
3 |
2023-12-17T01:03:40Z |
|
c3398ae |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Symbiotic |
3 |
2023-11-29T23:46:25Z |
|
3b13bba |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Pinaka |
3 |
2023-12-19T19:57:34 |
|
3eb862e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Mopsa (v1.0~pre2) |
3 |
2023-11-29T09:04:16Z |
|
678d810 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Kojak |
6 |
2023-12-03T02:24:09Z |
|
270cd1f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
17 |
2023-12-01T02:09:55Z |
|
8f85f68 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
ESBMC 7.4.0 kind |
3 |
2023-12-01T10:43:12Z |
|
ee4ce66 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-20T03:41:10+01:00 |
5a85b36 |
80cd592 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-20T02:29:18+01:00 |
3b13bba |
2fe51c8 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-19T14:28:32+01:00 |
68c3ffb |
422e6bd |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-19T05:12:21+01:00 |
884c98f |
4d937ab |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-17T21:42:38+01:00 |
0308247 |
1fc346d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-17T06:25:45+01:00 |
85b8d89 |
662a4db |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-05T14:20:31+01:00 |
9b316e1 |
2ee17f2 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-04T16:28:21+01:00 |
cc65c65 |
d8a0d89 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-04T11:29:24+01:00 |
a9d5a99 |
8c97070 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-04T01:18:18+01:00 |
c19ce3a |
2fd7763 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-03T18:30:51+01:00 |
800e749 |
52a57d0 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-03T09:58:36+01:00 |
2f8f5be |
c5232a3 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
22 |
2023-12-03T05:58:32+01:00 |
678d810 |
f1034a0 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-01T22:44:42+01:00 |
6505926 |
164cd6f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-01T18:11:05+01:00 |
8f85f68 |
2ea3f9d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-01T03:43:02+01:00 |
270cd1f |
0da1895 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-01T00:09:04+01:00 |
4e61256 |
566f5e6 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-11-30T12:19:08+01:00 |
cbb8c01 |
cbb8c01 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-11-30T05:49:10+01:00 |
|
b5b0c82 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-11-30T02:38:43+01:00 |
c3398ae |
415aeed |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-11-29T18:11:41+01:00 |
3eb862e |
f43bda9 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-11-29T08:13:13+01:00 |
543e4ed |
c19ce3a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
5 |
2023-12-03T22:21:17+01:00 |
|
884c98f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
5 |
2023-12-18T17:03:49+01:00 |
|
0308247 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CBMC |
7 |
2023-12-17T13:53:46+01:00 |
|
9b316e1 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Bubaak |
3 |
2023-12-05T07:42:58Z |
|
cc65c65 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Bubaak |
3 |
2023-12-04T05:28:26Z |
|
6505926 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Bubaak |
3 |
2023-12-01T19:58:20Z |
|
543e4ed |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
6 |
2023-11-29T00:17:57Z |
|
4e61256 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
2LS |
8 |
2023-11-30T20:41:58+01:00 |
|
a3ae02c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 7.4.0 |
3 |
2023-12-01T14:31:22Z |
|
ee4a8d4 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
3 |
2023-11-29T19:47:50Z |
|
83c18a0 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Pinaka |
3 |
2023-12-19T22:29:36 |
|
6159553 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
3 |
2023-12-01T02:09:11Z |
|
ac0650b |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
CBMC |
7 |
2023-12-17T19:21:17+01:00 |
|
68986a2 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2023-12-05T07:57:45Z |
|
e393130 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2023-12-04T13:52:46Z |
|
8e1d3bc |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2023-12-01T20:12:14Z |
|
af7931c |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
2LS |
7 |
2023-11-30T22:36:32+01:00 |
|
776e8c1 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: d4120cc3-c518-4bde-9bb1-c047c384cefe
creation_time: '2023-11-29T01:17:57+01:00'
producer:
name: Automizer
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_cd5d596e-2004-4e7a-bc22-b9b5507fe951/sv-benchmarks/c/termination-restricted-15/Sequence.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_cd5d596e-2004-4e7a-bc22-b9b5507fe951/sv-benchmarks/c/termination-restricted-15/Sequence.c
: 95ccbbbc448c04acb65590867534531dd0d1de0ae6cfb9bc69f5ca4c10abccd4
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_cd5d596e-2004-4e7a-bc22-b9b5507fe951/sv-benchmarks/c/termination-restricted-15/Sequence.c
file_hash: 95ccbbbc448c04acb65590867534531dd0d1de0ae6cfb9bc69f5ca4c10abccd4
line: 11
column: 0
function: main
value: ((0 <= i) && (5 == j))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_cd5d596e-2004-4e7a-bc22-b9b5507fe951/sv-benchmarks/c/termination-restricted-15/Sequence.c
file_hash: 95ccbbbc448c04acb65590867534531dd0d1de0ae6cfb9bc69f5ca4c10abccd4
line: 13
column: 0
function: main
value: ((5 <= j) && (0 <= i))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-11-29T07:49:01+01:00 |
|
86a47a5 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: b0a65faa-4b56-47b2-ad38-83a2c00377a7
creation_time: '2023-12-02T17:23:03+01:00'
producer:
name: Taipan
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e6ad819f-ef7f-4d1a-a897-dc208ab691de/sv-benchmarks/c/termination-restricted-15/Sequence.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e6ad819f-ef7f-4d1a-a897-dc208ab691de/sv-benchmarks/c/termination-restricted-15/Sequence.c
: 95ccbbbc448c04acb65590867534531dd0d1de0ae6cfb9bc69f5ca4c10abccd4
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_e6ad819f-ef7f-4d1a-a897-dc208ab691de/sv-benchmarks/c/termination-restricted-15/Sequence.c
file_hash: 95ccbbbc448c04acb65590867534531dd0d1de0ae6cfb9bc69f5ca4c10abccd4
line: 11
column: 0
function: main
value: ((0 <= i) && (5 == j))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e6ad819f-ef7f-4d1a-a897-dc208ab691de/sv-benchmarks/c/termination-restricted-15/Sequence.c
file_hash: 95ccbbbc448c04acb65590867534531dd0d1de0ae6cfb9bc69f5ca4c10abccd4
line: 13
column: 0
function: main
value: ((5 <= j) && (0 <= i))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-04T11:54:52+01:00 |
|
5a73961 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: ab38f47e-a611-4839-aded-b04ee37cca28
creation_time: '2023-12-03T03:24:09+01:00'
producer:
name: Kojak
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_37a4dd27-93a8-4a9e-89e1-3df218955546/sv-benchmarks/c/termination-restricted-15/Sequence.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_37a4dd27-93a8-4a9e-89e1-3df218955546/sv-benchmarks/c/termination-restricted-15/Sequence.c
: 95ccbbbc448c04acb65590867534531dd0d1de0ae6cfb9bc69f5ca4c10abccd4
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_37a4dd27-93a8-4a9e-89e1-3df218955546/sv-benchmarks/c/termination-restricted-15/Sequence.c
file_hash: 95ccbbbc448c04acb65590867534531dd0d1de0ae6cfb9bc69f5ca4c10abccd4
line: 11
column: 0
function: main
value: (((j <= 5) && (5 <= j)) && (0 <= i))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_37a4dd27-93a8-4a9e-89e1-3df218955546/sv-benchmarks/c/termination-restricted-15/Sequence.c
file_hash: 95ccbbbc448c04acb65590867534531dd0d1de0ae6cfb9bc69f5ca4c10abccd4
line: 13
column: 0
function: main
value: (5 <= j)
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-03T05:42:56+01:00 |
|
8d55c16 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: 8a11ea77-8367-448a-b6a4-54f64d0a2c77
creation_time: 2023-12-01T02:09:55Z
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/Sequence.c'''
task:
input_files:
- ../../sv-benchmarks/c/termination-restricted-15/Sequence.c
input_file_hashes:
../../sv-benchmarks/c/termination-restricted-15/Sequence.c: 95ccbbbc448c04acb65590867534531dd0d1de0ae6cfb9bc69f5ca4c10abccd4
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/Sequence.c
file_hash: 95ccbbbc448c04acb65590867534531dd0d1de0ae6cfb9bc69f5ca4c10abccd4
line: 11
column: 11
function: main
value: 5 == j
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/Sequence.c
file_hash: 95ccbbbc448c04acb65590867534531dd0d1de0ae6cfb9bc69f5ca4c10abccd4
line: 11
column: 11
function: main
value: j == 5
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/Sequence.c
file_hash: 95ccbbbc448c04acb65590867534531dd0d1de0ae6cfb9bc69f5ca4c10abccd4
line: 11
column: 11
function: main
value: (((((((((((((((((((((((((((((-22LL + (long long )i) + (long long )j >=
0LL && (12LL - (long long )i) + (long long )j >= 0LL) && (-12LL + (long long
)i) - (long long )j >= 0LL) && (22LL - (long long )i) - (long long )j >= 0LL)
&& i == 17) || (((((-21LL + (long long )i) + (long long )j >= 0LL && (11LL
- (long long )i) + (long long )j >= 0LL) && (-11LL + (long long )i) - (long
long )j >= 0LL) && (21LL - (long long )i) - (long long )j >= 0LL) && i ==
16)) || (((((-20LL + (long long )i) + (long long )j >= 0LL && (10LL - (long
long )i) + (long long )j >= 0LL) && (-10LL + (long long )i) - (long long )j
>= 0LL) && (20LL - (long long )i) - (long long )j >= 0LL) && i == 15)) ||
(((((-19LL + (long long )i) + (long long )j >= 0LL && (9LL - (long long )i)
+ (long long )j >= 0LL) && (-9LL + (long long )i) - (long long )j >= 0LL)
&& (19LL - (long long )i) - (long long )j >= 0LL) && i == 14)) || (((((-18LL
+ (long long )i) + (long long )j >= 0LL && (8LL - (long long )i) + (long long
)j >= 0LL) && (-8LL + (long long )i) - (long long )j >= 0LL) && (18LL - (long
long )i) - (long long )j >= 0LL) && i == 13)) || (((((-17LL + (long long )i)
+ (long long )j >= 0LL && (7LL - (long long )i) + (long long )j >= 0LL) &&
(-7LL + (long long )i) - (long long )j >= 0LL) && (17LL - (long long )i) -
(long long )j >= 0LL) && i == 12)) || (((((-16LL + (long long )i) + (long
long )j >= 0LL && (6LL - (long long )i) + (long long )j >= 0LL) && (-6LL +
(long long )i) - (long long )j >= 0LL) && (16LL - (long long )i) - (long long
)j >= 0LL) && i == 11)) || (((((-15LL + (long long )i) + (long long )j >=
0LL && (5LL - (long long )i) + (long long )j >= 0LL) && (-5LL + (long long
)i) - (long long )j >= 0LL) && (15LL - (long long )i) - (long long )j >= 0LL)
&& i == 10)) || (((((-14LL + (long long )i) + (long long )j >= 0LL && (4LL
- (long long )i) + (long long )j >= 0LL) && (-4LL + (long long )i) - (long
long )j >= 0LL) && (14LL - (long long )i) - (long long )j >= 0LL) && i ==
9)) || (((((-13LL + (long long )i) + (long long )j >= 0LL && (3LL - (long
long )i) + (long long )j >= 0LL) && (-3LL + (long long )i) - (long long )j
>= 0LL) && (13LL - (long long )i) - (long long )j >= 0LL) && i == 8)) || (((((-12LL
+ (long long )i) + (long long )j >= 0LL && (2LL - (long long )i) + (long long
)j >= 0LL) && (-2LL + (long long )i) - (long long )j >= 0LL) && (12LL - (long
long )i) - (long long )j >= 0LL) && i == 7)) || (((((25 <= i && i <= 100)
&& (-30LL + (long long )i) + (long long )j >= 0LL) && (95LL - (long long )i)
+ (long long )j >= 0LL) && (-20LL + (long long )i) - (long long )j >= 0LL)
&& (105LL - (long long )i) - (long long )j >= 0LL)) || (((((-11LL + (long
long )i) + (long long )j >= 0LL && (1LL - (long long )i) + (long long )j >=
0LL) && (-1LL + (long long )i) - (long long )j >= 0LL) && (11LL - (long long
)i) - (long long )j >= 0LL) && i == 6)) || (((((-29LL + (long long )i) + (long
long )j >= 0LL && (19LL - (long long )i) + (long long )j >= 0LL) && (-19LL
+ (long long )i) - (long long )j >= 0LL) && (29LL - (long long )i) - (long
long )j >= 0LL) && i == 24)) || (((((-10LL + (long long )i) + (long long )j
>= 0LL && (0LL - (long long )i) + (long long )j >= 0LL) && (10LL - (long long
)i) - (long long )j >= 0LL) && (long long )i - (long long )j >= 0LL) && i
== 5)) || (((((-28LL + (long long )i) + (long long )j >= 0LL && (18LL - (long
long )i) + (long long )j >= 0LL) && (-18LL + (long long )i) - (long long )j
>= 0LL) && (28LL - (long long )i) - (long long )j >= 0LL) && i == 23)) ||
(((((-9LL + (long long )i) + (long long )j >= 0LL && (-1LL - (long long )i)
+ (long long )j >= 0LL) && (1LL + (long long )i) - (long long )j >= 0LL) &&
(9LL - (long long )i) - (long long )j >= 0LL) && i == 4)) || (((((-27LL +
(long long )i) + (long long )j >= 0LL && (17LL - (long long )i) + (long long
)j >= 0LL) && (-17LL + (long long )i) - (long long )j >= 0LL) && (27LL - (long
long )i) - (long long )j >= 0LL) && i == 22)) || (((((-8LL + (long long )i)
+ (long long )j >= 0LL && (-2LL - (long long )i) + (long long )j >= 0LL) &&
(2LL + (long long )i) - (long long )j >= 0LL) && (8LL - (long long )i) - (long
long )j >= 0LL) && i == 3)) || (((((-26LL + (long long )i) + (long long )j
>= 0LL && (16LL - (long long )i) + (long long )j >= 0LL) && (-16LL + (long
long )i) - (long long )j >= 0LL) && (26LL - (long long )i) - (long long )j
>= 0LL) && i == 21)) || (((((-7LL + (long long )i) + (long long )j >= 0LL
&& (-3LL - (long long )i) + (long long )j >= 0LL) && (3LL + (long long )i)
- (long long )j >= 0LL) && (7LL - (long long )i) - (long long )j >= 0LL) &&
i == 2)) || (((((-25LL + (long long )i) + (long long )j >= 0LL && (15LL -
(long long )i) + (long long )j >= 0LL) && (-15LL + (long long )i) - (long
long )j >= 0LL) && (25LL - (long long )i) - (long long )j >= 0LL) && i ==
20)) || (((((-6LL + (long long )i) + (long long )j >= 0LL && (-4LL - (long
long )i) + (long long )j >= 0LL) && (4LL + (long long )i) - (long long )j
>= 0LL) && (6LL - (long long )i) - (long long )j >= 0LL) && i == 1)) || (((((-24LL
+ (long long )i) + (long long )j >= 0LL && (14LL - (long long )i) + (long
long )j >= 0LL) && (-14LL + (long long )i) - (long long )j >= 0LL) && (24LL
- (long long )i) - (long long )j >= 0LL) && i == 19)) || ((((((-5LL + (long
long )i) + (long long )j >= 0LL && (-5LL - (long long )i) + (long long )j
>= 0LL) && (5LL + (long long )i) - (long long )j >= 0LL) && (5LL - (long long
)i) - (long long )j >= 0LL) && 0 == i) && i == 0)) || (((((-23LL + (long long
)i) + (long long )j >= 0LL && (13LL - (long long )i) + (long long )j >= 0LL)
&& (-13LL + (long long )i) - (long long )j >= 0LL) && (23LL - (long long )i)
- (long long )j >= 0LL) && i == 18)
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/Sequence.c
file_hash: 95ccbbbc448c04acb65590867534531dd0d1de0ae6cfb9bc69f5ca4c10abccd4
line: 13
column: 11
function: main
value: i == 100
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/Sequence.c
file_hash: 95ccbbbc448c04acb65590867534531dd0d1de0ae6cfb9bc69f5ca4c10abccd4
line: 13
column: 11
function: main
value: ((((((((((-123LL + (long long )i) + (long long )j >= 0LL && (77LL - (long
long )i) + (long long )j >= 0LL) && (-77LL + (long long )i) - (long long )j
>= 0LL) && (123LL - (long long )i) - (long long )j >= 0LL) && j == 23) ||
(((((-120LL + (long long )i) + (long long )j >= 0LL && (80LL - (long long
)i) + (long long )j >= 0LL) && (-80LL + (long long )i) - (long long )j >=
0LL) && (120LL - (long long )i) - (long long )j >= 0LL) && j == 20)) || (((((-117LL
+ (long long )i) + (long long )j >= 0LL && (83LL - (long long )i) + (long
long )j >= 0LL) && (-83LL + (long long )i) - (long long )j >= 0LL) && (117LL
- (long long )i) - (long long )j >= 0LL) && j == 17)) || (((((-114LL + (long
long )i) + (long long )j >= 0LL && (86LL - (long long )i) + (long long )j
>= 0LL) && (-86LL + (long long )i) - (long long )j >= 0LL) && (114LL - (long
long )i) - (long long )j >= 0LL) && j == 14)) || (((((-111LL + (long long
)i) + (long long )j >= 0LL && (89LL - (long long )i) + (long long )j >= 0LL)
&& (-89LL + (long long )i) - (long long )j >= 0LL) && (111LL - (long long
)i) - (long long )j >= 0LL) && j == 11)) || (((((-108LL + (long long )i) +
(long long )j >= 0LL && (92LL - (long long )i) + (long long )j >= 0LL) &&
(-92LL + (long long )i) - (long long )j >= 0LL) && (108LL - (long long )i)
- (long long )j >= 0LL) && j == 8)) || ((((((-105LL + (long long )i) + (long
long )j >= 0LL && (95LL - (long long )i) + (long long )j >= 0LL) && (-95LL
+ (long long )i) - (long long )j >= 0LL) && (105LL - (long long )i) - (long
long )j >= 0LL) && 5 == j) && j == 5)
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
17 |
2023-12-01T04:34:01+01:00 |
|