Commit f94c72cc authored by MARCHE Claude's avatar MARCHE Claude

make more session files up-to-date

parent 9eb8c83c
......@@ -2,35 +2,34 @@
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/my_cosine/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="eprover" name="Eprover" version="1.0-004 Temi"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.7"/>
<prover id="vampire" name="Vampire" version="0.6"/>
<prover id="verit" name="veriT" version="200907"/>
<prover id="yices" name="Yices" version="1.0.11"/>
<prover id="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../my_cosine.why" verified="true" expanded="true">
<theory name="CosineSingle" verified="true" expanded="true">
<goal name="MethodError" sum="04d7ba2ad67e6273c77266e812fe0b5d" proved="true" expanded="true" shape="ainfix <=aabsainfix -ainfix -c1.0ainfix *c0.5ainfix *V0V0acosV0c0x1.p-24Iainfix <=aabsV0c0x1.p-5F">
<goal name="MethodError" sum="7e239f41b24f1cdcff5fb8b41e2d7b56" proved="true" expanded="true" shape="ainfix <=aabsainfix -ainfix -c1.0ainfix *c0.5ainfix *V0V0acosV0c0x1.p-24Iainfix <=aabsV0c0x1.p-5F">
<proof prover="coq" timelimit="2" edited="my_cosine_CosineSingle_MethodError_1.v" obsolete="false">
<result status="valid" time="3.61"/>
<result status="valid" time="3.70"/>
</proof>
</goal>
<goal name="TotalErrorFullyExpanded" sum="86136c1aa7501342a2789f26b4088e3b" proved="true" expanded="true" shape="ainfix <=aabsainfix -V3acosavalueV0c0x1.p-23Iainfix =V3aroundaNearestTiesToEvenainfix -c1.0V2Iainfix =V2aroundaNearestTiesToEvenainfix *c0.5V1Iainfix =V1aroundaNearestTiesToEvenainfix *avalueV0avalueV0FIainfix <=aabsainfix -ainfix -c1.0ainfix *c0.5ainfix *avalueV0avalueV0acosavalueV0c0x1.p-24Iainfix <=aabsavalueV0c0x1.p-5F">
<goal name="TotalErrorFullyExpanded" sum="2409a18fb6e445b84bbae02a54ba4323" proved="true" expanded="true" shape="ainfix <=aabsainfix -V3acosavalueV0c0x1.p-23Iainfix =V3aroundaNearestTiesToEvenainfix -c1.0V2Iainfix =V2aroundaNearestTiesToEvenainfix *c0.5V1Iainfix =V1aroundaNearestTiesToEvenainfix *avalueV0avalueV0FIainfix <=aabsainfix -ainfix -c1.0ainfix *c0.5ainfix *avalueV0avalueV0acosavalueV0c0x1.p-24Iainfix <=aabsavalueV0c0x1.p-5F">
<proof prover="gappa" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="TotalErrorExpanded" sum="1d2075874f81d542bc1500ae6147faec" proved="true" expanded="true" shape="LaroundaNearestTiesToEvenainfix *avalueV0avalueV0LaroundaNearestTiesToEvenainfix *c0.5V1LaroundaNearestTiesToEvenainfix -c1.0V2ainfix <=aabsainfix -V3acosavalueV0c0x1.p-23Iainfix <=aabsavalueV0c0x1.p-5F">
<goal name="TotalErrorExpanded" sum="ea45d1f6e4feb7e9f589f6e961e201a3" proved="true" expanded="true" shape="LaroundaNearestTiesToEvenainfix *avalueV0avalueV0LaroundaNearestTiesToEvenainfix *c0.5V1LaroundaNearestTiesToEvenainfix -c1.0V2ainfix <=aabsainfix -V3acosavalueV0c0x1.p-23Iainfix <=aabsavalueV0c0x1.p-5F">
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.80"/>
<result status="valid" time="0.67"/>
</proof>
</goal>
<goal name="TotalError" sum="84d328c047b191246fda42eaa2ab5255" proved="true" expanded="true" shape="Lacos_singleV0ainfix <=aabsainfix -avalueV1acosavalueV0c0x1.p-23Iainfix <=aabsavalueV0c0x1.p-5F">
<goal name="TotalError" sum="c17f399ee51ba2341075469ae08c758e" proved="true" expanded="true" shape="Lacos_singleV0ainfix <=aabsainfix -avalueV1acosavalueV0c0x1.p-23Iainfix <=aabsavalueV0c0x1.p-5F">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="2.13"/>
<result status="valid" time="2.51"/>
</proof>
</goal>
</theory>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/vstte10_aqueue/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.7"/>
<prover id="vampire" name="Vampire" version="0.6"/>
<prover id="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../vstte10_aqueue.mlw" verified="true" expanded="true">
<theory name="WP AmortizedQueue" verified="true" expanded="true">
<goal name="WP_parameter empty" expl="normal postcondition" sum="909ab0d6f233b4d2efe8d20c0f817588" proved="true" expanded="true">
<goal name="WP_parameter empty" expl="normal postcondition" sum="f7f3dcefcaeb59ee67d172452a0edb10" proved="true" expanded="false" shape="ainfix =asequenceamk queueaNilc0aNilc0aNilAainvamk queueaNilc0aNilc0">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter head" expl="correctness of parameter head" sum="df279e0806f4697dfb52c16a7712fd6c" proved="true" expanded="true">
<goal name="WP_parameter head" expl="correctness of parameter head" sum="2b221cb80523a4a507aa25aaf0aeee12" proved="true" expanded="false" shape="Lamk queueV0V1V2V3CV0aNilfaConsVwainfix =CasequenceV4aNilaNoneaConsVwaSomeV6aSomeV5Iainfix =asequenceV4aNilNAainvV4F">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter create" expl="correctness of parameter create" sum="5c6dc68135163c32716581f63366d671" proved="true" expanded="true">
<goal name="WP_parameter create" expl="correctness of parameter create" sum="c2695d7b03617e9abef11f5de228419b" proved="true" expanded="false" shape="LalengthV2iainfix >=V1V3ainfix =asequenceamk queueV0V1V2V3ainfix ++V0areverseV2Aainvamk queueV0V1V2V3ainfix =asequenceamk queueainfix ++V0areverseV2ainfix +V1V3aNilc0ainfix ++V0areverseV2Aainvamk queueainfix ++V0areverseV2ainfix +V1V3aNilc0Iainfix =V1alengthV0FFF">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.36"/>
<result status="valid" time="0.37"/>
</proof>
</goal>
<goal name="WP_parameter tail" expl="correctness of parameter tail" sum="e064c80f5f1ee95e0e494e4c080b5029" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter tail.1" expl="correctness of parameter tail" sum="8b9ca2a529eaada80a407300a55e20d0" proved="true" expanded="true">
<goal name="WP_parameter tail" expl="correctness of parameter tail" sum="f8b34aea12dd160ee2cc30f2fab779aa" proved="true" expanded="false" shape="Lamk queueV0V1V2V3CV0aNilfaConswVLamk queueV6V7V8V9ainfix =CasequenceV4aNilaNoneaConswVaSomeV11aSomeasequenceV10AainvV10Iainfix =asequenceV10ainfix ++V5areverseV2AainvV10FAainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV5Iainfix =asequenceV4aNilNAainvV4F">
<transf name="split_goal" proved="true" expanded="false">
<goal name="WP_parameter tail.1" expl="correctness of parameter tail" sum="3f6aae94bc1095c3b5c3c308f314b896" proved="true" expanded="false" shape="Lamk queueV0V1V2V3CV0aNilfaConswVtIainfix =asequenceV4aNilNAainvV4F">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter tail.2" expl="correctness of parameter tail" sum="a83fd8e5c78ad764dc9652839a39c57b" proved="true" expanded="true">
<goal name="WP_parameter tail.2" expl="correctness of parameter tail" sum="e7b9d14fb447a9a79fb4d34424a7ab7a" proved="true" expanded="false" shape="Lamk queueV0V1V2V3CV0aNiltaConswVainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV5Iainfix =asequenceV4aNilNAainvV4F">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter tail.3" expl="correctness of parameter tail" sum="f7542b33f71df9da29bb7e21b8e1311d" proved="true" expanded="true">
<goal name="WP_parameter tail.3" expl="correctness of parameter tail" sum="b62b83f35bb29029aba8ffd315846586" proved="true" expanded="false" shape="Lamk queueV0V1V2V3CV0aNiltaConswVLamk queueV6V7V8V9ainfix =CasequenceV4aNilaNoneaConswVaSomeV11aSomeasequenceV10AainvV10Iainfix =asequenceV10ainfix ++V5areverseV2AainvV10FIainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV5Iainfix =asequenceV4aNilNAainvV4F">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.12"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter enqueue" expl="correctness of parameter enqueue" sum="940fa98f53cd4fbeb614fd48b2922378" proved="true" expanded="true">
<goal name="WP_parameter enqueue" expl="correctness of parameter enqueue" sum="9344bf080656af98c8508850e13c448c" proved="true" expanded="false" shape="Lamk queueV1V2V3V4Lamk queueV6V7V8V9ainfix =asequenceV10ainfix ++asequenceV5aConsV0aNilAainvV10Iainfix =asequenceV10ainfix ++V1areverseaConsV0V3AainvV10FAainfix =ainfix +V4c1alengthaConsV0V3Aainfix =V2alengthV1IainvV5FF">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.09"/>
<result status="valid" time="0.10"/>
</proof>
</goal>
</theory>
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment