forked from sosy-lab/sv-witnesses
-
Notifications
You must be signed in to change notification settings - Fork 0
/
multivar_1-1.c.invariant_witness.yaml
49 lines (48 loc) · 1.46 KB
/
multivar_1-1.c.invariant_witness.yaml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
- entry_type: loop_invariant
metadata:
format_version: 0.1
uuid: 91023a0f-9f45-4385-88c4-1152ade45537
creation_time: 2021-05-05T15:18:43+02:00
producer:
name: CPAchecker
version: 2.0.1-svn
configuration: (Optional) svcomp21--04-kInduction
description: (Optional)
command_line: (Optional)
task:
input_files:
- multivar_1-1.c
input_file_hashes:
multivar_1-1.c: 511f45a8d763ef520f6d92e4135c8572805994a66531c6216b17157d0dde2f9c
specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
data_model: ILP32
language: C
location:
file_name: multivar_1-1.c
file_hash: 511f45a8d763ef520f6d92e4135c8572805994a66531c6216b17157d0dde2f9c
line: 22
column: 0
function: main
loop_invariant:
string: (x >= 1024U) && (x <= 4294967295U) && (y == x)
type: assertion
format: C
- entry_type: loop_invariant_certificate
metadata:
format_version: 0.1
uuid: 954affa9-32e4-4b35-85ae-888da3a6a53b
creation_time: 2021-05-05T15:18:43+02:00
producer:
name: CPAchecker
version: 2.0.1-svn
configuration: (Optional) svcomp21--04-kInduction
description: (Optional)
command_line: (Optional)
target:
uuid: 91023a0f-9f45-4385-88c4-1152ade45537
type: loop_invariant
file_hash: XXXf45a8d763ef520f6d92e4135c8572805994a66531c6216b17157d0dde2f9c
certification:
string: confirmed
type: verdict
format: confirmed | rejected