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

fix sessions (renaming of hypotheses cause of order change)

parent 6270a8fc
......@@ -14,9 +14,9 @@
<theory name="M1" proved="true">
<goal name="g" proved="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<transf name="cut" arg1="(0 +^ 0 = 2)">
<transf name="cut" arg1="(0 + 0 = 2)">
<goal name="g.0">
<transf name="cut" arg1="(1.0 + 1.3 = 2.2)">
<transf name="cut" arg1="(1.0 +^ 1.3 = 2.2)">
<goal name="g.0.0">
</goal>
<goal name="g.0.1">
......
......@@ -6,7 +6,7 @@
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../isqrt_von_neumann.mlw" proved="true">
<theory name="VonNeumann16" proved="true">
<goal name="sqr_add" proved="true">
......@@ -490,7 +490,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt64.39.0.0.0.1.0.0.0.1.1" proved="true">
<proof prover="4"><result status="valid" time="0.14" steps="241"/></proof>
<proof prover="4" timelimit="1"><result status="valid" time="0.14" steps="241"/></proof>
</goal>
</transf>
</goal>
......@@ -654,9 +654,9 @@
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter isqrt64.39.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.1.0.0.1.0.0.0.0.0.1" proved="true">
<transf name="rewrite" proved="true" arg1="h">
<transf name="rewrite" proved="true" arg1="h1">
<goal name="WP_parameter isqrt64.39.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.1.0.0.1.0.0.0.0.0.1.0" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="112"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="122"/></proof>
</goal>
</transf>
</goal>
......
......@@ -87,9 +87,9 @@
</transf>
<transf name="introduce_premises" proved="true" >
<goal name="inversion_mem_star_gen.0" proved="true">
<transf name="induction_arg_pr" proved="true" arg1="H2">
<transf name="induction_arg_pr" proved="true" arg1="H">
<goal name="inversion_mem_star_gen.0.0" proved="true">
<proof prover="5"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="inversion_mem_star_gen.0.1" proved="true">
<proof prover="5"><result status="valid" time="0.04"/></proof>
......@@ -98,16 +98,16 @@
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="inversion_mem_star_gen.0.3" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="inversion_mem_star_gen.0.4" proved="true">
<proof prover="5"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="inversion_mem_star_gen.0.5" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="inversion_mem_star_gen.0.6" proved="true">
<proof prover="5"><result status="valid" time="0.15"/></proof>
<proof prover="5"><result status="valid" time="0.10"/></proof>
</goal>
</transf>
</goal>
......@@ -201,7 +201,5 @@
</transf>
</goal>
</theory>
<theory name="DFA" proved="true">
</theory>
</file>
</why3session>
......@@ -2,6 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
......@@ -539,9 +540,9 @@
<goal name="permut_permutation.0.0" proved="true">
<transf name="destruct_alg" proved="true" arg1="a2">
<goal name="permut_permutation.0.0.0" proved="true">
<transf name="instantiate" proved="true" arg1="permut_exists" arg2="x1,x3">
<transf name="instantiate" proved="true" arg1="permut_exists" arg2="x2,x">
<goal name="permut_permutation.0.0.0.0" proved="true">
<proof prover="2"><result status="valid" time="0.04" steps="159"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="211"/></proof>
</goal>
</transf>
</goal>
......@@ -905,9 +906,9 @@
<goal name="WP_parameter lrs.26" expl="postcondition" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="WP_parameter lrs.26.0" expl="postcondition" proved="true">
<transf name="instantiate" proved="true" arg1="H15" arg2="x,y">
<transf name="instantiate" proved="true" arg1="H4" arg2="x,y">
<goal name="WP_parameter lrs.26.0.0" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="44"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="48"/></proof>
</goal>
</transf>
</goal>
......
......@@ -148,15 +148,15 @@
<goal name="WP_parameter pop.5.6" expl="VC for pop" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="WP_parameter pop.5.6.0" expl="VC for pop" proved="true">
<transf name="destruct" proved="true" arg1="H">
<transf name="destruct" proved="true" arg1="H11">
<goal name="WP_parameter pop.5.6.0.0" expl="VC for pop" proved="true">
<transf name="destruct" proved="true" arg1="H">
<transf name="destruct" proved="true" arg1="H11">
<goal name="WP_parameter pop.5.6.0.0.0" expl="VC for pop" proved="true">
<transf name="destruct" proved="true" arg1="H">
<transf name="destruct" proved="true" arg1="H11">
<goal name="WP_parameter pop.5.6.0.0.0.0" expl="VC for pop" proved="true">
<transf name="instantiate" proved="true" arg1="H" arg2="i+1">
<transf name="instantiate" proved="true" arg1="H11" arg2="i+1">
<goal name="WP_parameter pop.5.6.0.0.0.0.0" expl="VC for pop" proved="true">
<proof prover="5"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.04"/></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