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
a9dc92ad
Commit
a9dc92ad
authored
Oct 29, 2012
by
MARCHE Claude
Browse files
support for Z3 4.2
parent
b654ea31
Changes
4
Hide whitespace changes
Inline
Side-by-side
examples/einstein/why3session.xml
View file @
a9dc92ad
...
...
@@ -45,6 +45,14 @@
id=
"10"
name=
"Z3"
version=
"3.2"
/>
<prover
id=
"11"
name=
"Z3"
version=
"4.0"
/>
<prover
id=
"12"
name=
"Z3"
version=
"4.2"
/>
<file
name=
"../einstein.why"
verified=
"false"
...
...
@@ -178,6 +186,22 @@
archived=
"false"
>
<result
status=
"valid"
time=
"0.06"
/>
</proof>
<proof
prover=
"11"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.07"
/>
</proof>
<proof
prover=
"12"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.08"
/>
</proof>
</goal>
<goal
name=
"Wrong"
...
...
@@ -275,6 +299,22 @@
archived=
"false"
>
<result
status=
"timeout"
time=
"2.00"
/>
</proof>
<proof
prover=
"11"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.05"
/>
</proof>
<proof
prover=
"12"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.04"
/>
</proof>
</goal>
<goal
name=
"G2"
...
...
@@ -372,6 +412,22 @@
archived=
"false"
>
<result
status=
"valid"
time=
"0.05"
/>
</proof>
<proof
prover=
"11"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.07"
/>
</proof>
<proof
prover=
"12"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.07"
/>
</proof>
</goal>
</theory>
</file>
...
...
examples/genealogy/why3session.xml
View file @
a9dc92ad
...
...
@@ -39,6 +39,14 @@
version=
"3.2"
/>
<prover
id=
"9"
name=
"Z3"
version=
"4.0"
/>
<prover
id=
"10"
name=
"Z3"
version=
"4.2"
/>
<prover
id=
"11"
name=
"Zenon"
version=
"0.7.1"
/>
<file
...
...
@@ -137,6 +145,22 @@
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"10"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.03"
/>
</proof>
<proof
prover=
"11"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.33"
/>
</proof>
</goal>
...
...
@@ -226,6 +250,22 @@
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"10"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"11"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"2.10"
/>
</proof>
</goal>
...
...
@@ -315,6 +355,22 @@
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"10"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"11"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.30"
/>
</proof>
</goal>
...
...
@@ -388,6 +444,22 @@
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"10"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.03"
/>
</proof>
<proof
prover=
"11"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.25"
/>
</proof>
</goal>
...
...
@@ -477,6 +549,22 @@
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"10"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.03"
/>
</proof>
<proof
prover=
"11"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"6.59"
/>
</proof>
</goal>
...
...
@@ -566,6 +654,22 @@
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.01"
/>
</proof>
<proof
prover=
"10"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.03"
/>
</proof>
<proof
prover=
"11"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.27"
/>
</proof>
</goal>
...
...
@@ -647,6 +751,22 @@
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.01"
/>
</proof>
<proof
prover=
"10"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.03"
/>
</proof>
<proof
prover=
"11"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.38"
/>
</proof>
</goal>
...
...
examples/programs/isqrt/why3session.xml
View file @
a9dc92ad
...
...
@@ -29,6 +29,14 @@
id=
"6"
name=
"Z3"
version=
"3.2"
/>
<prover
id=
"7"
name=
"Z3"
version=
"4.0"
/>
<prover
id=
"8"
name=
"Z3"
version=
"4.2"
/>
<file
name=
"../isqrt.mlw"
verified=
"false"
...
...
@@ -38,7 +46,7 @@
locfile=
"../isqrt.mlw"
loclnum=
"4"
loccnumb=
"7"
loccnume=
"13"
verified=
"true"
expanded=
"
fals
e"
>
expanded=
"
tru
e"
>
<goal
name=
"WP_parameter isqrt"
locfile=
"../isqrt.mlw"
...
...
@@ -46,7 +54,7 @@
expl=
"parameter isqrt"
sum=
"64277e54f36ba5a32dedb1a194a25f0d"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"iainfix <=V1V0ainfix <ainfix -V0V3ainfix -V0V2Aainfix <=c0ainfix -V0V2Aainfix =V4asqrainfix +V3c1Aainfix >=V0asqrV3Aainfix >=V3c0Iainfix =V4ainfix +ainfix +V1ainfix *c2V3c1FIainfix =V3ainfix +V2c1Fainfix <V0asqrainfix +V2c1Aainfix <=asqrV2V0Aainfix >=V2c0Iainfix =V1asqrainfix +V2c1Aainfix >=V0asqrV2Aainfix >=V2c0FAainfix =c1asqrainfix +c0c1Aainfix >=V0asqrc0Aainfix >=c0c0Iainfix >=V0c0F"
>
<label
name=
"expl:parameter isqrt"
/>
...
...
@@ -66,6 +74,22 @@
archived=
"false"
>
<result
status=
"valid"
time=
"0.01"
/>
</proof>
<proof
prover=
"7"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.10"
/>
</proof>
<proof
prover=
"8"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.10"
/>
</proof>
</goal>
<goal
name=
"WP_parameter main"
...
...
@@ -74,7 +98,7 @@
expl=
"parameter main"
sum=
"27febadb619ab97b0f5570efb544d5b3"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"ainfix =V0c4Iainfix <c17asqrainfix +V0c1Aainfix <=asqrV0c17Aainfix >=V0c0FAainfix >=c17c0"
>
<label
name=
"expl:parameter main"
/>
...
...
@@ -86,6 +110,22 @@
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"7"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"8"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
</theory>
<theory
...
...
@@ -116,7 +156,7 @@
expl=
"postcondition"
sum=
"11395e2e0807e0a152ae8659ec21bd93"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"ainfix <V0ainfix *ainfix +c0c1ainfix +c0c1Aainfix <=ainfix *c0c0V0Iainfix =V0c0Iainfix >=V0c0F"
>
<label
name=
"expl:parameter sqrt"
/>
...
...
@@ -144,6 +184,22 @@
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"7"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"8"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.01"
/>
</proof>
</goal>
<goal
name=
"WP_parameter sqrt.2"
...
...
@@ -152,7 +208,7 @@
expl=
"postcondition"
sum=
"3ab61eabd3d2a91edcf1daa5821658bf"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"ainfix <V0ainfix *ainfix +c1c1ainfix +c1c1Aainfix <=ainfix *c1c1V0Iainfix <=V0c3Iainfix =V0c0NIainfix >=V0c0F"
>
<label
name=
"expl:parameter sqrt"
/>
...
...
@@ -180,6 +236,22 @@
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"7"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.01"
/>
</proof>
<proof
prover=
"8"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter sqrt.3"
...
...
@@ -203,7 +275,7 @@
expl=
"parameter sqrt"
sum=
"24aeef4693626abd3583f6b6921aba3d"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"ainfix >adivainfix +V0c1c2c0Iainfix <=V0c3NIainfix =V0c0NIainfix >=V0c0F"
>
<label
name=
"expl:parameter sqrt"
/>
...
...
@@ -231,6 +303,22 @@
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"7"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"8"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter sqrt.3.2"
...
...
@@ -239,7 +327,7 @@
expl=
"parameter sqrt"
sum=
"92c82885df59e2741ce4df823ca7822c"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"ainfix >V0c0Iainfix <=V0c3NIainfix =V0c0NIainfix >=V0c0F"
>
<label
name=
"expl:parameter sqrt"
/>
...
...
@@ -267,6 +355,22 @@
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"7"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"8"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter sqrt.3.3"
...
...
@@ -275,7 +379,7 @@
expl=
"parameter sqrt"
sum=
"fb51c594670b2b8984a4e1f8acf2af68"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"ainfix =adivainfix +V0c1c2adivainfix +adivV0V0V0c2Iainfix <=V0c3NIainfix =V0c0NIainfix >=V0c0F"
>
<label
name=
"expl:parameter sqrt"
/>
...
...
@@ -287,6 +391,22 @@
archived=
"false"
>
<result
status=
"valid"
time=
"0.03"
/>
</proof>
<proof
prover=
"7"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.04"
/>
</proof>
<proof
prover=
"8"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"timeout"
time=
"5.05"
/>
</proof>
</goal>
<goal
name=
"WP_parameter sqrt.3.4"
...
...
@@ -295,7 +415,7 @@
expl=
"parameter sqrt"
sum=
"1f2b528636f5a3179f0d71f5ce38fb47"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"ainfix <V0ainfix *ainfix +V0c1ainfix +V0c1Iainfix <=V0c3NIainfix =V0c0NIainfix >=V0c0F"
>
<label
name=
"expl:parameter sqrt"
/>
...
...
@@ -323,6 +443,22 @@
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"7"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.01"
/>
</proof>
<proof
prover=
"8"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter sqrt.3.5"
...
...
@@ -331,7 +467,7 @@
expl=
"parameter sqrt"
sum=
"ca389f1cbcafdb15628b4e6e6c6538b1"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"ainfix <V0ainfix *ainfix +adivainfix +V0c1c2c1ainfix +adivainfix +V0c1c2c1Iainfix <=V0c3NIainfix =V0c0NIainfix >=V0c0F"
>
<label
name=
"expl:parameter sqrt"
/>
...
...
@@ -359,6 +495,22 @@
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"7"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"8"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
</transf>
</goal>
...
...
@@ -384,7 +536,7 @@
expl=
"parameter sqrt"
sum=
"dbbf6c132fa37dd1bf514c64adea52e1"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"ainfix >V4c0Iainfix =V4adivainfix +adivV0V1V1c2FIainfix =V3V1FIainfix <V1V2Iainfix <V0ainfix *ainfix +V1c1ainfix +V1c1Aainfix <V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix =V1adivainfix +adivV0V2V2c2Aainfix >V2c0Aainfix >V1c0FIainfix <=V0c3NIainfix =V0c0NIainfix >=V0c0F"
>
<label
name=
"expl:parameter sqrt"
/>
...
...
@@ -412,6 +564,22 @@
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"7"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.03"
/>
</proof>
<proof
prover=
"8"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.03"
/>
</proof>
</goal>
<goal
name=
"WP_parameter sqrt.4.2"
...
...
@@ -420,7 +588,7 @@
expl=
"parameter sqrt"
sum=
"e227034cdab8f00eb1fac96f38ccca97"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"ainfix >V3c0Iainfix =V4adivainfix +adivV0V1V1c2FIainfix =V3V1FIainfix <V1V2Iainfix <V0ainfix *ainfix +V1c1ainfix +V1c1Aainfix <V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix =V1adivainfix +adivV0V2V2c2Aainfix >V2c0Aainfix >V1c0FIainfix <=V0c3NIainfix =V0c0NIainfix >=V0c0F"
>
<label
name=
"expl:parameter sqrt"
/>
...
...
@@ -448,6 +616,22 @@
archived=
"false"
>
<result
status=
"valid"
time=
"0.01"
/>
</proof>
<proof
prover=
"7"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
<proof
prover=
"8"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
</goal>
<goal
name=
"WP_parameter sqrt.4.3"
...
...
@@ -456,7 +640,7 @@
expl=
"parameter sqrt"
sum=
"c9f4a06133300f4616cdea414a4417a1"
proved=
"true"
expanded=
"
fals
e"
expanded=
"
tru
e"
shape=
"ainfix =V4adivainfix +adivV0V3V3c2Iainfix =V4adivainfix +adivV0V1V1c2FIainfix =V3V1FIainfix <V1V2Iainfix <V0ainfix *ainfix +V1c1ainfix +V1c1Aainfix <V0ainfix *ainfix +V2c1ainfix +V2c1Aainfix =V1adivainfix +adivV0V2V2c2Aainfix >V2c0Aainfix >V1c0FIainfix <=V0c3NIainfix =V0c0NIainfix >=V0c0F"
>
<label
name=
"expl:parameter sqrt"
/>
...
...
@@ -484,6 +668,22 @@
archived=
"false"
>
<result
status=
"valid"
time=
"0.01"
/>
</proof>
<proof
prover=
"7"
timelimit=
"5"
memlimit=
"4000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>