Skip to content
GitLab
Commit 2a6e896f authored by MARCHE Claude's avatar MARCHE Claude
Browse files

fixed example rightmostbittrick

parent 8a9be73d
Hide whitespace changes
Inline Side-by-side
examples/rightmostbittrick/why3session.xml
View file @ 2a6e896f
...@@ -8,7 +8,7 @@ ...@@ -8,7 +8,7 @@
<prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="5" memlimit="1000"/> <prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="5" memlimit="1000"/>
<prover id="6" name="Z3" version="4.4.0" timelimit="5" memlimit="1000"/> <prover id="6" name="Z3" version="4.4.0" timelimit="5" memlimit="1000"/>
<file name="../rightmostbittrick.mlw" expanded="true"> <file name="../rightmostbittrick.mlw" expanded="true">
<theory name="Rmbt" sum="6445b4e19089da0d1885e4a56720b0af" expanded="true"> <theory name="Rmbt" sum="d8b24ec80aa06627867242ad9426808a" expanded="true">
<goal name="WP_parameter rightmost_position_set" expl="VC for rightmost_position_set" expanded="true"> <goal name="WP_parameter rightmost_position_set" expl="VC for rightmost_position_set" expanded="true">
<transf name="split_goal_wp" expanded="true"> <transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter rightmost_position_set.1" expl="1. loop invariant init"> <goal name="WP_parameter rightmost_position_set.1" expl="1. loop invariant init">
...@@ -28,11 +28,8 @@ ...@@ -28,11 +28,8 @@
<proof prover="5"><result status="valid" time="0.02"/></proof> <proof prover="5"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter rightmost_position_set.4" expl="4. postcondition"> <goal name="WP_parameter rightmost_position_set.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="72"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.00"/></proof> <proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal> </goal>
<goal name="WP_parameter rightmost_position_set.5" expl="5. postcondition"> <goal name="WP_parameter rightmost_position_set.5" expl="5. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="72"/></proof> <proof prover="0"><result status="valid" time="0.05" steps="72"/></proof>
...@@ -50,7 +47,7 @@ ...@@ -50,7 +47,7 @@
</goal> </goal>
<goal name="WP_parameter rightmost_position_set.7" expl="7. postcondition"> <goal name="WP_parameter rightmost_position_set.7" expl="7. postcondition">
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof> <proof prover="6"><result status="valid" time="0.00"/></proof>
</goal> </goal>
<goal name="WP_parameter rightmost_position_set.8" expl="8. postcondition"> <goal name="WP_parameter rightmost_position_set.8" expl="8. postcondition">
<proof prover="0"><result status="valid" time="0.04" steps="71"/></proof> <proof prover="0"><result status="valid" time="0.04" steps="71"/></proof>
...@@ -78,32 +75,27 @@ ...@@ -78,32 +75,27 @@
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.03"/></proof> <proof prover="6"><result status="valid" time="0.03"/></proof>
</goal> </goal>
<goal name="WP_parameter rightmost_bit_trick.3" expl="3. assertion"> <goal name="WP_parameter rightmost_bit_trick.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.07" steps="108"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.04"/></proof> <proof prover="5"><result status="valid" time="0.03"/></proof>
</goal> </goal>
<goal name="WP_parameter rightmost_bit_trick.4" expl="4. postcondition"> <goal name="WP_parameter rightmost_bit_trick.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.20" steps="142"/></proof> <proof prover="0"><result status="valid" time="0.18" steps="134"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.03"/></proof> <proof prover="5"><result status="valid" time="0.03"/></proof>
</goal> </goal>
<goal name="WP_parameter rightmost_bit_trick.5" expl="5. postcondition"> <goal name="WP_parameter rightmost_bit_trick.5" expl="5. postcondition">
<proof prover="0"><result status="valid" time="0.18" steps="146"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="77"/></proof>
<proof prover="5"><result status="valid" time="0.03"/></proof> <proof prover="5"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter rightmost_bit_trick.6" expl="6. postcondition"> <goal name="WP_parameter rightmost_bit_trick.6" expl="6. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="79"/></proof> <proof prover="5"><result status="valid" time="0.06"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter rightmost_bit_trick.7" expl="7. postcondition"> <goal name="WP_parameter rightmost_bit_trick.7" expl="7. postcondition">
<proof prover="5"><result status="valid" time="0.06"/></proof> <proof prover="2"><result status="valid" time="0.18"/></proof>
</goal> </goal>
<goal name="WP_parameter rightmost_bit_trick.8" expl="8. postcondition"> <goal name="WP_parameter rightmost_bit_trick.8" expl="8. postcondition">
<proof prover="5"><result status="valid" time="0.06"/></proof> <proof prover="0"><result status="valid" time="0.15" steps="156"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick.9" expl="9. postcondition">
<proof prover="0"><result status="valid" time="0.15" steps="200"/></proof>
<proof prover="4"><result status="timeout" time="5.05"/></proof>
<proof prover="5"><result status="valid" time="0.03"/></proof> <proof prover="5"><result status="valid" time="0.03"/></proof>
</goal> </goal>
</transf> </transf>
......
Supports Markdown
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