Commit 836d876d authored by MARCHE Claude's avatar MARCHE Claude

fixed session for example Defunctionalization

parent 8d5de50b
......@@ -101,20 +101,18 @@
<proof
prover="0"
timelimit="5"
memlimit="4000"
edited="defunctionalization-DirectSem-eval_p3_1.why"
memlimit="1000"
obsolete="false"
archived="false">
<unedited/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="4000"
edited="defunctionalization-DirectSem-eval_p3_1.cvc"
memlimit="1000"
obsolete="false"
archived="false">
<unedited/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
......@@ -267,19 +265,19 @@
locfile="../defunctionalization.mlw"
loclnum="174" loccnumb="7" loccnume="26"
verified="true"
expanded="true">
expanded="false">
<goal
name="size_e_pos"
locfile="../defunctionalization.mlw"
loclnum="234" loccnumb="6" loccnume="16"
sum="eb5aa07168e469462f178125a5205dd8"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &gt;=asize_eV0c1F">
<transf
name="induction_ty_lex"
proved="true"
expanded="true">
expanded="false">
<goal
name="size_e_pos.1"
locfile="../defunctionalization.mlw"
......@@ -306,12 +304,12 @@
loclnum="243" loccnumb="6" loccnume="16"
sum="0e40c13aeafcdafe4170165169a51e89"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &gt;=asize_cV0c0F">
<transf
name="induction_ty_lex"
proved="true"
expanded="true">
expanded="false">
<goal
name="size_c_pos.1"
locfile="../defunctionalization.mlw"
......@@ -347,10 +345,9 @@
prover="0"
timelimit="5"
memlimit="1000"
edited="defunctionalization-Defunctionalization-WP_parameter_continue_2_1.why"
obsolete="false"
archived="false">
<unedited/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
......@@ -408,18 +405,9 @@
prover="1"
timelimit="5"
memlimit="1000"
edited="defunctionalization-Defunctionalization-WP_parameter_eval_2_1.cvc"
obsolete="false"
archived="false">
<unedited/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="4000"
obsolete="true"
archived="false">
<result status="timeout" time="4.99"/>
<result status="valid" time="0.05"/>
</proof>
<proof
prover="3"
......@@ -1161,19 +1149,19 @@
locfile="../defunctionalization.mlw"
loclnum="396" loccnumb="7" loccnume="19"
verified="true"
expanded="true">
expanded="false">
<goal
name="cps_correct_expr"
locfile="../defunctionalization.mlw"
loclnum="506" loccnumb="6" loccnume="22"
sum="cd46625f4a0c7a07bccf1bdfef1148e9"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =aeval_1V0V1ainfix @V1aeval_0V0FF">
<transf
name="induction_ty_lex"
proved="true"
expanded="true">
expanded="false">
<goal
name="cps_correct_expr.1"
locfile="../defunctionalization.mlw"
......@@ -1181,12 +1169,12 @@
expl="1."
sum="7518f6839f5abe78c9431c97b9706aeb"
proved="true"
expanded="true"
expanded="false"
shape="Cainfix =aeval_1V0V2ainfix @V2aeval_0V0FaCteVainfix =aeval_1V0V5ainfix @V5aeval_0V0FIainfix =aeval_1V3V6ainfix @V6aeval_0V3FIainfix =aeval_1V4V7ainfix @V7aeval_0V4FaSubVVV0F">
<transf
name="split_goal_wp"
proved="true"
expanded="true">
expanded="false">
<goal
name="cps_correct_expr.1.1"
locfile="../defunctionalization.mlw"
......@@ -1194,7 +1182,7 @@
expl="1."
sum="b6ef6589d20ca6cb06d93aef6e35ad31"
proved="true"
expanded="true"
expanded="false"
shape="Cainfix =aeval_1V0V2ainfix @V2aeval_0V0FaCteVtaSubVVV0F">
<proof
prover="0"
......@@ -1212,7 +1200,7 @@
expl="2."
sum="6c47e9bbe56b5ece0a62d228d6d88753"
proved="true"
expanded="true"
expanded="false"
shape="CtaCteVainfix =aeval_1V0V4ainfix @V4aeval_0V0FIainfix =aeval_1V2V5ainfix @V5aeval_0V2FIainfix =aeval_1V3V6ainfix @V6aeval_0V3FaSubVVV0F">
<proof
prover="4"
......@@ -1711,12 +1699,12 @@
loclnum="681" loccnumb="6" loccnume="16"
sum="5722d833d5d515a9f3dbcdb1f4b48814"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &gt;=asize_eV0c1F">
<transf
name="induction_ty_lex"
proved="true"
expanded="true">
expanded="false">
<goal
name="size_e_pos.1"
locfile="../defunctionalization.mlw"
......@@ -1743,12 +1731,12 @@
loclnum="692" loccnumb="6" loccnume="16"
sum="266dda67235b12b1fb5906e86caa3b62"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &gt;=asize_cV0c0F">
<transf
name="induction_ty_lex"
proved="true"
expanded="true">
expanded="false">
<goal
name="size_c_pos.1"
locfile="../defunctionalization.mlw"
......@@ -2296,7 +2284,7 @@
locfile="../defunctionalization.mlw"
loclnum="736" loccnumb="7" loccnume="25"
verified="true"
expanded="true">
expanded="false">
<goal
name="WP_parameter contract"
locfile="../defunctionalization.mlw"
......@@ -2393,12 +2381,12 @@
loclnum="905" loccnumb="6" loccnume="16"
sum="e5d26dcb7d5322646a9dc2fc1ef82380"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &gt;=asize_cV0c0F">
<transf
name="induction_ty_lex"
proved="true"
expanded="true">
expanded="false">
<goal
name="size_c_pos.1"
locfile="../defunctionalization.mlw"
......@@ -3066,19 +3054,19 @@
locfile="../defunctionalization.mlw"
loclnum="1084" loccnumb="7" loccnume="17"
verified="true"
expanded="true">
expanded="false">
<goal
name="size_c_pos"
locfile="../defunctionalization.mlw"
loclnum="1120" loccnumb="6" loccnume="16"
sum="b80c92891c5101a180df7bf9222d4878"
proved="true"
expanded="true"
expanded="false"
shape="ainfix &gt;=asize_cV0c0F">
<transf
name="induction_ty_lex"
proved="true"
expanded="true">
expanded="false">
<goal
name="size_c_pos.1"
locfile="../defunctionalization.mlw"
......
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