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
701397eb
Commit
701397eb
authored
Feb 23, 2016
by
MARCHE Claude
Browse files
sessions: more updates for Coq 8.5
parent
6c985576
Changes
105
Expand all
Hide whitespace changes
Inline
Side-by-side
examples/algo63/why3session.xml
View file @
701397eb
This diff is collapsed.
Click to expand it.
examples/arm/why3session.xml
View file @
701397eb
...
...
@@ -2,57 +2,56 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"1"
name=
"Z3"
version=
"3.2"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"2"
name=
"Alt-Ergo"
version=
"0.95.2"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"3"
name=
"Alt-Ergo"
version=
"0.99.1"
timelimit=
"5"
memlimit=
"0"
/>
<prover
id=
"1"
name=
"Z3"
version=
"3.2"
timelimit=
"5"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"3"
name=
"Alt-Ergo"
version=
"0.99.1"
timelimit=
"5"
steplimit=
"1"
memlimit=
"0"
/>
<file
name=
"../arm.mlw"
expanded=
"true"
>
<theory
name=
"M"
sum=
"0d719c3e6262bb28f7a388d2aa2d5410"
expanded=
"true"
>
<goal
name=
"WP_parameter insertion_sort"
expl=
"VC for insertion_sort"
>
<transf
name=
"split_goal_wp"
>
<goal
name=
"WP_parameter insertion_sort.1"
expl=
"1. loop invariant init"
>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"0.00"
steps=
"6"
/></proof>
<proof
prover=
"
3"
memlimit=
"1000
"
><result
status=
"valid"
time=
"0.00"
steps=
"6"
/></proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.2"
expl=
"2. loop invariant init"
>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"0.01"
steps=
"15"
/></proof>
<proof
prover=
"
3"
memlimit=
"1000
"
><result
status=
"valid"
time=
"0.01"
steps=
"15"
/></proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.3"
expl=
"3. type invariant"
>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"0.02"
steps=
"15"
/></proof>
<proof
prover=
"
3"
memlimit=
"1000
"
><result
status=
"valid"
time=
"0.02"
steps=
"15"
/></proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.4"
expl=
"4. index in array bounds"
>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"0.02"
steps=
"17"
/></proof>
<proof
prover=
"
3"
memlimit=
"1000
"
><result
status=
"valid"
time=
"0.02"
steps=
"17"
/></proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.5"
expl=
"5. index in array bounds"
>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"0.02"
steps=
"19"
/></proof>
<proof
prover=
"
3"
memlimit=
"1000
"
><result
status=
"valid"
time=
"0.02"
steps=
"19"
/></proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.6"
expl=
"6. index in array bounds"
>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"0.02"
steps=
"21"
/></proof>
<proof
prover=
"
3"
memlimit=
"1000
"
><result
status=
"valid"
time=
"0.02"
steps=
"21"
/></proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.7"
expl=
"7. index in array bounds"
>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"0.03"
steps=
"21"
/></proof>
<proof
prover=
"
3"
memlimit=
"1000
"
><result
status=
"valid"
time=
"0.03"
steps=
"21"
/></proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.8"
expl=
"8. index in array bounds"
>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"0.02"
steps=
"21"
/></proof>
<proof
prover=
"
3"
memlimit=
"1000
"
><result
status=
"valid"
time=
"0.02"
steps=
"21"
/></proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.9"
expl=
"9. index in array bounds"
>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"0.02"
steps=
"22"
/></proof>
<proof
prover=
"
3"
memlimit=
"1000
"
><result
status=
"valid"
time=
"0.02"
steps=
"22"
/></proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.10"
expl=
"10. loop invariant preservation"
>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"1.17"
steps=
"
80
"
/></proof>
<proof
prover=
"
3"
memlimit=
"1000
"
><result
status=
"valid"
time=
"1.17"
steps=
"
75
"
/></proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.11"
expl=
"11. loop variant decrease"
>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"0.02"
steps=
"24"
/></proof>
<proof
prover=
"
3"
memlimit=
"1000
"
><result
status=
"valid"
time=
"0.02"
steps=
"24"
/></proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.12"
expl=
"12. loop invariant preservation"
>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"0.02"
steps=
"27"
/></proof>
<proof
prover=
"
3"
memlimit=
"1000
"
><result
status=
"valid"
time=
"0.02"
steps=
"27"
/></proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.13"
expl=
"13. loop variant decrease"
>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"0.01"
steps=
"21"
/></proof>
<proof
prover=
"
3"
memlimit=
"1000
"
><result
status=
"valid"
time=
"0.01"
steps=
"21"
/></proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.14"
expl=
"14. type invariant"
>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"0.00"
steps=
"10"
/></proof>
<proof
prover=
"
3"
memlimit=
"1000
"
><result
status=
"valid"
time=
"0.00"
steps=
"10"
/></proof>
</goal>
<goal
name=
"WP_parameter insertion_sort.15"
expl=
"15. postcondition"
>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"0.01"
steps=
"10"
/></proof>
<proof
prover=
"
3"
memlimit=
"1000
"
><result
status=
"valid"
time=
"0.01"
steps=
"10"
/></proof>
</goal>
</transf>
</goal>
...
...
examples/binary_sqrt/why3session.xml
View file @
701397eb
...
...
@@ -2,56 +2,56 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"0"
name=
"CVC3"
version=
"2.4.1"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"
1
"
name=
"Z3"
version=
"
4.
3.
1
"
timelimit=
"
5
"
memlimit=
"1000"
/>
<prover
id=
"
2
"
name=
"
Z3
"
version=
"
3.2
"
timelimit=
"
30
"
memlimit=
"1000"
/>
<prover
id=
"
3
"
name=
"
Alt-Ergo
"
version=
"
0.95.2
"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"
4
"
name=
"
CVC4
"
version=
"
1
.3"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"0"
name=
"CVC3"
version=
"2.4.1"
timelimit=
"5"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"
2
"
name=
"Z3"
version=
"3.
2
"
timelimit=
"
30"
steplimit=
"1
"
memlimit=
"1000"
/>
<prover
id=
"
5
"
name=
"
Alt-Ergo
"
version=
"
0.99.1
"
timelimit=
"
5"
steplimit=
"1
"
memlimit=
"1000"
/>
<prover
id=
"
6
"
name=
"
CVC4
"
version=
"
1.4
"
timelimit=
"5"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"
7
"
name=
"
Z3
"
version=
"
4
.3
.2
"
timelimit=
"5"
steplimit=
"1"
memlimit=
"1000"
/>
<file
name=
"../binary_sqrt.mlw"
expanded=
"true"
>
<theory
name=
"BinarySqrt"
sum=
"6b669d31cbc3c11118695754ff2ebc1b"
expanded=
"true"
>
<goal
name=
"WP_parameter sqrt"
expl=
"VC for sqrt"
expanded=
"true"
>
<transf
name=
"split_goal_wp"
expanded=
"true"
>
<goal
name=
"WP_parameter sqrt.1"
expl=
"1. postcondition"
>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"
7
"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt.2"
expl=
"2. assertion"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"
3
"
><result
status=
"valid"
time=
"0.0
1"
steps=
"13
"
/></proof>
<proof
prover=
"
5
"
><result
status=
"valid"
time=
"0.0
1"
steps=
"12
"
/></proof>
<proof
prover=
"
7
"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt.3"
expl=
"3. assertion"
>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"
7
"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt.4"
expl=
"4. assertion"
>
<proof
prover=
"
3
"
><result
status=
"valid"
time=
"0.02"
steps=
"9"
/></proof>
<proof
prover=
"
5
"
><result
status=
"valid"
time=
"0.02"
steps=
"9"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt.5"
expl=
"5. assertion"
>
<proof
prover=
"
3
"
><result
status=
"valid"
time=
"0.03"
steps=
"2
6
"
/></proof>
<proof
prover=
"
5
"
><result
status=
"valid"
time=
"0.03"
steps=
"2
5
"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt.6"
expl=
"6. assertion"
>
<proof
prover=
"1"
timelimit=
"30"
><result
status=
"valid"
time=
"4.35"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"7"
timelimit=
"30"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt.7"
expl=
"7. variant decrease"
>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.
00
"
/></proof>
<proof
prover=
"
3
"
><result
status=
"valid"
time=
"0.
61"
steps=
"115
"
/></proof>
<proof
prover=
"
4
"
><result
status=
"valid"
time=
"0.0
4
"
/></proof>
<proof
prover=
"
5
"
><result
status=
"valid"
time=
"0.
40"
steps=
"109
"
/></proof>
<proof
prover=
"
6
"
><result
status=
"valid"
time=
"0.
04
"
/></proof>
<proof
prover=
"
7
"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt.8"
expl=
"8. precondition"
>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"
3
"
><result
status=
"valid"
time=
"0.01"
steps=
"11"
/></proof>
<proof
prover=
"
4
"
><result
status=
"valid"
time=
"0.0
1
"
/></proof>
<proof
prover=
"
5
"
><result
status=
"valid"
time=
"0.0
1"
steps=
"11
"
/></proof>
<proof
prover=
"
6
"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"
7
"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt.9"
expl=
"9. precondition"
>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"
3
"
><result
status=
"valid"
time=
"0.01"
steps=
"11"
/></proof>
<proof
prover=
"
4
"
><result
status=
"valid"
time=
"0.0
1
"
/></proof>
<proof
prover=
"
5
"
><result
status=
"valid"
time=
"0.0
1"
steps=
"11
"
/></proof>
<proof
prover=
"
6
"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"
7
"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt.10"
expl=
"10. precondition"
>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"
7
"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt.11"
expl=
"11. postcondition"
>
<proof
prover=
"
3
"
><result
status=
"valid"
time=
"0.
38
"
steps=
"2
3
"
/></proof>
<proof
prover=
"
5
"
><result
status=
"valid"
time=
"0.
20
"
steps=
"2
2
"
/></proof>
</goal>
</transf>
</goal>
...
...
@@ -59,27 +59,27 @@
<transf
name=
"split_goal_wp"
expanded=
"true"
>
<goal
name=
"WP_parameter sqrt_main.1"
expl=
"1. precondition"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"
3
"
><result
status=
"valid"
time=
"0.0
1"
steps=
"4
"
/></proof>
<proof
prover=
"
4
"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"
5
"
><result
status=
"valid"
time=
"0.0
1"
steps=
"4
"
/></proof>
<proof
prover=
"
6
"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"
7
"
><result
status=
"valid"
time=
"0.00"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt_main.2"
expl=
"2. precondition"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"
3
"
><result
status=
"valid"
time=
"0.00"
steps=
"4"
/></proof>
<proof
prover=
"
4
"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"
5
"
><result
status=
"valid"
time=
"0.00"
steps=
"4"
/></proof>
<proof
prover=
"
6
"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"
7
"
><result
status=
"valid"
time=
"0.00"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt_main.3"
expl=
"3. precondition"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"
3
"
><result
status=
"valid"
time=
"0.00"
steps=
"4"
/></proof>
<proof
prover=
"
4
"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"
5
"
><result
status=
"valid"
time=
"0.00"
steps=
"4"
/></proof>
<proof
prover=
"
6
"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"
7
"
><result
status=
"valid"
time=
"0.00"
/></proof>
</goal>
<goal
name=
"WP_parameter sqrt_main.4"
expl=
"4. postcondition"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
<proof
prover=
"
3
"
><result
status=
"valid"
time=
"0.01"
steps=
"8"
/></proof>
<proof
prover=
"
4
"
><result
status=
"valid"
time=
"0.0
1
"
/></proof>
<proof
prover=
"
5
"
><result
status=
"valid"
time=
"0.0
1"
steps=
"8
"
/></proof>
<proof
prover=
"
6
"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"
7
"
><result
status=
"valid"
time=
"0.0
0
"
/></proof>
</goal>
</transf>
</goal>
...
...
examples/bitvectors/bitvector/why3session.xml
View file @
701397eb
...
...
@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"
0
"
name=
"Coq"
version=
"8.
4pl6
"
timelimit=
"5"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"
1
"
name=
"Coq"
version=
"8.
5
"
timelimit=
"5"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"2"
name=
"Alt-Ergo"
version=
"0.99.1"
timelimit=
"5"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"3"
name=
"CVC3"
version=
"2.4.1"
timelimit=
"5"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"6"
name=
"CVC4"
version=
"1.4"
timelimit=
"5"
steplimit=
"1"
memlimit=
"4000"
/>
...
...
@@ -31,16 +31,16 @@
<proof
prover=
"6"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
<goal
name=
"to_nat_of_zero2"
>
<proof
prover=
"
0
"
edited=
"bitvector_BitVector_to_nat_of_zero2_1.v"
><result
status=
"valid"
time=
"0.92"
/></proof>
<proof
prover=
"
1
"
edited=
"bitvector_BitVector_to_nat_of_zero2_1.v"
><result
status=
"valid"
time=
"0.92"
/></proof>
</goal>
<goal
name=
"to_nat_of_zero"
>
<proof
prover=
"
0
"
timelimit=
"30"
edited=
"bitvector_BitVector_to_nat_of_zero_1.v"
><result
status=
"valid"
time=
"
2.78
"
/></proof>
<proof
prover=
"
1
"
timelimit=
"30"
edited=
"bitvector_BitVector_to_nat_of_zero_1.v"
><result
status=
"valid"
time=
"
1.54
"
/></proof>
</goal>
<goal
name=
"to_nat_of_one"
>
<proof
prover=
"
0
"
edited=
"bitvector_BitVector_to_nat_of_one_1.v"
><result
status=
"valid"
time=
"1.
86
"
/></proof>
<proof
prover=
"
1
"
edited=
"bitvector_BitVector_to_nat_of_one_1.v"
><result
status=
"valid"
time=
"1.
12
"
/></proof>
</goal>
<goal
name=
"to_nat_sub_footprint"
>
<proof
prover=
"
0
"
timelimit=
"7"
edited=
"bitvector_BitVector_to_nat_sub_footprint_1.v"
><result
status=
"valid"
time=
"
3.73
"
/></proof>
<proof
prover=
"
1
"
timelimit=
"7"
edited=
"bitvector_BitVector_to_nat_sub_footprint_1.v"
><result
status=
"valid"
time=
"
2.98
"
/></proof>
</goal>
<goal
name=
"nth_from_int_low_even"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.02"
steps=
"68"
/></proof>
...
...
@@ -72,7 +72,7 @@
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.11"
/></proof>
</goal>
<goal
name=
"nth_from_int2c_plus_pow2"
>
<proof
prover=
"
0
"
timelimit=
"10"
edited=
"bitvector_BitVector_nth_from_int2c_plus_pow2_1.v"
><result
status=
"valid"
time=
"
1.28
"
/></proof>
<proof
prover=
"
1
"
timelimit=
"10"
edited=
"bitvector_BitVector_nth_from_int2c_plus_pow2_1.v"
><result
status=
"valid"
time=
"
0.75
"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.12"
steps=
"85"
/></proof>
</goal>
</theory>
...
...
@@ -108,91 +108,91 @@
<proof
prover=
"3"
timelimit=
"3"
><result
status=
"valid"
time=
"0.07"
/></proof>
<proof
prover=
"6"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.04"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"2.59"
/></proof>
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.
53
"
/></proof>
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.
78
"
/></proof>
</goal>
<goal
name=
"Test5"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.05"
steps=
"71"
/></proof>
<proof
prover=
"3"
timelimit=
"3"
><result
status=
"valid"
time=
"0.07"
/></proof>
<proof
prover=
"6"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.04"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"2.62"
/></proof>
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.
50
"
/></proof>
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.
77
"
/></proof>
</goal>
<goal
name=
"Test6"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.05"
steps=
"71"
/></proof>
<proof
prover=
"3"
timelimit=
"3"
><result
status=
"valid"
time=
"0.07"
/></proof>
<proof
prover=
"6"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.05"
/></proof>
<proof
prover=
"9"
timelimit=
"9"
><result
status=
"valid"
time=
"2.52"
/></proof>
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.
51
"
/></proof>
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.
78
"
/></proof>
</goal>
<goal
name=
"to_nat_0x00000000"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.04"
steps=
"78"
/></proof>
<proof
prover=
"3"
timelimit=
"3"
><result
status=
"valid"
time=
"0.10"
/></proof>
<proof
prover=
"6"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.05"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"
2.83
"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"
3.40
"
/></proof>
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.52"
/></proof>
</goal>
<goal
name=
"to_nat_0x00000001"
>
<proof
prover=
"6"
timelimit=
"120"
memlimit=
"1000"
><result
status=
"valid"
time=
"
74.45
"
/></proof>
<proof
prover=
"6"
timelimit=
"120"
memlimit=
"1000"
><result
status=
"valid"
time=
"
88.62
"
/></proof>
</goal>
<goal
name=
"to_nat_0x00000003"
>
<proof
prover=
"6"
timelimit=
"120"
memlimit=
"1000"
><result
status=
"valid"
time=
"
6
5.1
1
"
/></proof>
<proof
prover=
"6"
timelimit=
"120"
memlimit=
"1000"
><result
status=
"valid"
time=
"
7
5.1
6
"
/></proof>
</goal>
<goal
name=
"to_nat_0x00000007"
>
<proof
prover=
"6"
timelimit=
"60"
><result
status=
"valid"
time=
"54.99"
/></proof>
</goal>
<goal
name=
"to_nat_0x0000000F"
>
<proof
prover=
"6"
timelimit=
"120"
memlimit=
"1000"
><result
status=
"valid"
time=
"
49.69
"
/></proof>
<proof
prover=
"6"
timelimit=
"120"
memlimit=
"1000"
><result
status=
"valid"
time=
"
57.06
"
/></proof>
</goal>
<goal
name=
"to_nat_0x0000001F"
>
<proof
prover=
"6"
timelimit=
"30"
><result
status=
"valid"
time=
"
39.21
"
/></proof>
<proof
prover=
"6"
timelimit=
"30"
><result
status=
"valid"
time=
"
46.67
"
/></proof>
</goal>
<goal
name=
"to_nat_0x0000003F"
>
<proof
prover=
"6"
timelimit=
"30"
><result
status=
"valid"
time=
"3
1.79
"
/></proof>
<proof
prover=
"6"
timelimit=
"30"
><result
status=
"valid"
time=
"3
7.38
"
/></proof>
</goal>
<goal
name=
"to_nat_0x0000007F"
>
<proof
prover=
"6"
timelimit=
"30"
><result
status=
"valid"
time=
"26.44"
/></proof>
</goal>
<goal
name=
"to_nat_0x000000FF"
>
<proof
prover=
"6"
timelimit=
"30"
><result
status=
"valid"
time=
"2
1.52
"
/></proof>
<proof
prover=
"6"
timelimit=
"30"
><result
status=
"valid"
time=
"2
7.95
"
/></proof>
</goal>
<goal
name=
"to_nat_0x000001FF"
>
<proof
prover=
"6"
timelimit=
"30"
><result
status=
"valid"
time=
"
17.48
"
/></proof>
<proof
prover=
"6"
timelimit=
"30"
><result
status=
"valid"
time=
"
24.51
"
/></proof>
</goal>
<goal
name=
"to_nat_0x000003FF"
>
<proof
prover=
"6"
timelimit=
"30"
><result
status=
"valid"
time=
"14.09"
/></proof>
</goal>
<goal
name=
"to_nat_0x000007FF"
>
<proof
prover=
"6"
timelimit=
"30"
><result
status=
"valid"
time=
"1
1
.1
8
"
/></proof>
<proof
prover=
"6"
timelimit=
"30"
><result
status=
"valid"
time=
"1
6
.1
7
"
/></proof>
</goal>
<goal
name=
"to_nat_0x00000FFF"
>
<proof
prover=
"6"
timelimit=
"30"
><result
status=
"valid"
time=
"
8
.9
5
"
/></proof>
<proof
prover=
"6"
timelimit=
"30"
><result
status=
"valid"
time=
"
11
.9
6
"
/></proof>
</goal>
<goal
name=
"to_nat_0x00001FFF"
>
<proof
prover=
"6"
timelimit=
"30"
><result
status=
"valid"
time=
"6.88"
/></proof>
</goal>
<goal
name=
"to_nat_0x00003FFF"
>
<proof
prover=
"6"
timelimit=
"30"
><result
status=
"valid"
time=
"
5
.40"
/></proof>
<proof
prover=
"6"
timelimit=
"30"
><result
status=
"valid"
time=
"
7
.40"
/></proof>
</goal>
<goal
name=
"to_nat_0x00007FFF"
>
<proof
prover=
"6"
timelimit=
"30"
><result
status=
"valid"
time=
"
4
.2
0
"
/></proof>
<proof
prover=
"6"
timelimit=
"30"
><result
status=
"valid"
time=
"
6
.2
9
"
/></proof>
</goal>
<goal
name=
"to_nat_0x0000FFFF"
>
<proof
prover=
"6"
memlimit=
"1000"
><result
status=
"valid"
time=
"3.1
0
"
/></proof>
<proof
prover=
"6"
memlimit=
"1000"
><result
status=
"valid"
time=
"3.
7
1"
/></proof>
</goal>
<goal
name=
"to_nat_0x0001FFFF"
>
<proof
prover=
"6"
memlimit=
"1000"
><result
status=
"valid"
time=
"
2.42
"
/></proof>
<proof
prover=
"6"
memlimit=
"1000"
><result
status=
"valid"
time=
"
3.17
"
/></proof>
</goal>
<goal
name=
"to_nat_0x0003FFFF"
>
<proof
prover=
"6"
memlimit=
"1000"
><result
status=
"valid"
time=
"
1.81
"
/></proof>
<proof
prover=
"6"
memlimit=
"1000"
><result
status=
"valid"
time=
"
2.64
"
/></proof>
</goal>
<goal
name=
"to_nat_0x0007FFFF"
>
<proof
prover=
"6"
memlimit=
"1000"
><result
status=
"valid"
time=
"1.56"
/></proof>
</goal>
<goal
name=
"to_nat_0x000FFFFF"
>
<proof
prover=
"6"
memlimit=
"1000"
><result
status=
"valid"
time=
"1.
09
"
/></proof>
<proof
prover=
"6"
memlimit=
"1000"
><result
status=
"valid"
time=
"1.
45
"
/></proof>
</goal>
<goal
name=
"to_nat_0x00FFFFFF"
>
<proof
prover=
"6"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.
30
"
/></proof>
<proof
prover=
"6"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.
44
"
/></proof>
</goal>
<goal
name=
"to_nat_0xFFFFFFFF"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.04"
steps=
"78"
/></proof>
...
...
examples/bts/12934/why3session.xml
View file @
701397eb
...
...
@@ -2,11 +2,11 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"
1
"
name=
"Coq"
version=
"8.
4pl6
"
timelimit=
"10"
memlimit=
"0"
/>
<prover
id=
"
0
"
name=
"Coq"
version=
"8.
5
"
timelimit=
"10"
steplimit=
"1"
memlimit=
"0"
/>
<file
name=
"../12934.why"
expanded=
"true"
>
<theory
name=
"BTS12934"
sum=
"e32351513bba9a37f680056dd466bcee"
expanded=
"true"
>
<goal
name=
"t"
expanded=
"true"
>
<proof
prover=
"
1
"
edited=
"12934_BTS12934_t_1.v"
><result
status=
"valid"
time=
"0.
78
"
/></proof>
<proof
prover=
"
0
"
edited=
"12934_BTS12934_t_1.v"
><result
status=
"valid"
time=
"0.
40
"
/></proof>
</goal>
</theory>
</file>
...
...
examples/bts/13849/why3session.xml
View file @
701397eb
...
...
@@ -2,11 +2,11 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"
1
"
name=
"Coq"
version=
"8.
4pl6
"
timelimit=
"10"
steplimit=
"1"
memlimit=
"0"
/>
<prover
id=
"
0
"
name=
"Coq"
version=
"8.
5
"
timelimit=
"10"
steplimit=
"1"
memlimit=
"0"
/>
<file
name=
"../13849.why"
expanded=
"true"
>
<theory
name=
"T"
sum=
"fe6d0a97ed129807ad9b025e583a359d"
expanded=
"true"
>
<goal
name=
"x"
expanded=
"true"
>
<proof
prover=
"
1
"
edited=
"13849_T_x_2.v"
><result
status=
"valid"
time=
"0.
66
"
/></proof>
<proof
prover=
"
0
"
edited=
"13849_T_x_2.v"
><result
status=
"valid"
time=
"0.
40
"
/></proof>
</goal>
</theory>
</file>
...
...
examples/bts/13854/why3session.xml
View file @
701397eb
...
...
@@ -2,14 +2,14 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"
1
"
name=
"Coq"
version=
"8.
4pl6
"
timelimit=
"5"
memlimit=
"0"
/>
<prover
id=
"
0
"
name=
"Coq"
version=
"8.
5
"
timelimit=
"5"
steplimit=
"1"
memlimit=
"0"
/>
<file
name=
"../13854.why"
>
<theory
name=
"T"
sum=
"e0ed6fa44df780ea63fc8d3dbdece469"
expanded=
"true"
>
<goal
name=
"g"
expanded=
"true"
>
<proof
prover=
"
1
"
edited=
"13854_T_g_1.v"
><result
status=
"valid"
time=
"0.
77
"
/></proof>
<proof
prover=
"
0
"
edited=
"13854_T_g_1.v"
><result
status=
"valid"
time=
"0.
50
"
/></proof>
</goal>
<goal
name=
"x"
expanded=
"true"
>
<proof
prover=
"
1
"
edited=
"13854_T_x_1.v"
><result
status=
"valid"
time=
"0.
77
"
/></proof>
<proof
prover=
"
0
"
edited=
"13854_T_x_1.v"
><result
status=
"valid"
time=
"0.
50
"
/></proof>
</goal>
</theory>
</file>
...
...
examples/check-builtin/euclideandivision/why3session.xml
View file @
701397eb
...
...
@@ -2,25 +2,25 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"
3
"
name=
"
CVC
3"
version=
"
2
.4.
1
"
timelimit=
"
10
"
memlimit=
"0"
/>
<prover
id=
"
5
"
name=
"
Z
3"
version=
"
4.3
.1"
timelimit=
"
5
"
memlimit=
"
100
0"
/>
<prover
id=
"6"
name=
"Z3"
version=
"3.2"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"7"
name=
"Alt-Ergo"
version=
"0.99.1"
timelimit=
"3"
memlimit=
"1000"
/>
<prover
id=
"8"
name=
"CVC4"
version=
"1.4"
timelimit=
"5"
memlimit=
"1000"
/>
<prover
id=
"9"
name=
"Z3"
version=
"4.3.2"
timelimit=
"10"
memlimit=
"0"
/>
<prover
id=
"
0
"
name=
"
Z
3"
version=
"
4
.4.
0
"
timelimit=
"
5
"
memlimit=
"
400
0"
/>
<prover
id=
"
3
"
name=
"
CVC
3"
version=
"
2.4
.1"
timelimit=
"
10"
steplimit=
"1
"
memlimit=
"0"
/>
<prover
id=
"6"
name=
"Z3"
version=
"3.2"
timelimit=
"5"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"7"
name=
"Alt-Ergo"
version=
"0.99.1"
timelimit=
"3"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"8"
name=
"CVC4"
version=
"1.4"
timelimit=
"5"
steplimit=
"1"
memlimit=
"1000"
/>
<prover
id=
"9"
name=
"Z3"
version=
"4.3.2"
timelimit=
"10"
steplimit=
"1"
memlimit=
"0"
/>
<file
name=
"../euclideandivision.why"
expanded=
"true"
>
<theory
name=
"Test"
sum=
"34acc475394bbedc4a443071938d84bc"
expanded=
"true"
>
<goal
name=
"G1"
expanded=
"true"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"6"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.01"
steps=
"4"
/></proof>
<proof
prover=
"8"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.00"
/></proof>
</goal>
<goal
name=
"G2"
expanded=
"true"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"6"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.00"
steps=
"2"
/></proof>
<proof
prover=
"8"
><result
status=
"valid"
time=
"0.00"
/></proof>
...
...
examples/check-builtin/floats/why3session.xml
View file @
701397eb
...
...
@@ -2,32 +2,32 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"0"
name=
"CVC3"
version=
"2.4.1"
timelimit=
"5"
memlimit=
"0"
/>
<prover
id=
"
3
"
name=
"Gappa"
version=
"1.
1.1
"
timelimit=
"5"
memlimit=
"0"
/>
<prover
id=
"4"
name=
"Alt-Ergo"
version=
"0.99.1"
timelimit=
"5"
memlimit=
"0"
/>
<prover
id=
"5"
name=
"Z3"
version=
"4.3.2"
timelimit=
"5"
memlimit=
"0"
/>
<prover
id=
"0"
name=
"CVC3"
version=
"2.4.1"
timelimit=
"5"
steplimit=
"1"
memlimit=
"0"
/>
<prover
id=
"
1
"
name=
"Gappa"
version=
"1.
2.0
"
timelimit=
"5"
steplimit=
"1"
memlimit=
"0"
/>
<prover
id=
"4"
name=
"Alt-Ergo"
version=
"0.99.1"
timelimit=
"5"
steplimit=
"1"
memlimit=
"0"
/>
<prover
id=
"5"
name=
"Z3"
version=
"4.3.2"
timelimit=
"5"
steplimit=
"1"
memlimit=
"0"
/>
<file
name=
"../floats.why"
expanded=
"true"
>
<theory
name=
"TestGappa"
sum=
"ed330ba56218830382ea9b26d56f5cd1"
expanded=
"true"
>
<goal
name=
"Round_single_01"
expanded=
"true"
>
<proof
prover=
"
3
"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.00"
/></proof>
</goal>
<goal
name=
"Round_double_01"
expanded=
"true"
>
<proof
prover=
"
3
"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.00"
/></proof>
</goal>
<goal
name=
"Test00"
expanded=
"true"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"
3
"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.01"
steps=
"5"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"Test01"
expanded=
"true"
>
<proof
prover=
"
3
"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.00"
/></proof>
</goal>
<goal
name=
"Test02"
expanded=
"true"
>
<proof
prover=
"
3
"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.00"
/></proof>
</goal>
<goal
name=
"Test03"
expanded=
"true"
>
<proof
prover=
"
3
"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"
1
"
><result
status=
"valid"
time=
"0.00"
/></proof>
</goal>
</theory>
</file>
...
...
examples/check-builtin/intreal/why3session.xml
View file @
701397eb
...
...
@@ -2,57 +2,57 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"0"
name=
"CVC3"
version=
"2.4.1"
timelimit=
"10"
memlimit=
"0"
/>
<prover
id=
"
3
"
name=
"
Spass
"
version=
"
3.7
"
timelimit=
"1
0
"
memlimit=
"0"
/>
<prover
id=
"
6
"
name=
"
Z3
"
version=
"3.
2
"
timelimit=
"10"
memlimit=
"0"
/>
<prover
id=
"
7
"
name=
"
Gappa
"
version=
"
1.1.1
"
timelimit=
"
2
"
memlimit=
"0"
/>
<prover
id=
"8"
name=
"Alt-Ergo"
version=
"0.99.1"
timelimit=
"10"
memlimit=
"0"
/>
<prover
id=
"9"
name=
"Z3"
version=
"4.3.2"
timelimit=
"10"
memlimit=
"0"
/>
<prover
id=
"0"
name=
"CVC3"
version=
"2.4.1"
timelimit=
"10"
steplimit=
"1"
memlimit=
"0"
/>
<prover
id=
"
1
"
name=
"
Gappa
"
version=
"
1.2.0
"
timelimit=
"
2"
steplimit=
"
1"
memlimit=
"0"
/>
<prover
id=
"
3
"
name=
"
Spass
"
version=
"3.
7
"
timelimit=
"10"
steplimit=
"1"
memlimit=
"0"
/>
<prover
id=
"
6
"
name=
"
Z3
"
version=
"
3.2
"
timelimit=
"
10"
steplimit=
"1
"
memlimit=
"0"
/>
<prover
id=
"8"
name=
"Alt-Ergo"
version=
"0.99.1"
timelimit=
"10"
steplimit=
"1"
memlimit=
"0"
/>
<prover
id=
"9"
name=
"Z3"
version=
"4.3.2"
timelimit=
"10"
steplimit=
"1"
memlimit=
"0"
/>
<file
name=
"../intreal.why"
expanded=
"true"
>
<theory
name=
"IntReal"
sum=
"3622340391eb2916078d6fa44290f09a"
expanded=
"true"
>
<goal
name=
"G1"
expanded=
"true"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"6"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"8"
><result
status=
"valid"
time=
"0.06"
steps=
"34"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.00"
/></proof>
</goal>
<goal
name=
"G2"
expanded=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"6"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"8"
><result
status=
"valid"
time=
"0.14"
steps=
"97"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"G3"
expanded=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"6"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"8"
><result
status=
"valid"
time=
"0.17"
steps=
"100"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
<goal
name=
"G4"
expanded=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"6"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"8"
><result
status=
"valid"
time=
"0.48"
steps=
"142"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
<goal
name=
"G5"
expanded=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"6"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"8"
><result
status=
"valid"
time=
"0.46"
steps=
"142"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
<goal
name=
"G6"
expanded=
"true"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.10"
/></proof>
<proof
prover=
"6"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"8"
><result
status=
"valid"
time=
"0.06"
steps=
"63"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
<goal
name=
"G7"
expanded=
"true"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"6"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.00"
/></proof>
<proof
prover=
"8"
><result
status=
"valid"
time=
"0.01"
steps=
"5"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
...
...
examples/check-builtin/propositional/why3session.xml
View file @
701397eb
...
...
@@ -2,15 +2,15 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"0"
name=
"CVC3"
version=
"2.4.1"
timelimit=
"10"
memlimit=
"0"
/>
<prover
id=
"
2
"
name=
"Z3"
version=
"
2.19
"
timelimit=
"10"
memlimit=
"0"
/>
<prover
id=
"3"
name=
"Spass"
version=
"3.7"
timelimit=
"10"
memlimit=
"0"
/>
<prover
id=
"4"
name=
"Alt-Ergo"
version=
"0.99.1"
timelimit=
"10"
memlimit=
"0"
/>
<prover
id=
"0"
name=
"CVC3"
version=
"2.4.1"
timelimit=
"10"
steplimit=
"1"
memlimit=
"0"
/>
<prover
id=
"
1
"
name=
"Z3"
version=
"
3.2
"
timelimit=
"10"
steplimit=
"1"
memlimit=
"0"
/>
<prover
id=
"3"
name=
"Spass"
version=
"3.7"
timelimit=
"10"
steplimit=
"1"
memlimit=
"0"