Commit 98141a3d authored by MARCHE Claude's avatar MARCHE Claude

update obsolete sessions

parent d8122567
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/bts/12475/why3session.xml">
<why3session name="bts/12475/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"/>
......@@ -12,12 +12,12 @@
<prover id="z3" name="Z3" version="2.19"/>
<file name="../12475.why" verified="true" expanded="true">
<theory name="Stmt" verified="true" expanded="true">
<goal name="toto" sum="face789c8c32bf3821575b3c51939cd0" proved="true" expanded="true" shape="ainfix <V0ainfix +aroundaUpV0c1.F">
<goal name="toto" sum="fb9c382631eb3331b29b3e2e91edb9ef" proved="true" expanded="true" shape="ainfix <V0ainfix +aroundaUpV0c1.F">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/check-builtin/array/why3session.xml">
<why3session name="check-builtin/array/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"/>
......@@ -12,7 +12,7 @@
<prover id="z3" name="Z3" version="2.19"/>
<file name="../array.why" verified="true" expanded="true">
<theory name="Test_simplify_array" verified="true" expanded="true">
<goal name="G1" sum="4b1f56125aaf6794df037dfd2cbfea62" proved="true" expanded="true" shape="ainfix =agetasetV2V1V0V1V0FF">
<goal name="G1" sum="236061dc63571fd08d3960c30b3a3ef2" proved="true" expanded="true" shape="ainfix =agetasetV2V1V0V1V0FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -26,7 +26,7 @@
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="G2" sum="dc80f74d142de8dda00f0aef8deca6c0" proved="true" expanded="true" shape="ainfix =agetasetV5V0V4V3V1Iainfix =agetV5V3V1Iainfix =V3V0NFF">
<goal name="G2" sum="513c66a055e3640e12c0ee979bfe922a" proved="true" expanded="true" shape="ainfix =agetasetV5V0V4V3V1Iainfix =agetV5V3V1Iainfix =V3V0NFF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -34,13 +34,13 @@
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="G3" sum="4aea5336be3a1feb8cf653e610e1d89a" proved="true" expanded="true" shape="ainfix =agetasetV2c1V1c0V0Iainfix =agetV2c0V0FF">
<goal name="G3" sum="24f733b6ec5fd3c898c797c4f8d4e82e" proved="true" expanded="true" shape="ainfix =agetasetV2c1V1c0V0Iainfix =agetV2c0V0FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -54,7 +54,7 @@
<result status="valid" time="0.15"/>
</proof>
</goal>
<goal name="G4" sum="5751bd67cfa24e03534046070269e911" proved="true" expanded="true" shape="ainfix =agetasetasetV2c1V1c0V0c1V1FF">
<goal name="G4" sum="c193125d14526422133026f1ae07551e" proved="true" expanded="true" shape="ainfix =agetasetasetV2c1V1c0V0c1V1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/check-builtin/bool/why3session.xml">
<why3session name="check-builtin/bool/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"/>
......@@ -40,18 +40,18 @@
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="G3" sum="f575ede69f52b10d8bfe591848ea3934" proved="true" expanded="true" shape="fIainfix =V2V0NAainfix =V1V2NAainfix =V0V1NF">
<goal name="G3" sum="601dae5d276391434bfebe04388a4f59" proved="true" expanded="true" shape="fIainfix =V2V0NAainfix =V1V2NAainfix =V0V1NF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.00"/>
<result status="unknown" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/check-builtin/euclideandivision/why3session.xml">
<why3session name="check-builtin/euclideandivision/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"/>
......@@ -12,7 +12,7 @@
<prover id="z3" name="Z3" version="2.19"/>
<file name="../euclideandivision.why" verified="true" expanded="true">
<theory name="Test" verified="true" expanded="true">
<goal name="G1" sum="fa1bf8929f550cd0d7bc90f8ce7be2eb" proved="true" expanded="true" shape="ainfix =amodc10c3c1">
<goal name="G1" sum="90824745f1a68d5b5da57840125d3fdf" proved="true" expanded="true" shape="ainfix =amodc10c3c1">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -23,10 +23,10 @@
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.00"/>
<result status="timeout" time="10.64"/>
</proof>
</goal>
<goal name="G2" sum="5800907ef13d303adf6e30c1b01a9dae" proved="true" expanded="true" shape="ainfix =adivc10c3c3">
<goal name="G2" sum="9b4f0670f5abfa09eb5977e0253d4fd7" proved="true" expanded="true" shape="ainfix =adivc10c3c3">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -37,7 +37,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="9.99"/>
<result status="timeout" time="10.01"/>
</proof>
</goal>
</theory>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/check-builtin/int/why3session.xml">
<why3session name="check-builtin/int/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"/>
......@@ -12,7 +12,7 @@
<prover id="z3" name="Z3" version="2.19"/>
<file name="../int.why" verified="true" expanded="true">
<theory name="Test" verified="true" expanded="true">
<goal name="G1" sum="d5111159f39ad797db77ad7e2d80a226" proved="true" expanded="true" shape="ainfix =ainfix *c5c10c50">
<goal name="G1" sum="f3b088189b6d1cad40811addc4d6803a" proved="true" expanded="true" shape="ainfix =ainfix *c5c10c50">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -23,10 +23,10 @@
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.03"/>
<result status="timeout" time="10.13"/>
</proof>
</goal>
<goal name="G2" sum="8dc6e7f38fd1fb7946a1212c89ba402d" proved="true" expanded="true" shape="ainfix =ainfix +ainfix -ainfix +V0V0V0V0ainfix *c2V0F">
<goal name="G2" sum="dc89477693660d3b4d1752799ab3ad92" proved="true" expanded="true" shape="ainfix =ainfix +ainfix -ainfix +V0V0V0V0ainfix *c2V0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -37,10 +37,10 @@
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.08"/>
<result status="timeout" time="10.05"/>
</proof>
</goal>
<goal name="CompatOrderAdd" sum="9385e56939c8dc201584ea4f3d9bc4af" proved="true" expanded="true" shape="ainfix <=ainfix +V0V2ainfix +V1V2Iainfix <=V0V1F">
<goal name="CompatOrderAdd" sum="995e98cb6b1a9efa72903110d4a87568" proved="true" expanded="true" shape="ainfix <=ainfix +V0V2ainfix +V1V2Iainfix <=V0V1F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -54,12 +54,12 @@
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="CompatOrderMult" sum="b98fa9a55f2216428fda1a415944f990" proved="true" expanded="true" shape="ainfix <=ainfix *V0V2ainfix *V1V2Iainfix <=c0V2Iainfix <=V0V1F">
<goal name="CompatOrderMult" sum="bf32d6e38f083eb3b1b4122103d07ed0" proved="true" expanded="true" shape="ainfix <=ainfix *V0V2ainfix *V1V2Iainfix <=c0V2Iainfix <=V0V1F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
......@@ -68,7 +68,7 @@
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="InvMult" sum="1bfe3b11addac18ebecd101596d63095" proved="true" expanded="true" shape="ainfix =aprefix -ainfix *V0V1ainfix *V0aprefix -V1Aainfix =ainfix *aprefix -V0V1aprefix -ainfix *V0V1F">
<goal name="InvMult" sum="0b46a39680d5f67d5f93c4c8f5b9804f" proved="true" expanded="true" shape="ainfix =aprefix -ainfix *V0V1ainfix *V0aprefix -V1Aainfix =ainfix *aprefix -V0V1aprefix -ainfix *V0V1F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -79,24 +79,24 @@
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="9.99"/>
<result status="timeout" time="10.03"/>
</proof>
</goal>
<goal name="InvSquare" sum="1b594a6b60e183e594b00faf939fcc3f" proved="true" expanded="true" shape="ainfix =ainfix *V0V0ainfix *aprefix -V0aprefix -V0F">
<goal name="InvSquare" sum="691e3b9ce7e619beb48133aec4131a7f" proved="true" expanded="true" shape="ainfix =ainfix *V0V0ainfix *aprefix -V0aprefix -V0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.03"/>
<result status="timeout" time="10.18"/>
</proof>
</goal>
<goal name="ZeroMult" sum="27316fd57c9735adb22695569bcb11a0" proved="true" expanded="true" shape="ainfix =c0ainfix *c0V0Aainfix =ainfix *V0c0c0F">
<goal name="ZeroMult" sum="160be6da3ce1512d4399229ce0fce605" proved="true" expanded="true" shape="ainfix =c0ainfix *c0V0Aainfix =ainfix *V0c0c0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -107,24 +107,24 @@
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.04"/>
<result status="timeout" time="10.06"/>
</proof>
</goal>
<goal name="SquareNonNeg1" sum="70ded199aa475245ae7cdcf94f7d1da3" proved="true" expanded="true" shape="ainfix <=c0ainfix *V0V0Iainfix <=V0c0F">
<goal name="SquareNonNeg1" sum="eeb4337e8e41c2167d24509f78284afb" proved="true" expanded="true" shape="ainfix <=c0ainfix *V0V0Iainfix <=V0c0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="9.98"/>
<result status="timeout" time="10.26"/>
</proof>
</goal>
<goal name="SquareNonNeg" sum="12fd5ee57cbbcb48649ccac8dfc81690" proved="true" expanded="true" shape="ainfix <=c0ainfix *V0V0F">
<goal name="SquareNonNeg" sum="2979802203c80db522016836bcf336a5" proved="true" expanded="true" shape="ainfix <=c0ainfix *V0V0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -135,10 +135,10 @@
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.03"/>
<result status="timeout" time="10.00"/>
</proof>
</goal>
<goal name="ZeroLessOne" sum="bdbf802a95888bb77a6252cc1cb557f7" proved="true" expanded="true" shape="ainfix <=c0c1">
<goal name="ZeroLessOne" sum="07a7198a41094f338830d92f862e0e1a" proved="true" expanded="true" shape="ainfix <=c0c1">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -149,12 +149,12 @@
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="9.98"/>
<result status="timeout" time="10.01"/>
</proof>
</goal>
</theory>
<theory name="MinMax" verified="true" expanded="true">
<goal name="G" sum="5ae270cf2070b36d0278c96a283e2a4d" proved="true" expanded="true" shape="ainfix =aminc1aminc3c2c1">
<goal name="G" sum="977fcbebad29e171c02a891ed8dac707" proved="true" expanded="true" shape="ainfix =aminc1aminc3c2c1">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -162,10 +162,10 @@
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.21"/>
<result status="timeout" time="10.22"/>
</proof>
</goal>
</theory>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/check-builtin/intreal/why3session.xml">
<why3session name="check-builtin/intreal/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"/>
......@@ -12,7 +12,7 @@
<prover id="z3" name="Z3" version="2.19"/>
<file name="../intreal.why" verified="true" expanded="true">
<theory name="IntReal" verified="true" expanded="true">
<goal name="G1" sum="06e7d94a89ff43145486bcbcbc3d7c13" proved="true" expanded="true" shape="ainfix =afrom_intc2c2.0">
<goal name="G1" sum="7ae3d391ca4e248e8a841334ac4f1d9d" proved="true" expanded="true" shape="ainfix =afrom_intc2c2.0">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
......@@ -23,91 +23,91 @@
<result status="valid" time="0.07"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.04"/>
<result status="timeout" time="10.67"/>
</proof>
</goal>
<goal name="G2" sum="5f25c7c89671e1d17dbb5851f1feb031" proved="true" expanded="true" shape="ainfix =afloorc1.5c1">
<goal name="G2" sum="8ff7189835efa75f9623ad70bac2eae6" proved="true" expanded="true" shape="ainfix =afloorc1.5c1">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.93"/>
<result status="valid" time="0.92"/>
</proof>
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.07"/>
<result status="timeout" time="10.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.05"/>
<result status="timeout" time="10.12"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.18"/>
<result status="timeout" time="10.54"/>
</proof>
</goal>
<goal name="G3" sum="55c350ce0a116adb480c1cddea69ba0b" proved="true" expanded="true" shape="ainfix =aceilc1.5c2">
<goal name="G3" sum="7c6bcdfb66c08ad38d4d871b74023df2" proved="true" expanded="true" shape="ainfix =aceilc1.5c2">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="1.22"/>
<result status="valid" time="1.23"/>
</proof>
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.04"/>
<result status="timeout" time="10.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.11"/>
<result status="timeout" time="10.12"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.04"/>
<result status="timeout" time="10.37"/>
</proof>
</goal>
<goal name="G4" sum="5d309eab0cb446104475d2a1e77ae019" proved="true" expanded="true" shape="ainfix =aflooraprefix -.c1.5aprefix -c2">
<goal name="G4" sum="c8f1d8059a7ad05ec4a1c3ab2fdaf0a3" proved="true" expanded="true" shape="ainfix =aflooraprefix -.c1.5aprefix -c2">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="4.36"/>
<result status="valid" time="4.43"/>
</proof>
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.05"/>
<result status="timeout" time="10.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.05"/>
<result status="timeout" time="10.12"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.47"/>
<result status="timeout" time="10.04"/>
</proof>
</goal>
<goal name="G5" sum="b646c11d8de292cdd85c8ab29a8c887c" proved="true" expanded="true" shape="ainfix =aceilaprefix -.c1.5aprefix -c1">
<goal name="G5" sum="8d756d1bd8b1304b50f1358d76aac9de" proved="true" expanded="true" shape="ainfix =aceilaprefix -.c1.5aprefix -c1">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="5.46"/>
<result status="valid" time="5.50"/>
</proof>
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.06"/>
<result status="timeout" time="10.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.04"/>
<result status="timeout" time="10.12"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.28"/>
<result status="timeout" time="9.91"/>
</proof>
</goal>
<goal name="G6" sum="a26ce155ad2967fb2870399291ee938b" proved="true" expanded="true" shape="ainfix <=afloorV0aceilV0F">
<goal name="G6" sum="538ef0db57e3022fc4a963e96b539e21" proved="true" expanded="true" shape="ainfix <=afloorV0aceilV0F">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.06"/>
</proof>
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.08"/>
<result status="timeout" time="10.12"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.30"/>
<result status="valid" time="0.31"/>
</proof>
</goal>
<goal name="G7" sum="62043952a600fc351594ea3c5fc79346" proved="true" expanded="true" shape="ainfix =afrom_intafloorV0V0NIainfix <afloorV0aceilV0F">
<goal name="G7" sum="01398fbc16051f0f43c46685432c8ab8" proved="true" expanded="true" shape="ainfix =afrom_intafloorV0V0NIainfix <afloorV0aceilV0F">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.11"/>
</proof>
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.01"/>
<result status="timeout" time="10.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.03"/>
<result status="timeout" time="10.32"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.42"/>
<result status="timeout" time="10.58"/>
</proof>
</goal>
</theory>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/check-builtin/minmax/why3session.xml">
<why3session name="check-builtin/minmax/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"/>
......@@ -12,7 +12,7 @@
<prover id="z3" name="Z3" version="2.19"/>
<file name="../minmax.why" verified="true" expanded="true">
<theory name="MinMax" verified="true" expanded="true">
<goal name="G" sum="f61c7c570e2c5d86e58a28a20684d47d" proved="true" expanded="true" shape="ainfix =aminV0amaxaminV2V0V1V0IageV1V0IageV2V0IageV2V1F">
<goal name="G" sum="bfe2729ea2bf0552e59c25f3fe06b469" proved="true" expanded="true" shape="ainfix =aminV0amaxaminV2V0V1V0IageV1V0IageV2V0IageV2V1F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -23,7 +23,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="G2" sum="f12ac01ccd7911072c03b4e7312a8955" proved="true" expanded="true" shape="ageV0V1Iainfix =amaxV0V1V0F">
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/check-builtin/real/why3session.xml">
<why3session name="check-builtin/real/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"/>
......@@ -12,49 +12,49 @@
<prover id="z3" name="Z3" version="2.19"/>
<file name="../real.why" verified="true" expanded="true">
<theory name="Test" verified="true" expanded="true">
<goal name="G1" sum="832ddb9ca6d4d32f25e03098a3607b6b" proved="true" expanded="true" shape="ainfix =ainfix *c5.5c10.c55.">
<goal name="G1" sum="3255e74479fcd477b7a93056adf258a2" proved="true" expanded="true" shape="ainfix =ainfix *c5.5c10.c55.">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="yices" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.00"/>
<result status="timeout" time="10.22"/>
</proof>
</goal>
<goal name="G2" sum="efe077a578905ccd7321f78fa8952077" proved="true" expanded="true" shape="ainfix =ainfix /c9.c3.c3.">
<goal name="G2" sum="7a8763f7f033a0d316f418db5c389983" proved="true" expanded="true" shape="ainfix =ainfix /c9.c3.c3.">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.34"/>
<result status="timeout" time="10.35"/>
</proof>
</goal>
<goal name="G3" sum="1885fdced1e38f18cc908dd034c5266e" proved="true" expanded="true" shape="ainfix =ainvc5.c0.2">
<goal name="G3" sum="3afdd97b5a5d9b418c7e0e7615f9b3f0" proved="true" expanded="true" shape="ainfix =ainvc5.c0.2">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.21"/>
<result status="timeout" time="10.17"/>
</proof>
</goal>
</theory>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/my_cosine/why3session.xml">
<why3session name="./my_cosine/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"/>
......@@ -12,24 +12,24 @@
<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="7e239f41b24f1cdcff5fb8b41e2d7b56" proved="true" expanded="true" shape="ainfix <=aabsainfix -ainfix -c1.0ainfix *c0.5ainfix *V0V0acosV0c0x1.p-24Iainfix <=aabsV0c0x1.p-5F">
<goal name="MethodError" sum="b6fc96a29dbb1492eab3c9b890206d87" 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.70"/>
<result status="valid" time="3.65"/>
</proof>
</goal>
<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">
<goal name="TotalErrorFullyExpanded" sum="762dc642d0fb95fdca3d3ef8644544fd" 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.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="TotalErrorExpanded" sum="ea45d1f6e4feb7e9f589f6e961e201a3" proved="true" expanded="true" shape="LaroundaNearestTiesToEvenainfix *avalueV0avalueV0LaroundaNearestTiesToEvenainfix *c0.5V1LaroundaNearestTiesToEvenainfix -c1.0V2ainfix <=aabsainfix -V3acosavalueV0c0x1.p-23Iainfix <=aabsavalueV0c0x1.p-5F">
<goal name="TotalErrorExpanded" sum="051b62e81c6bff02e662eeb7a0742164" 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.67"/>
<result status="valid" time="0.69"/>
</proof>
</goal>
<goal name="TotalError" sum="c17f399ee51ba2341075469ae08c758e" proved="true" expanded="true" shape="Lacos_singleV0ainfix <=aabsainfix -avalueV1acosavalueV0c0x1.p-23Iainfix <=aabsavalueV0c0x1.p-5F">
<goal name="TotalError" sum="d80467e1b72bec3f873fffec0574b3a7" 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.51"/>
<result status="valid" time="2.48"/>
</proof>
</goal>
</theory>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/assigning_meanings_to_programs/why3session.xml">
<why3session name="programs/assigning_meanings_to_programs/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="../assigning_meanings_to_programs.mlw" verified="true" expanded="true">
<theory name="WP Sum" verified="true" expanded="true">
<goal name="WP_parameter sum" expl="correctness of parameter sum" sum="e400c1902a93c2db3f58b823d005001b" proved="true" expanded="true">
<goal name="WP_parameter sum" expl=" parameter sum" sum="fa916cc5e0d85eec4bfc14a054b315d6" proved="true" expanded="true" shape="iainfix <=V4V1ainfix <ainfix -V1V6ainfix -V1V4Aainfix <=c0ainfix -V1V4Aainfix =V5asumV2c1V6Aainfix <=V6ainfix +V1c1Aainfix <=c1V6Iainfix =V6ainfix +V4c1FIainfix =V5ainfix +V3agetV2V4FAainfix <V4V0Aainfix <=c0V4ainfix =V3asumV2c1ainfix +V1c1Iainfix =V3asumV2c1V4Aainfix <=V4ainfix +V1c1Aainfix <=c1V4FFAainfix =c0asumV2c1c1Aainfix <=c1ainfix +V1c1Aainfix <=c1c1Iainfix <V1V0Aainfix <=c0V1FFF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
</theory>
<theory name="WP Division" verified="true" expanded="true">
<goal name="WP_parameter division" expl="correctness of parameter division" sum="c30339816d276e5cb31141054d5923e8" proved="true" expanded="true">
<goal name="WP_parameter division" expl=" parameter division" sum="ad4ca868c9bf9e2ed20071557da75449" proved="true" expanded="true" shape="iainfix >=V2V1ainfix <V4V2Aainfix <=c0V2Aainfix =V0ainfix +ainfix *V5V1V4Aainfix <=c0V4Iainfix =V5ainfix +V3c1FIainfix =V4ainfix -V2V1Fainfix =V0ainfix +ainfix *V3V1V2Aainfix <V2V1Aainfix <=c0V2Iainfix =V0ainfix +ainfix *V3V1V2Aainfix <=c0V2FFAainfix =V0ainfix +ainfix *c0V1V0Aainfix <=c0V0Iainfix <c0V1Aainfix <=c0V0FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/binary_search/why3session.xml">
<why3session name="programs/binary_search/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"/>
......@@ -12,12 +12,12 @@
<prover id="z3" name="Z3" version="2.19"/>
<file name="../binary_search.mlw" verified="true" expanded="true">
<theory name="WP M" verified="true" expanded="true">
<goal name="WP_parameter binary_search" expl="correctness of parameter binary_search" sum="e9025093975750a5eeb1344fc9d03b19" proved="true" expanded="true" shape="iainfix <=V4V3iainfix <agetV2ainfix +V4adivainfix -V3V4c2V1ainfix <ainfix -V3V5ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V6V3Aainfix <=V5V6Iainfix =agetV2V6V1Iainfix <V6V0Aainfix <=c0V6FAainfix <V3V0Aainfix <=c0V5Iainfix =V5ainfix +ainfix +V4adivainfix -V3V4c2c1Fiainfix >agetV2ainfix +V4adivainfix -V3V4c2V1ainfix <ainfix -V7V4ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V8V7Aainfix <=V4V8Iainfix =agetV2V8V1Iainfix <V8V0Aainfix <=c0V8FAainfix <V7V0Aainfix <=c0V4Iainfix =V7ainfix -ainfix +V4adivainfix -V3V4c2c1Fainfix =agetV2ainfix +V4adivainfix -V3V4c2V1Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <=ainfix +V4adivainfix -V3V4c2V3Aainfix <=V4ainfix +V4adivainfix -V3V4c2ainfix =agetV2V9V1NIainfix <V9V0Aainfix <=c0V9FIainfix <=V10V3Aainfix <=V4V10Iainfix =agetV2V10V1Iainfix <V10V0Aainfix <=c0V10FAainfix <V3V0Aainfix <=c0V4FFAainfix <=V11ainfix -V0c1Aainfix <=c0V11Iainfix =agetV2V11V1Iainfix <V11V0Aainfix <=c0V11FAainfix <ainfix -V0c1V0Aainfix <=c0c0Iainfix <=agetV2V12agetV2V13Iainfix <V13V0Aainfix <=V12V13Aainfix <=c0V12FFFF">
<goal name="WP_parameter binary_search" expl=" parameter binary_search" sum="45ec37717bb483a53698643fee4a5393" proved="true" expanded="true" shape="iainfix <=V4V3iainfix <agetV2ainfix +V4adivainfix -V3V4c2V1ainfix <ainfix -V3V5ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V6V3Aainfix <=V5V6Iainfix =agetV2V6V1Iainfix <V6V0Aainfix <=c0V6FAainfix <V3V0Aainfix <=c0V5Iainfix =V5ainfix +ainfix +V4adivainfix -V3V4c2c1Fiainfix >agetV2ainfix +V4adivainfix -V3V4c2V1ainfix <ainfix -V7V4ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V8V7Aainfix <=V4V8Iainfix =agetV2V8V1Iainfix <V8V0Aainfix <=c0V8FAainfix <V7V0Aainfix <=c0V4Iainfix =V7ainfix -ainfix +V4adivainfix -V3V4c2c1Fainfix =agetV2ainfix +V4adivainfix -V3V4c2V1Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <=ainfix +V4adivainfix -V3V4c2V3Aainfix <=V4ainfix +V4adivainfix -V3V4c2ainfix =agetV2V9V1NIainfix <V9V0Aainfix <=c0V9FIainfix <=V10V3Aainfix <=V4V10Iainfix =agetV2V10V1Iainfix <V10V0Aainfix <=c0V10FAainfix <V3V0Aainfix <=c0V4FFAainfix <=V11ainfix -V0c1Aainfix <=c0V11Iainfix =agetV2V11V1Iainfix <V11V0Aainfix <=c0V11FAainfix <ainfix -V0c1V0Aainfix <=c0c0Iainfix <=agetV2V12agetV2V13Iainfix <V13V0Aainfix <=V12V13Aainfix <=c0V12FFFF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/bresenham/why3session.xml">
<why3session name="programs/bresenham/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"/>
......@@ -12,14 +12,14 @@
<prover id="z3" name="Z3" version="2.19"/>
<file name="../bresenham.mlw" verified="true" expanded="true">
<theory name="WP M" verified="true" expanded="true">
<goal name="invariant_is_ok" sum="87247a176582485d3d20264a84801d09" proved="true" expanded="true" shape="abestV0V1Iainvariant_V0V1V2F">
<goal name="invariant_is_ok" sum="aea249aa6c35def5f1ab4cc822c59221" proved="true" expanded="true" shape="abestV0V1Iainvariant_V0V1V2F">
<proof prover="coq" timelimit="10" edited="bresenham_WP_M_invariant_is_ok_1.v" obsolete="false">
<result status="valid" time="1.23"/>
<result status="valid" time="1.22"/>
</proof>
</goal>
<goal name="WP_parameter bresenham" expl="correctness of parameter bresenham" sum="9eb8c0b7a7b5b8f389c3d8227071b47b" proved="true" expanded="true" shape="iainfix <=V2ax2iainfix <V0c0ainfix <ainfix -ainfix +ax2c1V4ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Aainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2Fainfix <ainfix -ainfix +ax2c1V7ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Aainvariant_V7V5V6Aainfix <=V7ainfix +ax2c1Aainfix <=c0V7Iainfix =V7ainfix +V2c1FIainfix =V6ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V5ainfix +V1c1FAabestV2V1tIainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFFAainvariant_c0c0ainfix -ainfix *c2ay2ax2Aainfix <=c0ainfix +ax2c1Aainfix <=c0c0">
<goal name="WP_parameter bresenham" expl=" parameter bresenham" sum="5f519ef1874e86cf7ab8d7e7fe744a24" proved="true" expanded="true" shape="iainfix <V0c0ainfix <ainfix -ainfix +ax2c1V4ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Aainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2Fainfix <ainfix -ainfix +ax2c1V7ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Aainvariant_V7V5V6Aainfix <=V7ainfix +ax2c1Aainfix <=c0V7Iainfix =V7ainfix +V2c1FIainfix =V6ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V5ainfix +V1c1FAabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFFAainvariant_c0c0ainfix -ainfix *c2ay2ax2Aainfix <=c0ainfix +ax2c1Aainfix <=c0c0">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter bresenham.1" expl="loop invariant init" sum="d74af23f66377fe846029ad998e78c6c" proved="true" expanded="true" shape="ainvariant_c0c0ainfix -ainfix *c2ay2ax2Aainfix <=c0ainfix +ax2c1Aainfix <=c0c0">