ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity

add a meta to mark a symbol as never removed by remove_unused*

Browse Source 
mark some lemmas on division of real as removable if not needed
This commit is contained in:
BONNOT Paul
2023-06-15 15:18:48 +00:00
committed by MARCHE Claude
parent f21b4d3d3b
commit 29c71dbd51
660 changed files with 8818 additions and 8665 deletions
Download Patch File Download Diff File Expand all files Collapse all files

26
examples/decrease1/why3session.xml
View File

@@ -12,43 +12,43 @@
<goal name="search&#39;vc" expl="VC for search" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="search&#39;vc.0" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="743"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="643"/></proof>
</goal>
<goal name="search&#39;vc.1" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="1030"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="930"/></proof>
</goal>
<goal name="search&#39;vc.2" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="11477"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="10487"/></proof>
</goal>
<goal name="search&#39;vc.3" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="13265"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="12261"/></proof>
</goal>
<goal name="search&#39;vc.4" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="11592"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="10602"/></proof>
</goal>
<goal name="search&#39;vc.5" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="11669"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="10679"/></proof>
</goal>
<goal name="search&#39;vc.6" expl="loop variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="12394"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="11390"/></proof>
</goal>
<goal name="search&#39;vc.7" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="11935"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="10937"/></proof>
</goal>
<goal name="search&#39;vc.8" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="13339"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="12335"/></proof>
</goal>
<goal name="search&#39;vc.9" expl="loop variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="12324"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="11320"/></proof>
</goal>
<goal name="search&#39;vc.10" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="11911"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="10913"/></proof>
</goal>
<goal name="search&#39;vc.11" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="15484"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="12816"/></proof>
</goal>
<goal name="search&#39;vc.12" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="12265"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="11261"/></proof>
</goal>
</transf>
</goal>

BIN
examples/decrease1/why3shapes.gz
View File

Binary file not shown.