From b48534a48c4da8f940a08bc8a0fce42d73aa3d4c Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr> Date: Wed, 23 May 2018 17:09:36 +0200 Subject: [PATCH] vstte12_tree_reconstruction: updated proof on moloch --- examples/vstte12_tree_reconstruction/why3session.xml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/examples/vstte12_tree_reconstruction/why3session.xml b/examples/vstte12_tree_reconstruction/why3session.xml index 21a158be0c..1ff6578dab 100644 --- a/examples/vstte12_tree_reconstruction/why3session.xml +++ b/examples/vstte12_tree_reconstruction/why3session.xml @@ -8,7 +8,7 @@ <prover id="5" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="7" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="8" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/> -<file name="../vstte12_tree_reconstruction.mlw"> +<file name="../vstte12_tree_reconstruction.mlw" proved="true"> <theory name="Tree" proved="true"> <goal name="VC depths" expl="VC for depths" proved="true"> <transf name="split_goal_right" proved="true" > @@ -94,7 +94,7 @@ <proof prover="4" timelimit="1"><result status="valid" time="0.56"/></proof> </goal> </theory> -<theory name="ZipperBased"> +<theory name="ZipperBased" proved="true"> <goal name="forest_depths_append" proved="true"> <proof prover="5" timelimit="10" memlimit="0" edited="vstte12_tree_reconstruction_WP_ZipperBased_forest_depths_append_1.v"><result status="valid" time="0.30"/></proof> </goal> @@ -127,10 +127,10 @@ </transf> </goal> <goal name="key_lemma" proved="true"> - <proof prover="1" edited="vstte12_tree_reconstruction_ZipperBased_key_lemma_2.v"><result status="valid" time="2.27"/></proof> + <proof prover="5" edited="vstte12_tree_reconstruction_ZipperBased_key_lemma_2.v"><result status="valid" time="2.27"/></proof> </goal> - <goal name="right_nil"> - <proof prover="5" timelimit="29" memlimit="0" obsolete="true" edited="vstte12_tree_reconstruction_WP_ZipperBased_right_nil_1.v"><result status="valid" time="3.14"/></proof> + <goal name="right_nil" proved="true"> + <proof prover="5" timelimit="29" memlimit="0" edited="vstte12_tree_reconstruction_WP_ZipperBased_right_nil_1.v"><result status="valid" time="1.54"/></proof> </goal> <goal name="main_lemma" proved="true"> <proof prover="4" timelimit="1"><result status="valid" time="0.07"/></proof> -- GitLab