Commit 8a20e6d4 authored by MARCHE Claude's avatar MARCHE Claude

update obsolete sessions

parent 6a89179d
...@@ -344,13 +344,13 @@ ...@@ -344,13 +344,13 @@
<goal name="eval_change_free.0.10.0.0.0" proved="true"> <goal name="eval_change_free.0.10.0.0.0" proved="true">
<transf name="destruct_alg" proved="true" arg1="x1"> <transf name="destruct_alg" proved="true" arg1="x1">
<goal name="eval_change_free.0.10.0.0.0.0" proved="true"> <goal name="eval_change_free.0.10.0.0.0.0" proved="true">
<proof prover="7"><result status="valid" time="0.13"/></proof> <proof prover="7"><result status="valid" time="0.15"/></proof>
</goal> </goal>
<goal name="eval_change_free.0.10.0.0.0.1" proved="true"> <goal name="eval_change_free.0.10.0.0.0.1" proved="true">
<proof prover="7"><result status="valid" time="0.18"/></proof> <proof prover="7"><result status="valid" time="0.13"/></proof>
</goal> </goal>
<goal name="eval_change_free.0.10.0.0.0.2" proved="true"> <goal name="eval_change_free.0.10.0.0.0.2" proved="true">
<proof prover="7"><result status="valid" time="0.15"/></proof> <proof prover="7"><result status="valid" time="0.18"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
...@@ -383,33 +383,33 @@ ...@@ -383,33 +383,33 @@
</goal> </goal>
<goal name="many_steps_seq.0.1.1" expl="recursive case" proved="true"> <goal name="many_steps_seq.0.1.1" expl="recursive case" proved="true">
<transf name="simplify_trivial_quantification_in_goal" proved="true" > <transf name="simplify_trivial_quantification_in_goal" proved="true" >
<goal name="many_steps_seq.0.1.1.0" proved="true"> <goal name="many_steps_seq.0.1.1.0" expl="recursive case" proved="true">
<transf name="introduce_premises" proved="true" > <transf name="introduce_premises" proved="true" >
<goal name="many_steps_seq.0.1.1.0.0" proved="true"> <goal name="many_steps_seq.0.1.1.0.0" expl="recursive case" proved="true">
<transf name="inversion_arg_pr" proved="true" arg1="H2"> <transf name="inversion_arg_pr" proved="true" arg1="H2">
<goal name="many_steps_seq.0.1.1.0.0.0" proved="true"> <goal name="many_steps_seq.0.1.1.0.0.0" expl="recursive case" proved="true">
<proof prover="7"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="many_steps_seq.0.1.1.0.0.1" expl="recursive case" proved="true">
<proof prover="7"><result status="valid" time="0.08"/></proof> <proof prover="7"><result status="valid" time="0.08"/></proof>
</goal> </goal>
<goal name="many_steps_seq.0.1.1.0.0.1" proved="true"> <goal name="many_steps_seq.0.1.1.0.0.2" expl="recursive case" proved="true">
<proof prover="7"><result status="valid" time="0.09"/></proof> <proof prover="7"><result status="valid" time="0.08"/></proof>
</goal> </goal>
<goal name="many_steps_seq.0.1.1.0.0.2" proved="true"> <goal name="many_steps_seq.0.1.1.0.0.3" expl="recursive case" proved="true">
<proof prover="7"><result status="valid" time="0.06"/></proof> <proof prover="7"><result status="valid" time="0.06"/></proof>
</goal> </goal>
<goal name="many_steps_seq.0.1.1.0.0.3" proved="true"> <goal name="many_steps_seq.0.1.1.0.0.4" expl="recursive case" proved="true">
<proof prover="7"><result status="valid" time="0.07"/></proof> <proof prover="7"><result status="valid" time="0.06"/></proof>
</goal> </goal>
<goal name="many_steps_seq.0.1.1.0.0.4" proved="true"> <goal name="many_steps_seq.0.1.1.0.0.5" expl="recursive case" proved="true">
<proof prover="7"><result status="valid" time="0.09"/></proof> <proof prover="7"><result status="valid" time="0.09"/></proof>
</goal> </goal>
<goal name="many_steps_seq.0.1.1.0.0.5" proved="true"> <goal name="many_steps_seq.0.1.1.0.0.6" expl="recursive case" proved="true">
<proof prover="7"><result status="valid" time="0.08"/></proof> <proof prover="7"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="many_steps_seq.0.1.1.0.0.6" proved="true">
<proof prover="7"><result status="valid" time="0.06"/></proof>
</goal> </goal>
<goal name="many_steps_seq.0.1.1.0.0.7" proved="true"> <goal name="many_steps_seq.0.1.1.0.0.7" expl="recursive case" proved="true">
<proof prover="7"><result status="valid" time="0.06"/></proof> <proof prover="7"><result status="valid" time="0.07"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
......
...@@ -275,7 +275,7 @@ ...@@ -275,7 +275,7 @@
<proof prover="1"><result status="valid" time="0.04" steps="124"/></proof> <proof prover="1"><result status="valid" time="0.04" steps="124"/></proof>
</goal> </goal>
<goal name="VC relax.3.0.0.4" expl="postcondition" proved="true"> <goal name="VC relax.3.0.0.4" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.92" steps="2464"/></proof> <proof prover="1"><result status="valid" time="0.69" steps="2464"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
......
...@@ -272,7 +272,7 @@ ...@@ -272,7 +272,7 @@
<goal name="VC compile_bexpr.3.4.1.0.0" expl="precondition" proved="true"> <goal name="VC compile_bexpr.3.4.1.0.0" expl="precondition" proved="true">
<transf name="compute_specified" proved="true" > <transf name="compute_specified" proved="true" >
<goal name="VC compile_bexpr.3.4.1.0.0.0" expl="precondition" proved="true"> <goal name="VC compile_bexpr.3.4.1.0.0.0" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.32" steps="344"/></proof> <proof prover="0"><result status="valid" time="0.18" steps="344"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
...@@ -543,7 +543,7 @@ ...@@ -543,7 +543,7 @@
<proof prover="0"><result status="valid" time="0.13" steps="55"/></proof> <proof prover="0"><result status="valid" time="0.13" steps="55"/></proof>
</goal> </goal>
<goal name="VC compile_com.5.4.0.0.0.12" expl="VC for compile_com" proved="true"> <goal name="VC compile_com.5.4.0.0.0.12" expl="VC for compile_com" proved="true">
<proof prover="0"><result status="valid" time="0.47" steps="605"/></proof> <proof prover="0"><result status="valid" time="0.46" steps="577"/></proof>
</goal> </goal>
<goal name="VC compile_com.5.4.0.0.0.13" expl="VC for compile_com" proved="true"> <goal name="VC compile_com.5.4.0.0.0.13" expl="VC for compile_com" proved="true">
<proof prover="0"><result status="valid" time="0.12" steps="61"/></proof> <proof prover="0"><result status="valid" time="0.12" steps="61"/></proof>
...@@ -555,7 +555,7 @@ ...@@ -555,7 +555,7 @@
<proof prover="0"><result status="valid" time="0.15" steps="89"/></proof> <proof prover="0"><result status="valid" time="0.15" steps="89"/></proof>
</goal> </goal>
<goal name="VC compile_com.5.4.0.0.0.16" expl="VC for compile_com" proved="true"> <goal name="VC compile_com.5.4.0.0.0.16" expl="VC for compile_com" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="1.34" steps="914"/></proof> <proof prover="0" timelimit="5"><result status="valid" time="1.34" steps="866"/></proof>
</goal> </goal>
<goal name="VC compile_com.5.4.0.0.0.17" expl="VC for compile_com" proved="true"> <goal name="VC compile_com.5.4.0.0.0.17" expl="VC for compile_com" proved="true">
<proof prover="0"><result status="valid" time="0.17" steps="95"/></proof> <proof prover="0"><result status="valid" time="0.17" steps="95"/></proof>
...@@ -573,7 +573,7 @@ ...@@ -573,7 +573,7 @@
<proof prover="0"><result status="valid" time="0.14" steps="55"/></proof> <proof prover="0"><result status="valid" time="0.14" steps="55"/></proof>
</goal> </goal>
<goal name="VC compile_com.5.4.0.0.0.22" expl="VC for compile_com" proved="true"> <goal name="VC compile_com.5.4.0.0.0.22" expl="VC for compile_com" proved="true">
<proof prover="0"><result status="valid" time="0.39" steps="411"/></proof> <proof prover="0"><result status="valid" time="0.39" steps="417"/></proof>
</goal> </goal>
<goal name="VC compile_com.5.4.0.0.0.23" expl="VC for compile_com" proved="true"> <goal name="VC compile_com.5.4.0.0.0.23" expl="VC for compile_com" proved="true">
<proof prover="0"><result status="valid" time="0.12" steps="55"/></proof> <proof prover="0"><result status="valid" time="0.12" steps="55"/></proof>
......
This diff is collapsed.
...@@ -20,10 +20,10 @@ ...@@ -20,10 +20,10 @@
<goal name="size_left.0" proved="true"> <goal name="size_left.0" proved="true">
<transf name="destruct_alg" proved="true" arg1="t"> <transf name="destruct_alg" proved="true" arg1="t">
<goal name="size_left.0.0" proved="true"> <goal name="size_left.0.0" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof> <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="size_left.0.1" proved="true"> <goal name="size_left.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof> <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
...@@ -39,7 +39,7 @@ ...@@ -39,7 +39,7 @@
<proof prover="3"><result status="valid" time="0.03"/></proof> <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal> </goal>
<goal name="all_trees_0.0.0.1" proved="true"> <goal name="all_trees_0.0.0.1" proved="true">
<proof prover="0"><result status="valid" time="0.24"/></proof> <proof prover="0"><result status="valid" time="0.38"/></proof>
</goal> </goal>
<goal name="all_trees_0.0.0.2" proved="true"> <goal name="all_trees_0.0.0.2" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof> <proof prover="3"><result status="valid" time="0.02"/></proof>
......
...@@ -471,7 +471,7 @@ ...@@ -471,7 +471,7 @@
<goal name="VC isqrt64.40.0.0.0" expl="VC for isqrt64" proved="true"> <goal name="VC isqrt64.40.0.0.0" expl="VC for isqrt64" proved="true">
<transf name="assert" proved="true" arg1="(x = add (sqr res_g) num)"> <transf name="assert" proved="true" arg1="(x = add (sqr res_g) num)">
<goal name="VC isqrt64.40.0.0.0.0" proved="true"> <goal name="VC isqrt64.40.0.0.0.0" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="0.58"/></proof> <proof prover="3" timelimit="5"><result status="valid" time="0.42"/></proof>
</goal> </goal>
<goal name="VC isqrt64.40.0.0.0.1" expl="VC for isqrt64" proved="true"> <goal name="VC isqrt64.40.0.0.0.1" expl="VC for isqrt64" proved="true">
<transf name="unfold" proved="true" arg1="sqr"> <transf name="unfold" proved="true" arg1="sqr">
...@@ -522,14 +522,14 @@ ...@@ -522,14 +522,14 @@
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.0" expl="true case" proved="true"> <goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.0" expl="true case" proved="true">
<transf name="unfold" proved="true" arg1="sqr" arg2="in" arg3="h"> <transf name="unfold" proved="true" arg1="sqr" arg2="in" arg3="h">
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.0.0" expl="true case" proved="true"> <goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.0.0" expl="true case" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="3.14"/></proof> <proof prover="3" timelimit="5"><result status="valid" time="1.98"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1" expl="false case" proved="true"> <goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1" expl="false case" proved="true">
<transf name="case" proved="true" arg1="(res_g = (0:t))"> <transf name="case" proved="true" arg1="(res_g = (0:t))">
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.0" expl="false case (true case)" proved="true"> <goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.0" expl="false case (true case)" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="3.69"/></proof> <proof prover="3" timelimit="5"><result status="valid" time="2.82"/></proof>
</goal> </goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1" expl="false case" proved="true"> <goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1" expl="false case" proved="true">
<transf name="rewrite" proved="true" arg1="to_uint_sub_bounded"> <transf name="rewrite" proved="true" arg1="to_uint_sub_bounded">
...@@ -601,7 +601,7 @@ ...@@ -601,7 +601,7 @@
<proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="2.80" steps="571"/></proof> <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="2.80" steps="571"/></proof>
</goal> </goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.0.0.0.1.0.0.0.1" proved="true"> <goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.0.0.0.1.0.0.0.1" proved="true">
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.78"/></proof> <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.88"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
...@@ -625,7 +625,7 @@ ...@@ -625,7 +625,7 @@
</transf> </transf>
</goal> </goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.0.1" proved="true"> <goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.0.1" proved="true">
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.44"/></proof> <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.96"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
...@@ -664,7 +664,7 @@ ...@@ -664,7 +664,7 @@
</transf> </transf>
</goal> </goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.1.0.0.1.0.0.0.0.1" proved="true"> <goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.1.0.0.1.0.0.0.0.1" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="2.76"/></proof> <proof prover="3" timelimit="5"><result status="valid" time="1.84"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
...@@ -688,12 +688,12 @@ ...@@ -688,12 +688,12 @@
</transf> </transf>
</goal> </goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.1.0.1" proved="true"> <goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.1.0.1" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="1.74"/></proof> <proof prover="3" timelimit="5"><result status="valid" time="1.21"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.1.1" proved="true"> <goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.1.1" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="2.68"/></proof> <proof prover="3" timelimit="5"><result status="valid" time="1.85"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
...@@ -717,7 +717,7 @@ ...@@ -717,7 +717,7 @@
<proof prover="1"><result status="valid" time="0.02" steps="124"/></proof> <proof prover="1"><result status="valid" time="0.02" steps="124"/></proof>
</goal> </goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.1.1" proved="true"> <goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.1.1" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="0.64"/></proof> <proof prover="3" timelimit="5"><result status="valid" time="0.47"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
......
...@@ -283,7 +283,7 @@ ...@@ -283,7 +283,7 @@
<goal name="VC add.9.0.0.2.0.0" expl="VC for add" proved="true"> <goal name="VC add.9.0.0.2.0.0" expl="VC for add" proved="true">
<transf name="case" proved="true" arg1="(i=i1)"> <transf name="case" proved="true" arg1="(i=i1)">
<goal name="VC add.9.0.0.2.0.0.0" expl="true case" proved="true"> <goal name="VC add.9.0.0.2.0.0.0" expl="true case" proved="true">
<proof prover="6"><result status="valid" time="0.03" steps="53"/></proof> <proof prover="6"><result status="valid" time="0.03" steps="35"/></proof>
</goal> </goal>
<goal name="VC add.9.0.0.2.0.0.1" expl="false case" proved="true"> <goal name="VC add.9.0.0.2.0.0.1" expl="false case" proved="true">
<transf name="inline_all" proved="true" > <transf name="inline_all" proved="true" >
......
...@@ -313,7 +313,7 @@ ...@@ -313,7 +313,7 @@
<goal name="VC list_seg_sublistl.6.0.0" expl="postcondition" proved="true"> <goal name="VC list_seg_sublistl.6.0.0" expl="postcondition" proved="true">
<transf name="assert" proved="true" arg1="(l1 = empty)"> <transf name="assert" proved="true" arg1="(l1 = empty)">
<goal name="VC list_seg_sublistl.6.0.0.0" proved="true"> <goal name="VC list_seg_sublistl.6.0.0.0" proved="true">
<proof prover="0"><result status="valid" time="2.42"/></proof> <proof prover="0"><result status="valid" time="2.07"/></proof>
</goal> </goal>
<goal name="VC list_seg_sublistl.6.0.0.1" expl="postcondition" proved="true"> <goal name="VC list_seg_sublistl.6.0.0.1" expl="postcondition" proved="true">
<transf name="assert" proved="true" arg1="(forall l:seq &#39;a. empty ++ l = l)"> <transf name="assert" proved="true" arg1="(forall l:seq &#39;a. empty ++ l = l)">
...@@ -530,7 +530,7 @@ ...@@ -530,7 +530,7 @@
<goal name="VC in_place_reverse.12" expl="loop invariant preservation" proved="true"> <goal name="VC in_place_reverse.12" expl="loop invariant preservation" proved="true">
<transf name="introduce_premises" proved="true" > <transf name="introduce_premises" proved="true" >
<goal name="VC in_place_reverse.12.0" expl="loop invariant preservation" proved="true"> <goal name="VC in_place_reverse.12.0" expl="loop invariant preservation" proved="true">
<proof prover="1" timelimit="30"><result status="valid" time="16.15" steps="8570"/></proof> <proof prover="1" timelimit="30"><result status="valid" time="16.15" steps="8656"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
......
...@@ -7,10 +7,6 @@ ...@@ -7,10 +7,6 @@
<prover id="2" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="2" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../max_matrix.mlw" proved="true"> <file name="../max_matrix.mlw" proved="true">
<theory name="Bitset" proved="true">
</theory>
<theory name="HashTable" proved="true">
</theory>
<theory name="MaxMatrixMemo" proved="true"> <theory name="MaxMatrixMemo" proved="true">
<goal name="VC n" expl="VC for n" proved="true"> <goal name="VC n" expl="VC for n" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="1"/></proof> <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
......
...@@ -255,7 +255,7 @@ ...@@ -255,7 +255,7 @@
<goal name="VC maximum_subarray.23.0.0.0" expl="loop invariant preservation" proved="true"> <goal name="VC maximum_subarray.23.0.0.0" expl="loop invariant preservation" proved="true">
<transf name="case" proved="true" arg1="(h&#39; &lt; i)"> <transf name="case" proved="true" arg1="(h&#39; &lt; i)">
<goal name="VC maximum_subarray.23.0.0.0.0" expl="true case (loop invariant preservation)" proved="true"> <goal name="VC maximum_subarray.23.0.0.0.0" expl="true case (loop invariant preservation)" proved="true">
<proof prover="4"><result status="valid" time="0.16"/></proof> <proof prover="4"><result status="valid" time="0.04"/></proof>
</goal> </goal>
<goal name="VC maximum_subarray.23.0.0.0.1" expl="false case (loop invariant preservation)" proved="true"> <goal name="VC maximum_subarray.23.0.0.0.1" expl="false case (loop invariant preservation)" proved="true">
<proof prover="3"><result status="valid" time="0.12"/></proof> <proof prover="3"><result status="valid" time="0.12"/></proof>
...@@ -273,7 +273,7 @@ ...@@ -273,7 +273,7 @@
<goal name="VC maximum_subarray.23.0.0" expl="loop invariant preservation" proved="true"> <goal name="VC maximum_subarray.23.0.0" expl="loop invariant preservation" proved="true">
<transf name="inline_goal" proved="true" > <transf name="inline_goal" proved="true" >
<goal name="VC maximum_subarray.23.0.0.0" expl="loop invariant preservation" proved="true"> <goal name="VC maximum_subarray.23.0.0.0" expl="loop invariant preservation" proved="true">
<proof prover="4" timelimit="30" memlimit="4000"><result status="valid" time="4.16"/></proof> <proof prover="4" timelimit="30" memlimit="4000"><result status="valid" time="1.10"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
...@@ -303,10 +303,10 @@ ...@@ -303,10 +303,10 @@
<goal name="VC maximum_subarray.29.0.0" expl="loop invariant preservation" proved="true"> <goal name="VC maximum_subarray.29.0.0" expl="loop invariant preservation" proved="true">
<transf name="case" proved="true" arg1="(h&#39; &lt; i)"> <transf name="case" proved="true" arg1="(h&#39; &lt; i)">
<goal name="VC maximum_subarray.29.0.0.0" expl="true case (loop invariant preservation)" proved="true"> <goal name="VC maximum_subarray.29.0.0.0" expl="true case (loop invariant preservation)" proved="true">
<proof prover="4"><result status="valid" time="0.19"/></proof> <proof prover="4"><result status="valid" time="0.04"/></proof>
</goal> </goal>
<goal name="VC maximum_subarray.29.0.0.1" expl="false case (loop invariant preservation)" proved="true"> <goal name="VC maximum_subarray.29.0.0.1" expl="false case (loop invariant preservation)" proved="true">
<proof prover="3"><result status="valid" time="0.34"/></proof> <proof prover="3"><result status="valid" time="0.08"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
......
This diff is collapsed.
...@@ -15,10 +15,10 @@ ...@@ -15,10 +15,10 @@
<proof prover="1"><result status="valid" time="0.01"/></proof> <proof prover="1"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="VC fast_exp_imperative.1" expl="precondition" proved="true"> <goal name="VC fast_exp_imperative.1" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof> <proof prover="1"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="VC fast_exp_imperative.2" expl="precondition" proved="true"> <goal name="VC fast_exp_imperative.2" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof> <proof prover="1"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC fast_exp_imperative.3" expl="assertion" proved="true"> <goal name="VC fast_exp_imperative.3" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof> <proof prover="1"><result status="valid" time="0.02"/></proof>
......
...@@ -10,8 +10,6 @@ ...@@ -10,8 +10,6 @@
<prover id="7" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="7" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="10" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="10" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../queens.mlw" proved="true"> <file name="../queens.mlw" proved="true">
<theory name="S" proved="true">
</theory>
<theory name="NQueensSetsTermination" proved="true"> <theory name="NQueensSetsTermination" proved="true">
<goal name="VC t" expl="VC for t" proved="true"> <goal name="VC t" expl="VC for t" proved="true">
<transf name="split_goal_right" proved="true" > <transf name="split_goal_right" proved="true" >
......
...@@ -15,8 +15,6 @@ ...@@ -15,8 +15,6 @@
<proof prover="5"><result status="valid" time="0.02"/></proof> <proof prover="5"><result status="valid" time="0.02"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="Sig" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Rope" proved="true"> <theory name="Rope" proved="true">
<goal name="VC length" expl="VC for length" proved="true"> <goal name="VC length" expl="VC for length" proved="true">
<proof prover="5"><result status="valid" time="0.00"/></proof> <proof prover="5"><result status="valid" time="0.00"/></proof>
......
...@@ -185,20 +185,20 @@ ...@@ -185,20 +185,20 @@
<goal name="VC tree_of_array.7.0.0" expl="assertion" proved="true"> <goal name="VC tree_of_array.7.0.0" expl="assertion" proved="true">
<transf name="destruct_alg" proved="true" arg1="r"> <transf name="destruct_alg" proved="true" arg1="r">
<goal name="VC tree_of_array.7.0.0.0" expl="assertion" proved="true"> <goal name="VC tree_of_array.7.0.0.0" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.05"/></proof> <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal> </goal>
<goal name="VC tree_of_array.7.0.0.1" expl="assertion" proved="true"> <goal name="VC tree_of_array.7.0.0.1" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof> <proof prover="3"><result status="valid" time="0.08"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="VC tree_of_array.7.0.1" expl="assertion" proved="true"> <goal name="VC tree_of_array.7.0.1" expl="assertion" proved="true">
<transf name="destruct_alg" proved="true" arg1="r"> <transf name="destruct_alg" proved="true" arg1="r">
<goal name="VC tree_of_array.7.0.1.0" expl="assertion" proved="true"> <goal name="VC tree_of_array.7.0.1.0" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof> <proof prover="3"><result status="valid" time="0.05"/></proof>
</goal> </goal>
<goal name="VC tree_of_array.7.0.1.1" expl="assertion" proved="true"> <goal name="VC tree_of_array.7.0.1.1" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.08"/></proof> <proof prover="3"><result status="valid" time="0.06"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
...@@ -294,10 +294,10 @@ ...@@ -294,10 +294,10 @@
<goal name="VC update.0" expl="VC for update" proved="true"> <goal name="VC update.0" expl="VC for update" proved="true">
<transf name="destruct_alg" proved="true" arg1="t"> <transf name="destruct_alg" proved="true" arg1="t">
<goal name="VC update.0.0" expl="VC for update" proved="true"> <goal name="VC update.0.0" expl="VC for update" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof> <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal> </goal>
<goal name="VC update.0.1" expl="VC for update" proved="true"> <goal name="VC update.0.1" expl="VC for update" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof> <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
......
...@@ -32,19 +32,19 @@ ...@@ -32,19 +32,19 @@
<proof prover="0"><result status="valid" time="0.00" steps="20"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="20"/></proof>
</goal> </goal>
<goal name="VC mult_naive.8" expl="index in matrix bounds" proved="true"> <goal name="VC mult_naive.8" expl="index in matrix bounds" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
</goal> </goal>
<goal name="VC mult_naive.9" expl="index in matrix bounds" proved="true"> <goal name="VC mult_naive.9" expl="index in matrix bounds" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
</goal> </goal>
<goal name="VC mult_naive.10" expl="index in matrix bounds" proved="true"> <goal name="VC mult_naive.10" expl="index in matrix bounds" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
</goal> </goal>
<goal name="VC mult_naive.11" expl="loop invariant preservation" proved="true"> <goal name="VC mult_naive.11" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="34"/></proof> <proof prover="0"><result status="valid" time="0.05" steps="39"/></proof>
</goal> </goal>
<goal name="VC mult_naive.12" expl="loop invariant preservation" proved="true"> <goal name="VC mult_naive.12" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="77"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="135"/></proof>
</goal> </goal>
<goal name="VC mult_naive.13" expl="loop invariant preservation" proved="true"> <goal name="VC mult_naive.13" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="24"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
...@@ -56,10 +56,10 @@ ...@@ -56,10 +56,10 @@
<proof prover="0"><result status="valid" time="0.01" steps="15"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
</goal> </goal>
<goal name="VC mult_naive.16" expl="loop invariant preservation" proved="true"> <goal name="VC mult_naive.16" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="30"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="31"/></proof>
</goal> </goal>
<goal name="VC mult_naive.17" expl="loop invariant preservation" proved="true"> <goal name="VC mult_naive.17" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="55"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="56"/></proof>
</goal> </goal>
<goal name="VC mult_naive.18" expl="out of loop bounds" proved="true"> <goal name="VC mult_naive.18" expl="out of loop bounds" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="15"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
...@@ -68,7 +68,7 @@ ...@@ -68,7 +68,7 @@
<proof prover="0"><result status="valid" time="0.00" steps="7"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
</goal> </goal>
<goal name="VC mult_naive.20" expl="postcondition" proved="true"> <goal name="VC mult_naive.20" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="22"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
</goal> </goal>
<goal name="VC mult_naive.21" expl="out of loop bounds" proved="true"> <goal name="VC mult_naive.21" expl="out of loop bounds" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
......
...@@ -52,16 +52,16 @@ ...@@ -52,16 +52,16 @@
<proof prover="0"><result status="valid" time="0.01" steps="32"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="32"/></proof>
</goal> </goal>
<goal name="VC maximum_submatrix.14" expl="index in array bounds" proved="true"> <goal name="VC maximum_submatrix.14" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="31"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="32"/></proof>
</goal> </goal>
<goal name="VC maximum_submatrix.15" expl="index in array bounds" proved="true"> <goal name="VC maximum_submatrix.15" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="31"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="32"/></proof>
</goal> </goal>
<goal name="VC maximum_submatrix.16" expl="loop invariant preservation" proved="true"> <goal name="VC maximum_submatrix.16" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="135"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="136"/></proof>
</goal> </goal>
<goal name="VC maximum_submatrix.17" expl="loop invariant preservation" proved="true"> <goal name="VC maximum_submatrix.17" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="135"/></proof> <proof prover="0"><result status="valid" time="0.04" steps="136"/></proof>
</goal> </goal>
<goal name="VC maximum_submatrix.18" expl="assertion" proved="true"> <goal name="VC maximum_submatrix.18" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="1.76" steps="860"/></proof> <proof prover="0"><result status="valid" time="1.76" steps="860"/></proof>
......
...@@ -152,13 +152,13 @@ ...@@ -152,13 +152,13 @@
<goal name="VC main.17.3.0.0" expl="VC for main" proved="true"> <goal name="VC main.17.3.0.0" expl="VC for main" proved="true">
<transf name="split_goal_right" proved="true" > <transf name="split_goal_right" proved="true" >
<goal name="VC main.17.3.0.0.0" expl="VC for main" proved="true"> <goal name="VC main.17.3.0.0.0" expl="VC for main" proved="true">
<