Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit f09527ac authored by MARCHE Claude's avatar MARCHE Claude

update broken sessions

parent 9cdac097
......@@ -4,6 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../vstte12_combinators.mlw" proved="true">
<theory name="Combinators" proved="true">
<goal name="VC eq" expl="VC for eq" proved="true">
......@@ -94,31 +95,31 @@
<goal name="VC value_in_context.1" expl="precondition" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="VC value_in_context.1.0" expl="precondition" proved="true">
<transf name="destruct_alg" proved="true" arg1="(subst c t)">
<transf name="destruct_alg_subst" proved="true" arg1="(subst c t)">
<goal name="VC value_in_context.1.0.0" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC value_in_context.1.0.1" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC value_in_context.1.0.2" expl="precondition" proved="true">
<transf name="destruct_alg" proved="true" arg1="x">
<transf name="destruct_alg_subst" proved="true" arg1="x3">
<goal name="VC value_in_context.1.0.2.0" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="34"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC value_in_context.1.0.2.1" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="34"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC value_in_context.1.0.2.2" expl="precondition" proved="true">
<transf name="destruct_alg" proved="true" arg1="x">
<transf name="destruct_alg_subst" proved="true" arg1="x4">
<goal name="VC value_in_context.1.0.2.2.0" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="46"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC value_in_context.1.0.2.2.1" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="38"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC value_in_context.1.0.2.2.2" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="62"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
......@@ -134,31 +135,31 @@
<goal name="VC value_in_context.3" expl="precondition" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="VC value_in_context.3.0" expl="precondition" proved="true">
<transf name="destruct_alg" proved="true" arg1="(subst c t)">
<transf name="destruct_alg_subst" proved="true" arg1="(subst c t)">
<goal name="VC value_in_context.3.0.0" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="24"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC value_in_context.3.0.1" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC value_in_context.3.0.2" expl="precondition" proved="true">
<transf name="destruct_alg" proved="true" arg1="x">
<transf name="destruct_alg_subst" proved="true" arg1="x3">
<goal name="VC value_in_context.3.0.2.0" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="34"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC value_in_context.3.0.2.1" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="34"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC value_in_context.3.0.2.2" expl="precondition" proved="true">
<transf name="destruct_alg" proved="true" arg1="x">
<transf name="destruct_alg_subst" proved="true" arg1="x4">
<goal name="VC value_in_context.3.0.2.2.0" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="46"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC value_in_context.3.0.2.2.1" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="38"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC value_in_context.3.0.2.2.2" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="62"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></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