Commit 566a5e90 authored by MARCHE Claude's avatar MARCHE Claude

ported example bignum

parent 1a0cb206
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.4.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../bignum.mlw" expanded="true">
<theory name="BigNum" sum="458e30d62c074211297da3625c3a7e6f" expanded="true">
<goal name="VC base" expl="VC for base">
<proof prover="2"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC nonneg" expl="VC for nonneg" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC nonneg.1" expl="1. variant decrease">
<proof prover="2"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="VC nonneg.2" expl="2. precondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC nonneg.3" expl="3. postcondition" expanded="true">
<proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
</transf>
</goal>
<goal name="VC msd" expl="VC for msd" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC msd.1" expl="1. variant decrease">
<proof prover="2"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="VC msd.2" expl="2. precondition">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC msd.3" expl="3. postcondition" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="VC add_digit" expl="VC for add_digit">
<transf name="split_goal_wp">
<goal name="VC add_digit.1" expl="1. variant decrease">
<proof prover="2"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="VC add_digit.2" expl="2. precondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC add_digit.3" expl="3. precondition">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC add_digit.4" expl="4. postcondition">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC add_digit.5" expl="5. postcondition">
<proof prover="2"><result status="valid" time="0.03" steps="82"/></proof>
</goal>
</transf>
</goal>
<goal name="VC add_cin" expl="VC for add_cin">
<transf name="split_goal_wp">
<goal name="VC add_cin.1" expl="1. precondition">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC add_cin.2" expl="2. precondition">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC add_cin.3" expl="3. precondition">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC add_cin.4" expl="4. precondition">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC add_cin.5" expl="5. precondition">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC add_cin.6" expl="6. precondition">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC add_cin.7" expl="7. variant decrease">
<proof prover="2"><result status="valid" time="0.03" steps="26"/></proof>
</goal>
<goal name="VC add_cin.8" expl="8. precondition">
<proof prover="1" timelimit="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC add_cin.9" expl="9. variant decrease">
<proof prover="2"><result status="valid" time="0.03" steps="26"/></proof>
</goal>
<goal name="VC add_cin.10" expl="10. precondition">
<proof prover="3"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC add_cin.11" expl="11. postcondition">
<transf name="split_goal_wp">
<goal name="VC add_cin.11.1" expl="1. postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="VC add_cin.11.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="VC add_cin.11.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="VC add_cin.11.4" expl="4. postcondition">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC add_cin.11.5" expl="5. postcondition">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
<goal name="VC add_cin.12" expl="12. postcondition">
<proof prover="2"><result status="valid" time="0.31" steps="113"/></proof>
</goal>
</transf>
</goal>
<goal name="VC add" expl="VC for add" expanded="true">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
</theory>
</file>
</why3session>
<?xml version="1.0" encoding="UTF-8"?>
<!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.01" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../bignum.mlw">
<theory name="BigNum" sum="cf395b347f7215e18d58f74c8b3507a5">
<goal name="WP_parameter nonneg" expl="VC for nonneg">
<transf name="split_goal_wp">
<goal name="WP_parameter nonneg.1" expl="1. postcondition">
<proof prover="0"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="WP_parameter nonneg.2" expl="2. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter nonneg.3" expl="3. precondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter nonneg.4" expl="4. postcondition">
<transf name="compute_in_goal">
<goal name="WP_parameter nonneg.4.1" expl="1. postcondition">
<proof prover="0"><result status="valid" time="5.21" steps="114"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter msd" expl="VC for msd">
<transf name="split_goal_wp">
<goal name="WP_parameter msd.1" expl="1. postcondition">
<proof prover="0"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="WP_parameter msd.2" expl="2. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter msd.3" expl="3. precondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter msd.4" expl="4. postcondition">
<transf name="compute_in_goal">
<goal name="WP_parameter msd.4.1" expl="1. postcondition">
<proof prover="0"><result status="valid" time="1.62" steps="80"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter add_digit" expl="VC for add_digit">
<transf name="split_goal_wp">
<goal name="WP_parameter add_digit.1" expl="1. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="WP_parameter add_digit.2" expl="2. postcondition">
<proof prover="0"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
<goal name="WP_parameter add_digit.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter add_digit.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
<goal name="WP_parameter add_digit.5" expl="5. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter add_digit.6" expl="6. precondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter add_digit.7" expl="7. precondition">
<proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="WP_parameter add_digit.8" expl="8. postcondition">
<transf name="compute_in_goal">
<goal name="WP_parameter add_digit.8.1" expl="1. postcondition">
<proof prover="0"><result status="timeout" time="5.99"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter add_digit.9" expl="9. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter add_cin" expl="VC for add_cin">
<transf name="split_goal_wp">
<goal name="WP_parameter add_cin.1" expl="1. precondition">
<proof prover="0"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
<goal name="WP_parameter add_cin.2" expl="2. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter add_cin.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="WP_parameter add_cin.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="WP_parameter add_cin.5" expl="5. precondition">
<proof prover="0"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
<goal name="WP_parameter add_cin.6" expl="6. precondition">
<proof prover="0"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
<goal name="WP_parameter add_cin.7" expl="7. postcondition">
<proof prover="0"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="WP_parameter add_cin.8" expl="8. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter add_cin.9" expl="9. precondition">
<proof prover="0"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
<goal name="WP_parameter add_cin.10" expl="10. precondition">
<proof prover="0"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
<goal name="WP_parameter add_cin.11" expl="11. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter add_cin.12" expl="12. postcondition">
<proof prover="0"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="WP_parameter add_cin.13" expl="13. variant decrease">
<proof prover="0"><result status="valid" time="0.03" steps="14"/></proof>
</goal>
<goal name="WP_parameter add_cin.14" expl="14. precondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter add_cin.15" expl="15. postcondition">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter add_cin.16" expl="16. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="WP_parameter add_cin.17" expl="17. variant decrease">
<proof prover="0"><result status="valid" time="0.03" steps="14"/></proof>
</goal>
<goal name="WP_parameter add_cin.18" expl="18. precondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter add_cin.19" expl="19. postcondition">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter add_cin.20" expl="20. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter add" expl="VC for add">
<proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
</theory>
</file>
</why3session>
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