Le registre Docker de Gitlab est désormais activé. Pour l'utiliser dans vos projets : Settings -> General -> Permissions -> Container registry. L'équipe transversale GitLab (SED/SESI/SEISM).

Commit 4d31cd3d by Andrei Paskevich

update some sessions

parent c0df9356
Pipeline #23065 passed with stages
in 14 minutes 11 seconds
......@@ -4,13 +4,14 @@
<why3session shape_version="4">
<prover id="0" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../mccarthy_vc_sp.mlw" proved="true">
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../mccarthy_vc_sp.mlw">
<theory name="McCarthy91" proved="true">
<goal name="VC f91" expl="VC for f91" proved="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC f91_nonrec" expl="VC for f91_nonrec" proved="true">
<proof prover="1"><result status="valid" time="0.21"/></proof>
<proof prover="2"><result status="valid" time="0.27" steps="532"/></proof>
</goal>
<goal name="VC f91_pseudorec" expl="VC for f91_pseudorec" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
......
......@@ -165,9 +165,9 @@ let () = Trans.register_transform
(Trans.decl eliminate_exists None)
~desc:"Replace axioms of the form 'exists x. P' by 'constant x axiom P'."
let simplify_intros =
Trans.compose Simplify_formula.simplify_trivial_wp_quantification introduce_premises
Trans.compose Simplify_formula.simplify_trivial_wp_quantification
introduce_premises
let split_intros_goal_wp =
Trans.compose_l Split_goal.split_goal_right (Trans.singleton simplify_intros)
......@@ -180,7 +180,10 @@ let split_intros_premise_wp =
let () = Trans.register_transform_l
"split_intros_goal_wp" split_intros_goal_wp
~desc:"The@ recommended@ splitting@ transformation@ to@ apply@ on@ VCs@ generated@ by@ WP@ (split_goal_right@ followed@ by@ simplify_trivial_quantifications@ followed@ by@ introduce_premises)."
~desc:"The@ recommended@ splitting@ transformation@ to@ apply@ \
on@ VCs@ generated@ by@ WP@ (split_goal_right@ followed@ \
by@ simplify_trivial_quantifications@ followed@ by@ \
introduce_premises)."
let () = Trans.register_transform_l
"split_intros_all_wp" split_intros_all_wp
......
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