Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
04823205
Commit
04823205
authored
Aug 25, 2014
by
MARCHE Claude
Browse files
fixed some sessions (Coq8.4 pl3 -> pl4)
parent
60a59d69
Changes
119
Expand all
Hide whitespace changes
Inline
Side-by-side
examples/algo63/why3session.xml
View file @
04823205
...
...
@@ -511,7 +511,7 @@
<ip_library
name=
"why3"
/>
<ip_qualid
name=
"unit"
/>
</ts_pos>
<ts_pos
name=
"ref"
arity=
"1"
id=
"23
12
"
<ts_pos
name=
"ref"
arity=
"1"
id=
"23
36
"
ip_theory=
"Ref"
>
<ip_library
name=
"ref"
/>
<ip_qualid
name=
"ref"
/>
...
...
@@ -541,226 +541,226 @@
<ip_library
name=
"int"
/>
<ip_qualid
name=
"infix >"
/>
</ls_pos>
<ls_pos
name=
"infix +"
id=
"1
382
"
<ls_pos
name=
"infix +"
id=
"1
459
"
ip_theory=
"Int"
>
<ip_library
name=
"int"
/>
<ip_qualid
name=
"infix +"
/>
</ls_pos>
<ls_pos
name=
"prefix -"
id=
"1
383
"
<ls_pos
name=
"prefix -"
id=
"1
460
"
ip_theory=
"Int"
>
<ip_library
name=
"int"
/>
<ip_qualid
name=
"prefix -"
/>
</ls_pos>
<ls_pos
name=
"infix *"
id=
"1
384
"
<ls_pos
name=
"infix *"
id=
"1
461
"
ip_theory=
"Int"
>
<ip_library
name=
"int"
/>
<ip_qualid
name=
"infix *"
/>
</ls_pos>
<ls_pos
name=
"prefix !"
id=
"23
18
"
<ls_pos
name=
"prefix !"
id=
"23
42
"
ip_theory=
"Ref"
>
<ip_library
name=
"ref"
/>
<ip_qualid
name=
"prefix !"
/>
</ls_pos>
<ls_pos
name=
"get"
id=
"24
64
"
<ls_pos
name=
"get"
id=
"24
88
"
ip_theory=
"Map"
>
<ip_library
name=
"map"
/>
<ip_qualid
name=
"get"
/>
</ls_pos>
<ls_pos
name=
"set"
id=
"24
67
"
<ls_pos
name=
"set"
id=
"24
91
"
ip_theory=
"Map"
>
<ip_library
name=
"map"
/>
<ip_qualid
name=
"set"
/>
</ls_pos>
<ls_pos
name=
"mixfix [<-]"
id=
"2
487
"
<ls_pos
name=
"mixfix [<-]"
id=
"2
511
"
ip_theory=
"Map"
>
<ip_library
name=
"map"
/>
<ip_qualid
name=
"mixfix [<-]"
/>
</ls_pos>
<ls_pos
name=
"const"
id=
"25
18
"
<ls_pos
name=
"const"
id=
"25
42
"
ip_theory=
"Map"
>
<ip_library
name=
"map"
/>
<ip_qualid
name=
"const"
/>
</ls_pos>
<ls_pos
name=
"occ"
id=
"29
03
"
<ls_pos
name=
"occ"
id=
"29
27
"
ip_theory=
"Occ"
>
<ip_library
name=
"map"
/>
<ip_qualid
name=
"occ"
/>
</ls_pos>
<ls_pos
name=
"get"
id=
"31
08
"
<ls_pos
name=
"get"
id=
"31
32
"
ip_theory=
"Array"
>
<ip_library
name=
"array"
/>
<ip_qualid
name=
"get"
/>
</ls_pos>
<ls_pos
name=
"set"
id=
"31
23
"
<ls_pos
name=
"set"
id=
"31
47
"
ip_theory=
"Array"
>
<ip_library
name=
"array"
/>
<ip_qualid
name=
"set"
/>
</ls_pos>
<ls_pos
name=
"mixfix []"
id=
"31
48
"
<ls_pos
name=
"mixfix []"
id=
"31
72
"
ip_theory=
"Array"
>
<ip_library
name=
"array"
/>
<ip_qualid
name=
"mixfix []"
/>
</ls_pos>
<ls_pos
name=
"mixfix [<-]"
id=
"31
65
"
<ls_pos
name=
"mixfix [<-]"
id=
"31
89
"
ip_theory=
"Array"
>
<ip_library
name=
"array"
/>
<ip_qualid
name=
"mixfix [<-]"
/>
</ls_pos>
<ls_pos
name=
"make"
id=
"32
66
"
<ls_pos
name=
"make"
id=
"32
90
"
ip_theory=
"Array"
>
<ip_library
name=
"array"
/>
<ip_qualid
name=
"make"
/>
</ls_pos>
<ls_pos
name=
"array_eq"
id=
"35
42
"
<ls_pos
name=
"array_eq"
id=
"35
66
"
ip_theory=
"ArrayEq"
>
<ip_library
name=
"array"
/>
<ip_qualid
name=
"array_eq"
/>
</ls_pos>
<pr_pos
name=
"Assoc"
id=
"1
385
"
<pr_pos
name=
"Assoc"
id=
"1
462
"
ip_theory=
"Int"
>
<ip_library
name=
"int"
/>
<ip_qualid
name=
"CommutativeGroup"
/>
<ip_qualid
name=
"Assoc"
/>
</pr_pos>
<pr_pos
name=
"Unit_def_l"
id=
"1
392
"
<pr_pos
name=
"Unit_def_l"
id=
"1
469
"
ip_theory=
"Int"
>
<ip_library
name=
"int"
/>
<ip_qualid
name=
"CommutativeGroup"
/>
<ip_qualid
name=
"Unit_def_l"
/>
</pr_pos>
<pr_pos
name=
"Unit_def_r"
id=
"1
395
"
<pr_pos
name=
"Unit_def_r"
id=
"1
472
"
ip_theory=
"Int"
>
<ip_library
name=
"int"
/>
<ip_qualid
name=
"CommutativeGroup"
/>
<ip_qualid
name=
"Unit_def_r"
/>
</pr_pos>
<pr_pos
name=
"Inv_def_l"
id=
"1
398
"
<pr_pos
name=
"Inv_def_l"
id=
"1
475
"
ip_theory=
"Int"
>
<ip_library
name=
"int"
/>
<ip_qualid
name=
"CommutativeGroup"
/>
<ip_qualid
name=
"Inv_def_l"
/>
</pr_pos>
<pr_pos
name=
"Inv_def_r"
id=
"14
01
"
<pr_pos
name=
"Inv_def_r"
id=
"14
78
"
ip_theory=
"Int"
>
<ip_library
name=
"int"
/>
<ip_qualid
name=
"CommutativeGroup"
/>
<ip_qualid
name=
"Inv_def_r"
/>
</pr_pos>
<pr_pos
name=
"Comm"
id=
"14
04
"
<pr_pos
name=
"Comm"
id=
"14
81
"
ip_theory=
"Int"
>
<ip_library
name=
"int"
/>
<ip_qualid
name=
"CommutativeGroup"
/>
<ip_qualid
name=
"Comm"
/>
<ip_qualid
name=
"Comm"
/>
</pr_pos>
<pr_pos
name=
"Assoc"
id=
"14
09
"
<pr_pos
name=
"Assoc"
id=
"14
86
"
ip_theory=
"Int"
>
<ip_library
name=
"int"
/>
<ip_qualid
name=
"Assoc"
/>
<ip_qualid
name=
"Assoc"
/>
</pr_pos>
<pr_pos
name=
"Mul_distr_l"
id=
"14
16
"
<pr_pos
name=
"Mul_distr_l"
id=
"14
93
"
ip_theory=
"Int"
>
<ip_library
name=
"int"
/>
<ip_qualid
name=
"Mul_distr_l"
/>
</pr_pos>
<pr_pos
name=
"Mul_distr_r"
id=
"1
423
"
<pr_pos
name=
"Mul_distr_r"
id=
"1
500
"
ip_theory=
"Int"
>
<ip_library
name=
"int"
/>
<ip_qualid
name=
"Mul_distr_r"
/>
</pr_pos>
<pr_pos
name=
"Comm"
id=
"1
441
"
<pr_pos
name=
"Comm"
id=
"1
518
"
ip_theory=
"Int"
>
<ip_library
name=
"int"
/>
<ip_qualid
name=
"Comm"
/>
<ip_qualid
name=
"Comm"
/>
</pr_pos>
<pr_pos
name=
"Unitary"
id=
"1
446
"
<pr_pos
name=
"Unitary"
id=
"1
523
"
ip_theory=
"Int"
>
<ip_library
name=
"int"
/>
<ip_qualid
name=
"Unitary"
/>
</pr_pos>
<pr_pos
name=
"NonTrivialRing"
id=
"1
449
"
<pr_pos
name=
"NonTrivialRing"
id=
"1
526
"
ip_theory=
"Int"
>
<ip_library
name=
"int"
/>
<ip_qualid
name=
"NonTrivialRing"
/>
</pr_pos>
<pr_pos
name=
"Refl"
id=
"1
461
"
<pr_pos
name=
"Refl"
id=
"1
538
"
ip_theory=
"Int"
>
<ip_library
name=
"int"
/>
<ip_qualid
name=
"Refl"
/>
</pr_pos>
<pr_pos
name=
"Trans"
id=
"1
464
"
<pr_pos
name=
"Trans"
id=
"1
541
"
ip_theory=
"Int"
>
<ip_library
name=
"int"
/>
<ip_qualid
name=
"Trans"
/>
</pr_pos>
<pr_pos
name=
"Antisymm"
id=
"1
471
"
<pr_pos
name=
"Antisymm"
id=
"1
548
"
ip_theory=
"Int"
>
<ip_library
name=
"int"
/>
<ip_qualid
name=
"Antisymm"
/>
</pr_pos>
<pr_pos
name=
"Total"
id=
"1
476
"
<pr_pos
name=
"Total"
id=
"1
553
"
ip_theory=
"Int"
>
<ip_library
name=
"int"
/>
<ip_qualid
name=
"Total"
/>
</pr_pos>
<pr_pos
name=
"ZeroLessOne"
id=
"1
481
"
<pr_pos
name=
"ZeroLessOne"
id=
"1
558
"
ip_theory=
"Int"
>
<ip_library
name=
"int"
/>
<ip_qualid
name=
"ZeroLessOne"
/>
</pr_pos>
<pr_pos
name=
"CompatOrderMult"
id=
"1
489
"
<pr_pos
name=
"CompatOrderMult"
id=
"1
566
"
ip_theory=
"Int"
>
<ip_library
name=
"int"
/>
<ip_qualid
name=
"CompatOrderMult"
/>
</pr_pos>
<pr_pos
name=
"Select_eq"
id=
"25
00
"
<pr_pos
name=
"Select_eq"
id=
"25
24
"
ip_theory=
"Map"
>
<ip_library
name=
"map"
/>
<ip_qualid
name=
"Select_eq"
/>
</pr_pos>
<pr_pos
name=
"Select_neq"
id=
"25
09
"
<pr_pos
name=
"Select_neq"
id=
"25
33
"
ip_theory=
"Map"
>
<ip_library
name=
"map"
/>
<ip_qualid
name=
"Select_neq"
/>
</pr_pos>
<pr_pos
name=
"Const"
id=
"25
20
"
<pr_pos
name=
"Const"
id=
"25
44
"
ip_theory=
"Map"
>
<ip_library
name=
"map"
/>
<ip_qualid
name=
"Const"
/>
</pr_pos>
<pr_pos
name=
"exchange_set"
id=
"2
599
"
<pr_pos
name=
"exchange_set"
id=
"2
623
"
ip_theory=
"MapExchange"
>
<ip_library
name=
"map"
/>
<ip_qualid
name=
"exchange_set"
/>
</pr_pos>
<pr_pos
name=
"occ_right_no_add"
id=
"291
7
"
<pr_pos
name=
"occ_right_no_add"
id=
"29
4
1"
ip_theory=
"Occ"
>
<ip_library
name=
"map"
/>
<ip_qualid
name=
"occ_right_no_add"
/>
</pr_pos>
<pr_pos
name=
"occ_bounds"
id=
"29
3
5"
<pr_pos
name=
"occ_bounds"
id=
"295
9
"
ip_theory=
"Occ"
>
<ip_library
name=
"map"
/>
<ip_qualid
name=
"occ_bounds"
/>
</pr_pos>
<pr_pos
name=
"occ_append"
id=
"29
44
"
<pr_pos
name=
"occ_append"
id=
"29
68
"
ip_theory=
"Occ"
>
<ip_library
name=
"map"
/>
<ip_qualid
name=
"occ_append"
/>
</pr_pos>
<pr_pos
name=
"occ_neq"
id=
"29
55
"
<pr_pos
name=
"occ_neq"
id=
"29
79
"
ip_theory=
"Occ"
>
<ip_library
name=
"map"
/>
<ip_qualid
name=
"occ_neq"
/>
</pr_pos>
<pr_pos
name=
"occ_exists"
id=
"29
66
"
<pr_pos
name=
"occ_exists"
id=
"29
90
"
ip_theory=
"Occ"
>
<ip_library
name=
"map"
/>
<ip_qualid
name=
"occ_exists"
/>
</pr_pos>
<pr_pos
name=
"occ_pos"
id=
"
2977
"
<pr_pos
name=
"occ_pos"
id=
"
3001
"
ip_theory=
"Occ"
>
<ip_library
name=
"map"
/>
<ip_qualid
name=
"occ_pos"
/>
...
...
@@ -781,133 +781,133 @@
<meta_arg_ls
id=
"293"
/>
</meta>
<meta
name=
"remove_logic"
>
<meta_arg_ls
id=
"1
382
"
/>
<meta_arg_ls
id=
"1
459
"
/>
</meta>
<meta
name=
"remove_logic"
>
<meta_arg_ls
id=
"1
383
"
/>
<meta_arg_ls
id=
"1
460
"
/>
</meta>
<meta
name=
"remove_logic"
>
<meta_arg_ls
id=
"1
384
"
/>
<meta_arg_ls
id=
"1
461
"
/>
</meta>
<meta
name=
"remove_logic"
>
<meta_arg_ls
id=
"23
18
"
/>
<meta_arg_ls
id=
"23
42
"
/>
</meta>
<meta
name=
"remove_logic"
>
<meta_arg_ls
id=
"24
64
"
/>
<meta_arg_ls
id=
"24
88
"
/>
</meta>
<meta
name=
"remove_logic"
>
<meta_arg_ls
id=
"24
67
"
/>
<meta_arg_ls
id=
"24
91
"
/>
</meta>
<meta
name=
"remove_logic"
>
<meta_arg_ls
id=
"2
487
"
/>
<meta_arg_ls
id=
"2
511
"
/>
</meta>
<meta
name=
"remove_logic"
>
<meta_arg_ls
id=
"25
18
"
/>
<meta_arg_ls
id=
"25
42
"
/>
</meta>
<meta
name=
"remove_logic"
>
<meta_arg_ls
id=
"29
03
"
/>
<meta_arg_ls
id=
"29
27
"
/>
</meta>
<meta
name=
"remove_logic"
>
<meta_arg_ls
id=
"31
08
"
/>
<meta_arg_ls
id=
"31
32
"
/>
</meta>
<meta
name=
"remove_logic"
>
<meta_arg_ls
id=
"31
23
"
/>
<meta_arg_ls
id=
"31
47
"
/>
</meta>
<meta
name=
"remove_logic"
>
<meta_arg_ls
id=
"31
48
"
/>
<meta_arg_ls
id=
"31
72
"
/>
</meta>
<meta
name=
"remove_logic"
>
<meta_arg_ls
id=
"31
65
"
/>
<meta_arg_ls
id=
"31
89
"
/>
</meta>
<meta
name=
"remove_logic"
>
<meta_arg_ls
id=
"32
66
"
/>
<meta_arg_ls
id=
"32
90
"
/>
</meta>
<meta
name=
"remove_logic"
>
<meta_arg_ls
id=
"35
42
"
/>
<meta_arg_ls
id=
"35
66
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"1
385
"
/>
<meta_arg_pr
id=
"1
462
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"1
392
"
/>
<meta_arg_pr
id=
"1
469
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"1
395
"
/>
<meta_arg_pr
id=
"1
472
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"1
398
"
/>
<meta_arg_pr
id=
"1
475
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"14
01
"
/>
<meta_arg_pr
id=
"14
78
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"14
04
"
/>
<meta_arg_pr
id=
"14
81
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"14
09
"
/>
<meta_arg_pr
id=
"14
86
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"14
16
"
/>
<meta_arg_pr
id=
"14
93
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"1
423
"
/>
<meta_arg_pr
id=
"1
500
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"1
441
"
/>
<meta_arg_pr
id=
"1
518
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"1
446
"
/>
<meta_arg_pr
id=
"1
523
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"1
449
"
/>
<meta_arg_pr
id=
"1
526
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"1
461
"
/>
<meta_arg_pr
id=
"1
538
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"1
464
"
/>
<meta_arg_pr
id=
"1
541
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"1
471
"
/>
<meta_arg_pr
id=
"1
548
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"1
476
"
/>
<meta_arg_pr
id=
"1
553
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"1
481
"
/>
<meta_arg_pr
id=
"1
558
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"1
489
"
/>
<meta_arg_pr
id=
"1
566
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"25
00
"
/>
<meta_arg_pr
id=
"25
24
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"25
09
"
/>
<meta_arg_pr
id=
"25
33
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"25
20
"
/>
<meta_arg_pr
id=
"25
44
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"2
599
"
/>
<meta_arg_pr
id=
"2
623
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"291
7
"
/>
<meta_arg_pr
id=
"29
4
1"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"29
3
5"
/>
<meta_arg_pr
id=
"295
9
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"29
44
"
/>
<meta_arg_pr
id=
"29
68
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"29
55
"
/>
<meta_arg_pr
id=
"29
79
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"29
66
"
/>
<meta_arg_pr
id=
"29
90
"
/>
</meta>
<meta
name=
"remove_prop"
>
<meta_arg_pr
id=
"
2977
"
/>
<meta_arg_pr
id=
"
3001
"
/>
</meta>
<meta
name=
"remove_type"
>
<meta_arg_ts
id=
"2"
/>
...
...
@@ -922,7 +922,7 @@
<meta_arg_ts
id=
"21"
/>
</meta>
<meta
name=
"remove_type"
>
<meta_arg_ts
id=
"23
12
"
/>
<meta_arg_ts
id=
"23
36
"
/>
</meta>
<goal
name=
"WP_parameter partition.4"
expl=
"4. postcondition"
sum=
"6bbc0be90784bfdecb88b379603e1ae6"
>
<transf
name=
"eliminate_builtin"
>
...
...
examples/bellman_ford/why3session.xml
View file @
04823205
This diff is collapsed.
Click to expand it.
examples/bellman_ford/why3shapes.gz
View file @
04823205
No preview for this file type
examples/binary_sqrt/why3session.xml
View file @
04823205
...
...
@@ -8,72 +8,72 @@
<prover
id=
"3"
name=
"CVC4"
version=
"1.3"
timelimit=
"5"
memlimit=
"1000"
/>
<file
name=
"../binary_sqrt.mlw"
expanded=
"true"
>
<theory
name=
"BinarySqrt"
expanded=
"true"
>
<goal
name=
"WP_parameter sqrt"
expl=
"VC for sqrt"
sum=
"
d25a3c0ea8edfcd623e6c047ca09fad5
"
expanded=
"true"
>
<goal
name=
"WP_parameter sqrt"
expl=
"VC for sqrt"
sum=
"
434505d91f169f2b67aa7ecd2f79c26d
"
expanded=
"true"
>
<transf
name=
"split_goal"
expanded=
"true"
>
<goal
name=
"WP_parameter sqrt.1"
expl=
"1. postcondition"
sum=
"
19871722ba65be421a62a57da3b3f16d
"
>
<goal
name=
"WP_parameter sqrt.1"
expl=
"1. postcondition"
sum=
"
b4359c27c751534cddf64e13a826d039
"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt.2"
expl=
"2. assertion"
sum=
"
a702f7f544c0300edfcbe76e8f78279
5"
>
<goal
name=
"WP_parameter sqrt.2"
expl=
"2. assertion"
sum=
"
27320a86722961d218d6ba29096ce82
5"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt.3"
expl=
"3. assertion"
sum=
"
72103cb
e6
b
7c
4ccc99096b9b7a34813
9"
>
<goal
name=
"WP_parameter sqrt.3"
expl=
"3. assertion"
sum=
"
4b29f20c8021
e6
9
7c
2520071c95e904
9"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt.4"
expl=
"4. assertion"
sum=
"
5363dae742f6c969aa8addbf507e271
4"
>
<goal
name=
"WP_parameter sqrt.4"
expl=
"4. assertion"
sum=
"
24fffe650b71956e36d5bcfb898f66e
4"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt.5"
expl=
"5. assertion"
sum=
"
6bf2148bd91e818a82b0971d7b9d9e30
"
>
<goal
name=
"WP_parameter sqrt.5"
expl=
"5. assertion"
sum=
"
b7f2b06f5aeb330d479fa4416a193b5e
"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt.6"
expl=
"6. assertion"
sum=
"2
9982125fd495c2a7b642b480e2574b1
"
>
<proof
prover=
"1"
><result
status=
"
valid
"
time=
"
4.3
9"
/></proof>
<goal
name=
"WP_parameter sqrt.6"
expl=
"6. assertion"
sum=
"2
742deb4bf19442876c68f1190d3166b
"
>
<proof
prover=
"1"
><result
status=
"
timeout
"
time=
"
8.9
9"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt.7"
expl=
"7. variant decrease"
sum=
"
4f3b89e0252d31f2fad81ad399e74a7f
"
>
<goal
name=
"WP_parameter sqrt.7"
expl=
"7. variant decrease"
sum=
"
7971f31dfe403547b507e011f28204bc
"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.27"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt.8"
expl=
"8. precondition"
sum=
"
d7cb8a8eda36e6a9d8caa63495827e74
"
>
<goal
name=
"WP_parameter sqrt.8"
expl=
"8. precondition"
sum=
"
6d08fa6a833ef1be3db326b55af1bf6f
"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt.9"
expl=
"9. precondition"
sum=
"
47e7054825ef077f0c24d4390e518343
"
>
<goal
name=
"WP_parameter sqrt.9"
expl=
"9. precondition"
sum=
"
35389a433aaad3cc1b636744aaf9f0f8
"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt.10"
expl=
"10. precondition"
sum=
"
ec913fce000919fe171c3e23d0bed32e
"
>
<goal
name=
"WP_parameter sqrt.10"
expl=
"10. precondition"
sum=
"
8155cd4e2f97a5d5eb9dad700c2bba2d
"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt.11"
expl=
"11. postcondition"
sum=
"
521597c8e5279a701821dc56d364966f
"
>
<goal
name=
"WP_parameter sqrt.11"
expl=
"11. postcondition"
sum=
"
c668080a1ee8138e01d25f19f99e0334
"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.38"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"WP_parameter sqrt_main"
expl=
"VC for sqrt_main"
sum=
"
d6dc5d421c0f3b3991c06542877c8ced
"
expanded=
"true"
>
<goal
name=
"WP_parameter sqrt_main"
expl=
"VC for sqrt_main"
sum=
"
bf6cc9bae44dc6bf42e0f0a1f5f87cb5
"
expanded=
"true"
>
<transf
name=
"split_goal_wp"
expanded=
"true"
>
<goal
name=
"WP_parameter sqrt_main.1"
expl=
"1. precondition"
sum=
"
3a7291d34de0a630c653918c8a771a
cc"
>
<goal
name=
"WP_parameter sqrt_main.1"
expl=
"1. precondition"
sum=
"
e78b9af2a57a8f6e1abd2fd9878c5e
cc"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.00"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt_main.2"
expl=
"2. precondition"
sum=
"1
6261f
bd9c
451aa163dd1e01b9874a83
"
>
<goal
name=
"WP_parameter sqrt_main.2"
expl=
"2. precondition"
sum=
"1
fb01364a35
bd
8
9c
04f57f23b99383cd
"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.00"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt_main.3"
expl=
"3. precondition"
sum=
"
b99a2dcaff7c06eaa53d4c65dc5faf02
"
>
<goal
name=
"WP_parameter sqrt_main.3"
expl=
"3. precondition"
sum=
"
54678c5dbe2efad67f1175d0fba76007
"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.00"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt_main.4"
expl=
"4. postcondition"
sum=
"
a9380c26c230dbe03a4fb5c5b7c30194
"
>
<goal
name=
"WP_parameter sqrt_main.4"
expl=
"4. postcondition"
sum=
"
76b96896d79794587a1e5d7f042d1639
"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.01"
/></proof>
...
...
examples/binary_sqrt/why3shapes.gz
View file @
04823205
No preview for this file type
examples/bitvectors/bitvector/why3session.xml
View file @
04823205
...
...
@@ -3,79 +3,79 @@
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"0"
name=
"CVC4"
version=
"1.2"
timelimit=
"30"
memlimit=
"4000"
/>
<prover
id=
"1"
name=
"C
VC3
"
version=
"
2
.4
.1
"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"2"
name=
"
Alt-Ergo
"
version=
"
0.95
.1"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"3"
name=
"
Z3
"
version=
"
2
.1
9
"
timelimit=
"
3
"
memlimit=
"1000"
/>
<prover
id=
"4"
name=
"Z3"
version=
"
4.3
.1"
timelimit=
"
5
"
memlimit=
"1000"
/>
<prover
id=
"5"
name=
"
CVC
3"
version=
"
2.2
"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"6"
name=
"
Z
3"
version=
"
3
.2"
timelimit=
"
3
"
memlimit=
"1000"
/>
<prover
id=
"7"
name=
"
Coq
"
version=
"
8.4pl3
"
timelimit=
"
5
"
memlimit=
"1000"
/>
<prover
id=
"1"
name=
"C
oq
"
version=
"
8
.4
pl4
"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"2"
name=
"
CVC3
"
version=
"
2.4
.1"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"3"
name=
"
Alt-Ergo
"
version=
"
0.95
.1"
timelimit=
"
5
"
memlimit=
"1000"
/>
<prover
id=
"4"
name=
"Z3"
version=
"
2
.1
9
"
timelimit=
"
3
"
memlimit=
"1000"
/>
<prover
id=
"5"
name=
"
Z
3"
version=
"
4.3.1
"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"6"
name=
"
CVC
3"
version=
"
2
.2"
timelimit=
"
5
"
memlimit=
"1000"
/>
<prover
id=
"7"
name=
"
Z3
"
version=
"
3.2
"
timelimit=
"
3
"
memlimit=
"1000"
/>
<file
name=
"../bitvector.why"
expanded=
"true"
>
<theory
name=
"BitVector"
expanded=
"true"
>
<goal
name=
"Nth_bw_xor_v1true"
sum=
"39dfc6b8b3984c52b27e1a03353cc120"
>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"0.10"
/></proof>
<proof
prover=
"
5
"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"
3
"
><result
status=
"valid"
time=
"0.10"
/></proof>
<proof
prover=
"
6
"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
<goal
name=
"Nth_bw_xor_v1false"
sum=
"8f96dc626081c1fda6a6367a0c33e860"
>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"
5
"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"
6
"
><result
status=
"valid"
time=
"0.00"
/></proof>
</goal>
<goal
name=
"Nth_bw_xor_v2true"
sum=
"7f272fb1bc61eb7b34b65925a9cb32b8"
>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"0.07"
/></proof>
<proof
prover=
"
5
"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"
3
"
><result
status=
"valid"
time=
"0.07"
/></proof>