Skip to content

GitLab

why3
why3
Commit 9eb8c83c authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

make some session files up-to-date

parent 5fc52562
Hide whitespace changes
Inline Side-by-side
Showing with 503 additions and 439 deletions
examples/check-builtin/ac/why3session.xml
View file @ 9eb8c83c
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/check-builtin/ac/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<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="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../ac.why" verified="true" expanded="true">
<theory name="Test" verified="true" expanded="true">
<goal name="G1" sum="bb6db914adb3909c925fcf44bf71f57d" proved="true" expanded="true">
<goal name="G1" sum="fa87ff4f5d7bfd19a59c9e156ce503b1" proved="true" expanded="true" shape="ainfix =afV0V1afV1V0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -14,10 +23,10 @@
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="G2" sum="0ea5f5c71116d14a913f0b8472566d9d" proved="true" expanded="true">
<goal name="G2" sum="596822f280e706913494c5aafa0c406d" proved="true" expanded="true" shape="ainfix =afafV0V1V2afV0afV1V2F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -28,7 +37,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
......
examples/check-builtin/array/why3session.xml
View file @ 9eb8c83c
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/check-builtin/array/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<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="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../array.why" verified="true" expanded="true">
<theory name="Test_simplify_array" verified="true" expanded="true">
<goal name="G1" sum="6ba9acd1575b0f736753d499a8efa246" proved="true" expanded="true">
<goal name="G1" sum="4b1f56125aaf6794df037dfd2cbfea62" proved="true" expanded="true" shape="ainfix =agetasetV2V1V0V1V0FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="G2" sum="ba915c2a50e7cb9f66307625030ee440" proved="true" expanded="true">
<goal name="G2" sum="dc80f74d142de8dda00f0aef8deca6c0" proved="true" expanded="true" shape="ainfix =agetasetV5V0V4V3V1Iainfix =agetV5V3V1Iainfix =V3V0NFF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -25,27 +34,27 @@
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="G3" sum="b23fa0a82a81a38100f4990bc5abb06e" proved="true" expanded="true">
<goal name="G3" sum="4aea5336be3a1feb8cf653e610e1d89a" proved="true" expanded="true" shape="ainfix =agetasetV2c1V1c0V0Iainfix =agetV2c0V0FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.26"/>
<result status="valid" time="0.15"/>
</proof>
</goal>
<goal name="G4" sum="d3736da01102cfb2b3afd57824a993b6" proved="true" expanded="true">
<goal name="G4" sum="5751bd67cfa24e03534046070269e911" proved="true" expanded="true" shape="ainfix =agetasetasetV2c1V1c0V0c1V1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -56,7 +65,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.33"/>
<result status="valid" time="0.19"/>
</proof>
</goal>
</theory>
......
examples/check-builtin/bool/why3session.xml
View file @ 9eb8c83c
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/check-builtin/bool/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<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="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../bool.why" verified="true" expanded="true">
<theory name="Test" verified="true" expanded="true">
<goal name="G1" sum="7a4b1e7f9f3ee4396d85e1a8843f6c12" proved="true" expanded="true">
<goal name="G1" sum="5e6719215b28357019f9093ba80a13ae" proved="true" expanded="true" shape="ainfix =aTrueaFalseN">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -11,27 +20,27 @@
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="G2" sum="20e7efb7a2beea23a901d014d3170906" proved="true" expanded="true">
<goal name="G2" sum="c7425a171e64e10c6cdebdcf3addcadc" proved="true" expanded="true" shape="ainfix =V0aFalseOainfix =V0aTrueF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="G3" sum="2b68363a02d3c401d7a5e6cdbe821586" proved="true" expanded="true">
<goal name="G3" sum="f575ede69f52b10d8bfe591848ea3934" proved="true" expanded="true" shape="fIainfix =V2V0NAainfix =V1V2NAainfix =V0V1NF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -39,10 +48,10 @@
<result status="unknown" time="0.00"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
......
examples/check-builtin/euclideandivision/why3session.xml
View file @ 9eb8c83c
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/check-builtin/euclideandivision/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<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="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../euclideandivision.why" verified="true" expanded="true">
<theory name="Test" verified="true" expanded="true">
<goal name="G1" sum="ea3bac3defe8dd6c6d07e6bb9584018e" proved="true" expanded="true">
<goal name="G1" sum="fa1bf8929f550cd0d7bc90f8ce7be2eb" proved="true" expanded="true" shape="ainfix =amodc10c3c1">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.01"/>
<result status="timeout" time="10.00"/>
</proof>
</goal>
<goal name="G2" sum="dcd09929b230a018d26799f2df130ea7" proved="true" expanded="true">
<goal name="G2" sum="5800907ef13d303adf6e30c1b01a9dae" proved="true" expanded="true" shape="ainfix =adivc10c3c3">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.06"/>
<result status="timeout" time="9.99"/>
</proof>
</goal>
</theory>
......
examples/check-builtin/int/why3session.xml
View file @ 9eb8c83c
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/check-builtin/int/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<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="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../int.why" verified="true" expanded="true">
<theory name="Test" verified="true" expanded="true">
<goal name="G1" sum="98b174d6537c40a661dc0b7d6f3e520b" proved="true" expanded="true">
<goal name="G1" sum="d5111159f39ad797db77ad7e2d80a226" proved="true" expanded="true" shape="ainfix =ainfix *c5c10c50">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -14,10 +23,10 @@
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.05"/>
<result status="timeout" time="10.03"/>
</proof>
</goal>
<goal name="G2" sum="175866f81a3b591fe7df5ff8ff1ef55b" proved="true" expanded="true">
<goal name="G2" sum="8dc6e7f38fd1fb7946a1212c89ba402d" proved="true" expanded="true" shape="ainfix =ainfix +ainfix -ainfix +V0V0V0V0ainfix *c2V0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -28,124 +37,124 @@
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="9.86"/>
<result status="timeout" time="10.08"/>
</proof>
</goal>
<goal name="CompatOrderAdd" sum="02c33f1f120f2b572184ff1c06167612" proved="true" expanded="true">
<goal name="CompatOrderAdd" sum="9385e56939c8dc201584ea4f3d9bc4af" proved="true" expanded="true" shape="ainfix <=ainfix +V0V2ainfix +V1V2Iainfix <=V0V1F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="CompatOrderMult" sum="2e444ab191874072ca95793d2879fedc" proved="true" expanded="true">
<goal name="CompatOrderMult" sum="b98fa9a55f2216428fda1a415944f990" proved="true" expanded="true" shape="ainfix <=ainfix *V0V2ainfix *V1V2Iainfix <=c0V2Iainfix <=V0V1F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="InvMult" sum="4907a61fa41e315f3b1560b2b81da1c7" proved="true" expanded="true">
<goal name="InvMult" sum="1bfe3b11addac18ebecd101596d63095" proved="true" expanded="true" shape="ainfix =aprefix -ainfix *V0V1ainfix *V0aprefix -V1Aainfix =ainfix *aprefix -V0V1aprefix -ainfix *V0V1F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.13"/>
<result status="timeout" time="9.99"/>
</proof>
</goal>
<goal name="InvSquare" sum="6d651319668b874df6ffff5949ff351a" proved="true" expanded="true">
<goal name="InvSquare" sum="1b594a6b60e183e594b00faf939fcc3f" proved="true" expanded="true" shape="ainfix =ainfix *V0V0ainfix *aprefix -V0aprefix -V0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.00"/>
<result status="timeout" time="10.03"/>
</proof>
</goal>
<goal name="ZeroMult" sum="03cb0ff22ce434d243461722498d91be" proved="true" expanded="true">
<goal name="ZeroMult" sum="27316fd57c9735adb22695569bcb11a0" proved="true" expanded="true" shape="ainfix =c0ainfix *c0V0Aainfix =ainfix *V0c0c0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.05"/>
<result status="timeout" time="10.04"/>
</proof>
</goal>
<goal name="SquareNonNeg1" sum="49c00266b63c5dd81016599a42c3c974" proved="true" expanded="true">
<goal name="SquareNonNeg1" sum="70ded199aa475245ae7cdcf94f7d1da3" proved="true" expanded="true" shape="ainfix <=c0ainfix *V0V0Iainfix <=V0c0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.02"/>
<result status="timeout" time="9.98"/>
</proof>
</goal>
<goal name="SquareNonNeg" sum="a764585ab6e7bc8dfc325378da917597" proved="true" expanded="true">
<goal name="SquareNonNeg" sum="12fd5ee57cbbcb48649ccac8dfc81690" proved="true" expanded="true" shape="ainfix <=c0ainfix *V0V0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.02"/>
<result status="timeout" time="10.03"/>
</proof>
</goal>
<goal name="ZeroLessOne" sum="56f411cdab6239e1fe4ea11ea3fee8f6" proved="true" expanded="true">
<goal name="ZeroLessOne" sum="bdbf802a95888bb77a6252cc1cb557f7" proved="true" expanded="true" shape="ainfix <=c0c1">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.22"/>
<result status="timeout" time="9.98"/>
</proof>
</goal>
</theory>
<theory name="MinMax" verified="true" expanded="true">
<goal name="G" sum="c78ae26be8a59b8e491e9ac728bbc370" proved="true" expanded="true">
<goal name="G" sum="5ae270cf2070b36d0278c96a283e2a4d" proved="true" expanded="true" shape="ainfix =aminc1aminc3c2c1">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -153,10 +162,10 @@
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.18"/>
<result status="timeout" time="10.21"/>
</proof>
</goal>
</theory>
......
examples/check-builtin/intreal/why3session.xml
View file @ 9eb8c83c
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/check-builtin/intreal/why3session.xml">
<file name="../intreal.why" verified="false" expanded="true">
<theory name="IntReal" verified="false" expanded="true">
<goal name="G1" sum="41cbb072f0422d7fc2669af8ba21266b" proved="true" expanded="true">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<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="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../intreal.why" verified="true" expanded="true">
<theory name="IntReal" verified="true" expanded="true">
<goal name="G1" sum="06e7d94a89ff43145486bcbcbc3d7c13" proved="true" expanded="true" shape="ainfix =afrom_intc2c2.0">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.29"/>
<result status="unknown" time="0.16"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.11"/>
<result status="valid" time="0.07"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="9.71"/>
<result status="timeout" time="10.04"/>
</proof>
</goal>
<goal name="G2" sum="fc8aef6289612cfc6453aa02b65cb4d7" proved="true" expanded="true">
<goal name="G2" sum="5f25c7c89671e1d17dbb5851f1feb031" proved="true" expanded="true" shape="ainfix =afloorc1.5c1">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="1.13"/>
<result status="valid" time="0.93"/>
</proof>
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.04"/>
<result status="timeout" time="10.07"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.12"/>
<result status="timeout" time="10.05"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="9.80"/>
<result status="timeout" time="10.18"/>
</proof>
</goal>
<goal name="G3" sum="2b144ec692c704a919d42bcaaa43cccc" proved="true" expanded="true">
<goal name="G3" sum="55c350ce0a116adb480c1cddea69ba0b" proved="true" expanded="true" shape="ainfix =aceilc1.5c2">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="1.70"/>
<result status="valid" time="1.22"/>
</proof>
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.03"/>
<result status="timeout" time="10.04"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.11"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.09"/>
<result status="timeout" time="10.04"/>
</proof>
</goal>
<goal name="G4" sum="b72371e68b7e34dd72abf019ccb87857" proved="false" expanded="true">
<goal name="G4" sum="5d309eab0cb446104475d2a1e77ae019" proved="true" expanded="true" shape="ainfix =aflooraprefix -.c1.5aprefix -c2">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="6.56"/>
<result status="valid" time="4.36"/>
</proof>
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.07"/>
<result status="timeout" time="10.05"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.11"/>
<result status="timeout" time="10.05"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="9.89"/>
<result status="timeout" time="10.47"/>
</proof>
</goal>
<goal name="G5" sum="ebaa33d09abd898b1e9a54523d586c6d" proved="false" expanded="true">
<goal name="G5" sum="b646c11d8de292cdd85c8ab29a8c887c" proved="true" expanded="true" shape="ainfix =aceilaprefix -.c1.5aprefix -c1">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="7.67"/>
<result status="valid" time="5.46"/>
</proof>
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.08"/>
<result status="timeout" time="10.06"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.22"/>
<result status="timeout" time="10.04"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="9.92"/>
<result status="timeout" time="10.28"/>
</proof>
</goal>
<goal name="G6" sum="a6faa76e2ab2363d3142000b50f8e230" proved="true" expanded="true">
<goal name="G6" sum="a26ce155ad2967fb2870399291ee938b" proved="true" expanded="true" shape="ainfix <=afloorV0aceilV0F">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.14"/>
<result status="valid" time="0.05"/>
</proof>
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.22"/>
<result status="timeout" time="10.08"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.48"/>
<result status="valid" time="0.30"/>
</proof>
</goal>
<goal name="G7" sum="6c4f130bd29b7d8dad7df3d02454e299" proved="true" expanded="true">
<goal name="G7" sum="62043952a600fc351594ea3c5fc79346" proved="true" expanded="true" shape="ainfix =afrom_intafloorV0V0NIainfix <afloorV0aceilV0F">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.11"/>
</proof>
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.11"/>
<result status="timeout" time="10.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.12"/>
<result status="timeout" time="10.03"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.27"/>
<result status="timeout" time="10.42"/>
</proof>
</goal>
</theory>
......
examples/check-builtin/minmax/why3session.xml
View file @ 9eb8c83c
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/check-builtin/minmax/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<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="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../minmax.why" verified="true" expanded="true">
<theory name="MinMax" verified="true" expanded="true">
<goal name="G" sum="351de8b4cf3d0c7d450f7d1d2f9cc553" proved="true" expanded="true">
<goal name="G" sum="f61c7c570e2c5d86e58a28a20684d47d" proved="true" expanded="true" shape="ainfix =aminV0amaxaminV2V0V1V0IageV1V0IageV2V0IageV2V1F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -11,13 +20,13 @@
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="G2" sum="8baabb472e41827dd5336185f0c4a555" proved="true" expanded="true">
<goal name="G2" sum="f12ac01ccd7911072c03b4e7312a8955" proved="true" expanded="true" shape="ageV0V1Iainfix =amaxV0V1V0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -25,10 +34,10 @@
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
......