Commit f9f4a69c authored by MARCHE Claude's avatar MARCHE Claude

fix sessions (renamed hypotheses due to change of order)

parent dab85923
......@@ -14,9 +14,9 @@
<theory name="M1" proved="true">
<goal name="g" proved="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<transf name="cut" arg1="(0 +^ 0 = 2)">
<transf name="cut" arg1="(0 + 0 = 2)">
<goal name="g.0">
<transf name="cut" arg1="(1.0 + 1.3 = 2.2)">
<transf name="cut" arg1="(1.0 +^ 1.3 = 2.2)">
<goal name="g.0.0">
</goal>
<goal name="g.0.1">
......
......@@ -6,7 +6,7 @@
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="4000"/>
<prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../isqrt_von_neumann.mlw" proved="true">
<theory name="VonNeumann16" proved="true">
<goal name="sqr_add2" proved="true">
......@@ -490,7 +490,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.0.1.1" proved="true">
<proof prover="4" timelimit="1" memlimit="1000"><result status="valid" time="0.14" steps="267"/></proof>
<proof prover="4"><result status="valid" time="0.14" steps="267"/></proof>
</goal>
</transf>
</goal>
......@@ -598,7 +598,7 @@
<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" proved="true">
<transf name="rewrite" proved="true" arg1="&lt;-" arg2="to_uint_add_bounded">
<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.0" proved="true">
<proof prover="4"><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 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>
......@@ -654,9 +654,10 @@
<proof prover="2"><result status="valid" time="0.01"/></proof>
</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.0.1" proved="true">
<transf name="rewrite" proved="true" arg1="h">
<transf name="rewrite" proved="true" arg1="h1">
<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.0.1.0" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="119"/></proof>
<proof prover="3"><result status="timeout" time="1.00"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="132"/></proof>
</goal>
</transf>
</goal>
......
......@@ -501,10 +501,10 @@
</goal>
<goal name="VC sub_valid_coloring_white.8.1.0.1.0.1" expl="VC for sub_valid_coloring_white" proved="true">
<proof prover="2" timelimit="5"><result status="valid" time="2.12"/></proof>
<transf name="remove" proved="true" arg1="real,bool,tuple0,unit,tuple2,map,coloring,stack,zero,one,(-),(+),( * ),(&lt;),(-),(&gt;),(&lt;=),(&gt;=),get,set,([&lt;-]),is_nil,length,mem,size_forest,between_range_forest,valid_nums_forest,count_forest,eq_coloring,size_stack,even_forest,final_forest,any_forest,unchanged,inverse,any_stack,disjoint_stack,x3,x4,x5,Assoc,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm,Assoc1,Mul_distr_l,Mul_distr_r,Comm1,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,is_nil_spec,Length_nonnegative,Length_nil,Append_assoc,Append_l_nil,Append_length,mem_append,mem_decomp,size_forest_nonneg,count_forest_nonneg,mem_app,size_stack_nonneg,any_forest_frame,any_stack_frame,inverse_frame,inverse_frame2,inverse_any,inverse_final,inverse_white,white_final_exclusive,final_unique,inverse_inverse,sub_not_nil,sub_empty,sub_weaken1,sub_weaken2,not_mem_st,sub_frame,sub_no_rep2,white_valid,final_valid,valid_coloring_set,head_and_tail,sub_valid_coloring_f1,sub_valid_coloring,white_white,H1,H2,H3">
<transf name="remove" proved="true" arg1="real,bool,tuple0,unit,tuple2,map,coloring,stack,zero,one,(-),(+),( * ),(&lt;),(-),(&gt;),(&lt;=),(&gt;=),get,set,([&lt;-]),is_nil,length,mem,size_forest,between_range_forest,valid_nums_forest,count_forest,eq_coloring,size_stack,even_forest,final_forest,any_forest,unchanged,inverse,any_stack,disjoint_stack,x2,Assoc,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm,Assoc1,Mul_distr_l,Mul_distr_r,Comm1,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,is_nil_spec,Length_nonnegative,Length_nil,Append_assoc,Append_l_nil,Append_length,mem_append,mem_decomp,size_forest_nonneg,count_forest_nonneg,mem_app,size_stack_nonneg,any_forest_frame,any_stack_frame,inverse_frame,inverse_frame2,inverse_any,inverse_final,inverse_white,white_final_exclusive,final_unique,inverse_inverse,sub_not_nil,sub_empty,sub_weaken1,sub_weaken2,not_mem_st,sub_frame,sub_no_rep2,white_valid,final_valid,valid_coloring_set,head_and_tail,sub_valid_coloring_f1,sub_valid_coloring,white_white,H1,H2,H3">
<goal name="VC sub_valid_coloring_white.8.1.0.1.0.1.0" expl="VC for sub_valid_coloring_white" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.16"/></proof>
<proof prover="4" timelimit="5"><result status="valid" time="0.83"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.14"/></proof>
<proof prover="4" timelimit="5"><result status="valid" time="0.80"/></proof>
</goal>
</transf>
</goal>
......
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