ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity

updated sessions

Browse Source
This commit is contained in:
Claude Marche
2015-10-19 16:05:58 +02:00
parent a8cfacb551
commit a120c27e27
91 changed files with 499 additions and 507 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
examples/decrease1/why3session.xml
View File

@@ -3,8 +3,8 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.2" timelimit="5" memlimit="1000"/>
<prover id="1" name="Coq" version="8.4pl4" timelimit="10" memlimit="0"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="3" name="Coq" version="8.4pl6" timelimit="10" memlimit="0"/>
<prover id="4" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
<prover id="5" name="CVC3" version="2.2" timelimit="10" memlimit="0"/>
<prover id="6" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
@@ -13,7 +13,7 @@
<file name="../decrease1.mlw" expanded="true">
<theory name="Decrease1" sum="7c49cfeea622335075ec3d6212620b2b" expanded="true">
<goal name="decrease1_induction" expanded="true">
<proof prover="1" edited="decrease1_Decrease1_decrease1_induction_2.v"><result status="valid" time="1.10"/></proof>
<proof prover="3" edited="decrease1_Decrease1_decrease1_induction_2.v"><result status="valid" time="1.10"/></proof>
</goal>
<goal name="WP_parameter search" expl="VC for search" expanded="true">
<transf name="split_goal_wp" expanded="true">