Commit f980be35 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

updated proof session

parent 031ff21c
......@@ -11,7 +11,7 @@
<prover id="6" name="CVC3" version="2.2" timelimit="10" memlimit="0"/>
<prover id="7" name="Z3" version="4.3.1" timelimit="25" memlimit="1000"/>
<prover id="8" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<prover id="9" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
<prover id="9" name="Alt-Ergo" version="0.95.2" timelimit="30" memlimit="1000"/>
<file name="../queens.mlw" expanded="true">
<theory name="S" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
......@@ -50,7 +50,7 @@
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
<theory name="NQueensSets" sum="017b4c7e41a2213317cbf236650cda36">
<theory name="NQueensSets" sum="14da2f360ed52a151a2f3b49a07da083">
<goal name="WP_parameter t3" expl="VC for t3">
<transf name="split_goal_wp">
<goal name="WP_parameter t3.1" expl="1. loop invariant init">
......@@ -2901,35 +2901,35 @@
<goal name="WP_parameter zero" expl="VC for zero" expanded="true">
<proof prover="4"><result status="valid" time="0.06"/></proof>
<proof prover="7" timelimit="6"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="valid" time="0.06" steps="13"/></proof>
<proof prover="9" timelimit="6"><result status="valid" time="0.06" steps="13"/></proof>
</goal>
<goal name="WP_parameter remove_singleton" expl="VC for remove_singleton" expanded="true">
<proof prover="7" timelimit="6"><result status="valid" time="0.18"/></proof>
<proof prover="9" edited="queens-Bits-WP_parameter_remove_singleton_1.why"><result status="valid" time="2.00" steps="717"/></proof>
<proof prover="9"><result status="valid" time="1.91" steps="717"/></proof>
</goal>
<goal name="WP_parameter add_singleton" expl="VC for add_singleton" expanded="true">
<proof prover="7" timelimit="6"><result status="valid" time="0.07"/></proof>
<proof prover="9"><result status="valid" time="0.33" steps="460"/></proof>
<proof prover="9" timelimit="6"><result status="valid" time="0.33" steps="460"/></proof>
</goal>
<goal name="WP_parameter mul2" expl="VC for mul2" expanded="true">
<proof prover="7" timelimit="30"><result status="valid" time="0.31"/></proof>
<proof prover="9" timelimit="30"><result status="valid" time="0.46" steps="202"/></proof>
<proof prover="9"><result status="valid" time="0.46" steps="202"/></proof>
</goal>
<goal name="WP_parameter div2" expl="VC for div2" expanded="true">
<proof prover="7" timelimit="30"><result status="valid" time="0.02"/></proof>
<proof prover="9" timelimit="30"><result status="valid" time="0.05" steps="58"/></proof>
<proof prover="9"><result status="valid" time="0.05" steps="58"/></proof>
</goal>
<goal name="WP_parameter diff" expl="VC for diff" expanded="true">
<proof prover="4"><result status="valid" time="0.24"/></proof>
<proof prover="7" timelimit="6"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="valid" time="0.79" steps="198"/></proof>
<proof prover="9" timelimit="6"><result status="valid" time="0.79" steps="198"/></proof>
</goal>
<goal name="WP_parameter rightmost_bit_trick" expl="VC for rightmost_bit_trick" expanded="true">
<proof prover="4" timelimit="30"><result status="timeout" time="29.92"/></proof>
</goal>
<goal name="WP_parameter below" expl="VC for below" expanded="true">
<proof prover="7" timelimit="30"><result status="valid" time="0.02"/></proof>
<proof prover="9" timelimit="30"><result status="valid" time="0.12" steps="92"/></proof>
<proof prover="9"><result status="valid" time="0.12" steps="92"/></proof>
</goal>
</theory>
</file>
......
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