Skip to content

GitLab

why3
why3
Commit 1f56973a authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

update some proofs

parent 4c38b07f
Hide whitespace changes
Inline Side-by-side
Showing with 31 additions and 25 deletions
examples/bitvectors/bitvector/why3session.xml
View file @ 1f56973a
......@@ -2,6 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
......@@ -9,29 +10,29 @@
<prover id="9" name="Z3" version="3.2" timelimit="3" steplimit="0" memlimit="1000"/>
<prover id="10" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../bitvector.why" expanded="true">
<theory name="BitVector" sum="d28eacb18daec312a94869cf046a4a41">
<theory name="BitVector" sum="c4ff36c29781f4dff63c679396f367ed">
<goal name="Nth_bw_xor_v1true">
<proof prover="2"><result status="valid" time="0.08" steps="85"/></proof>
<proof prover="2"><result status="valid" time="0.08" steps="81"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Nth_bw_xor_v1false">
<proof prover="2"><result status="valid" time="0.08" steps="109"/></proof>
<proof prover="2"><result status="valid" time="0.08" steps="79"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="6"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="Nth_bw_xor_v2true">
<proof prover="2"><result status="valid" time="0.03" steps="79"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="76"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="Nth_bw_xor_v2false">
<proof prover="2"><result status="valid" time="0.05" steps="80"/></proof>
<proof prover="2"><result status="valid" time="0.05" steps="75"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="to_nat_of_zero2">
<proof prover="1" edited="bitvector_BitVector_to_nat_of_zero2_1.v"><result status="valid" time="0.48"/></proof>
<proof prover="1" edited="bitvector_BitVector_to_nat_of_zero2_1.v"><result status="valid" time="0.27"/></proof>
</goal>
<goal name="to_nat_of_zero">
<proof prover="1" timelimit="30" edited="bitvector_BitVector_to_nat_of_zero_1.v"><result status="valid" time="1.01"/></proof>
......@@ -76,15 +77,21 @@
<proof prover="2"><result status="valid" time="0.33" steps="94"/></proof>
</goal>
</theory>
<theory name="BV32" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="BV32" sum="a0fcda0647776d464a20420f1fa826cd" expanded="true">
<goal name="size_positive">
<proof prover="0"><result status="valid" time="0.01" steps="67"/></proof>
</goal>
</theory>
<theory name="BV64" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="BV64" sum="da0d37391270396f45ce23a4e79415f4" expanded="true">
<goal name="size_positive">
<proof prover="0"><result status="valid" time="0.01" steps="67"/></proof>
</goal>
</theory>
<theory name="BV32_64" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="TestBv32" sum="fbb6835562fff27fbb68db392fbf344b">
<theory name="TestBv32" sum="233ed1a6c337cb7b35979edde7b4dc9a" expanded="true">
<goal name="Test1">
<proof prover="2"><result status="valid" time="0.06" steps="72"/></proof>
<proof prover="2"><result status="valid" time="0.06" steps="70"/></proof>
<proof prover="3" timelimit="3"><result status="valid" time="0.07"/></proof>
<proof prover="6"><result status="valid" time="0.04"/></proof>
<proof prover="10"><result status="valid" time="0.53"/></proof>
......@@ -138,7 +145,7 @@
<proof prover="6" timelimit="120"><result status="valid" time="77.09"/></proof>
</goal>
<goal name="to_nat_0x00000007">
<proof prover="6" timelimit="60" memlimit="4000"><result status="valid" time="63.29"/></proof>
<proof prover="6" timelimit="60" memlimit="4000"><result status="valid" time="54.25"/></proof>
</goal>
<goal name="to_nat_0x0000000F">
<proof prover="6" timelimit="120"><result status="valid" time="46.07"/></proof>
......@@ -147,13 +154,13 @@
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="38.43"/></proof>
</goal>
<goal name="to_nat_0x0000003F">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="38.26"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="31.33"/></proof>
</goal>
<goal name="to_nat_0x0000007F">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="31.80"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="25.66"/></proof>
</goal>
<goal name="to_nat_0x000000FF">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="24.52"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="21.04"/></proof>
</goal>
<goal name="to_nat_0x000001FF">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="17.53"/></proof>
......@@ -186,7 +193,7 @@
<proof prover="6"><result status="valid" time="1.77"/></proof>
</goal>
<goal name="to_nat_0x0007FFFF">
<proof prover="6"><result status="valid" time="1.56"/></proof>
<proof prover="6"><result status="valid" time="1.26"/></proof>
</goal>
<goal name="to_nat_0x000FFFFF">
<proof prover="6"><result status="valid" time="0.89"/></proof>
......
examples/patience/why3session.xml
View file @ 1f56973a
......@@ -80,21 +80,21 @@
<proof prover="7"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
</theory>
<theory name="PatienceAbstract" sum="36ba7bd72737670607b37962ef7efb1c" expanded="true">
<goal name="VC play_card" expl="VC for play_card" expanded="true">
<transf name="split_goal_wp" expanded="true">
<theory name="PatienceAbstract" sum="36ba7bd72737670607b37962ef7efb1c">
<goal name="VC play_card" expl="VC for play_card">
<transf name="split_goal_wp">
<goal name="VC play_card.1" expl="1. loop bounds">
<proof prover="7"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="VC play_card.2" expl="2. loop invariant init">
<proof prover="7"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC play_card.3" expl="3. postcondition" expanded="true">
<transf name="introduce_premises" expanded="true">
<goal name="VC play_card.3.1" expl="1. postcondition" expanded="true">
<transf name="inline_goal" expanded="true">
<goal name="VC play_card.3.1.1" expl="1. postcondition" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC play_card.3" expl="3. postcondition">
<transf name="introduce_premises">
<goal name="VC play_card.3.1" expl="1. postcondition">
<transf name="inline_goal">
<goal name="VC play_card.3.1.1" expl="1. postcondition">
<transf name="split_goal_wp">
<goal name="VC play_card.3.1.1.1" expl="1. VC for play_card">
<proof prover="7"><result status="valid" time="0.05" steps="47"/></proof>
</goal>
......@@ -135,7 +135,6 @@
<proof prover="7"><result status="valid" time="0.51" steps="143"/></proof>
</goal>
<goal name="VC play_card.3.1.1.14" expl="14. VC for play_card">
<proof prover="1"><undone/></proof>
<proof prover="7"><result status="valid" time="1.64" steps="423"/></proof>
</goal>
<goal name="VC play_card.3.1.1.15" expl="15. VC for play_card">
......
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