Skip to content
Snippets Groups Projects
Select Git revision
  • e6809fcc81da8feb7cfdf5d9271e691aff92e1fe
  • master default protected
2 results

why3session.xml.bak

Blame
  • why3session.xml.bak 10.08 KiB
    <?xml version="1.0" encoding="UTF-8"?>
    <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
    "http://why3.lri.fr/why3session.dtd">
    <why3session shape_version="5">
    <prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
    <prover id="1" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
    <file name="../state.mlw" proved="true">
    <theory name="State" proved="true">
     <goal name="VC get" expl="VC for get" proved="true">
     <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
     </goal>
     <goal name="VC set" expl="VC for set" proved="true">
     <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
     </goal>
     <goal name="VC mixfix []" expl="VC for mixfix []" proved="true">
     <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
     </goal>
     <goal name="VC mixfix [&lt;-]" expl="VC for mixfix [<-]" proved="true">
     <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
     </goal>
     <goal name="VC const" expl="VC for const" proved="true">
     <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
     </goal>
    </theory>
    <theory name="Reg" proved="true">
     <goal name="VC read" expl="VC for read" proved="true">
     <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
     </goal>
     <goal name="VC write" expl="VC for write" proved="true">
     <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
     </goal>
     <goal name="VC const" expl="VC for const" proved="true">
     <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
     </goal>
    </theory>
    </file>
    <file name="../imp_test.mlw">
    <theory name="Imp_test">
     <goal name="ex1" proved="true">
     <proof prover="0"><result status="valid" time="0.02" steps="82"/></proof>
     </goal>
     <goal name="ex2" proved="true">
     <proof prover="0"><result status="valid" time="0.03" steps="101"/></proof>
     </goal>
     <goal name="ex3" proved="true">
     <proof prover="0"><result status="valid" time="0.02" steps="97"/></proof>
     <proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
     </goal>
     <goal name="ex4">
     <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="97"/></proof>
     </goal>
     <goal name="ex5">
     <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="97"/></proof>
     </goal>
     <goal name="ex6">
     <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="74"/></proof>
     </goal>
     <goal name="ex7">
     <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="84"/></proof>
     </goal>
     <goal name="ex8">
     <proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="100"/></proof>
     </goal>
    </theory>
    </file>
    <file name="../imp_ex_assignment.mlw">
    <theory name="Imp_ex">
     <goal name="VC aeval_ex" expl="VC for aeval_ex" proved="true">
     <proof prover="0"><result status="valid" time="0.68" steps="783"/></proof>
     </goal>
     <goal name="VC beval_ex" expl="VC for beval_ex" proved="true">
     <proof prover="0"><result status="valid" time="0.20" steps="667"/></proof>
     </goal>
     <goal name="VC ceval_ex" expl="VC for ceval_ex">
     <transf name="split_vc" >
      <goal name="VC ceval_ex.0" expl="postcondition" proved="true">
      <proof prover="0"><result status="valid" time="0.02" steps="74"/></proof>
      </goal>
      <goal name="VC ceval_ex.1" expl="postcondition">
      <proof prover="0"><result status="timeout" time="1.00"/></proof>
      </goal>
      <goal name="VC ceval_ex.2" expl="postcondition">
      <proof prover="0"><result status="timeout" time="1.00"/></proof>
      </goal>
      <goal name="VC ceval_ex.3" expl="postcondition">
      <proof prover="0"><result status="timeout" time="1.00"/></proof>
      </goal>
      <goal name="VC ceval_ex.4" expl="postcondition">
      <proof prover="0"><result status="timeout" time="1.00"/></proof>
      </goal>
     </transf>
     </goal>
    </theory>
    </file>
    <file name="../imp_ex.mlw" proved="true">
    <theory name="Imp_Ex" proved="true">
     <goal name="VC aeval_ex" expl="VC for aeval_ex" proved="true">
     <proof prover="0"><result status="valid" time="0.52" steps="783"/></proof>
     </goal>
     <goal name="VC beval_ex" expl="VC for beval_ex" proved="true">
     <proof prover="0"><result status="valid" time="0.22" steps="667"/></proof>
     </goal>
     <goal name="VC ceval_ex" expl="VC for ceval_ex" proved="true">
     <proof prover="0"><result status="valid" time="0.08" steps="237"/></proof>
     </goal>
    </theory>
    </file>
    <file name="../imp.mlw" proved="true">
    <theory name="Imp" proved="true">
     <goal name="ceval_deterministic_aux" proved="true">
     <transf name="induction_pr" proved="true" >
      <goal name="ceval_deterministic_aux.0" proved="true">
      <proof prover="0"><result status="valid" time="0.05" steps="135"/></proof>
      </goal>
      <goal name="ceval_deterministic_aux.1" proved="true">
      <proof prover="0"><result status="valid" time="0.08" steps="180"/></proof>
      </goal>
      <goal name="ceval_deterministic_aux.2" proved="true">
      <transf name="induction_pr" proved="true" >
       <goal name="ceval_deterministic_aux.2.0" proved="true">
       <proof prover="0"><result status="valid" time="0.02" steps="84"/></proof>
       </goal>
       <goal name="ceval_deterministic_aux.2.1" proved="true">
       <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
       </goal>
       <goal name="ceval_deterministic_aux.2.2" proved="true">
       <proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
       <proof prover="1"><result status="valid" time="0.11"/></proof>
       </goal>
       <goal name="ceval_deterministic_aux.2.3" proved="true">
       <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
       </goal>
       <goal name="ceval_deterministic_aux.2.4" proved="true">
       <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
       </goal>
       <goal name="ceval_deterministic_aux.2.5" proved="true">
       <proof prover="0"><result status="valid" time="0.02" steps="85"/></proof>
       </goal>
       <goal name="ceval_deterministic_aux.2.6" proved="true">
       <proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
       </goal>
      </transf>
      </goal>
      <goal name="ceval_deterministic_aux.3" proved="true">
      <transf name="induction_pr" proved="true" >
       <goal name="ceval_deterministic_aux.3.0" proved="true">
       <proof prover="0"><result status="valid" time="0.02" steps="84"/></proof>
       </goal>
       <goal name="ceval_deterministic_aux.3.1" proved="true">
       <proof prover="0"><result status="valid" time="0.02" steps="86"/></proof>
       </goal>
       <goal name="ceval_deterministic_aux.3.2" proved="true">
       <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
       </goal>
       <goal name="ceval_deterministic_aux.3.3" proved="true">
       <proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
       <proof prover="1"><result status="valid" time="0.06"/></proof>
       </goal>
       <goal name="ceval_deterministic_aux.3.4" proved="true">
       <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
       </goal>
       <goal name="ceval_deterministic_aux.3.5" proved="true">
       <proof prover="0"><result status="valid" time="0.03" steps="85"/></proof>
       </goal>
       <goal name="ceval_deterministic_aux.3.6" proved="true">
       <proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
       </goal>
      </transf>
      </goal>
      <goal name="ceval_deterministic_aux.4" proved="true">
      <transf name="induction_pr" proved="true" >
       <goal name="ceval_deterministic_aux.4.0" proved="true">
       <proof prover="0"><result status="valid" time="0.02" steps="84"/></proof>
       </goal>
       <goal name="ceval_deterministic_aux.4.1" proved="true">
       <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
       </goal>
       <goal name="ceval_deterministic_aux.4.2" proved="true">
       <proof prover="0"><result status="valid" time="0.02" steps="86"/></proof>
       </goal>
       <goal name="ceval_deterministic_aux.4.3" proved="true">
       <proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
       </goal>
       <goal name="ceval_deterministic_aux.4.4" proved="true">
       <proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
       <proof prover="1"><result status="valid" time="0.06"/></proof>
       </goal>
       <goal name="ceval_deterministic_aux.4.5" proved="true">
       <proof prover="0"><result status="valid" time="0.02" steps="85"/></proof>
       </goal>
       <goal name="ceval_deterministic_aux.4.6" proved="true">
       <proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
       </goal>
      </transf>
      </goal>
      <goal name="ceval_deterministic_aux.5" proved="true">
      <proof prover="0"><result status="valid" time="0.05" steps="133"/></proof>
      </goal>
      <goal name="ceval_deterministic_aux.6" proved="true">
      <transf name="induction_pr" proved="true" >
       <goal name="ceval_deterministic_aux.6.0" proved="true">
       <proof prover="0"><result status="valid" time="0.02" steps="85"/></proof>
       </goal>
       <goal name="ceval_deterministic_aux.6.1" proved="true">
       <proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
       </goal>
       <goal name="ceval_deterministic_aux.6.2" proved="true">
       <proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
       </goal>
       <goal name="ceval_deterministic_aux.6.3" proved="true">
       <proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
       </goal>
       <goal name="ceval_deterministic_aux.6.4" proved="true">
       <proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
       </goal>
       <goal name="ceval_deterministic_aux.6.5" proved="true">
       <proof prover="0"><result status="valid" time="0.02" steps="86"/></proof>
       </goal>
       <goal name="ceval_deterministic_aux.6.6" proved="true">
       <proof prover="0" obsolete="true"><result status="timeout" time="1.00"/></proof>
       <proof prover="1"><result status="valid" time="0.11"/></proof>
       </goal>
      </transf>
      </goal>
     </transf>
     </goal>
     <goal name="ceval_deterministic" proved="true">
     <proof prover="0"><result status="valid" time="0.03" steps="107"/></proof>
     </goal>
     <goal name="VC beval">
     <proof prover="0"><result status="valid" time="0.02" steps="73"/></proof>
     </goal>
     <goal name="VC aeval">
     <proof prover="0"><result status="valid" time="0.01" steps="73"/></proof>
     </goal>
    </theory>
    </file>
    </why3session>