Skip to content

Commit

Permalink
Update sessions
Browse files Browse the repository at this point in the history
  • Loading branch information
@dewert99
dewert99 committed Jul 25, 2024
1 parent 15dcef7 commit 7d7d2b5
Show file tree
Hide file tree
Showing 2 changed files with 79 additions and 0 deletions.
79 changes: 79 additions & 0 deletions creusot/tests/should_succeed/list_reversal_lasso/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,25 +5,84 @@
<prover id="0" name="CVC4" version="1.8" timelimit="5" steplimit="0" memlimit="2000"/>
<prover id="1" name="Z3" version="4.12.4" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.5.3" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="2.5.2" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC5" version="1.0.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="coma" proved="true">
<path name=".."/><path name="list_reversal_lasso.coma"/>
<theory name="Core_Ptr_NonNull_NonNull_Type" proved="true">
<goal name="vc_t_nonnull" proved="true">
<proof prover="3"><result status="valid" time="0.033599" steps="1"/></proof>
</goal>
</theory>
<theory name="Core_Marker_PhantomData_Type" proved="true">
<goal name="vc_t_phantomdata" proved="true">
<proof prover="3"><result status="valid" time="0.013425" steps="1"/></proof>
</goal>
</theory>
<theory name="Core_Ptr_Unique_Unique_Type" proved="true">
<goal name="vc_t_unique" proved="true">
<proof prover="3"><result status="valid" time="0.012142" steps="1"/></proof>
</goal>
</theory>
<theory name="Alloc_RawVec_Cap_Type" proved="true">
<goal name="vc_t_cap" proved="true">
<proof prover="3"><result status="valid" time="0.016167" steps="1"/></proof>
</goal>
</theory>
<theory name="Alloc_RawVec_RawVec_Type" proved="true">
<goal name="vc_t_rawvec" proved="true">
<proof prover="3"><result status="valid" time="0.014030" steps="1"/></proof>
</goal>
</theory>
<theory name="Alloc_Vec_Vec_Type" proved="true">
<goal name="vc_t_vec" proved="true">
<proof prover="3"><result status="valid" time="0.008600" steps="1"/></proof>
</goal>
</theory>
<theory name="Alloc_Alloc_Global_Type" proved="true">
<goal name="vc_t_global" proved="true">
<proof prover="3"><result status="valid" time="0.017907" steps="1"/></proof>
</goal>
</theory>
<theory name="ListReversalLasso_Memory_Type" proved="true">
<goal name="vc_t_memory" proved="true">
<proof prover="3"><result status="valid" time="0.013956" steps="1"/></proof>
</goal>
</theory>
<theory name="ListReversalLasso_Impl1_Index" proved="true">
<goal name="vc_index&#39;0" proved="true">
<proof prover="3"><result status="valid" time="0.020150" steps="1"/></proof>
</goal>
<goal name="vc_index" proved="true">
<proof prover="4"><result status="valid" time="0.046154" steps="9439"/></proof>
</goal>
</theory>
<theory name="ListReversalLasso_Impl2_IndexMut" proved="true">
<goal name="vc_index_mut&#39;0" proved="true">
<proof prover="3"><result status="valid" time="0.015651" steps="1"/></proof>
</goal>
<goal name="vc_index_mut" proved="true">
<proof prover="4"><result status="valid" time="0.041927" steps="13978"/></proof>
</goal>
</theory>
<theory name="ListReversalLasso_Impl4_ListReversalSafe" proved="true">
<goal name="vc_index_mut&#39;0" proved="true">
<proof prover="3"><result status="valid" time="0.022975" steps="1"/></proof>
</goal>
<goal name="vc_index&#39;0" proved="true">
<proof prover="3"><result status="valid" time="0.017021" steps="1"/></proof>
</goal>
<goal name="vc_list_reversal_safe" proved="true">
<proof prover="4"><result status="valid" time="0.101834" steps="26672"/></proof>
</goal>
</theory>
<theory name="ListReversalLasso_Impl4_ListReversalList" proved="true">
<goal name="vc_replace&#39;0" proved="true">
<proof prover="3"><result status="valid" time="0.018193" steps="1"/></proof>
</goal>
<goal name="vc_index_mut&#39;0" proved="true">
<proof prover="3"><result status="valid" time="0.015694" steps="1"/></proof>
</goal>
<goal name="vc_list_reversal_list" proved="true">
<transf name="split_vc" proved="true" >
<goal name="vc_list_reversal_list.0" expl="loop invariant" proved="true">
Expand Down Expand Up @@ -72,6 +131,12 @@
</goal>
</theory>
<theory name="ListReversalLasso_Impl4_ListReversalLoop" proved="true">
<goal name="vc_replace&#39;0" proved="true">
<proof prover="3"><result status="valid" time="0.020078" steps="1"/></proof>
</goal>
<goal name="vc_index_mut&#39;0" proved="true">
<proof prover="3"><result status="valid" time="0.025578" steps="1"/></proof>
</goal>
<goal name="vc_list_reversal_loop" proved="true">
<transf name="split_vc" proved="true" >
<goal name="vc_list_reversal_loop.0" expl="loop invariant" proved="true">
Expand Down Expand Up @@ -173,6 +238,12 @@
</goal>
</theory>
<theory name="ListReversalLasso_Impl4_ListReversalLasso" proved="true">
<goal name="vc_replace&#39;0" proved="true">
<proof prover="3"><result status="valid" time="0.023459" steps="1"/></proof>
</goal>
<goal name="vc_index_mut&#39;0" proved="true">
<proof prover="3"><result status="valid" time="0.014802" steps="1"/></proof>
</goal>
<goal name="vc_list_reversal_lasso" proved="true">
<transf name="split_vc" proved="true" >
<goal name="vc_list_reversal_lasso.0" expl="loop invariant" proved="true">
Expand Down Expand Up @@ -415,6 +486,14 @@
</transf>
</goal>
</theory>
<theory name="Core_Option_Option_Type" proved="true">
<goal name="vc_none" proved="true">
<proof prover="3"><result status="valid" time="0.012629" steps="1"/></proof>
</goal>
<goal name="vc_some" proved="true">
<proof prover="3"><result status="valid" time="0.012645" steps="1"/></proof>
</goal>
</theory>
<theory name="ListReversalLasso_Impl4_FindPtrInSeq_Impl" proved="true">
<goal name="vc_find_ptr_in_seq" proved="true">
<proof prover="4"><result status="valid" time="0.042008" steps="8450"/></proof>
Expand Down
Binary file modified creusot/tests/should_succeed/list_reversal_lasso/why3shapes.gz
View file
Binary file not shown.

0 comments on commit 7d7d2b5

Please sign in to comment.