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

Discriminate: relaxed parameters

parent a20d4ec9
theory BuiltIn
meta "select_inst" "all"
meta "select_lskept" "all"
meta "select_lsinst" "none"
meta "select_inst" "goal"
meta "select_lskept" "goal"
meta "select_lsinst" "goal"
meta "select_kept" "all"
end
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -28,7 +28,7 @@
locfile="../algo64.mlw"
loclnum="37" loccnumb="10" loccnume="19"
expl="VC for quicksort"
sum="e7a9e5262f0a3ce52cb36df9234c1156"
sum="328c05719eeb64b687e3902dd9ca37e2"
proved="true"
expanded="true"
shape="iasorted_subV1V2ainfix +V3c1Aapermut_subV1V1V2ainfix +V3c1asorted_subV8V2ainfix +V3c1Aapermut_subV1V8V2ainfix +V3c1Aapermut_subV7V8V2ainfix +V3c1Iasorted_subV8V5ainfix +V3c1Aapermut_subV7V8V5ainfix +V3c1Aainfix <=c0V0FAainfix <V3V0Aainfix <=V5V3Aainfix <=c0V5Aainfix <ainfix -V3V5ainfix -V3V2Aainfix <=c0ainfix -V3V2Aapermut_subV6V7V2ainfix +V3c1Iasorted_subV7V2ainfix +V4c1Aapermut_subV6V7V2ainfix +V4c1Aainfix <=c0V0FAainfix <V4V0Aainfix <=V2V4Aainfix <=c0V2Aainfix <ainfix -V4V2ainfix -V3V2Aainfix <=c0ainfix -V3V2Iainfix >=agetV6V10V9Iainfix <=V10V3Aainfix <=V5V10FAainfix =agetV6V11V9Iainfix <V11V5Aainfix <V4V11FAainfix <=agetV6V12V9Iainfix <=V12V4Aainfix <=V2V12FEAapermut_subV1V6V2ainfix +V3c1Aainfix <=V5V3Aainfix <V4V5Aainfix <=V2V4Aainfix <=c0V0FAainfix <V3V0Aainfix <V2V3Aainfix <=c0V2ainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0F">
......@@ -43,7 +43,7 @@
locfile="../algo64.mlw"
loclnum="37" loccnumb="10" loccnume="19"
expl="1. precondition"
sum="10046b5481a01c5b51bb31be6e4d4d4e"
sum="4007b3499fa86c232968170da2a50f0c"
proved="true"
expanded="true"
shape="preconditionainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0F">
......@@ -63,7 +63,7 @@
locfile="../algo64.mlw"
loclnum="37" loccnumb="10" loccnume="19"
expl="2. variant decrease"
sum="125a91b9e4bd34db62afce1be81eee91"
sum="259042e29719e4671f18df5036471822"
proved="true"
expanded="true"
shape="variant decreaseainfix <ainfix -V4V2ainfix -V3V2Aainfix <=c0ainfix -V3V2Iainfix >=agetV6V8V7Iainfix <=V8V3Aainfix <=V5V8FAainfix =agetV6V9V7Iainfix <V9V5Aainfix <V4V9FAainfix <=agetV6V10V7Iainfix <=V10V4Aainfix <=V2V10FEAapermut_subV1V6V2ainfix +V3c1Aainfix <=V5V3Aainfix <V4V5Aainfix <=V2V4Aainfix <=c0V0FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0F">
......@@ -83,7 +83,7 @@
locfile="../algo64.mlw"
loclnum="37" loccnumb="10" loccnume="19"
expl="3. precondition"
sum="0f09d807de4624d527adb62488c5fcf4"
sum="24cdc1b9564352dcbd4b236510549079"
proved="true"
expanded="true"
shape="preconditionainfix <V4V0Aainfix <=V2V4Aainfix <=c0V2Iainfix >=agetV6V8V7Iainfix <=V8V3Aainfix <=V5V8FAainfix =agetV6V9V7Iainfix <V9V5Aainfix <V4V9FAainfix <=agetV6V10V7Iainfix <=V10V4Aainfix <=V2V10FEAapermut_subV1V6V2ainfix +V3c1Aainfix <=V5V3Aainfix <V4V5Aainfix <=V2V4Aainfix <=c0V0FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0F">
......@@ -103,7 +103,7 @@
locfile="../algo64.mlw"
loclnum="37" loccnumb="10" loccnume="19"
expl="4. assertion"
sum="2172d6511ad64bce0cb9797f4cc5c3d5"
sum="65562f84d37913134f76ad7cd6cc8acb"
proved="true"
expanded="true"
shape="assertionapermut_subV6V7V2ainfix +V3c1Iasorted_subV7V2ainfix +V4c1Aapermut_subV6V7V2ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V2V4Aainfix <=c0V2Iainfix >=agetV6V9V8Iainfix <=V9V3Aainfix <=V5V9FAainfix =agetV6V10V8Iainfix <V10V5Aainfix <V4V10FAainfix <=agetV6V11V8Iainfix <=V11V4Aainfix <=V2V11FEAapermut_subV1V6V2ainfix +V3c1Aainfix <=V5V3Aainfix <V4V5Aainfix <=V2V4Aainfix <=c0V0FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0F">
......@@ -123,7 +123,7 @@
locfile="../algo64.mlw"
loclnum="37" loccnumb="10" loccnume="19"
expl="5. variant decrease"
sum="8a7ae232d6b324b953a510937681d83d"
sum="6c6ebd1ed639adcabfa2691f8ec8be57"
proved="true"
expanded="true"
shape="variant decreaseainfix <ainfix -V3V5ainfix -V3V2Aainfix <=c0ainfix -V3V2Iapermut_subV6V7V2ainfix +V3c1Iasorted_subV7V2ainfix +V4c1Aapermut_subV6V7V2ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V2V4Aainfix <=c0V2Iainfix >=agetV6V9V8Iainfix <=V9V3Aainfix <=V5V9FAainfix =agetV6V10V8Iainfix <V10V5Aainfix <V4V10FAainfix <=agetV6V11V8Iainfix <=V11V4Aainfix <=V2V11FEAapermut_subV1V6V2ainfix +V3c1Aainfix <=V5V3Aainfix <V4V5Aainfix <=V2V4Aainfix <=c0V0FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0F">
......@@ -143,7 +143,7 @@
locfile="../algo64.mlw"
loclnum="37" loccnumb="10" loccnume="19"
expl="6. precondition"
sum="f51f242786a7b28b3858df083de84603"
sum="8f2775046676af6106a7391a7beabe31"
proved="true"
expanded="true"
shape="preconditionainfix <V3V0Aainfix <=V5V3Aainfix <=c0V5Iapermut_subV6V7V2ainfix +V3c1Iasorted_subV7V2ainfix +V4c1Aapermut_subV6V7V2ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V2V4Aainfix <=c0V2Iainfix >=agetV6V9V8Iainfix <=V9V3Aainfix <=V5V9FAainfix =agetV6V10V8Iainfix <V10V5Aainfix <V4V10FAainfix <=agetV6V11V8Iainfix <=V11V4Aainfix <=V2V11FEAapermut_subV1V6V2ainfix +V3c1Aainfix <=V5V3Aainfix <V4V5Aainfix <=V2V4Aainfix <=c0V0FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0F">
......@@ -163,7 +163,7 @@
locfile="../algo64.mlw"
loclnum="37" loccnumb="10" loccnume="19"
expl="7. assertion"
sum="290e8d20829c2ea09f8ca6ac6219aa2c"
sum="4b4a959d7af8bf12115eff8ccb7bd978"
proved="true"
expanded="true"
shape="assertionapermut_subV7V8V2ainfix +V3c1Iasorted_subV8V5ainfix +V3c1Aapermut_subV7V8V5ainfix +V3c1Aainfix <=c0V0FIainfix <V3V0Aainfix <=V5V3Aainfix <=c0V5Iapermut_subV6V7V2ainfix +V3c1Iasorted_subV7V2ainfix +V4c1Aapermut_subV6V7V2ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V2V4Aainfix <=c0V2Iainfix >=agetV6V10V9Iainfix <=V10V3Aainfix <=V5V10FAainfix =agetV6V11V9Iainfix <V11V5Aainfix <V4V11FAainfix <=agetV6V12V9Iainfix <=V12V4Aainfix <=V2V12FEAapermut_subV1V6V2ainfix +V3c1Aainfix <=V5V3Aainfix <V4V5Aainfix <=V2V4Aainfix <=c0V0FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0F">
......@@ -183,7 +183,7 @@
locfile="../algo64.mlw"
loclnum="37" loccnumb="10" loccnume="19"
expl="8. postcondition"
sum="1fc81bbf8033f10f80a871666ff638d6"
sum="e0147f17d264e89f19453d5cd3b9320b"
proved="true"
expanded="true"
shape="postconditionapermut_subV1V8V2ainfix +V3c1Iapermut_subV7V8V2ainfix +V3c1Iasorted_subV8V5ainfix +V3c1Aapermut_subV7V8V5ainfix +V3c1Aainfix <=c0V0FIainfix <V3V0Aainfix <=V5V3Aainfix <=c0V5Iapermut_subV6V7V2ainfix +V3c1Iasorted_subV7V2ainfix +V4c1Aapermut_subV6V7V2ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V2V4Aainfix <=c0V2Iainfix >=agetV6V10V9Iainfix <=V10V3Aainfix <=V5V10FAainfix =agetV6V11V9Iainfix <V11V5Aainfix <V4V11FAainfix <=agetV6V12V9Iainfix <=V12V4Aainfix <=V2V12FEAapermut_subV1V6V2ainfix +V3c1Aainfix <=V5V3Aainfix <V4V5Aainfix <=V2V4Aainfix <=c0V0FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0F">
......@@ -203,7 +203,7 @@
locfile="../algo64.mlw"
loclnum="37" loccnumb="10" loccnume="19"
expl="9. postcondition"
sum="2732ec2f89e2400f11d3e0afede93c7a"
sum="60032adbc209b4f54d85739de85c2b44"
proved="true"
expanded="true"
shape="postconditionasorted_subV8V2ainfix +V3c1Iapermut_subV7V8V2ainfix +V3c1Iasorted_subV8V5ainfix +V3c1Aapermut_subV7V8V5ainfix +V3c1Aainfix <=c0V0FIainfix <V3V0Aainfix <=V5V3Aainfix <=c0V5Iapermut_subV6V7V2ainfix +V3c1Iasorted_subV7V2ainfix +V4c1Aapermut_subV6V7V2ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V2V4Aainfix <=c0V2Iainfix >=agetV6V10V9Iainfix <=V10V3Aainfix <=V5V10FAainfix =agetV6V11V9Iainfix <V11V5Aainfix <V4V11FAainfix <=agetV6V12V9Iainfix <=V12V4Aainfix <=V2V12FEAapermut_subV1V6V2ainfix +V3c1Aainfix <=V5V3Aainfix <V4V5Aainfix <=V2V4Aainfix <=c0V0FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0F">
......@@ -223,7 +223,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="55.75"/>
<result status="valid" time="93.50"/>
</proof>
</goal>
<goal
......@@ -231,7 +231,7 @@
locfile="../algo64.mlw"
loclnum="37" loccnumb="10" loccnume="19"
expl="10. postcondition"
sum="52fed150ed032a75da9910f9c6ae9717"
sum="01653fdfcffe9ea7b225766d1d5219c4"
proved="true"
expanded="true"
shape="postconditionapermut_subV1V1V2ainfix +V3c1INainfix &lt;V2V3Iainfix &lt;V3V0Aainfix &lt;=V2V3Aainfix &lt;=c0V2Aainfix &lt;=c0V0F">
......@@ -251,7 +251,7 @@
locfile="../algo64.mlw"
loclnum="37" loccnumb="10" loccnume="19"
expl="11. postcondition"
sum="269e484c5a64ce4d6cc45e556594ed2e"
sum="deed4f33be59d1049529b9dd9e33402c"
proved="true"
expanded="true"
shape="postconditionasorted_subV1V2ainfix +V3c1INainfix &lt;V2V3Iainfix &lt;V3V0Aainfix &lt;=V2V3Aainfix &lt;=c0V2Aainfix &lt;=c0V0F">
......
This diff is collapsed.
......@@ -24,7 +24,7 @@
locfile="../arm.mlw"
loclnum="16" loccnumb="6" loccnume="20"
expl="VC for insertion_sort"
sum="ff4534d299565274c09d1a7200c24c10"
sum="f940591114a5a2f92e254b9fe7e4a80e"
proved="false"
expanded="false"
shape="iainfix &lt;=V6c45Aainfix =V7c9Aainfix &lt;=c0V0iainfix &lt;ainfix -c10V16ainfix -c10V5Aainfix &lt;=c0ainfix -c10V5Aainfix &lt;=ainfix *c2V12ainfix *ainfix -V16c2ainfix -V16c1Aainfix =V10ainfix -V16c2AainvV14Aainfix &lt;=V16c11Aainfix &lt;=c2V16Iainfix =V16ainfix +V5c1Fainfix &lt;V22V11Aainfix &lt;=c0V11Aainfix &lt;=ainfix *c2V17ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V22Aainvamk arrayV0V21Aainfix &lt;=V22V5Aainfix &lt;=c1V22Iainfix =V22ainfix -V11c1FIainfix =V21asetV19V20agetV13V11Aainfix &lt;=c0V0FAainfix &lt;V20V0Aainfix &lt;=c0V20Lainfix -V11c1Iainfix =V19asetV13V11agetV13V18Aainfix &lt;=c0V0FAainfix &lt;V11V0Aainfix &lt;=c0V11Aainfix &lt;V18V0Aainfix &lt;=c0V18Lainfix -V11c1Aainfix &lt;V11V0Aainfix &lt;=c0V11Iainfix =V17ainfix +V12c1Fainfix &lt;agetV13V11agetV13V15Aainfix &lt;V11V0Aainfix &lt;=c0V11Aainfix &lt;V15V0Aainfix &lt;=c0V15Aainfix &lt;=c0V0Lainfix -V11c1Iainfix &lt;=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix &lt;=V11V5Aainfix &lt;=c1V11Lamk arrayV0V13FAainfix &lt;=ainfix *c2V6ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V5AainvV9Aainfix &lt;=V5V5Aainfix &lt;=c1V5Iainfix =V10ainfix +V7c1Fainfix &lt;=V5c10Iainfix &lt;=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix &lt;=V5c11Aainfix &lt;=c2V5Lamk arrayV0V8FAainfix &lt;=ainfix *c2V1ainfix *ainfix -c2c2ainfix -c2c1Aainfix =V2ainfix -c2c2AainvV4Aainfix &lt;=c2c11Aainfix &lt;=c2c2Iainfix =V1c0Aainfix =V2c0AainvV4Aainfix &lt;=c0V0Lamk arrayV0V3FF">
......@@ -50,7 +50,7 @@
locfile="../arm.mlw"
loclnum="120" loccnumb="6" loccnume="18"
expl="VC for path_init_l2"
sum="a673c6b14e3f66097ab6521a75fc2975"
sum="13ee9e621a3499b8bf1124dff3328e0f"
proved="true"
expanded="true"
shape="ainv_l2V5V0V2Iainfix =V5amixfix [&lt;-]V1ainfix -V0c16V4FIainfix =V4c2FIainfix =V3c0FIainfix =V2c0FIainvV1AaseparationV0F">
......@@ -78,7 +78,7 @@
locfile="../arm.mlw"
loclnum="127" loccnumb="6" loccnume="18"
expl="VC for path_l2_exit"
sum="850b762a046fc7dd2686d4a5b7033244"
sum="1f09826b67be51d5b87f720f399ba7d6"
proved="true"
expanded="true"
shape="ainfix =V0c9Iainfix =V4aFalseIainfix &lt;=V3c10qainfix =V4aTrueFIainfix =V3amixfix []V2ainfix -V1c16FIainv_l2V2V1V0AaseparationV1F">
......
......@@ -24,7 +24,7 @@
locfile="../assigning_meanings_to_programs.mlw"
loclnum="12" loccnumb="6" loccnume="9"
expl="VC for sum"
sum="9ce3e09613751b22aec78ab286a1ccb3"
sum="1f2a0aceb76ac64fe74ba1cb24f480ff"
proved="true"
expanded="true"
shape="iainfix =V3asumV1c1ainfix +V2c1ainfix &lt;ainfix -V2V6ainfix -V2V4Aainfix &lt;=c0ainfix -V2V4Aainfix =V5asumV1c1V6Aainfix &lt;=V6ainfix +V2c1Aainfix &lt;=c1V6Iainfix =V6ainfix +V4c1FIainfix =V5ainfix +V3agetV1V4FAainfix &lt;V4V0Aainfix &lt;=c0V4ainfix &lt;=V4V2Iainfix =V3asumV1c1V4Aainfix &lt;=V4ainfix +V2c1Aainfix &lt;=c1V4FAainfix =c0asumV1c1c1Aainfix &lt;=c1ainfix +V2c1Aainfix &lt;=c1c1Iainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;=c0V0F">
......
......@@ -24,7 +24,7 @@
locfile="../binary_search.mlw"
loclnum="17" loccnumb="6" loccnume="19"
expl="VC for binary_search"
sum="08847e78e28f9e02c4b8da41705b16fc"
sum="90a1476b0d7f875a0e59360b5542a4fa"
proved="true"
expanded="true"
shape="iNainfix =agetV1V5V2Iainfix &lt;V5V0Aainfix &lt;=c0V5Fiiainfix =agetV1V6V2Aainfix &lt;V6V0Aainfix &lt;=c0V6ainfix &lt;ainfix -V7V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V8V7Aainfix &lt;=V4V8Iainfix =agetV1V8V2Iainfix &lt;V8V0Aainfix &lt;=c0V8FAainfix &lt;V7V0Aainfix &lt;=c0V4Iainfix =V7ainfix -V6c1Fainfix &gt;agetV1V6V2Aainfix &lt;V6V0Aainfix &lt;=c0V6ainfix &lt;ainfix -V3V9ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V10V3Aainfix &lt;=V9V10Iainfix =agetV1V10V2Iainfix &lt;V10V0Aainfix &lt;=c0V10FAainfix &lt;V3V0Aainfix &lt;=c0V9Iainfix =V9ainfix +V6c1Fainfix &lt;agetV1V6V2Aainfix &lt;V6V0Aainfix &lt;=c0V6Aainfix &lt;=V6V3Aainfix &lt;=V4V6Lainfix +V4adivainfix -V3V4c2ainfix &lt;=V4V3Iainfix &lt;=V11V3Aainfix &lt;=V4V11Iainfix =agetV1V11V2Iainfix &lt;V11V0Aainfix &lt;=c0V11FAainfix &lt;V3V0Aainfix &lt;=c0V4FAainfix &lt;=V12ainfix -V0c1Aainfix &lt;=c0V12Iainfix =agetV1V12V2Iainfix &lt;V12V0Aainfix &lt;=c0V12FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Iainfix &lt;=agetV1V13agetV1V14Iainfix &lt;V14V0Aainfix &lt;=V13V14Aainfix &lt;=c0V13FAainfix &lt;=c0V0F">
......@@ -59,7 +59,7 @@
locfile="../binary_search.mlw"
loclnum="60" loccnumb="6" loccnume="19"
expl="VC for binary_search"
sum="7302df6e214500c9c3bd1a2ae61f34ce"
sum="d4bfbfcbdb6c193efb4fafa560a91672"
proved="true"
expanded="true"
shape="iNainfix =agetV1V5V2Iainfix &lt;V5V0Aainfix &lt;=c0V5Fiiainfix =agetV1V6V2Aainfix &lt;V6V0Aainfix &lt;=c0V6ainfix &lt;ainfix -V7V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V8V7Aainfix &lt;=V4V8Iainfix =agetV1V8V2Iainfix &lt;V8V0Aainfix &lt;=c0V8FAainfix &lt;V7V0Aainfix &lt;=c0V4Iainfix =V7ainfix -V6c1Fainfix &gt;agetV1V6V2Aainfix &lt;V6V0Aainfix &lt;=c0V6ainfix &lt;ainfix -V3V9ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V10V3Aainfix &lt;=V9V10Iainfix =agetV1V10V2Iainfix &lt;V10V0Aainfix &lt;=c0V10FAainfix &lt;V3V0Aainfix &lt;=c0V9Iainfix =V9ainfix +V6c1Fainfix &lt;agetV1V6V2Aainfix &lt;V6V0Aainfix &lt;=c0V6Iainfix &lt;=V6V3Aainfix &lt;=V4V6FAainfix &lt;=V4V3ainfix &lt;=V4V3Iainfix &lt;=V11V3Aainfix &lt;=V4V11Iainfix =agetV1V11V2Iainfix &lt;V11V0Aainfix &lt;=c0V11FAainfix &lt;V3V0Aainfix &lt;=c0V4FAainfix &lt;=V12ainfix -V0c1Aainfix &lt;=c0V12Iainfix =agetV1V12V2Iainfix &lt;V12V0Aainfix &lt;=c0V12FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Iainfix &lt;=agetV1V13agetV1V14Iainfix &lt;V14V0Aainfix &lt;=V13V14Aainfix &lt;=c0V13FAainfix &lt;=c0V0F">
......@@ -86,7 +86,7 @@
locfile="../binary_search.mlw"
loclnum="100" loccnumb="6" loccnume="19"
expl="VC for binary_search"
sum="65cd85f330f0ad5752c4568a313833cc"
sum="b8cee34167a755ace3b9f1e21b33147d"
proved="true"
expanded="true"
shape="iNainfix =agetV1V5V2Iainfix &lt;V5V0Aainfix &lt;=c0V5Fiiainfix =agetV1V7V2Aainfix &lt;V7V0Aainfix &lt;=c0V7ainfix &lt;ainfix -V8V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V9V8Aainfix &lt;=V4V9Iainfix =agetV1V9V2Iainfix &lt;V9V0Aainfix &lt;=c0V9FAainfix &lt;V8V0Aainfix &lt;=c0V4Iainfix =V8ainfix -V7c1FAainfix &lt;=ainfix -V7c1amax_intAainfix &lt;=amin_intainfix -V7c1ainfix &gt;agetV1V7V2Aainfix &lt;V7V0Aainfix &lt;=c0V7ainfix &lt;ainfix -V3V10ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V11V3Aainfix &lt;=V10V11Iainfix =agetV1V11V2Iainfix &lt;V11V0Aainfix &lt;=c0V11FAainfix &lt;V3V0Aainfix &lt;=c0V10Iainfix =V10ainfix +V7c1FAainfix &lt;=ainfix +V7c1amax_intAainfix &lt;=amin_intainfix +V7c1ainfix &lt;agetV1V7V2Aainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;=V7V3Aainfix &lt;=V4V7Lainfix +V4V6Aainfix &lt;=ainfix +V4V6amax_intAainfix &lt;=amin_intainfix +V4V6Ladivainfix -V3V4c2Aainfix &lt;=ainfix -V3V4amax_intAainfix &lt;=amin_intainfix -V3V4ainfix &lt;=V4V3Iainfix &lt;=V12V3Aainfix &lt;=V4V12Iainfix =agetV1V12V2Iainfix &lt;V12V0Aainfix &lt;=c0V12FAainfix &lt;V3V0Aainfix &lt;=c0V4FAainfix &lt;=V13ainfix -V0c1Aainfix &lt;=c0V13Iainfix =agetV1V13V2Iainfix &lt;V13V0Aainfix &lt;=c0V13FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Aainfix &lt;=ainfix -V0c1amax_intAainfix &lt;=amin_intainfix -V0c1Iainfix &lt;=agetV1V14agetV1V15Iainfix &lt;V15V0Aainfix &lt;=V14V15Aainfix &lt;=c0V14FAainfix &lt;=V0amax_intAainfix &lt;=c0V0F">
......
......@@ -39,7 +39,7 @@
name="G1"
locfile="../array.why"
loclnum="4" loccnumb="7" loccnume="9"
sum="4b18b5e9ed1cb2e0329467ed5aa63218"
sum="9e110ad1929b5e8fc4f8245ddd7e2e62"
proved="true"
expanded="true"
shape="ainfix =agetasetV2V1V0V1V0FF">
......@@ -96,7 +96,7 @@
name="G2"
locfile="../array.why"
loclnum="6" loccnumb="7" loccnume="9"
sum="627171699b87946dbd6ad9d85efdfd3f"
sum="51d8da14e6a96a75ad5c2e0a41c49410"
proved="true"
expanded="true"
shape="ainfix =agetasetV4V0V3V2V1Iainfix =agetV4V2V1INainfix =V2V0FF">
......@@ -153,7 +153,7 @@
name="G3"
locfile="../array.why"
loclnum="10" loccnumb="7" loccnume="9"
sum="1844832a4c576d2a6968388a8471551f"
sum="54fe4ed8312547c3ff3e144873ea5938"
proved="true"
expanded="true"
shape="ainfix =agetasetV2c1V1c0V0Iainfix =agetV2c0V0FF">
......@@ -210,7 +210,7 @@
name="G4"
locfile="../array.why"
loclnum="13" loccnumb="7" loccnume="9"
sum="7e93c34f69527d7fb298d8fb6700c00e"
sum="5acf5443076725da68a264b0f0e40354"
proved="true"
expanded="true"
shape="ainfix =agetasetasetV2c1V1c0V0c1V1FF">
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -24,7 +24,7 @@
locfile="../fib_memo.mlw"
loclnum="33" loccnumb="10" loccnume="14"
expl="VC for fibo"
sum="d534d4014aafb7d9e129140fa0680e9e"
sum="89f6a0a8763135562e58d9522abe9a8f"
proved="true"
expanded="true"
shape="iainvV5Aainfix =ainfix +afibV4afibV2afibV0IainvV5FAainvV3Aainfix &lt;=c0V4Lainfix -V0c1IainvV3FAainvV1Aainfix &lt;=c0V2Lainfix -V0c2ainvV1Aainfix =c1afibV0ainfix &lt;=V0c1IainvV1Aainfix &lt;=c0V0FF">
......@@ -44,7 +44,7 @@
locfile="../fib_memo.mlw"
loclnum="41" loccnumb="7" loccnume="16"
expl="VC for memo_fibo"
sum="dd7ca3265f158c30003f38b2292a5cf4"
sum="2e6cd9c9303224853b6d0b63d113a87c"
proved="true"
expanded="true"
shape="ainvV4Aainfix =V3afibV0Iainfix =V4asetV2V0aSomeV3FIainvV2LafibV0FAainvV1Aainfix &lt;=c0V0Iainfix =agetV1V0aNoneAainvV1Aainfix =V5afibV0Iainfix =agetV1V0aSomeV5FIainvV1Aainfix &lt;=c0V0FF">
......@@ -59,7 +59,7 @@
locfile="../fib_memo.mlw"
loclnum="41" loccnumb="7" loccnume="16"
expl="1. postcondition"
sum="75e8ce32a14eb992f93a17aa02f2667f"
sum="304d2b1fcca3103de952b313dda607e4"
proved="true"
expanded="true"
shape="postconditionainvV1Aainfix =V2afibV0Iainfix =agetV1V0aSomeV2FIainvV1Aainfix &lt;=c0V0FF">
......@@ -79,7 +79,7 @@
locfile="../fib_memo.mlw"
loclnum="41" loccnumb="7" loccnume="16"
expl="2. precondition"
sum="783b32e575b842ca8d353d40a8b9544f"
sum="6ece570e2b60c27e1e4a240e9ebc4d02"
proved="true"
expanded="true"
shape="preconditionainvV1Aainfix &lt;=c0V0Iainfix =agetV1V0aNoneIainvV1Aainfix &lt;=c0V0FF">
......@@ -99,7 +99,7 @@
locfile="../fib_memo.mlw"
loclnum="41" loccnumb="7" loccnume="16"
expl="3. postcondition"
sum="7f1a9a91134e9fb7590f757988e71e16"
sum="a8392d62466c8d39b494b9c2ef0edd51"
proved="true"
expanded="true"
shape="postconditionainvV4Aainfix =V3afibV0Iainfix =V4asetV2V0aSomeV3FIainvV2LafibV0FIainvV1Aainfix &lt;=c0V0Iainfix =agetV1V0aNoneIainvV1Aainfix &lt;=c0V0FF">
......
......@@ -23,7 +23,7 @@
name="size_nonneg"
locfile="../fill.mlw"
loclnum="23" loccnumb="8" loccnume="19"
sum="a88fe98443b22fd9ca81a0fe000f5bfa"
sum="1add01d9ea22bf5100c21a8dff355d8e"
proved="true"
expanded="true"
shape="ainfix &gt;=asizeV0c0F">
......@@ -45,7 +45,7 @@
locfile="../fill.mlw"
loclnum="23" loccnumb="8" loccnume="19"
expl="1."
sum="653d9ffd8fbcdd8b08fab32695b6e3fd"
sum="7eb3e23636162e1b6c02f741cdf7295e"
proved="true"
expanded="false"
shape="Cainfix &gt;=asizeV0c0aNullainfix &gt;=asizeV0c0Iainfix &gt;=asizeV1c0Iainfix &gt;=asizeV3c0aNodeVVVV0F">
......@@ -65,7 +65,7 @@
locfile="../fill.mlw"
loclnum="25" loccnumb="10" loccnume="14"
expl="VC for fill"
sum="0b3b1c0d5b82819f85c764c60b0fee14"
sum="341c641ddf8ff6c88dde19775c400ae5"
proved="true"
expanded="true"
shape="CacontainsV0agetV2V4Iainfix &lt;V4V3Aainfix &lt;=V3V4FAainfix =agetV2V5agetV2V5Iainfix &lt;V5V3Aainfix &lt;=c0V5FAainfix &lt;=V3V1Aainfix &lt;=V3V3aNulliacontainsV0agetV9V11Iainfix &lt;V11V10Aainfix &lt;=V3V11FAainfix =agetV9V12agetV2V12Iainfix &lt;V12V3Aainfix &lt;=c0V12FAainfix &lt;=V10V1Aainfix &lt;=V3V10acontainsV0agetV15V17Iainfix &lt;V17V16Aainfix &lt;=V3V17FAainfix =agetV15V18agetV2V18Iainfix &lt;V18V3Aainfix &lt;=c0V18FAainfix &lt;=V16V1Aainfix &lt;=V3V16IacontainsV8agetV15V19Iainfix &lt;V19V16Aainfix &lt;=V14V19FAainfix =agetV15V20agetV13V20Iainfix &lt;V20V14Aainfix &lt;=c0V20FAainfix &lt;=V16V1Aainfix &lt;=V14V16Aainfix &lt;=c0V1FFAainfix &lt;=V14V1Aainfix &lt;=c0V14Aainfix &lt;asizeV8asizeV0Aainfix &lt;=c0asizeV0Lainfix +V10c1Iainfix =V13asetV9V10V7Aainfix &lt;=c0V1FAainfix &lt;V10V1Aainfix &lt;=c0V10Nainfix =V10V1IacontainsV6agetV9V21Iainfix &lt;V21V10Aainfix &lt;=V3V21FAainfix =agetV9V22agetV2V22Iainfix &lt;V22V3Aainfix &lt;=c0V22FAainfix &lt;=V10V1Aainfix &lt;=V3V10Aainfix &lt;=c0V1FFAainfix &lt;=V3V1Aainfix &lt;=c0V3Aainfix &lt;asizeV6asizeV0Aainfix &lt;=c0asizeV0aNodeVVVV0Iainfix &lt;=V3V1Aainfix &lt;=c0V3Aainfix &lt;=c0V1F">
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -28,7 +28,7 @@
locfile="../array_max.mlw"
loclnum="21" loccnumb="6" loccnume="9"
expl="VC for max"
sum="c3ec2b5cc0b8c3ed0c6ab2fadf5dc1bc"
sum="709d10694ba5d9dd6333cff3c3a7ba81"
proved="true"
expanded="true"
shape="iainfix &lt;=agetV1V4agetV1V3Iainfix &lt;V4V0Aainfix &lt;=c0V4FAainfix &lt;V3V0Aainfix &lt;=c0V3iainfix &lt;ainfix -V5V3ainfix -V2V3Aainfix &lt;=c0ainfix -V2V3Aainfix &lt;=agetV1V6amaxagetV1V3agetV1V5Iainfix &lt;V6V0Aainfix &lt;V5V6Oainfix &lt;V6V3Aainfix &lt;=c0V6FAainfix &lt;V5V0Aainfix &lt;=V3V5Aainfix &lt;=c0V3Iainfix =V5ainfix -V2c1Fainfix &lt;ainfix -V2V7ainfix -V2V3Aainfix &lt;=c0ainfix -V2V3Aainfix &lt;=agetV1V8amaxagetV1V7agetV1V2Iainfix &lt;V8V0Aainfix &lt;V2V8Oainfix &lt;V8V7Aainfix &lt;=c0V8FAainfix &lt;V2V0Aainfix &lt;=V7V2Aainfix &lt;=c0V7Iainfix =V7ainfix +V3c1Fainfix &lt;=agetV1V3agetV1V2Aainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V2V0Aainfix &lt;=c0V2Nainfix =V3V2Iainfix &lt;=agetV1V9amaxagetV1V3agetV1V2Iainfix &lt;V9V0Aainfix &lt;V2V9Oainfix &lt;V9V3Aainfix &lt;=c0V9FAainfix &lt;V2V0Aainfix &lt;=V3V2Aainfix &lt;=c0V3FAainfix &lt;=agetV1V10amaxagetV1c0agetV1ainfix -V0c1Iainfix &lt;V10V0Aainfix &lt;ainfix -V0c1V10Oainfix &lt;V10c0Aainfix &lt;=c0V10FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0ainfix -V0c1Aainfix &lt;=c0c0Iainfix &lt;c0V0Aainfix &lt;=c0V0F">
......
......@@ -35,7 +35,7 @@
locfile="../duplets.mlw"
loclnum="43" loccnumb="6" loccnume="12"
expl="VC for duplet"
sum="da16a325dd41dd659b5e6a62813bdfb9"
sum="6b15a16a5df4d7e9e85c7ee0ed427bed"
proved="true"
expanded="true"
shape="fINais_dupletV3V5V6INCfaNoneainfix =V7agetV1V5aSomeVV2Iainfix &lt;V6V0Aainfix &lt;V5V6Aainfix &lt;V5ainfix +V4c1Aainfix &lt;=c0V5FAiNais_dupletV3V12V13INCfaNoneainfix =V14agetV1V12aSomeVV2Iainfix &lt;V13V0Aainfix &lt;V12V13Aainfix &lt;V12ainfix +V8c1Aainfix &lt;=c0V12FINais_dupletV3V8V15Iainfix &lt;V15ainfix +V10c1Aainfix &lt;V8V15FAiNais_dupletV3V8V17Iainfix &lt;V17ainfix +V16c1Aainfix &lt;V8V17FNCfaNoneainfix =V20agetV1V18aSomeVV2Aais_dupletV3V18V19Iainfix =V19V16Aainfix =V18V8Fainfix =agetV1V16V9Aainfix &lt;V16V0Aainfix &lt;=c0V16INais_dupletV3V8V21Iainfix &lt;V21V16Aainfix &lt;V8V21FIainfix &lt;=V16V10Aainfix &lt;=V11V16FANais_dupletV3V8V22Iainfix &lt;V22V11Aainfix &lt;V8V22FIainfix &lt;=V11V10ANais_dupletV3V23V24INCfaNoneainfix =V25agetV1V23aSomeVV2Iainfix &lt;V24V0Aainfix &lt;V23V24Aainfix &lt;V23ainfix +V8c1Aainfix &lt;=c0V23FIainfix &gt;V11V10Lainfix +V8c1Lainfix -V0c1Nais_dupletV3V26V27INCfaNoneainfix =V28agetV1V26aSomeVV2Iainfix &lt;V27V0Aainfix &lt;V26V27Aainfix &lt;V26ainfix +V8c1Aainfix &lt;=c0V26FCfaNoneainfix =V29V9aSomeVV2LagetV1V8Aainfix &lt;V8V0Aainfix &lt;=c0V8INais_dupletV3V30V31INCfaNoneainfix =V32agetV1V30aSomeVV2Iainfix &lt;V31V0Aainfix &lt;V30V31Aainfix &lt;V30V8Aainfix &lt;=c0V30FIainfix &lt;=V8V4Aainfix &lt;=c0V8FANais_dupletV3V33V34INCfaNoneainfix =V35agetV1V33aSomeVV2Iainfix &lt;V34V0Aainfix &lt;V33V34Aainfix &lt;V33c0Aainfix &lt;=c0V33FIainfix &lt;=c0V4AfIainfix &gt;c0V4Lainfix -V0c2INCfaNoneainfix =V38agetV1V36aSomeVV2Aais_dupletV3V36V37EAainfix &lt;=c2V0Aainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -63,7 +63,7 @@
locfile="../duplets.mlw"
loclnum="74" loccnumb="6" loccnume="13"
expl="VC for duplets"
sum="4658940c6746265baf8a378b2918b363"
sum="9dab27f087b66d55d95c9a19f502ffde"
proved="true"
expanded="true"
shape="Nainfix =agetV1V3agetV1V5Aais_dupletV2V5V6Aais_dupletV2V3V4INainfix =agetV1V4agetV1V5Aais_dupletV2V5V6FANainfix =agetV1V4agetV1V7Aais_dupletV2V7V8EAainfix &lt;=c2V0Aainfix &lt;V4V0Aainfix &lt;=c0V4Iais_dupletV2V3V4FAais_dupletV2V9V10EAainfix &lt;=c2V0INainfix =agetV1V11agetV1V13Aais_dupletV2V13V14Aais_dupletV2V11V12EAainfix &lt;=c4V0Aainfix &lt;=c0V0Lamk arrayV0V1F">
......
......@@ -20,7 +20,7 @@
locfile="../foveoos11_challenge1.mlw"
loclnum="13" loccnumb="6" loccnume="9"
expl="VC for max"
sum="b63c0da8eca803644bccc40fbcdf21db"
sum="4e27305c00a5b1efd875f40b6b3b9ea0"
proved="true"
expanded="true"
shape="iainfix &lt;=agetV1V4agetV1V3Iainfix &lt;V4V0Aainfix &lt;=c0V4FAainfix &lt;V3V0Aainfix &lt;=c0V3iainfix &lt;ainfix -V5V3ainfix -V2V3Aainfix &lt;=c0ainfix -V2V3Aainfix &lt;=agetV1V6agetV1V3Oainfix &lt;=agetV1V6agetV1V5Iainfix &lt;V6V0Aainfix &lt;V5V6Oainfix &lt;V6V3Aainfix &lt;=c0V6FAainfix &lt;V5V0Aainfix &lt;=V3V5Aainfix &lt;=c0V3Iainfix =V5ainfix -V2c1Fainfix &lt;ainfix -V2V7ainfix -V2V3Aainfix &lt;=c0ainfix -V2V3Aainfix &lt;=agetV1V8agetV1V7Oainfix &lt;=agetV1V8agetV1V2Iainfix &lt;V8V0Aainfix &lt;V2V8Oainfix &lt;V8V7Aainfix &lt;=c0V8FAainfix &lt;V2V0Aainfix &lt;=V7V2Aainfix &lt;=c0V7Iainfix =V7ainfix +V3c1Fainfix &lt;=agetV1V3agetV1V2Aainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V2V0Aainfix &lt;=c0V2Nainfix =V3V2Iainfix &lt;=agetV1V9agetV1V3Oainfix &lt;=agetV1V9agetV1V2Iainfix &lt;V9V0Aainfix &lt;V2V9Oainfix &lt;V9V3Aainfix &lt;=c0V9FAainfix &lt;V2V0Aainfix &lt;=V3V2Aainfix &lt;=c0V3FAainfix &lt;=agetV1V10agetV1c0Oainfix &lt;=agetV1V10agetV1ainfix -V0c1Iainfix &lt;V10V0Aainfix &lt;ainfix -V0c1V10Oainfix &lt;V10c0Aainfix &lt;=c0V10FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0ainfix -V0c1Aainfix &lt;=c0c0Iainfix &gt;V0c0Aainfix &lt;=c0V0F">
......@@ -35,7 +35,7 @@
locfile="../foveoos11_challenge1.mlw"
loclnum="13" loccnumb="6" loccnume="9"
expl="1. loop invariant init"
sum="7e9e4b83aca33699bb4220a55024e5b4"
sum="20206df170e8be49e614376241d91d7a"
proved="true"
expanded="false"
shape="loop invariant initainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0ainfix -V0c1Aainfix &lt;=c0c0Iainfix &gt;V0c0Aainfix &lt;=c0V0F">
......@@ -55,7 +55,7 @@
locfile="../foveoos11_challenge1.mlw"
loclnum="13" loccnumb="6" loccnume="9"
expl="2. loop invariant init"
sum="39383d72235958d2147f919f7c852879"
sum="8f86aed076e799af4cc66d1c5290737b"
proved="true"
expanded="false"
shape="loop invariant initainfix &lt;=agetV1V2agetV1c0Oainfix &lt;=agetV1V2agetV1ainfix -V0c1Iainfix &lt;V2V0Aainfix &lt;ainfix -V0c1V2Oainfix &lt;V2c0Aainfix &lt;=c0V2FIainfix &gt;V0c0Aainfix &lt;=c0V0F">
......@@ -75,7 +75,7 @@
locfile="../foveoos11_challenge1.mlw"
loclnum="13" loccnumb="6" loccnume="9"
expl="3. precondition"
sum="16ea9b83d3da10ea9d90c13726fd9eea"
sum="822aaae7e1efd62219f6d58ebf4cd9cc"
proved="true"
expanded="false"
shape="preconditionainfix &lt;V2V0Aainfix &lt;=c0V2INainfix =V3V2Iainfix &lt;=agetV1V4agetV1V3Oainfix &lt;=agetV1V4agetV1V2Iainfix &lt;V4V0Aainfix &lt;V2V4Oainfix &lt;V4V3Aainfix &lt;=c0V4FAainfix &lt;V2V0Aainfix &lt;=V3V2Aainfix &lt;=c0V3FIainfix &gt;V0c0Aainfix &lt;=c0V0F">
......@@ -95,7 +95,7 @@
locfile="../foveoos11_challenge1.mlw"
loclnum="13" loccnumb="6" loccnume="9"
expl="4. precondition"
sum="45da1de8c187466f26e3fd4acbff0442"
sum="6c431585b3f034c69db2eab736e157cf"
proved="true"
expanded="false"
shape="preconditionainfix &lt;V3V0Aainfix &lt;=c0V3Iainfix &lt;V2V0Aainfix &lt;=c0V2INainfix =V3V2Iainfix &lt;=agetV1V4agetV1V3Oainfix &lt;=agetV1V4agetV1V2Iainfix &lt;V4V0Aainfix &lt;V2V4Oainfix &lt;V4V3Aainfix &lt;=c0V4FAainfix &lt;V2V0Aainfix &lt;=V3V2Aainfix &lt;=c0V3FIainfix &gt;V0c0Aainfix &lt;=c0V0F">
......@@ -115,7 +115,7 @@
locfile="../foveoos11_challenge1.mlw"
loclnum="13" loccnumb="6" loccnume="9"
expl="5. loop invariant preservation"
sum="0c7786e4f097f35bd263344f4da0c9a1"
sum="8a30947ffb89dc14be463058c7154d82"
proved="true"
expanded="false"
shape="loop invariant preservationainfix &lt;V2V0Aainfix &lt;=V4V2Aainfix &lt;=c0V4Iainfix =V4ainfix +V3c1FIainfix &lt;=agetV1V3agetV1V2Iainfix &lt;V3V0Aainfix &lt;=c0V3Iainfix &lt;V2V0Aainfix &lt;=c0V2INainfix =V3V2Iainfix &lt;=agetV1V5agetV1V3Oainfix &lt;=agetV1V5agetV1V2Iainfix &lt;V5V0Aainfix &lt;V2V5Oainfix &lt;V5V3Aainfix &lt;=c0V5FAainfix &lt;V2V0Aainfix &lt;=V3V2Aainfix &lt;=c0V3FIainfix &gt;V0c0Aainfix &lt;=c0V0F">
......@@ -135,7 +135,7 @@
locfile="../foveoos11_challenge1.mlw"
loclnum="13" loccnumb="6" loccnume="9"
expl="6. loop invariant preservation"
sum="4419b516cc82e4d3fb529ac41703e5e3"
sum="fa6be6618d2a98b34326bdb885665d19"
proved="true"
expanded="false"
shape="loop invariant preservationainfix &lt;=agetV1V5agetV1V4Oainfix &lt;=agetV1V5agetV1V2Iainfix &lt;V5V0Aainfix &lt;V2V5Oainfix &lt;V5V4Aainfix &lt;=c0V5FIainfix =V4ainfix +V3c1FIainfix &lt;=agetV1V3agetV1V2Iainfix &lt;V3V0Aainfix &lt;=c0V3Iainfix &lt;V2V0Aainfix &lt;=c0V2INainfix =V3V2Iainfix &lt;=agetV1V6agetV1V3Oainfix &lt;=agetV1V6agetV1V2Iainfix &lt;V6V0Aainfix &lt;V2V6Oainfix &lt;V6V3Aainfix &lt;=c0V6FAainfix &lt;V2V0Aainfix &lt;=V3V2Aainfix &lt;=c0V3FIainfix &gt;V0c0Aainfix &lt;=c0V0F">
......@@ -155,7 +155,7 @@
locfile="../foveoos11_challenge1.mlw"
loclnum="13" loccnumb="6" loccnume="9"
expl="7. loop variant decrease"
sum="b1ea77998fa00afc9c9b6ced61f25e7b"
sum="4c41d575d22ce6a5a68c464ccba44325"
proved="true"
expanded="false"
shape="loop variant decreaseainfix &lt;ainfix -V2V4ainfix -V2V3Aainfix &lt;=c0ainfix -V2V3Iainfix =V4ainfix +V3c1FIainfix &lt;=agetV1V3agetV1V2Iainfix &lt;V3V0Aainfix &lt;=c0V3Iainfix &lt;V2V0Aainfix &lt;=c0V2INainfix =V3V2Iainfix &lt;=agetV1V5agetV1V3Oainfix &lt;=agetV1V5agetV1V2Iainfix &lt;V5V0Aainfix &lt;V2V5Oainfix &lt;V5V3Aainfix &lt;=c0V5FAainfix &lt;V2V0Aainfix &lt;=V3V2Aainfix &lt;=c0V3FIainfix &gt;V0c0Aainfix &lt;=c0V0F">
......@@ -175,7 +175,7 @@
locfile="../foveoos11_challenge1.mlw"
loclnum="13" loccnumb="6" loccnume="9"
expl="8. loop invariant preservation"
sum="2756b3ab55001c838e63a0635c0196aa"
sum="4ada797bf573120142940064cadf659a"
proved="true"
expanded="false"
shape="loop invariant preservationainfix &lt;V4V0Aainfix &lt;=V3V4Aainfix &lt;=c0V3Iainfix =V4ainfix -V2c1FINainfix &lt;=agetV1V3agetV1V2Iainfix &lt;V3V0Aainfix &lt;=c0V3Iainfix &lt;V2V0Aainfix &lt;=c0V2INainfix =V3V2Iainfix &lt;=agetV1V5agetV1V3Oainfix &lt;=agetV1V5agetV1V2Iainfix &lt;V5V0Aainfix &lt;V2V5Oainfix &lt;V5V3Aainfix &lt;=c0V5FAainfix &lt;V2V0Aainfix &lt;=V3V2Aainfix &lt;=c0V3FIainfix &gt;V0c0Aainfix &lt;=c0V0F">
......@@ -195,7 +195,7 @@
locfile="../foveoos11_challenge1.mlw"
loclnum="13" loccnumb="6" loccnume="9"
expl="9. loop invariant preservation"
sum="b3fdaf9058af028ff390c3256077a568"
sum="293c715c66579ee4e14681eccb12dbd4"
proved="true"
expanded="false"
shape="loop invariant preservationainfix &lt;=agetV1V5agetV1V3Oainfix &lt;=agetV1V5agetV1V4Iainfix &lt;V5V0Aainfix &lt;V4V5Oainfix &lt;V5V3Aainfix &lt;=c0V5FIainfix =V4ainfix -V2c1FINainfix &lt;=agetV1V3agetV1V2Iainfix &lt;V3V0Aainfix &lt;=c0V3Iainfix &lt;V2V0Aainfix &lt;=c0V2INainfix =V3V2Iainfix &lt;=agetV1V6agetV1V3Oainfix &lt;=agetV1V6agetV1V2Iainfix &lt;V6V0Aainfix &lt;V2V6Oainfix &lt;V6V3Aainfix &lt;=c0V6FAainfix &lt;V2V0Aainfix &lt;=V3V2Aainfix &lt;=c0V3FIainfix &gt;V0c0Aainfix &lt;=c0V0F">
......@@ -215,7 +215,7 @@
locfile="../foveoos11_challenge1.mlw"
loclnum="13" loccnumb="6" loccnume="9"
expl="10. loop variant decrease"
sum="bc7e63f5c2443b76078a4b4417280b4d"
sum="39563dd62bb1b37986e26830ebc24ef2"
proved="true"
expanded="false"
shape="loop variant decreaseainfix &lt;ainfix -V4V3ainfix -V2V3Aainfix &lt;=c0ainfix -V2V3Iainfix =V4ainfix -V2c1FINainfix &lt;=agetV1V3agetV1V2Iainfix &lt;V3V0Aainfix &lt;=c0V3Iainfix &lt;V2V0Aainfix &lt;=c0V2INainfix =V3V2Iainfix &lt;=agetV1V5agetV1V3Oainfix &lt;=agetV1V5agetV1V2Iainfix &lt;V5V0Aainfix &lt;V2V5Oainfix &lt;V5V3Aainfix &lt;=c0V5FAainfix &lt;V2V0Aainfix &lt;=V3V2Aainfix &lt;=c0V3FIainfix &gt;V0c0Aainfix &lt;=c0V0F">
......@@ -235,7 +235,7 @@
locfile="../foveoos11_challenge1.mlw"
loclnum="13" loccnumb="6" loccnume="9"
expl="11. postcondition"
sum="0dccfd9d5470bd3bb12b95c56a26d4c5"
sum="0f35a81f3e347a33e5b0ab721837bb41"
proved="true"
expanded="false"
shape="postconditionainfix &lt;V3V0Aainfix &lt;=c0V3INNainfix =V3V2Iainfix &lt;=agetV1V4agetV1V3Oainfix &lt;=agetV1V4agetV1V2Iainfix &lt;V4V0Aainfix &lt;V2V4Oainfix &lt;V4V3Aainfix &lt;=c0V4FAainfix &lt;V2V0Aainfix &lt;=V3V2Aainfix &lt;=c0V3FIainfix &gt;V0c0Aainfix &lt;=c0V0F">
......@@ -255,7 +255,7 @@
locfile="../foveoos11_challenge1.mlw"
loclnum="13" loccnumb="6" loccnume="9"
expl="12. postcondition"
sum="977b2c2cbdd17313155e9d3b3993700d"
sum="401ed7c87c7629cf02aa03e4a41df9bb"
proved="true"
expanded="false"
shape="postconditionainfix &lt;=agetV1V4agetV1V3Iainfix &lt;V4V0Aainfix &lt;=c0V4FINNainfix =V3V2Iainfix &lt;=agetV1V5agetV1V3Oainfix &lt;=agetV1V5agetV1V2Iainfix &lt;V5V0Aainfix &lt;V2V5Oainfix &lt;V5V3Aainfix &lt;=c0V5FAainfix &lt;V2V0Aainfix &lt;=V3V2Aainfix &lt;=c0V3FIainfix &gt;V0c0Aainfix &lt;=c0V0F">
......
This diff is collapsed.
......@@ -16,7 +16,7 @@
locfile="../hamming_sequence.mlw"
loclnum="23" loccnumb="6" loccnume="13"
expl="VC for hamming"
sum="46d148e56c25a6b60d4c8098f04baac6"
sum="93d02a39fe7690fc84c5f58851f53cc5"
proved="false"
expanded="true"
shape="ainfix =agetV8V9ahammingV9Iainfix &lt;V9V0Aainfix &lt;=c0V9FAainfix &lt;=c0V0Iainfix &gt;V3agetV8ainfix +V1c1Aainfix &gt;V5agetV8ainfix +V1c1Aainfix &gt;V7agetV8ainfix +V1c1Aainfix =V3ainfix *c5agetV8V2Aainfix =V5ainfix *c3agetV8V4Aainfix =V7ainfix *c2agetV8V6Aiiiainfix &gt;V18agetV12ainfix +V10c1Aainfix &gt;V16agetV12ainfix +V10c1Aainfix &gt;V14agetV12ainfix +V10c1Aainfix =V18ainfix *c5agetV12V17Aainfix =V16ainfix *c3agetV12V15Aainfix =V14ainfix *c2agetV12V13ainfix &lt;V19V0Aainfix &lt;=c0V19Iainfix =V19ainfix +V17c1Fainfix &lt;=V18V11Fainfix &lt;V20V0Aainfix &lt;=c0V20Iainfix =V20ainfix +V15c1Fainfix &lt;=V16V11Fainfix &lt;V21V0Aainfix &lt;=c0V21Iainfix =V21ainfix +V13c1Fainfix &lt;=V14V11FIainfix =V12asetV8V10V11Aainfix &lt;=c0V0FAainfix &lt;V10V0Aainfix &lt;=c0V10Aainfix &lt;=c0V0LaminV7aminV5V3Iainfix &gt;V3agetV8V10Aainfix &gt;V5agetV8V10Aainfix &gt;V7agetV8V10Aainfix =V3ainfix *c5agetV8V2Aainfix =V5ainfix *c3agetV8V4Aainfix =V7ainfix *c2agetV8V6Iainfix &lt;=V10V1Aainfix &lt;=c0V10FFAainfix &gt;c5agetaconstc0c0Aainfix &gt;c3agetaconstc0c0Aainfix &gt;c2agetaconstc0c0Aainfix =c5ainfix *c5agetaconstc0c0Aainfix =c3ainfix *c3agetaconstc0c0Aainfix =c2ainfix *c2agetaconstc0c0Iainfix &lt;=c0V1Aainfix =agetaconstc0V22ahammingV22Iainfix &lt;V22V0Aainfix &lt;=c0V22FIainfix &gt;c0V1Lainfix -V0c1Iainfix &lt;=c0V0Aainfix &gt;=V0c0Iainfix &gt;=V0c1F">
......
This diff is collapsed.
......@@ -34,7 +34,7 @@
name="Test1"
locfile="../formula.why"
loclnum="47" loccnumb="7" loccnume="12"
sum="45bf001b7ff4e3ad37645a0de72f1803"
sum="bb895b30ba659fcab00d3a6bc4a96a4a"
proved="true"
expanded="true"
shape="ainfix =aevalaForaFnotaFatomV0aFfalseV1aFalseLasetaconstaFalseV0aTrueLamk_identc0">
......@@ -60,7 +60,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.19"/>
<result status="valid" time="0.07"/>
</proof>
</goal>
</theory>
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -31,7 +31,7 @@
name="not_eqseq"
locfile="../lcp.mlw"
loclnum="18" loccnumb="8" loccnume="17"
sum="3b6fd254a3936f837aab00b2d6a49ee0"
sum="31f89860390353addc3ee725afbd6eec"
proved="true"
expanded="true"
shape="NaeqseqV0V1V2V4Iainfix &lt;V3V4FINainfix =amixfix []V0ainfix +V1V3amixfix []V0ainfix +V2V3Iainfix &lt;=c0V3F">
......@@ -49,7 +49,7 @@
locfile="../lcp.mlw"
loclnum="23" loccnumb="6" loccnume="9"
expl="VC for lcp"
sum="8cf118e7cf16541f0d2c17208ef711a9"
sum="f388dee8aa0d936513f63327837df147"
proved="true"
expanded="true"
shape="iNaeqseqV4V2V3V6Iainfix &lt;V5V6FAaeqseqV4V2V3V5iNaeqseqV4V2V3V7Iainfix &lt;V5V7FAaeqseqV4V2V3V5iNaeqseqV4V2V3V10Iainfix &lt;V5V10FAaeqseqV4V2V3V5ainfix &lt;ainfix -V0V11ainfix -V0V5Aainfix &lt;=c0ainfix -V0V5AaeqseqV4V2V3V11Iainfix =V11ainfix +V5c1Fainfix =agetV1V9agetV1V8Aainfix &lt;V9V0Aainfix &lt;=c0V9Lainfix +V2V5Aainfix &lt;V8V0Aainfix &lt;=c0V8Lainfix +V3V5ainfix &lt;ainfix +V3V5V0ainfix &lt;ainfix +V2V5V0IaeqseqV4V2V3V5FAaeqseqV4V2V3c0Iainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -64,7 +64,7 @@
locfile="../lcp.mlw"
loclnum="23" loccnumb="6" loccnume="9"
expl="1. loop invariant init"
sum="1a49b9afa3f6436f6eca1bc2f8613288"
sum="fb0205c203e8d4d72915b2ecca2ae6a8"
proved="true"
expanded="false"
shape="loop invariant initaeqseqV4V2V3c0Iainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -84,7 +84,7 @@
locfile="../lcp.mlw"
loclnum="23" loccnumb="6" loccnume="9"
expl="2. precondition"
sum="48bcaad9334b3214cd72a4fcf2e1f0e7"
sum="6d03b3136291a83764c310ce01f0314b"
proved="true"
expanded="false"
shape="preconditionainfix &lt;V6V0Aainfix &lt;=c0V6Lainfix +V3V5Iainfix &lt;ainfix +V3V5V0Iainfix &lt;ainfix +V2V5V0IaeqseqV4V2V3V5FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -104,7 +104,7 @@
locfile="../lcp.mlw"
loclnum="23" loccnumb="6" loccnume="9"
expl="3. precondition"
sum="c13105aebb2c1f193f79b15a6d91c871"
sum="befd1264d4ccf88dc8aa1d2cf223e1b8"
proved="true"
expanded="false"
shape="preconditionainfix &lt;V7V0Aainfix &lt;=c0V7Lainfix +V2V5Iainfix &lt;V6V0Aainfix &lt;=c0V6Lainfix +V3V5Iainfix &lt;ainfix +V3V5V0Iainfix &lt;ainfix +V2V5V0IaeqseqV4V2V3V5FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -124,7 +124,7 @@
locfile="../lcp.mlw"
loclnum="23" loccnumb="6" loccnume="9"
expl="4. loop invariant preservation"
sum="4da7079a41a489d808c6972c01ec8975"
sum="79ac59d247082109e360d7cce582e78a"
proved="true"
expanded="false"
shape="loop invariant preservationaeqseqV4V2V3V8Iainfix =V8ainfix +V5c1FIainfix =agetV1V7agetV1V6Iainfix &lt;V7V0Aainfix &lt;=c0V7Lainfix +V2V5Iainfix &lt;V6V0Aainfix &lt;=c0V6Lainfix +V3V5Iainfix &lt;ainfix +V3V5V0Iainfix &lt;ainfix +V2V5V0IaeqseqV4V2V3V5FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -144,7 +144,7 @@
locfile="../lcp.mlw"
loclnum="23" loccnumb="6" loccnume="9"
expl="5. loop variant decrease"
sum="d6fdcbd1a9dc2a47b7ba658c848203c0"
sum="82eee4ab969f84d3a69dfc97eb941770"
proved="true"
expanded="false"
shape="loop variant decreaseainfix &lt;ainfix -V0V8ainfix -V0V5Aainfix &lt;=c0ainfix -V0V5Iainfix =V8ainfix +V5c1FIainfix =agetV1V7agetV1V6Iainfix &lt;V7V0Aainfix &lt;=c0V7Lainfix +V2V5Iainfix &lt;V6V0Aainfix &lt;=c0V6Lainfix +V3V5Iainfix &lt;ainfix +V3V5V0Iainfix &lt;ainfix +V2V5V0IaeqseqV4V2V3V5FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -164,7 +164,7 @@
locfile="../lcp.mlw"
loclnum="23" loccnumb="6" loccnume="9"
expl="6. postcondition"
sum="d36407ec0b0f57625e78dcbb53174d84"
sum="98277fea2e5c43263bb8e99ea6e7c341"
proved="true"
expanded="false"
shape="postconditionaeqseqV4V2V3V5INainfix =agetV1V7agetV1V6Iainfix &lt;V7V0Aainfix &lt;=c0V7Lainfix +V2V5Iainfix &lt;V6V0Aainfix &lt;=c0V6Lainfix +V3V5Iainfix &lt;ainfix +V3V5V0Iainfix &lt;ainfix +V2V5V0IaeqseqV4V2V3V5FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -184,7 +184,7 @@
locfile="../lcp.mlw"
loclnum="23" loccnumb="6" loccnume="9"
expl="7. postcondition"
sum="1deba654860b4f8e46ff02f018d44636"
sum="f5f35b332b8250544f927a083f7242b1"
proved="true"
expanded="true"
shape="postconditionNaeqseqV4V2V3V8Iainfix &lt;V5V8FINainfix =agetV1V7agetV1V6Iainfix &lt;V7V0Aainfix &lt;=c0V7Lainfix +V2V5Iainfix &lt;V6V0Aainfix &lt;=c0V6Lainfix +V3V5Iainfix &lt;ainfix +V3V5V0Iainfix &lt;ainfix +V2V5V0IaeqseqV4V2V3V5FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -199,7 +199,7 @@
locfile="../lcp.mlw"
loclnum="23" loccnumb="6" loccnume="9"
expl="1. postcondition"
sum="4d5ce1ddc24e4884454aa2ef7a816ad1"
sum="7c6b9cf9121bb23f55cef9c119b199d4"
proved="true"
expanded="true"
shape="postconditionNainfix =amixfix []V4ainfix +V2V9amixfix []V4ainfix +V3V9Iainfix &lt;V9V8Aainfix &lt;=c0V9FAainfix &lt;=ainfix +V3V8alengthV4Aainfix &lt;=ainfix +V2V8alengthV4Aainfix &lt;=c0V8Iainfix &lt;V5V8FINainfix =agetV1V7agetV1V6Iainfix &lt;V7V0Aainfix =c0V7Oainfix &lt;c0V7Lainfix +V2V5Iainfix &lt;V6V0Aainfix =c0V6Oainfix &lt;c0V6Lainfix +V3V5Iainfix &lt;ainfix +V3V5V0Iainfix &lt;ainfix +V2V5V0Iainfix =amixfix []V4ainfix +V2V10amixfix []V4ainfix +V3V10Iainfix &lt;V10V5Aainfix &lt;=c0V10FAainfix &lt;=ainfix +V3V5alengthV4Aainfix &lt;=ainfix +V2V5alengthV4Aainfix &lt;=c0V5FIainfix &lt;V3V0Aainfix =c0V3Oainfix &lt;c0V3Aainfix &lt;V2V0Aainfix =c0V2Oainfix &lt;c0V2Aainfix =c0V0Oainfix &lt;c0V0Lamk arrayV0V1F">
......@@ -237,7 +237,7 @@
locfile="../lcp.mlw"
loclnum="23" loccnumb="6" loccnume="9"
expl="8. postcondition"
sum="e28ff42177f0a65635e9db4241d72ef8"
sum="3e6b26abdda924b4b360e647c36a3fe9"
proved="true"
expanded="false"
shape="postconditionaeqseqV4V2V3V5INainfix &lt;ainfix +V3V5V0Iainfix &lt;ainfix +V2V5V0IaeqseqV4V2V3V5FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -257,7 +257,7 @@
locfile="../lcp.mlw"
loclnum="23" loccnumb="6" loccnume="9"
expl="9. postcondition"
sum="9a9a9ac6a5044190cf7b6e53cb1ddbed"
sum="dd28b411499d6c2c7e2d313b5410482d"
proved="true"
expanded="false"
shape="postconditionNaeqseqV4V2V3V6Iainfix &lt;V5V6FINainfix &lt;ainfix +V3V5V0Iainfix &lt;ainfix +V2V5V0IaeqseqV4V2V3V5FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -277,7 +277,7 @@
locfile="../lcp.mlw"
loclnum="23" loccnumb="6" loccnume="9"
expl="10. postcondition"
sum="f089dacd456dc026a74bd92270d249c2"
sum="e543f04d026b949b6d7134d4738180d9"
proved="true"
expanded="false"
shape="postconditionaeqseqV4V2V3V5INainfix &lt;ainfix +V2V5V0IaeqseqV4V2V3V5FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;=c0V0Lamk arrayV0V1F">
......@@ -297,7 +297,7 @@
locfile="../lcp.mlw"
loclnum="23" loccnumb="6" loccnume="9"
expl="11. postcondition"
sum="f2289e8eedf7789ccbc3dd39b6727735"
sum="1dace31ecd42ec06d69560656f14f787"
proved="true"
expanded="false"
shape="postconditionNaeqseqV4V2V3V6Iainfix &lt;V5V6FINainfix &lt;ainfix +V2V5V0IaeqseqV4V2V3V5FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;=c0V0Lamk arrayV0V1F">
......
This diff is collapsed.
......@@ -46,11 +46,20 @@
</proof>
<proof
prover="3"
<<<<<<< Updated upstream
timelimit="60"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.09"/>
=======
timelimit="5"
memlimit="4000"
edited="my_cosine-CosineSingle-MethodError_1.tptp"
obsolete="false"
archived="false">
<result status="timeout" time="10.47"/>
>>>>>>> Stashed changes
</proof>
</goal>
<goal
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.