Commit 070c6ff5 authored by MARCHE Claude's avatar MARCHE Claude

update sessions

parent c27a7862
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="check-builtin/real/why3session.xml" shape_version="2">
name="examples/check-builtin/real/why3session.xml" shape_version="2">
<prover
id="0"
name="Alt-Ergo"
......@@ -40,13 +40,13 @@
expanded="true">
<theory
name="Test"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="1" loccnumb="7" loccnume="11"
verified="true"
expanded="false">
<goal
name="G1"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="3" loccnumb="7" loccnume="9"
sum="f207e29e9079f1be6781c87d4c160c81"
proved="true"
......@@ -111,7 +111,7 @@
</goal>
<goal
name="G2"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="4" loccnumb="7" loccnume="9"
sum="9e04fefcbd74163191244b6b8d7562ea"
proved="true"
......@@ -168,7 +168,7 @@
</goal>
<goal
name="G3"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="5" loccnumb="7" loccnume="9"
sum="1a2d5acb41bac2a5d5a5ae9a44802cf2"
proved="true"
......@@ -218,13 +218,13 @@
</theory>
<theory
name="TestInfix"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="8" loccnumb="7" loccnume="16"
verified="true"
expanded="false">
<goal
name="Add"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="10" loccnumb="7" loccnume="10"
sum="0e9baf7fe8694089437161de221049eb"
proved="true"
......@@ -281,7 +281,7 @@
</goal>
<goal
name="Sub"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="11" loccnumb="7" loccnume="10"
sum="b96ec09f1f28908a2a176b392f18f9d1"
proved="true"
......@@ -338,7 +338,7 @@
</goal>
<goal
name="Neg"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="12" loccnumb="7" loccnume="10"
sum="d23a894b757b84a44b8fff0618108d37"
proved="true"
......@@ -395,7 +395,7 @@
</goal>
<goal
name="Mul"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="13" loccnumb="7" loccnume="10"
sum="e29404325109ec3f401b46eee6e14b98"
proved="true"
......@@ -452,7 +452,7 @@
</goal>
<goal
name="Div"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="14" loccnumb="7" loccnume="10"
sum="c06e2f7b6439bb0fb78135acce05d589"
proved="true"
......@@ -509,7 +509,7 @@
</goal>
<goal
name="Inv"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="15" loccnumb="7" loccnume="10"
sum="7a5279ca7f27da7d779586f6eb3b0123"
proved="true"
......@@ -559,13 +559,13 @@
</theory>
<theory
name="SquareTest"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="19" loccnumb="7" loccnume="17"
verified="true"
expanded="false">
<goal
name="Sqrt_zero"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="23" loccnumb="8" loccnume="17"
sum="b353ced9b0f041c36c827f26d50b3acd"
proved="true"
......@@ -622,7 +622,7 @@
</goal>
<goal
name="Sqrt_one"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="24" loccnumb="8" loccnume="16"
sum="e8ec282b918f9ea65664f75b3f6ba8f4"
proved="true"
......@@ -679,7 +679,7 @@
</goal>
<goal
name="Sqrt_four"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="25" loccnumb="8" loccnume="17"
sum="84ef0743ccce40f492768328498afce8"
proved="true"
......@@ -737,17 +737,17 @@
</theory>
<theory
name="ExpLogTest"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="29" loccnumb="7" loccnume="17"
verified="true"
expanded="false">
expanded="true">
<goal
name="Log_e"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="33" loccnumb="8" loccnume="13"
sum="da0b025851b39560876d3ece835be34c"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =alogaec1.0">
<proof
prover="6"
......@@ -793,17 +793,17 @@
</theory>
<theory
name="PowerIntTest"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="38" loccnumb="7" loccnume="19"
verified="true"
expanded="false">
expanded="true">
<goal
name="Pow_2_2"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="42" loccnumb="8" loccnume="15"
sum="b4f39dbe2ac4dd89e455abedb473c966"
sum="fef17c8a45382b4eb8b4a61320e3c724"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =apowerc2.0c2c4.0">
<proof
prover="6"
......@@ -811,7 +811,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="3.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="2"
......@@ -819,7 +819,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="0"
......@@ -835,7 +835,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.16"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
......@@ -851,7 +851,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="3.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
......@@ -865,17 +865,17 @@
</theory>
<theory
name="PowerRealTest"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="47" loccnumb="7" loccnume="20"
verified="true"
expanded="false">
expanded="true">
<goal
name="Pow_2_2"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="51" loccnumb="8" loccnume="15"
sum="38a4f95c27069a2dc6dcd4d7442ce8f7"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =apowc2.0c2.0c4.0">
<proof
prover="6"
......@@ -905,17 +905,17 @@
</theory>
<theory
name="TrigonometryTest"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="56" loccnumb="7" loccnume="23"
verified="false"
expanded="true">
<goal
name="Cos_2_pi"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="62" loccnumb="8" loccnume="16"
sum="fed2556e175a5a894d0c067466ee4ba5"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =acosainfix *c2.0apic1.0">
<proof
prover="6"
......@@ -960,11 +960,11 @@
</goal>
<goal
name="Sin_2_pi"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="63" loccnumb="8" loccnume="16"
sum="f3bd7f5c25e900c5b9192d125cd94d8d"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =asinainfix *c2.0apic0.">
<proof
prover="6"
......@@ -1017,7 +1017,7 @@
</goal>
<goal
name="Tan_pi_3"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="64" loccnumb="8" loccnume="16"
sum="71dffba24c326a5ef2b7a294be8367b5"
proved="false"
......@@ -1058,7 +1058,7 @@
</goal>
<goal
name="Atan_1"
locfile="check-builtin/real/../real.why"
locfile="examples/check-builtin/real/../real.why"
loclnum="65" loccnumb="8" loccnume="14"
sum="706631d649ed857b77c6d151ceb04080"
proved="false"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/users/demons/melquion/src/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="programs/fibonacci/why3session.xml" shape_version="2">
<prover
......@@ -129,7 +129,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
......@@ -180,7 +180,7 @@
locfile="programs/fibonacci/../fibonacci.mlw"
loclnum="82" loccnumb="10" loccnume="16"
expl="parameter logfib"
sum="2526b0e81d12220c19c57324bf629779"
sum="be18b57a378e8f58833c62cc4852ff5c"
proved="true"
expanded="true"
shape="iainfix =V0c0ainfix =apoweramk tc1c1c1c0V0amk tainfix +c1c0c0c0c1iainfix =amodV0c2c0ainfix =apoweramk tc1c1c1c0V0amk tainfix +V3V4V4V4V3Lainfix *V2ainfix +V1ainfix +V1V2Lainfix +ainfix *V1V1ainfix *V2V2ainfix =apoweramk tc1c1c1c0V0amk tainfix +V5V6V6V6V5Lainfix +ainfix *ainfix +V1V2ainfix +V1V2ainfix *V2V2Lainfix *V2ainfix +V1ainfix +V1V2Iainfix =apoweramk tc1c1c1c0adivV0c2amk tainfix +V1V2V2V2V1FAainfix &gt;=adivV0c2c0Aainfix &lt;adivV0c2V0Aainfix &lt;=c0V0Iainfix &gt;=V0c0F">
......@@ -195,7 +195,7 @@
locfile="programs/fibonacci/../fibonacci.mlw"
loclnum="82" loccnumb="10" loccnume="16"
expl="normal postcondition"
sum="36d3b040d642938ca7ab1c11a0386d09"
sum="54ff9f48d80a0d661479ac9f4110b022"
proved="true"
expanded="true"
shape="ainfix =apoweramk tc1c1c1c0V0amk tainfix +c1c0c0c0c1Iainfix =V0c0Iainfix &gt;=V0c0F">
......@@ -215,7 +215,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
......@@ -223,7 +223,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="5"
......@@ -239,7 +239,7 @@
locfile="programs/fibonacci/../fibonacci.mlw"
loclnum="82" loccnumb="10" loccnume="16"
expl="variant decreases"
sum="9110e5c78dde7dc854b68f0123a1f7d6"
sum="024ee6b3b1eb5f5cb113823603c892cf"
proved="true"
expanded="true"
shape="ainfix &lt;adivV0c2V0Aainfix &lt;=c0V0Iainfix =V0c0NIainfix &gt;=V0c0F">
......@@ -259,7 +259,7 @@
locfile="programs/fibonacci/../fibonacci.mlw"
loclnum="82" loccnumb="10" loccnume="16"
expl="precondition"
sum="1a9530915bb70f4970658760154ce9be"
sum="f98d6f543cdf82e62fc44c18db5e7230"
proved="true"
expanded="true"
shape="ainfix &gt;=adivV0c2c0Iainfix =V0c0NIainfix &gt;=V0c0F">
......@@ -271,7 +271,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
......@@ -287,7 +287,7 @@
locfile="programs/fibonacci/../fibonacci.mlw"
loclnum="82" loccnumb="10" loccnume="16"
expl="normal postcondition"
sum="e0752ea6e2dbb33d3166821685e4cb5e"
sum="807ed294a6590eb6e850dbd8ab7ffd80"
proved="true"
expanded="false"
shape="iainfix =amodV0c2c0ainfix =apoweramk tc1c1c1c0V0amk tainfix +V3V4V4V4V3Lainfix *V2ainfix +V1ainfix +V1V2Lainfix +ainfix *V1V1ainfix *V2V2ainfix =apoweramk tc1c1c1c0V0amk tainfix +V5V6V6V6V5Lainfix +ainfix *ainfix +V1V2ainfix +V1V2ainfix *V2V2Lainfix *V2ainfix +V1ainfix +V1V2Iainfix =apoweramk tc1c1c1c0adivV0c2amk tainfix +V1V2V2V2V1FIainfix &gt;=adivV0c2c0Aainfix &lt;adivV0c2V0Aainfix &lt;=c0V0Iainfix =V0c0NIainfix &gt;=V0c0F">
......@@ -300,7 +300,7 @@
edited="fibonacci_WP_FibonacciLogarithmic_WP_parameter_logfib_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.71"/>
<result status="valid" time="0.61"/>
</proof>
</goal>
</transf>
......@@ -309,7 +309,7 @@
name="fib_m"
locfile="programs/fibonacci/../fibonacci.mlw"
loclnum="105" loccnumb="8" loccnume="13"
sum="050824b0dde7854ecda811bf66dcd3a7"
sum="a63b2ce2736615025314f4148f50ebfc"
proved="true"
expanded="true"
shape="ainfix =afibV0aa21V1Aainfix =afibainfix +V0c1aa11V1Lapoweram1110V0Iainfix &gt;=V0c0F">
......@@ -320,7 +320,7 @@
edited="fibonacci_WP_FibonacciLogarithmic_fib_m_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.57"/>
<result status="valid" time="0.56"/>
</proof>
</goal>
<goal
......@@ -328,7 +328,7 @@
locfile="programs/fibonacci/../fibonacci.mlw"
loclnum="109" loccnumb="6" loccnume="10"
expl="parameter fibo"
sum="7d85b79fbc6d3c189b9db5c7bca4161d"
sum="c3f07c9fe36f4699cf6d127472aa26e7"
proved="true"
expanded="false"
shape="ainfix =V2afibV0Iainfix =apoweramk tc1c1c1c0V0amk tainfix +V1V2V2V2V1FAainfix &gt;=V0c0Iainfix &gt;=V0c0F">
......@@ -348,7 +348,7 @@
memlimit="0"
obsolete="false"
archived="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 "/users/demons/melquion/src/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="programs/power/why3session.xml" shape_version="2">
<prover
......@@ -33,7 +33,7 @@
locfile="programs/power/../power.mlw"
loclnum="12" loccnumb="10" loccnume="18"
expl="parameter fast_exp"
sum="1d493baac0984392d82deabdc40d138d"
sum="5d2dbc7b3b3cc6dd8b9270ada26a4fe1"
proved="true"
expanded="true"
shape="iainfix =V1c0ainfix =c1apowerV0V1ainfix =iainfix =amodV1c2c0ainfix *V2V2ainfix *ainfix *V2V2V0apowerV0V1LapowerV0adivV1c2Aainfix &lt;=c0adivV1c2Aainfix &lt;adivV1c2V1Aainfix &lt;=c0V1Iainfix &lt;=c0V1F">
......@@ -45,7 +45,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.34"/>
<result status="valid" time="0.63"/>
</proof>
</goal>
<goal
......@@ -53,7 +53,7 @@
locfile="programs/power/../power.mlw"
loclnum="26" loccnumb="6" loccnume="25"
expl="parameter fast_exp_imperative"
sum="702cbee10d47aea1f53c1fea2a7a3217"
sum="146ef0ae7be3162b87b8ff835e41b36a"
proved="true"
expanded="true"
shape="iainfix &gt;V2c0iainfix =amodV2c2c1ainfix &lt;V7V2Aainfix &lt;=c0V2Aainfix =ainfix *V5apowerV6V7apowerV0V1Aainfix &lt;=c0V7Iainfix =V7adivV2c2FIainfix =V6ainfix *V3V3FIainfix =V5ainfix *V4V3Fainfix &lt;V9V2Aainfix &lt;=c0V2Aainfix =ainfix *V4apowerV8V9apowerV0V1Aainfix &lt;=c0V9Iainfix =V9adivV2c2FIainfix =V8ainfix *V3V3Fainfix =V4apowerV0V1Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix &lt;=c0V2FAainfix =ainfix *c1apowerV0V1apowerV0V1Aainfix &lt;=c0V1Iainfix &lt;=c0V1F">
......@@ -68,7 +68,7 @@
locfile="programs/power/../power.mlw"
loclnum="26" loccnumb="6" loccnume="25"
expl="loop invariant init"
sum="012b0f52a831bf99e53c11a1668fcca4"
sum="ad4c055baa1407245020e28fb785ba9f"
proved="true"
expanded="true"
shape="ainfix =ainfix *c1apowerV0V1apowerV0V1Aainfix &lt;=c0V1Iainfix &lt;=c0V1F">
......@@ -88,7 +88,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
......@@ -104,7 +104,7 @@
locfile="programs/power/../power.mlw"
loclnum="26" loccnumb="6" loccnume="25"
expl="loop invariant preservation"
sum="e4420e6abf973848f1848269a2d610fb"
sum="13044e594a3030772f89e9f60f9063df"
proved="true"
expanded="true"
shape="ainfix =ainfix *V5apowerV6V7apowerV0V1Aainfix &lt;=c0V7Iainfix =V7adivV2c2FIainfix =V6ainfix *V3V3FIainfix =V5ainfix *V4V3FIainfix =amodV2c2c1Iainfix &gt;V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix &lt;=c0V2FIainfix &lt;=c0V1F">
......@@ -119,7 +119,7 @@
locfile="programs/power/../power.mlw"
loclnum="26" loccnumb="6" loccnume="25"
expl="parameter fast_exp_imperative"
sum="30230b2fae551e81b9a81ccc63aa4f80"
sum="2344073fadc09d4910ac2999968acf33"
proved="true"
expanded="true"
shape="ainfix &lt;=c0V7Iainfix =V7adivV2c2FIainfix =V6ainfix *V3V3FIainfix =V5ainfix *V4V3FIainfix =amodV2c2c1Iainfix &gt;V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix &lt;=c0V2FIainfix &lt;=c0V1F">
......@@ -131,7 +131,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
......@@ -139,7 +139,7 @@
locfile="programs/power/../power.mlw"
loclnum="26" loccnumb="6" loccnume="25"
expl="parameter fast_exp_imperative"
sum="6a8ac636d9bbf31e8177f1bb0fa6f595"
sum="a58d242ec3503637599faaa5d1a82ac6"
proved="true"
expanded="true"
shape="ainfix =ainfix *V5apowerV6V7apowerV0V1Iainfix =V7adivV2c2FIainfix =V6ainfix *V3V3FIainfix =V5ainfix *V4V3FIainfix =amodV2c2c1Iainfix &gt;V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix &lt;=c0V2FIainfix &lt;=c0V1F">
......@@ -152,7 +152,7 @@
edited="power_M_WP_parameter_fast_exp_imperative_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.62"/>
<result status="valid" time="0.56"/>
</proof>
</goal>
</transf>
......@@ -162,7 +162,7 @@
locfile="programs/power/../power.mlw"
loclnum="26" loccnumb="6" loccnume="25"
expl="loop variant decreases"
sum="7546e1ec40eda0d6e155c79001082e2b"
sum="85f37d57cd9814e76384b34b3e77bd56"
proved="true"
expanded="true"
shape="ainfix &lt;V7V2Aainfix &lt;=c0V2Iainfix =V7adivV2c2FIainfix =V6ainfix *V3V3FIainfix =V5ainfix *V4V3FIainfix =amodV2c2c1Iainfix &gt;V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix &lt;=c0V2FIainfix &lt;=c0V1F">
......@@ -174,7 +174,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
......@@ -190,7 +190,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
......@@ -198,7 +198,7 @@
locfile="programs/power/../power.mlw"
loclnum="26" loccnumb="6" loccnume="25"
expl="loop invariant preservation"
sum="3f1e48e808eb9427dc75810577d5bbc9"
sum="f04174bb93fc9a97e8c3970d3b4fa67b"
proved="true"
expanded="true"
shape="ainfix =ainfix *V4apowerV5V6apowerV0V1Aainfix &lt;=c0V6Iainfix =V6adivV2c2FIainfix =V5ainfix *V3V3FIainfix =amodV2c2c1NIainfix &gt;V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix &lt;=c0V2FIainfix &lt;=c0V1F">
......@@ -213,7 +213,7 @@
locfile="programs/power/../power.mlw"
loclnum="26" loccnumb="6" loccnume="25"
expl="parameter fast_exp_imperative"
sum="4ff3476a487a46b317298d8cc80935f0"
sum="c40518c1390bb87940d1a913516d5454"
proved="true"
expanded="true"
shape="ainfix &lt;=c0V6Iainfix =V6adivV2c2FIainfix =V5ainfix *V3V3FIainfix =amodV2c2c1NIainfix &gt;V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix &lt;=c0V2FIainfix &lt;=c0V1F">
......@@ -225,7 +225,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
......@@ -233,7 +233,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
......@@ -249,7 +249,7 @@
locfile="programs/power/../power.mlw"
loclnum="26" loccnumb="6" loccnume="25"
expl="parameter fast_exp_imperative"
sum="51acba726e3547655858ecdf95282d50"
sum="c17b6c4983c24dfa5bc0591038a2bee3"
proved="true"
expanded="true"
shape="ainfix =ainfix *V4apowerV5V6apowerV0V1Iainfix =V6adivV2c2FIainfix =V5ainfix *V3V3FIainfix =amodV2c2c1NIainfix &gt;V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix &lt;=c0V2FIainfix &lt;=c0V1F">
......@@ -262,7 +262,7 @@
edited="power_WP_M_WP_parameter_fast_exp_imperative_3.v"
obsolete="false"
archived="false">
<result status="valid" time="0.63"/>
<result status="valid" time="0.62"/>
</proof>
</goal>
</transf>
......@@ -272,7 +272,7 @@
locfile="programs/power/../power.mlw"
loclnum="26" loccnumb="6" loccnume="25"
expl="loop variant decreases"
sum="af10b48a5033d26c83f3d3b2ba546a02"
sum="ede4281eedd671e2f6461100d44b34a2"
proved="true"
expanded="true"
shape="ainfix &lt;V6V2Aainfix &lt;=c0V2Iainfix =V6adivV2c2FIainfix =V5ainfix *V3V3FIainfix =amodV2c2c1NIainfix &gt;V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix &lt;=c0V2FIainfix &lt;=c0V1F">
......@@ -284,7 +284,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
......@@ -292,7 +292,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
......@@ -308,7 +308,7 @@
locfile="programs/power/../power.mlw"
loclnum="26" loccnumb="6" loccnume="25"
expl="normal postcondition"
sum="f06747057f68d0993b46c115ca726543"
sum="48a9c79cc9b30da9de2dedb5852b9189"
proved="true"
expanded="true"
shape="ainfix =V4apowerV0V1Iainfix &gt;V2c0NIainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix &lt;=c0V2FIainfix &lt;=c0V1F">
......@@ -323,7 +323,7 @@
locfile="programs/power/../power.mlw"
loclnum="26" loccnumb="6" loccnume="25"
expl="normal postcondition"
sum="f06747057f68d0993b46c115ca726543"
sum="48a9c79cc9b30da9de2dedb5852b9189"
proved="true"
expanded="true"
shape="ainfix =V4apowerV0V1Iainfix &gt;V2c0NIainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix &lt;=c0V2FIainfix &lt;=c0V1F">
......
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -20,7 +20,7 @@
name="pow_eps2_max_int"
locfile="tests-provers/coq-interval/../coq-interval.why"
loclnum="6" loccnumb="7" loccnume="23"
sum="af4e3aae419b8421e306b6c39490401a"
sum="b5f712d3c2d0add5ba666a70b3ff7137"
proved="true"
expanded="true"
shape="ainfix &lt;=apowerainfix +c1.0ainfix +c0x7.p-50c0x3.p-53c2147483647c2.0">
......@@ -31,7 +31,7 @@
edited="coqmninterval_P_pow_eps2_max_int_1.v"
obsolete="false"
archived="false">
<result status="valid" time="2.35"/>
<result status="valid" time="2.36"/>
</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