Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
2e1cc466
Commit
2e1cc466
authored
May 18, 2012
by
MARCHE Claude
Browse files
updated sessions
parent
5302f41d
Changes
102
Expand all
Hide whitespace changes
Inline
Side-by-side
examples/bitvectors/bitvector/why3session.xml
View file @
2e1cc466
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/
home/marche/why3/share
/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/
usr/local/share/why3
/why3session.dtd">
<why3session
name=
"bitvectors/bitvector/why3session.xml"
>
<prover
...
...
@@ -54,7 +54,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
0
"
/>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
<proof
prover=
"0"
...
...
@@ -62,7 +62,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.2
0
"
/>
<result
status=
"valid"
time=
"0.2
1
"
/>
</proof>
<proof
prover=
"2"
...
...
@@ -70,7 +70,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
0
"
/>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
</goal>
<goal
...
...
@@ -120,7 +120,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
5
"
/>
<result
status=
"valid"
time=
"0.0
4
"
/>
</proof>
<proof
prover=
"2"
...
...
@@ -145,7 +145,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
0
"
/>
<result
status=
"valid"
time=
"0.0
1
"
/>
</proof>
<proof
prover=
"0"
...
...
@@ -179,7 +179,7 @@
edited=
"bitvector_BitVector_to_nat_of_zero2_1.v"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"1.
1
2"
/>
<result
status=
"valid"
time=
"1.2
0
"
/>
</proof>
</goal>
<goal
...
...
@@ -197,7 +197,7 @@
edited=
"bitvector_BitVector_to_nat_of_zero_1.v"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.
7
8"
/>
<result
status=
"valid"
time=
"0.8
5
"
/>
</proof>
</goal>
<goal
...
...
@@ -215,7 +215,7 @@
edited=
"bitvector_BitVector_to_nat_of_one_1.v"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.
86
"
/>
<result
status=
"valid"
time=
"0.
93
"
/>
</proof>
</goal>
<goal
...
...
@@ -233,7 +233,7 @@
edited=
"bitvector_BitVector_to_nat_sub_footprint_1.v"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"1.
68
"
/>
<result
status=
"valid"
time=
"1.
74
"
/>
</proof>
</goal>
<goal
...
...
@@ -258,7 +258,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.2
4
"
/>
<result
status=
"valid"
time=
"0.2
6
"
/>
</proof>
<proof
prover=
"2"
...
...
@@ -291,7 +291,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.
19
"
/>
<result
status=
"valid"
time=
"0.
20
"
/>
</proof>
<proof
prover=
"2"
...
...
@@ -299,7 +299,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
6
"
/>
<result
status=
"valid"
time=
"0.0
7
"
/>
</proof>
</goal>
<goal
...
...
@@ -324,7 +324,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
3
"
/>
<result
status=
"valid"
time=
"0.0
4
"
/>
</proof>
<proof
prover=
"2"
...
...
@@ -357,7 +357,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.
58
"
/>
<result
status=
"valid"
time=
"0.
60
"
/>
</proof>
<proof
prover=
"2"
...
...
@@ -390,7 +390,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.6
0
"
/>
<result
status=
"valid"
time=
"0.6
2
"
/>
</proof>
<proof
prover=
"2"
...
...
@@ -398,7 +398,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.1
1
"
/>
<result
status=
"valid"
time=
"0.1
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -423,7 +423,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
7
"
/>
<result
status=
"valid"
time=
"0.0
8
"
/>
</proof>
<proof
prover=
"2"
...
...
@@ -456,7 +456,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.
1
2"
/>
<result
status=
"timeout"
time=
"5.
0
2"
/>
</proof>
<proof
prover=
"0"
...
...
@@ -488,7 +488,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
</goal>
</theory>
...
...
@@ -541,7 +541,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.1
8
"
/>
<result
status=
"valid"
time=
"0.1
9
"
/>
</proof>
</goal>
<goal
...
...
@@ -566,7 +566,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
2
"
/>
<result
status=
"valid"
time=
"0.0
3
"
/>
</proof>
</goal>
<goal
...
...
@@ -641,7 +641,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.0
2
"
/>
<result
status=
"valid"
time=
"0.0
3
"
/>
</proof>
</goal>
<goal
...
...
@@ -732,7 +732,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"6"
...
...
@@ -740,7 +740,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -765,7 +765,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"0"
...
...
@@ -781,7 +781,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"6"
...
...
@@ -789,7 +789,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -823,7 +823,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"0"
...
...
@@ -839,7 +839,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"6"
...
...
@@ -847,7 +847,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -888,7 +888,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"6"
...
...
@@ -896,7 +896,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -921,7 +921,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"0"
...
...
@@ -937,7 +937,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"6"
...
...
@@ -945,7 +945,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -978,7 +978,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
2
"
/>
<result
status=
"timeout"
time=
"5.0
1
"
/>
</proof>
<proof
prover=
"2"
...
...
@@ -986,7 +986,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"6"
...
...
@@ -994,7 +994,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -1019,7 +1019,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"0"
...
...
@@ -1035,7 +1035,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"6"
...
...
@@ -1043,7 +1043,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -1068,7 +1068,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"0"
...
...
@@ -1076,7 +1076,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
2
"
/>
<result
status=
"timeout"
time=
"5.0
1
"
/>
</proof>
<proof
prover=
"2"
...
...
@@ -1092,7 +1092,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -1117,7 +1117,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"0"
...
...
@@ -1133,7 +1133,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"6"
...
...
@@ -1141,7 +1141,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -1166,7 +1166,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"0"
...
...
@@ -1182,7 +1182,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"6"
...
...
@@ -1190,7 +1190,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -1215,7 +1215,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"0"
...
...
@@ -1231,7 +1231,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"6"
...
...
@@ -1239,7 +1239,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -1264,7 +1264,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"0"
...
...
@@ -1280,7 +1280,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"6"
...
...
@@ -1288,7 +1288,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -1313,7 +1313,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"0"
...
...
@@ -1329,7 +1329,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"6"
...
...
@@ -1337,7 +1337,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -1362,7 +1362,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"0"
...
...
@@ -1378,7 +1378,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"6"
...
...
@@ -1386,7 +1386,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -1411,7 +1411,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"0"
...
...
@@ -1427,7 +1427,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"6"
...
...
@@ -1435,7 +1435,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -1460,7 +1460,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"0"
...
...
@@ -1476,7 +1476,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"6"
...
...
@@ -1484,7 +1484,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -1509,7 +1509,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"0"
...
...
@@ -1525,7 +1525,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"6"
...
...
@@ -1533,7 +1533,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -1558,7 +1558,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"0"
...
...
@@ -1574,7 +1574,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
<proof
prover=
"6"
...
...
@@ -1582,7 +1582,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.0
1
"
/>
<result
status=
"timeout"
time=
"5.0
2
"
/>
</proof>
</goal>
<goal
...
...
@@ -1607,7 +1607,7 @@
memlimit=
"1000"
obsolete=
"false"