Commit e87fe95e authored by MARCHE Claude's avatar MARCHE Claude

example gcd: updated proofs, checking division by zero

parent 6e9ded77
......@@ -51,7 +51,7 @@
</transf>
</goal>
</theory>
<theory name="BinaryGcd" sum="0de53aebb66ffe2ace03e6f6e89c0907">
<theory name="BinaryGcd" sum="997a789233dd38206c142045ca328997">
<goal name="even1">
<proof prover="7" timelimit="6"><result status="valid" time="0.06" steps="16"/></proof>
</goal>
......@@ -87,46 +87,55 @@
<goal name="VC binary_gcd.2" expl="2. precondition">
<proof prover="7"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="VC binary_gcd.3" expl="3. division by zero">
<goal name="VC binary_gcd.3" expl="3. precondition">
<proof prover="7"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="VC binary_gcd.4" expl="4. precondition">
<proof prover="7"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC binary_gcd.5" expl="5. division by zero">
<proof prover="7"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="VC binary_gcd.4" expl="4. division by zero">
<goal name="VC binary_gcd.6" expl="6. division by zero">
<proof prover="7"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC binary_gcd.5" expl="5. variant decrease">
<goal name="VC binary_gcd.7" expl="7. variant decrease">
<proof prover="7"><result status="valid" time="0.04" steps="19"/></proof>
</goal>
<goal name="VC binary_gcd.6" expl="6. precondition">
<goal name="VC binary_gcd.8" expl="8. precondition">
<proof prover="7"><result status="valid" time="0.02" steps="16"/></proof>
</goal>
<goal name="VC binary_gcd.7" expl="7. division by zero">
<goal name="VC binary_gcd.9" expl="9. division by zero">
<proof prover="7"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="VC binary_gcd.8" expl="8. variant decrease">
<goal name="VC binary_gcd.10" expl="10. variant decrease">
<proof prover="7"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC binary_gcd.9" expl="9. precondition">
<goal name="VC binary_gcd.11" expl="11. precondition">
<proof prover="7"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC binary_gcd.10" expl="10. division by zero">
<goal name="VC binary_gcd.12" expl="12. precondition">
<proof prover="7"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="VC binary_gcd.13" expl="13. division by zero">
<proof prover="7"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="VC binary_gcd.11" expl="11. variant decrease">
<goal name="VC binary_gcd.14" expl="14. variant decrease">
<proof prover="7"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC binary_gcd.12" expl="12. precondition">
<goal name="VC binary_gcd.15" expl="15. precondition">
<proof prover="7"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC binary_gcd.13" expl="13. division by zero">
<goal name="VC binary_gcd.16" expl="16. division by zero">
<proof prover="7"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC binary_gcd.14" expl="14. variant decrease">
<goal name="VC binary_gcd.17" expl="17. variant decrease">
<proof prover="7"><result status="valid" time="0.04" steps="24"/></proof>
</goal>
<goal name="VC binary_gcd.15" expl="15. precondition">
<goal name="VC binary_gcd.18" expl="18. precondition">
<proof prover="7"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
<goal name="VC binary_gcd.16" expl="16. postcondition">
<goal name="VC binary_gcd.19" expl="19. postcondition">
<proof prover="8"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
......
......@@ -51,7 +51,7 @@
</transf>
</goal>
</theory>
<theory name="BinaryGcd" sum="b0618b3f5d4ce4520643c4d190df2ed9">
<theory name="BinaryGcd" sum="95664ddbe38ef16f39ae9ef12ab1c735">
<goal name="even1">
<proof prover="0"><result status="valid" time="0.03" steps="16"/></proof>
</goal>
......@@ -87,56 +87,65 @@
<goal name="VC binary_gcd.2" expl="2. precondition">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC binary_gcd.3" expl="3. division by zero">
<goal name="VC binary_gcd.3" expl="3. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="VC binary_gcd.4" expl="4. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="VC binary_gcd.5" expl="5. division by zero">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC binary_gcd.4" expl="4. division by zero">
<goal name="VC binary_gcd.6" expl="6. division by zero">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC binary_gcd.5" expl="5. variant decrease">
<goal name="VC binary_gcd.7" expl="7. variant decrease">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC binary_gcd.6" expl="6. precondition">
<goal name="VC binary_gcd.8" expl="8. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="16"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC binary_gcd.7" expl="7. division by zero">
<goal name="VC binary_gcd.9" expl="9. division by zero">
<proof prover="0"><result status="valid" time="0.02" steps="8"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC binary_gcd.8" expl="8. variant decrease">
<goal name="VC binary_gcd.10" expl="10. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC binary_gcd.9" expl="9. precondition">
<goal name="VC binary_gcd.11" expl="11. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC binary_gcd.10" expl="10. division by zero">
<goal name="VC binary_gcd.12" expl="12. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC binary_gcd.13" expl="13. division by zero">
<proof prover="0"><result status="valid" time="0.03" steps="8"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC binary_gcd.11" expl="11. variant decrease">
<goal name="VC binary_gcd.14" expl="14. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC binary_gcd.12" expl="12. precondition">
<goal name="VC binary_gcd.15" expl="15. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="8"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC binary_gcd.13" expl="13. division by zero">
<goal name="VC binary_gcd.16" expl="16. division by zero">
<proof prover="0"><result status="valid" time="0.02" steps="8"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC binary_gcd.14" expl="14. variant decrease">
<goal name="VC binary_gcd.17" expl="17. variant decrease">
<proof prover="0"><result status="valid" time="0.04" steps="24"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC binary_gcd.15" expl="15. precondition">
<goal name="VC binary_gcd.18" expl="18. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC binary_gcd.16" expl="16. postcondition">
<goal name="VC binary_gcd.19" expl="19. postcondition">
<proof prover="2"><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