Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
119
Issues
119
List
Boards
Labels
Service Desk
Milestones
Merge Requests
16
Merge Requests
16
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
f181fd76
Commit
f181fd76
authored
May 19, 2017
by
MARCHE Claude
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
updated sessions related to bitvectors
parent
2a84e635
Changes
7
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
7 changed files
with
357 additions
and
331 deletions
+357
-331
examples/TODO
examples/TODO
+0
-3
examples/esterel/why3session.xml
examples/esterel/why3session.xml
+41
-38
examples/esterel/why3shapes.gz
examples/esterel/why3shapes.gz
+0
-0
examples/hackers-delight/why3session.xml
examples/hackers-delight/why3session.xml
+74
-50
examples/hackers-delight/why3shapes.gz
examples/hackers-delight/why3shapes.gz
+0
-0
examples/queens_bv/why3session.xml
examples/queens_bv/why3session.xml
+242
-240
examples/queens_bv/why3shapes.gz
examples/queens_bv/why3shapes.gz
+0
-0
No files found.
examples/TODO
View file @
f181fd76
...
...
@@ -4,12 +4,10 @@ bignum.mlw
counting_sort.mlw
cursor.mlw
dijkstra.mlw
esterel.mlw
ewd673.mlw
fibonacci.mlw
find.mlw
gcd.mlw
hackers-delight.mlw
hashtbl_impl.mlw
ieee_float.mlw
kmp.mlw
...
...
@@ -17,7 +15,6 @@ knuth_prime_numbers.mlw
koda_ruskey.mlw
linked_list_rev.mlw
optimal_replay.mlw
queens_bv.mlw
queens.mlw
random_access_list.mlw
residual.mlw
...
...
examples/esterel/why3session.xml
View file @
f181fd76
...
...
@@ -4,65 +4,68 @@
<why3session
shape_version=
"4"
>
<prover
id=
"0"
name=
"CVC4"
version=
"1.4"
timelimit=
"5"
steplimit=
"4000"
memlimit=
"4000"
/>
<prover
id=
"1"
name=
"Alt-Ergo"
version=
"1.01"
timelimit=
"5"
steplimit=
"4000"
memlimit=
"4000"
/>
<prover
id=
"
3"
name=
"Z3"
version=
"4.5.0
"
timelimit=
"5"
steplimit=
"4000"
memlimit=
"4000"
/>
<prover
id=
"
2"
name=
"Z3"
version=
"4.4.1
"
timelimit=
"5"
steplimit=
"4000"
memlimit=
"4000"
/>
<file
name=
"../esterel.mlw"
expanded=
"true"
>
<theory
name=
"Esterel"
sum=
"
9f8fa8eee909c60475c4373c5616d837
"
expanded=
"true"
>
<goal
name=
"
WP_parameter union"
expl=
"VC for union"
expanded=
"true
"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.16"
steps=
"
220
"
/></proof>
<theory
name=
"Esterel"
sum=
"
1b203f09cfa5ce87bbfdb875a8522626
"
expanded=
"true"
>
<goal
name=
"
VC union"
expl=
"VC for union
"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.16"
steps=
"
197
"
/></proof>
</goal>
<goal
name=
"
WP_parameter intersection"
expl=
"VC for intersection"
expanded=
"true
"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.18"
steps=
"1
98
"
/></proof>
<goal
name=
"
VC intersection"
expl=
"VC for intersection
"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.18"
steps=
"1
75
"
/></proof>
</goal>
<goal
name=
"
WP_parameter aboveMin"
expl=
"VC for aboveMin"
expanded=
"true
"
>
<transf
name=
"split_goal_wp"
expanded=
"true"
>
<goal
name=
"
WP_parameter aboveMin.1"
expl=
"1. assertion"
expanded=
"true
"
>
<proof
prover=
"
1"
><result
status=
"valid"
time=
"0.15"
steps=
"225
"
/></proof>
<goal
name=
"
VC aboveMin"
expl=
"VC for aboveMin
"
>
<transf
name=
"split_goal_wp"
>
<goal
name=
"
VC aboveMin.1"
expl=
"1. precondition
"
>
<proof
prover=
"
2"
timelimit=
"1"
steplimit=
"0"
memlimit=
"1000"
><result
status=
"valid"
time=
"0.01
"
/></proof>
</goal>
<goal
name=
"WP_parameter aboveMin.2"
expl=
"2. assertion"
expanded=
"true"
>
<goal
name=
"VC aboveMin.2"
expl=
"2. assertion"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.15"
steps=
"220"
/></proof>
</goal>
<goal
name=
"VC aboveMin.3"
expl=
"3. assertion"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.22"
/></proof>
<proof
prover=
"
3"
><result
status=
"valid"
time=
"0.28
"
/></proof>
<proof
prover=
"
2"
><result
status=
"valid"
time=
"0.52
"
/></proof>
</goal>
<goal
name=
"
WP_parameter aboveMin.3"
expl=
"3. assertion"
expanded=
"true
"
>
<goal
name=
"
VC aboveMin.4"
expl=
"4. assertion
"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.42"
/></proof>
</goal>
<goal
name=
"
WP_parameter aboveMin.4"
expl=
"4. type invariant"
expanded=
"true
"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.30"
steps=
"3
36
"
/></proof>
<goal
name=
"
VC aboveMin.5"
expl=
"5. precondition
"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.30"
steps=
"3
03
"
/></proof>
</goal>
<goal
name=
"
WP_parameter aboveMin.5"
expl=
"5. postcondition"
expanded=
"true
"
>
<goal
name=
"
VC aboveMin.6"
expl=
"6. postcondition
"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.02"
steps=
"7
0
"
/></proof>
<proof
prover=
"
3
"
><result
status=
"valid"
time=
"0.01"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.02"
steps=
"7
6
"
/></proof>
<proof
prover=
"
2
"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"
WP_parameter maxUnion"
expl=
"VC for maxUnion"
expanded=
"true
"
>
<transf
name=
"split_goal_wp"
expanded=
"true"
>
<goal
name=
"
WP_parameter maxUnion.1"
expl=
"1. precondition"
expanded=
"true
"
>
<goal
name=
"
VC maxUnion"
expl=
"VC for maxUnion
"
>
<transf
name=
"split_goal_wp"
>
<goal
name=
"
VC maxUnion.1"
expl=
"1. precondition
"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.05"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.0
1"
steps=
"72
"
/></proof>
<proof
prover=
"
3"
><result
status=
"valid"
time=
"0.01
"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.0
2"
steps=
"71
"
/></proof>
<proof
prover=
"
2"
><result
status=
"valid"
time=
"0.02
"
/></proof>
</goal>
<goal
name=
"
WP_parameter maxUnion.2"
expl=
"2. precondition"
expanded=
"true
"
>
<goal
name=
"
VC maxUnion.2"
expl=
"2. precondition
"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.05"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.0
2"
steps=
"73
"
/></proof>
<proof
prover=
"
3"
><result
status=
"valid"
time=
"0.02
"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.0
1"
steps=
"72
"
/></proof>
<proof
prover=
"
2"
><result
status=
"valid"
time=
"0.01
"
/></proof>
</goal>
<goal
name=
"
WP_parameter maxUnion.3"
expl=
"3. assertion"
expanded=
"true
"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.
13
"
/></proof>
<proof
prover=
"
3"
><result
status=
"valid"
time=
"0.33
"
/></proof>
<goal
name=
"
VC maxUnion.3"
expl=
"3. assertion
"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.
25
"
/></proof>
<proof
prover=
"
2"
><result
status=
"valid"
time=
"0.60
"
/></proof>
</goal>
<goal
name=
"
WP_parameter maxUnion.4"
expl=
"4. postcondition"
expanded=
"true
"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.
14
"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"1.
27"
steps=
"1464
"
/></proof>
<goal
name=
"
VC maxUnion.4"
expl=
"4. postcondition
"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.
27
"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"1.
54"
steps=
"1796
"
/></proof>
</goal>
<goal
name=
"
WP_parameter maxUnion.5"
expl=
"5. postcondition"
expanded=
"true
"
>
<transf
name=
"split_goal_wp"
expanded=
"true"
>
<goal
name=
"
WP_parameter maxUnion.5.1"
expl=
"1. postcondition"
expanded=
"true
"
>
<goal
name=
"
VC maxUnion.5"
expl=
"5. postcondition
"
>
<transf
name=
"split_goal_wp"
>
<goal
name=
"
VC maxUnion.5.1"
expl=
"1. postcondition
"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.06"
/></proof>
</goal>
<goal
name=
"
WP_parameter maxUnion.5.2"
expl=
"2. postcondition"
expanded=
"true
"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.
16
"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.
23"
steps=
"388
"
/></proof>
<goal
name=
"
VC maxUnion.5.2"
expl=
"2. postcondition
"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.
34
"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.
52"
steps=
"531
"
/></proof>
</goal>
</transf>
</goal>
...
...
examples/esterel/why3shapes.gz
View file @
f181fd76
No preview for this file type
examples/hackers-delight/why3session.xml
View file @
f181fd76
...
...
@@ -4,70 +4,94 @@
<why3session
shape_version=
"4"
>
<prover
id=
"0"
name=
"Alt-Ergo"
version=
"1.30"
timelimit=
"1"
steplimit=
"0"
memlimit=
"4000"
/>
<prover
id=
"1"
name=
"CVC4"
version=
"1.4"
timelimit=
"5"
steplimit=
"0"
memlimit=
"1000"
/>
<prover
id=
"2"
name=
"Z3"
version=
"4.5.0"
timelimit=
"5"
steplimit=
"0"
memlimit=
"1000"
/>
<prover
id=
"3"
name=
"Z3"
version=
"4.4.0"
timelimit=
"5"
steplimit=
"0"
memlimit=
"1000"
/>
<prover
id=
"4"
name=
"Z3"
version=
"4.4.1"
timelimit=
"
5
"
steplimit=
"0"
memlimit=
"1000"
/>
<prover
id=
"4"
name=
"Z3"
version=
"4.4.1"
timelimit=
"
1
"
steplimit=
"0"
memlimit=
"1000"
/>
<prover
id=
"5"
name=
"CVC4"
version=
"1.4"
alternative=
"noBV"
timelimit=
"5"
steplimit=
"0"
memlimit=
"1000"
/>
<prover
id=
"6"
name=
"Z3"
version=
"4.5.0"
alternative=
"noBV"
timelimit=
"5"
steplimit=
"0"
memlimit=
"1000"
/>
<prover
id=
"7"
name=
"Alt-Ergo"
version=
"1.01"
timelimit=
"5"
steplimit=
"0"
memlimit=
"1000"
/>
<prover
id=
"8"
name=
"Z3"
version=
"4.3.2"
timelimit=
"5"
steplimit=
"0"
memlimit=
"1000"
/>
<prover
id=
"9"
name=
"Z3"
version=
"4.4.1"
alternative=
"noBV"
timelimit=
"5"
steplimit=
"0"
memlimit=
"1000"
/>
<file
name=
"../hackers-delight.mlw"
expanded=
"true"
>
<theory
name=
"Utils"
sum=
"d41d8cd98f00b204e9800998ecf8427e"
>
<theory
name=
"Utils"
sum=
"64594dbb34442cbedbefba55bb980d5a"
>
<goal
name=
"VC one"
expl=
"VC for one"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
<goal
name=
"VC two"
expl=
"VC for two"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
<goal
name=
"VC lastbit"
expl=
"VC for lastbit"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
<goal
name=
"VC count"
expl=
"VC for count"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.01"
/></proof>
</goal>
</theory>
<theory
name=
"Utils_Spec"
sum=
"
dbfb25729f606aabb7a0a4256fe408c7"
expanded=
"true
"
>
<theory
name=
"Utils_Spec"
sum=
"
c762b40e892254317e70b85c2f78ad12
"
>
<goal
name=
"countZero"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
<goal
name=
"numOfZero"
>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.
18"
steps=
"206
"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.
36"
steps=
"252
"
/></proof>
</goal>
<goal
name=
"countStep"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"3.12"
/></proof>
<transf
name=
"split_goal_wp"
>
<goal
name=
"countStep.1"
expl=
"1."
>
<proof
prover=
"1"
timelimit=
"10"
memlimit=
"4000"
><result
status=
"valid"
time=
"4.00"
/></proof>
</goal>
<goal
name=
"countStep.2"
expl=
"2."
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.32"
/></proof>
</goal>
<goal
name=
"countStep.3"
expl=
"3."
>
<proof
prover=
"1"
timelimit=
"10"
memlimit=
"4000"
><result
status=
"valid"
time=
"2.94"
/></proof>
</goal>
<goal
name=
"countStep.4"
expl=
"4."
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.45"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"
WP_parameter
numof_shift"
expl=
"VC for numof_shift"
>
<goal
name=
"
VC
numof_shift"
expl=
"VC for numof_shift"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.24"
/></proof>
</goal>
<goal
name=
"WP_parameter countSpec_Aux"
expl=
"VC for countSpec_Aux"
expanded=
"true"
>
<transf
name=
"split_goal_wp"
expanded=
"true"
>
<goal
name=
"WP_parameter countSpec_Aux.1"
expl=
"1. postcondition"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
<goal
name=
"WP_parameter countSpec_Aux.2"
expl=
"2. variant decrease"
>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.23"
steps=
"253"
/></proof>
<goal
name=
"VC countSpec_Aux"
expl=
"VC for countSpec_Aux"
>
<transf
name=
"split_goal_wp"
>
<goal
name=
"VC countSpec_Aux.1"
expl=
"1. variant decrease"
>
<transf
name=
"split_goal_wp"
>
<goal
name=
"VC countSpec_Aux.1.1"
expl=
"1. variant decrease"
>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.33"
steps=
"237"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"
WP_parameter countSpec_Aux.3"
expl=
"3
. assertion"
>
<goal
name=
"
VC countSpec_Aux.2"
expl=
"2
. assertion"
>
<transf
name=
"split_goal_wp"
>
<goal
name=
"
WP_parameter countSpec_Aux.3
.1"
expl=
"1. assertion"
>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.45"
steps=
"454
"
/></proof>
<goal
name=
"
VC countSpec_Aux.2
.1"
expl=
"1. assertion"
>
<proof
prover=
"7"
timelimit=
"1"
><result
status=
"valid"
time=
"0.56"
steps=
"490
"
/></proof>
</goal>
<goal
name=
"
WP_parameter countSpec_Aux.3
.2"
expl=
"2. assertion"
>
<proof
prover=
"
7"
><result
status=
"valid"
time=
"0.54"
steps=
"532
"
/></proof>
<goal
name=
"
VC countSpec_Aux.2
.2"
expl=
"2. assertion"
>
<proof
prover=
"
1"
timelimit=
"1"
><result
status=
"valid"
time=
"0.27
"
/></proof>
</goal>
<goal
name=
"
WP_parameter countSpec_Aux.3
.3"
expl=
"3. assertion"
>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.83"
steps=
"541
"
/></proof>
<goal
name=
"
VC countSpec_Aux.2
.3"
expl=
"3. assertion"
>
<proof
prover=
"7"
timelimit=
"1"
><result
status=
"valid"
time=
"0.90"
steps=
"543
"
/></proof>
</goal>
<goal
name=
"
WP_parameter countSpec_Aux.3
.4"
expl=
"4. assertion"
>
<proof
prover=
"5"
timelimit=
"6"
memlimit=
"4500"
><result
status=
"valid"
time=
"2.50
"
/></proof>
<goal
name=
"
VC countSpec_Aux.2
.4"
expl=
"4. assertion"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"3.06
"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"WP_parameter countSpec_Aux.4"
expl=
"4. postcondition"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.31"
/></proof>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.11"
/></proof>
<goal
name=
"VC countSpec_Aux.3"
expl=
"3. postcondition"
>
<proof
prover=
"1"
timelimit=
"1"
><result
status=
"valid"
time=
"0.61"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"countSpec"
>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.05"
steps=
"81"
/></proof>
</goal>
<goal
name=
"
WP_parameter
hamming_spec"
expl=
"VC for hamming_spec"
>
<goal
name=
"
VC
hamming_spec"
expl=
"VC for hamming_spec"
>
<transf
name=
"split_goal_wp"
>
<goal
name=
"
WP_parameter
hamming_spec.1"
expl=
"1. assertion"
>
<goal
name=
"
VC
hamming_spec.1"
expl=
"1. assertion"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"
WP_parameter
hamming_spec.2"
expl=
"2. postcondition"
>
<goal
name=
"
VC
hamming_spec.2"
expl=
"2. postcondition"
>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"4"
timelimit=
"5"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
</transf>
</goal>
...
...
@@ -77,40 +101,40 @@
<goal
name=
"separation"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.19"
/></proof>
</goal>
<goal
name=
"
WP_parameter
numof_or"
expl=
"VC for numof_or"
>
<goal
name=
"
VC
numof_or"
expl=
"VC for numof_or"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.48"
/></proof>
</goal>
<goal
name=
"
WP_parameter
triangleInequalityInt"
expl=
"VC for triangleInequalityInt"
>
<goal
name=
"
VC
triangleInequalityInt"
expl=
"VC for triangleInequalityInt"
>
<transf
name=
"split_goal_wp"
>
<goal
name=
"
WP_parameter
triangleInequalityInt.1"
expl=
"1. assertion"
>
<goal
name=
"
VC
triangleInequalityInt.1"
expl=
"1. assertion"
>
<transf
name=
"split_goal_wp"
>
<goal
name=
"
WP_parameter
triangleInequalityInt.1.1"
expl=
"1. VC for triangleInequalityInt"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.
49
"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.17"
steps=
"21
9
"
/></proof>
<goal
name=
"
VC
triangleInequalityInt.1.1"
expl=
"1. VC for triangleInequalityInt"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.
91
"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.17"
steps=
"21
7
"
/></proof>
</goal>
<goal
name=
"
WP_parameter
triangleInequalityInt.1.2"
expl=
"2. VC for triangleInequalityInt"
>
<goal
name=
"
VC
triangleInequalityInt.1.2"
expl=
"2. VC for triangleInequalityInt"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.21"
/></proof>
<proof
prover=
"
6"
><result
status=
"valid"
time=
"0.64
"
/></proof>
<proof
prover=
"
7"
><result
status=
"valid"
time=
"0.70"
steps=
"468
"
/></proof>
<proof
prover=
"
8"
><result
status=
"valid"
time=
"0.65
"
/></proof>
<proof
prover=
"
7"
><result
status=
"valid"
time=
"0.70"
steps=
"280
"
/></proof>
<proof
prover=
"
8"
><result
status=
"valid"
time=
"0.95
"
/></proof>
<proof
prover=
"
9"
><result
status=
"valid"
time=
"0.64
"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"
WP_parameter
triangleInequalityInt.2"
expl=
"2. postcondition"
>
<goal
name=
"
VC
triangleInequalityInt.2"
expl=
"2. postcondition"
>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.05"
steps=
"146"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"triangleInequality"
expanded=
"true"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.
39"
steps=
"723
"
/></proof>
<goal
name=
"triangleInequality"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.
55"
steps=
"637
"
/></proof>
</goal>
</theory>
<theory
name=
"Hackers_delight"
sum=
"
c0f28015432daa6163200c3d45c0f1e6"
expanded=
"true
"
>
<goal
name=
"
WP_parameter
ascii"
expl=
"VC for ascii"
>
<theory
name=
"Hackers_delight"
sum=
"
7696378314ab14595555f7fee9f70833
"
>
<goal
name=
"
VC
ascii"
expl=
"VC for ascii"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.09"
/></proof>
</goal>
<goal
name=
"asciiProp"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"
0.73
"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"
1.14
"
/></proof>
</goal>
<goal
name=
"iso"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.43"
/></proof>
...
...
@@ -119,7 +143,7 @@
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.09"
/></proof>
</goal>
<goal
name=
"nthGray"
>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.
76"
steps=
"870
"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.
45"
steps=
"375
"
/></proof>
</goal>
<goal
name=
"lastNthGray"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
...
...
@@ -161,13 +185,13 @@
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.06"
/></proof>
</goal>
<goal
name=
"Ac"
>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.
41"
steps=
"454
"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.
67"
steps=
"465
"
/></proof>
</goal>
<goal
name=
"Ad"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.06"
/></proof>
</goal>
<goal
name=
"Ae"
>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.05"
steps=
"
79
"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.05"
steps=
"
80
"
/></proof>
</goal>
<goal
name=
"Af"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.03"
/></proof>
...
...
examples/hackers-delight/why3shapes.gz
View file @
f181fd76
No preview for this file type
examples/queens_bv/why3session.xml
View file @
f181fd76
This diff is collapsed.
Click to expand it.
examples/queens_bv/why3shapes.gz
View file @
f181fd76
No preview for this file type
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment