Commit 63b26ce4 authored by MARCHE Claude's avatar MARCHE Claude

update obsolete proof sessions

parent 21699e75
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="examples/check-builtin/floats/why3session.xml">
name="check-builtin/floats/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
......@@ -9,7 +9,7 @@
<prover
id="coq"
name="Coq"
version="8.2pl1"/>
version="8.3pl2"/>
<prover
id="cvc3"
name="CVC3"
......@@ -17,11 +17,23 @@
<prover
id="gappa"
name="Gappa"
version="0.13.0"/>
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"
......@@ -36,7 +48,7 @@
expanded="true">
<goal
name="Round_single_01"
sum="b356284ef3c67cc31bb22f6c7deae9f0"
sum="4350d059bf72b21b36729eaccc394959"
proved="true"
expanded="true"
shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.99999ap-4">
......@@ -45,12 +57,12 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Round_double_01"
sum="a981e04c08472362dcca34e0f3487b74"
sum="fc4b69caf28748e651e23f375e300b70"
proved="true"
expanded="true"
shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.999999999999ap-4">
......@@ -59,12 +71,12 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test00"
sum="532babe00b8785ec6f7286621c12a512"
sum="d126875bf4fc484b4b44c2b52b9da437"
proved="true"
expanded="true"
shape="ainfix <=aprefix -c3.0V0Iainfix <=aabsV0c2.0F">
......@@ -73,33 +85,33 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="gappa"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test01"
sum="a2dc5970c8ef3c553ea90e0fc634da83"
sum="bcbfbae3da81b362e99b319253ef2a20"
proved="true"
expanded="true"
shape="ainfix <=aabsainfix -ainfix *avalueV0avalueV0aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix <=avalueV0c2.0Aainfix <=aprefix -c2.0avalueV0F">
......@@ -108,12 +120,12 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test02"
sum="eb102544c66926067fe7350ea3f1ba87"
sum="1d3e20e12a14b6bd91a25d057da3b098"
proved="true"
expanded="true"
shape="ainfix <=aabsainfix -ainfix *avalueV1avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix =V1V0Iainfix <=aabsavalueV0c2.0F">
......@@ -122,12 +134,12 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test03"
sum="3d36d4470fa7e12c3ba550960abf7a6c"
sum="42c26c3443d67722883a37dfe8f9253c"
proved="true"
expanded="true"
shape="ainfix <=asqrtainfix *ainfix -avalueV2ainfix *avalueV0avalueV0ainfix -avalueV1ainfix *avalueV0avalueV0c0x1.p-52Iainfix =V2V1Iainfix =avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0Iainfix <=aabsavalueV0c2.0F">
......@@ -136,7 +148,7 @@
timelimit="5"
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="programs/muller/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../muller.mlw" verified="true" expanded="true">
<theory name="WP Muller" verified="true" expanded="true">
<goal name="WP_parameter compact" expl="parameter compact" sum="199cbe3428eff0829e3355f60d4e5947" proved="true" expanded="true" shape="iainfix =agetV1V6c0Nainfix <=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V8anum_ofV1c0ainfix +V6c1Aainfix <=c0V8Iainfix =V8ainfix +V5c1FIainfix =V7asetV4V5agetV1V6FAainfix <V5V2Aainfix <=c0V5Aainfix <V6V0Aainfix <=c0V6ainfix <=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V5anum_ofV1c0ainfix +V6c1Aainfix <=c0V5Aainfix <V6V0Aainfix <=c0V6Iainfix <=anum_ofV1c0V6V6Aainfix =V5anum_ofV1c0V6Aainfix <=c0V5Iainfix <=V6ainfix -V0c1Aainfix <=c0V6FFFAainfix <=anum_ofV1c0c0c0Aainfix =V3anum_ofV1c0c0Aainfix <=c0V3Iainfix <=c0ainfix -V0c1Iainfix =V3c0FAainfix >=V2c0Iainfix <=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix <=c0V2Aiainfix =agetV1V9c0Nainfix <=anum_ofV1c0ainfix +V9c1ainfix +V9c1Aainfix =V10anum_ofV1c0ainfix +V9c1Aainfix <=c0V10Iainfix =V10ainfix +V2c1Fainfix <=anum_ofV1c0ainfix +V9c1ainfix +V9c1Aainfix =V2anum_ofV1c0ainfix +V9c1Aainfix <=c0V2Aainfix <V9V0Aainfix <=c0V9Iainfix <=anum_ofV1c0V9V9Aainfix =V2anum_ofV1c0V9Aainfix <=c0V2Iainfix <=V9ainfix -V0c1Aainfix <=c0V9FFAainfix <=anum_ofV1c0c0c0Aainfix =c0anum_ofV1c0c0Aainfix <=c0c0Iainfix <=c0ainfix -V0c1Aiainfix =agetV1V14c0Nainfix <=anum_ofV1c0ainfix +V14c1ainfix +V14c1Aainfix =V16anum_ofV1c0ainfix +V14c1Aainfix <=c0V16Iainfix =V16ainfix +V13c1FIainfix =V15asetV12V13agetV1V14FAainfix <V13c0Aainfix <=c0V13Aainfix <V14V0Aainfix <=c0V14ainfix <=anum_ofV1c0ainfix +V14c1ainfix +V14c1Aainfix =V13anum_ofV1c0ainfix +V14c1Aainfix <=c0V13Aainfix <V14V0Aainfix <=c0V14Iainfix <=anum_ofV1c0V14V14Aainfix =V13anum_ofV1c0V14Aainfix <=c0V13Iainfix <=V14ainfix -V0c1Aainfix <=c0V14FFFAainfix <=anum_ofV1c0c0c0Aainfix =V11anum_ofV1c0c0Aainfix <=c0V11Iainfix <=c0ainfix -V0c1Iainfix =V11c0FAainfix >=c0c0Iainfix >c0ainfix -V0c1FF">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter compact.1" expl="precondition" sum="6c3030d41d5aca45af2bdfb8c97604fc" proved="true" expanded="true" shape="ainfix >=c0c0Iainfix >c0ainfix -V0c1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<why3session
name="programs/muller/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="../muller.mlw"
verified="true"
expanded="true">
<theory
name="WP Muller"
verified="true"
expanded="true">
<goal
name="WP_parameter compact"
expl="parameter compact"
sum="64672b3e7a2efc092b0ee8b665eafa4d"
proved="true"
expanded="true"
shape="iainfix =agetV1V6c0Nainfix <=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V8anum_ofV1c0ainfix +V6c1Aainfix <=c0V8Iainfix =V8ainfix +V5c1FIainfix =V7asetV4V5agetV1V6FAainfix <V5V2Aainfix <=c0V5Aainfix <V6V0Aainfix <=c0V6ainfix <=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V5anum_ofV1c0ainfix +V6c1Aainfix <=c0V5Aainfix <V6V0Aainfix <=c0V6Iainfix <=anum_ofV1c0V6V6Aainfix =V5anum_ofV1c0V6Aainfix <=c0V5Iainfix <=V6ainfix -V0c1Aainfix <=c0V6FFFAainfix <=anum_ofV1c0c0c0Aainfix =V3anum_ofV1c0c0Aainfix <=c0V3Iainfix <=c0ainfix -V0c1Iainfix =V3c0FAainfix >=V2c0Iainfix <=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix <=c0V2Aiainfix =agetV1V9c0Nainfix <=anum_ofV1c0ainfix +V9c1ainfix +V9c1Aainfix =V10anum_ofV1c0ainfix +V9c1Aainfix <=c0V10Iainfix =V10ainfix +V2c1Fainfix <=anum_ofV1c0ainfix +V9c1ainfix +V9c1Aainfix =V2anum_ofV1c0ainfix +V9c1Aainfix <=c0V2Aainfix <V9V0Aainfix <=c0V9Iainfix <=anum_ofV1c0V9V9Aainfix =V2anum_ofV1c0V9Aainfix <=c0V2Iainfix <=V9ainfix -V0c1Aainfix <=c0V9FFAainfix <=anum_ofV1c0c0c0Aainfix =c0anum_ofV1c0c0Aainfix <=c0c0Iainfix <=c0ainfix -V0c1Aiainfix =agetV1V14c0Nainfix <=anum_ofV1c0ainfix +V14c1ainfix +V14c1Aainfix =V16anum_ofV1c0ainfix +V14c1Aainfix <=c0V16Iainfix =V16ainfix +V13c1FIainfix =V15asetV12V13agetV1V14FAainfix <V13c0Aainfix <=c0V13Aainfix <V14V0Aainfix <=c0V14ainfix <=anum_ofV1c0ainfix +V14c1ainfix +V14c1Aainfix =V13anum_ofV1c0ainfix +V14c1Aainfix <=c0V13Aainfix <V14V0Aainfix <=c0V14Iainfix <=anum_ofV1c0V14V14Aainfix =V13anum_ofV1c0V14Aainfix <=c0V13Iainfix <=V14ainfix -V0c1Aainfix <=c0V14FFFAainfix <=anum_ofV1c0c0c0Aainfix =V11anum_ofV1c0c0Aainfix <=c0V11Iainfix <=c0ainfix -V0c1Iainfix =V11c0FAainfix >=c0c0Iainfix >c0ainfix -V0c1FF">
<transf
name="split_goal"
proved="true"
expanded="true">
<goal
name="WP_parameter compact.1"
expl="precondition"
sum="7ab9a7fe054cc3f79fce84360c33c0fb"
proved="true"
expanded="true"
shape="ainfix >=c0c0Iainfix >c0ainfix -V0c1FF">
<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.03"/>
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="WP_parameter compact.2" expl="for loop initialization" sum="2bcce785c763c3cb52e78fd3d7d04937" proved="true" expanded="true" shape="ainfix <=anum_ofV1c0c0c0Aainfix =V2anum_ofV1c0c0Aainfix <=c0V2Iainfix <=c0ainfix -V0c1Iainfix =V2c0FIainfix >=c0c0Iainfix >c0ainfix -V0c1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<goal
name="WP_parameter compact.2"
expl="for loop initialization"
sum="846707997ff357d052b12b2b479875f5"
proved="true"
expanded="true"
shape="ainfix <=anum_ofV1c0c0c0Aainfix =V2anum_ofV1c0c0Aainfix <=c0V2Iainfix <=c0ainfix -V0c1Iainfix =V2c0FIainfix >=c0c0Iainfix >c0ainfix -V0c1FF">
<proof
prover="cvc3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<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.03"/>
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter compact.3" expl="for loop preservation" sum="de475910adf8d5aa313ce875c86833e8" proved="true" expanded="true" shape="iainfix =agetV1V5c0Nainfix <=anum_ofV1c0ainfix +V5c1ainfix +V5c1Aainfix =V7anum_ofV1c0ainfix +V5c1Aainfix <=c0V7Iainfix =V7ainfix +V4c1FIainfix =V6asetV3V4agetV1V5FAainfix <V4c0Aainfix <=c0V4Aainfix <V5V0Aainfix <=c0V5ainfix <=anum_ofV1c0ainfix +V5c1ainfix +V5c1Aainfix =V4anum_ofV1c0ainfix +V5c1Aainfix <=c0V4Aainfix <V5V0Aainfix <=c0V5Iainfix <=anum_ofV1c0V5V5Aainfix =V4anum_ofV1c0V5Aainfix <=c0V4Iainfix <=V5ainfix -V0c1Aainfix <=c0V5FFFIainfix <=c0ainfix -V0c1Iainfix =V2c0FIainfix >=c0c0Iainfix >c0ainfix -V0c1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<goal
name="WP_parameter compact.3"
expl="for loop preservation"
sum="846df15b2d09e49c92d2c3fcb5ae5b2b"
proved="true"
expanded="true"
shape="iainfix =agetV1V5c0Nainfix <=anum_ofV1c0ainfix +V5c1ainfix +V5c1Aainfix =V7anum_ofV1c0ainfix +V5c1Aainfix <=c0V7Iainfix =V7ainfix +V4c1FIainfix =V6asetV3V4agetV1V5FAainfix <V4c0Aainfix <=c0V4Aainfix <V5V0Aainfix <=c0V5ainfix <=anum_ofV1c0ainfix +V5c1ainfix +V5c1Aainfix =V4anum_ofV1c0ainfix +V5c1Aainfix <=c0V4Aainfix <V5V0Aainfix <=c0V5Iainfix <=anum_ofV1c0V5V5Aainfix =V4anum_ofV1c0V5Aainfix <=c0V4Iainfix <=V5ainfix -V0c1Aainfix <=c0V5FFFIainfix <=c0ainfix -V0c1Iainfix =V2c0FIainfix >=c0c0Iainfix >c0ainfix -V0c1FF">
<proof
prover="cvc3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter compact.4" expl="for loop initialization" sum="f5287bb871d14db412179b4328d414ea" proved="true" expanded="true" shape="ainfix <=anum_ofV1c0c0c0Aainfix =c0anum_ofV1c0c0Aainfix <=c0c0Iainfix <=c0ainfix -V0c1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<goal
name="WP_parameter compact.4"
expl="for loop initialization"
sum="e9dbcffca310c8d6b9006e842776e9a9"
proved="true"
expanded="true"
shape="ainfix <=anum_ofV1c0c0c0Aainfix =c0anum_ofV1c0c0Aainfix <=c0c0Iainfix <=c0ainfix -V0c1FF">
<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.03"/>
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter compact.5" expl="for loop preservation" sum="90345f3f3fbf5ffccfe847869df0b67e" proved="true" expanded="true" shape="iainfix =agetV1V3c0Nainfix <=anum_ofV1c0ainfix +V3c1ainfix +V3c1Aainfix =V4anum_ofV1c0ainfix +V3c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1Fainfix <=anum_ofV1c0ainfix +V3c1ainfix +V3c1Aainfix =V2anum_ofV1c0ainfix +V3c1Aainfix <=c0V2Aainfix <V3V0Aainfix <=c0V3Iainfix <=anum_ofV1c0V3V3Aainfix =V2anum_ofV1c0V3Aainfix <=c0V2Iainfix <=V3ainfix -V0c1Aainfix <=c0V3FFIainfix <=c0ainfix -V0c1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<goal
name="WP_parameter compact.5"
expl="for loop preservation"
sum="ae7a8a36678a4aa212199a9a1af9d1aa"
proved="true"
expanded="true"
shape="iainfix =agetV1V3c0Nainfix <=anum_ofV1c0ainfix +V3c1ainfix +V3c1Aainfix =V4anum_ofV1c0ainfix +V3c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1Fainfix <=anum_ofV1c0ainfix +V3c1ainfix +V3c1Aainfix =V2anum_ofV1c0ainfix +V3c1Aainfix <=c0V2Aainfix <V3V0Aainfix <=c0V3Iainfix <=anum_ofV1c0V3V3Aainfix =V2anum_ofV1c0V3Aainfix <=c0V2Iainfix <=V3ainfix -V0c1Aainfix <=c0V3FFIainfix <=c0ainfix -V0c1FF">
<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.05"/>
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.04"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter compact.6" expl="precondition" sum="cc20a288fcb1a7dd081072845705f406" proved="true" expanded="true" shape="ainfix >=V2c0Iainfix <=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix <=c0V2FIainfix <=c0ainfix -V0c1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<goal
name="WP_parameter compact.6"
expl="precondition"
sum="38edff5bd35566635e235b736236c61d"
proved="true"
expanded="true"
shape="ainfix >=V2c0Iainfix <=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix <=c0V2FIainfix <=c0ainfix -V0c1FF">
<proof
prover="cvc3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter compact.7" expl="for loop initialization" sum="c808a28af9ecbd8d0c27c0c39fd0a7a6" proved="true" expanded="true" shape="ainfix <=anum_ofV1c0c0c0Aainfix =V3anum_ofV1c0c0Aainfix <=c0V3Iainfix <=c0ainfix -V0c1Iainfix =V3c0FIainfix >=V2c0Iainfix <=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix <=c0V2FIainfix <=c0ainfix -V0c1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<goal
name="WP_parameter compact.7"
expl="for loop initialization"
sum="eb82285d7d3d60ca39435ee968e03f4c"
proved="true"
expanded="true"
shape="ainfix <=anum_ofV1c0c0c0Aainfix =V3anum_ofV1c0c0Aainfix <=c0V3Iainfix <=c0ainfix -V0c1Iainfix =V3c0FIainfix >=V2c0Iainfix <=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix <=c0V2FIainfix <=c0ainfix -V0c1FF">
<proof
prover="cvc3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter compact.8" expl="for loop preservation" sum="a64be74b762c3de543dddce122a7c4cf" proved="true" expanded="true" shape="iainfix =agetV1V6c0Nainfix <=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V8anum_ofV1c0ainfix +V6c1Aainfix <=c0V8Iainfix =V8ainfix +V5c1FIainfix =V7asetV4V5agetV1V6FAainfix <V5V2Aainfix <=c0V5Aainfix <V6V0Aainfix <=c0V6ainfix <=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V5anum_ofV1c0ainfix +V6c1Aainfix <=c0V5Aainfix <V6V0Aainfix <=c0V6Iainfix <=anum_ofV1c0V6V6Aainfix =V5anum_ofV1c0V6Aainfix <=c0V5Iainfix <=V6ainfix -V0c1Aainfix <=c0V6FFFIainfix <=c0ainfix -V0c1Iainfix =V3c0FIainfix >=V2c0Iainfix <=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix <=c0V2FIainfix <=c0ainfix -V0c1FF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.10"/>
<goal
name="WP_parameter compact.8"
expl="for loop preservation"
sum="33bcca83eb809eebe713a95d46403d05"
proved="true"
expanded="true"
shape="iainfix =agetV1V6c0Nainfix <=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V8anum_ofV1c0ainfix +V6c1Aainfix <=c0V8Iainfix =V8ainfix +V5c1FIainfix =V7asetV4V5agetV1V6FAainfix <V5V2Aainfix <=c0V5Aainfix <V6V0Aainfix <=c0V6ainfix <=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V5anum_ofV1c0ainfix +V6c1Aainfix <=c0V5Aainfix <V6V0Aainfix <=c0V6Iainfix <=anum_ofV1c0V6V6Aainfix =V5anum_ofV1c0V6Aainfix <=c0V5Iainfix <=V6ainfix -V0c1Aainfix <=c0V6FFFIainfix <=c0ainfix -V0c1Iainfix =V3c0FIainfix >=V2c0Iainfix <=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix <=c0V2FIainfix <=c0ainfix -V0c1FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.09"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.05"/>
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
......
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