Commit 87ecd4a0 authored by MARCHE Claude's avatar MARCHE Claude

FoVeOOS competition

parent c6e87211
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="duplets/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
<prover
id="coq"
name="Coq"
version="8.2pl1"/>
<prover
id="coq-realize"
name="Coq Realize"
version="8.2pl1"/>
<prover
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="eprover"
name="Eprover"
version="1.4 Namring"/>
<prover
id="gappa"
name="Gappa"
version="0.15.1"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
name="Spass"
version="3.7"/>
<prover
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="verit"
name="veriT"
version="dev"/>
<prover
id="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3"
name="Z3"
version="2.19"/>
<file
name="../duplets.mlw"
verified="true"
expanded="true">
<theory
name="Option"
verified="true"
expanded="true">
</theory>
<theory
name="WP Duplets"
verified="true"
expanded="true">
<goal
name="WP_parameter duplet"
expl="parameter duplet"
sum="509c3337d0e7364ff34fdb5503cee188"
proved="true"
expanded="true"
shape="Lamk arrayV0V2fAais_dupletV3V4V5NFIais_dupletV3V6V7NICV1aNonefaSomeVainfix =V8agetV2V6NIainfix <V7V0Aainfix <V6V7Aainfix <V6ainfix +ainfix -V0c2c1Aainfix <=c0V6FALagetV2V9iCV1aNonefaSomeVainfix =V11V10ais_dupletV3V12V13NICV1aNonefaSomeVainfix =V14agetV2V12NIainfix <V13V0Aainfix <V12V13Aainfix <V12ainfix +V9c1Aainfix <=c0V12Fais_dupletV3V15V16NICV1aNonefaSomeVainfix =V17agetV2V15NIainfix <V16V0Aainfix <V15V16Aainfix <V15ainfix +V9c1Aainfix <=c0V15FIais_dupletV3V9V18NIainfix <V18ainfix +ainfix -V0c1c1Aainfix <V9V18FAiainfix =agetV2V19V10CV1aNonefaSomeVainfix =V22agetV2V20NAais_dupletV3V20V21Iainfix =aTuple2V20V21aTuple2V9V19Fais_dupletV3V9V23NIainfix <V23ainfix +V19c1Aainfix <V9V23FAainfix <V19V0Aainfix <=c0V19Iais_dupletV3V9V24NIainfix <V24V19Aainfix <V9V24FIainfix <=V19ainfix -V0c1Aainfix <=ainfix +V9c1V19FAais_dupletV3V9V25NIainfix <V25ainfix +V9c1Aainfix <V9V25FIainfix <=ainfix +V9c1ainfix -V0c1Aais_dupletV3V26V27NICV1aNonefaSomeVainfix =V28agetV2V26NIainfix <V27V0Aainfix <V26V27Aainfix <V26ainfix +V9c1Aainfix <=c0V26FIainfix >ainfix +V9c1ainfix -V0c1Aainfix <V9V0Aainfix <=c0V9Iais_dupletV3V29V30NICV1aNonefaSomeVainfix =V31agetV2V29NIainfix <V30V0Aainfix <V29V30Aainfix <V29V9Aainfix <=c0V29FIainfix <=V9ainfix -V0c2Aainfix <=c0V9FAais_dupletV3V32V33NICV1aNonefaSomeVainfix =V34agetV2V32NIainfix <V33V0Aainfix <V32V33Aainfix <V32c0Aainfix <=c0V32FIainfix <=c0ainfix -V0c2AfAais_dupletV3V35V36NFIainfix >c0ainfix -V0c2ICV1aNonefaSomeVainfix =V39agetV2V37NAais_dupletV3V37V38EAainfix <=c2V0FFF">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.14"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.14"/>
</proof>
</goal>
<goal
name="WP_parameter duplets"
expl="parameter duplets"
sum="25edcda36324ea8e9b14810e5d5eb36c"
proved="true"
expanded="true"
shape="Lamk arrayV0V1ainfix =agetV1V3agetV1V5NAais_dupletV2V5V6Aais_dupletV2V3V4Iainfix =agetV1V4agetV1V5NAais_dupletV2V5V6FAainfix =agetV1V4agetV1V7NAais_dupletV2V7V8EAainfix <=c2V0Aainfix <V4V0Aainfix <=c0V4Iais_dupletV2V3V4FAais_dupletV2V9V10EAainfix <=c2V0Iainfix =agetV1V11agetV1V13NAais_dupletV2V13V14Aais_dupletV2V11V12EAainfix <=c4V0FF">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.06"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.05"/>
</proof>
</goal>
</theory>
</file>
</why3session>
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