Skip to content

why3
why3
Commit 9b17d241 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

update sessions after the last commit

parent 1b769a78
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 2690 additions and 2856 deletions
examples/bts/12475/why3session.xml
View file @ 9b17d241
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="examples/bts/12475/why3session.xml">
name="bts/12475/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -21,10 +21,10 @@
<file
name="../12475.why"
verified="true"
expanded="true">
expanded="false">
<theory
name="Stmt"
locfile="examples/bts/12475/../12475.why"
locfile="bts/12475/../12475.why"
loclnum="1" loccnumb="7" loccnume="11"
verified="true"
expanded="true">
......@@ -33,9 +33,9 @@
</label>
<goal
name="toto"
locfile="examples/bts/12475/../12475.why"
locfile="bts/12475/../12475.why"
loclnum="6" loccnumb="7" loccnume="11"
sum="2ba9689c5337113bcea3af15657e9144"
sum="bef94593fc244d7e427d59e3543a820b"
proved="true"
expanded="true"
shape="ainfix <V0ainfix +aroundaUpV0c1.F">
......@@ -44,7 +44,7 @@
timelimit="2"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
......
examples/bts/12934/why3session.xml
View file @ 9b17d241
......@@ -3,68 +3,32 @@
<why3session
name="bts/12934/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.94"/>
<prover
id="coq"
id="0"
name="Coq"
version="8.3pl3"/>
<prover
id="cvc3-2.2"
name="CVC3"
version="2.2"/>
<prover
id="eprover"
name="Eprover"
version="1.4"/>
<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-2"
name="Z3"
version="2.19"/>
<file
name="../12934.why"
verified="true"
expanded="true">
expanded="false">
<theory
name="BTS12934"
locfile="bts/12934/../12934.why"
loclnum="2" loccnumb="7" loccnume="15"
verified="true"
expanded="true">
<goal
name="t"
sum="4ea941b2e4ad31dfd61e8106d4db42ad"
locfile="bts/12934/../12934.why"
loclnum="8" loccnumb="7" loccnume="8"
sum="9432f4497e1405d3077c8e5e4666a0fa"
proved="true"
expanded="true"
shape="t">
<proof
prover="coq"
prover="0"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.45"/>
</proof>
</goal>
......
examples/bts/13849/why3session.xml
View file @ 9b17d241
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="examples/bts/13849/why3session.xml">
name="bts/13849/why3session.xml">
<prover
id="0"
name="Coq"
......@@ -9,18 +9,18 @@
<file
name="../13849.why"
verified="true"
expanded="true">
expanded="false">
<theory
name="T"
locfile="examples/bts/13849/../13849.why"
locfile="bts/13849/../13849.why"
loclnum="4" loccnumb="7" loccnume="8"
verified="true"
expanded="true">
<goal
name="x"
locfile="examples/bts/13849/../13849.why"
locfile="bts/13849/../13849.why"
loclnum="19" loccnumb="6" loccnume="7"
sum="15dd0a14b365705789dc555517dcc6cd"
sum="f9dfa1ef69ac351dd3f83658b2409a0d"
proved="true"
expanded="true"
shape="ainfix =ab1ab2">
......
examples/bts/13853/why3session.xml
View file @ 9b17d241
......@@ -21,7 +21,7 @@
locfile="bts/13853/../13853.mlw"
loclnum="16" loccnumb="8" loccnume="9"
expl="exceptional postcondition"
sum="e1beec1ee049a06190316b698fd46877"
sum="b94bdf7e8e0d350ccc769aa2abfed2a5"
proved="true"
expanded="false"
shape="t">
......@@ -41,7 +41,7 @@
locfile="bts/13853/../13853.mlw"
loclnum="18" loccnumb="7" loccnume="8"
expl="exceptional postcondition"
sum="5e073fd874cb745c16e29e63a5caab88"
sum="290f50192a8d9eb5fed96206ef53b3b4"
proved="true"
expanded="false"
shape="t">
......
examples/bts/13854/why3session.xml
View file @ 9b17d241
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="13854/why3session.xml">
name="bts/13854/why3session.xml">
<prover
id="0"
name="Coq"
......@@ -9,18 +9,18 @@
<file
name="../13854.why"
verified="true"
expanded="true">
expanded="false">
<theory
name="T"
locfile="13854/../13854.why"
locfile="bts/13854/../13854.why"
loclnum="1" loccnumb="7" loccnume="8"
verified="true"
expanded="true">
<goal
name="g"
locfile="13854/../13854.why"
locfile="bts/13854/../13854.why"
loclnum="6" loccnumb="7" loccnume="8"
sum="54a27536c38d94e56a04e1a84c5f21e6"
sum="0fd57a4666fe36603f9625e61ed1a171"
proved="true"
expanded="true"
shape="ainfix =aTuple0afaTuple0">
......@@ -35,9 +35,9 @@
</goal>
<goal
name="x"
locfile="13854/../13854.why"
locfile="bts/13854/../13854.why"
loclnum="8" loccnumb="7" loccnume="8"
sum="0c0178555cd601b6589cfe58c26d04bb"
sum="c90085b1cee92272eb0fef6707c9b64e"
proved="true"
expanded="true"
shape="ainfix =aAaTuple0aBN">
......@@ -47,7 +47,7 @@
edited="13854_T_x_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.45"/>
<result status="valid" time="0.46"/>
</proof>
</goal>
</theory>
......
examples/check-builtin/ac/why3session.xml
View file @ 9b17d241
......@@ -3,124 +3,102 @@
<why3session
name="check-builtin/ac/why3session.xml">
<prover
id="alt-ergo"
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="coq"
name="Coq"
version="8.3pl3"/>
<prover
id="cvc3-2.2"
id="1"
name="CVC3"
version="2.2"/>
<prover
id="eprover"
name="Eprover"
version="1.4"/>
<prover
id="gappa"
name="Gappa"
version="0.15.1"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
id="2"
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-2"
id="3"
name="Z3"
version="2.19"/>
<file
name="../ac.why"
verified="true"
expanded="true">
expanded="false">
<theory
name="Test"
locfile="check-builtin/ac/../ac.why"
loclnum="1" loccnumb="7" loccnume="11"
verified="true"
expanded="true">
<goal
name="G1"
sum="3ed218cda6e2619e7275356787a4dbc5"
locfile="check-builtin/ac/../ac.why"
loclnum="5" loccnumb="12" loccnume="14"
sum="1407925033bf3e71a98c24f86b8de2f8"
proved="true"
expanded="true"
shape="ainfix =afV0V1afV1V0F">
<proof
prover="cvc3-2.2"
prover="3"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
prover="2"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="z3-2"
prover="1"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="spass"
prover="0"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="G2"
sum="cb73bd67a24d5f4f652f750fd1da138a"
locfile="check-builtin/ac/../ac.why"
loclnum="6" loccnumb="12" loccnume="14"
sum="d3e5051a2fd2b6f6b99aab05848f7c06"
proved="true"
expanded="true"
shape="ainfix =afafV0V1V2afV0afV1V2F">
<proof
prover="cvc3-2.2"
prover="3"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
prover="2"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="z3-2"
prover="1"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="spass"
prover="0"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
......
examples/check-builtin/array/why3session.xml
View file @ 9b17d241
......@@ -3,203 +3,177 @@
<why3session
name="check-builtin/array/why3session.xml">
<prover
id="alt-ergo"
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="coq"
name="Coq"
version="8.3pl3"/>
<prover
id="cvc3-2.2"
id="1"
name="CVC3"
version="2.2"/>
<prover
id="cvc3-2.4"
name="CVC3"
version="2.4.1"/>
<prover
id="eprover"
name="Eprover"
version="1.4"/>
<prover
id="gappa"
name="Gappa"
version="0.15.1"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
id="2"
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-2"
id="3"
name="Z3"
version="2.19"/>
<prover
id="z3-3"
name="Z3"
version="3.2"/>
<file
name="../array.why"
verified="true"
expanded="true">
expanded="false">
<theory
name="Test_simplify_array"
locfile="check-builtin/array/../array.why"
loclnum="1" loccnumb="7" loccnume="26"
verified="true"
expanded="true">
<goal
name="G1"
sum="6ac7b14e664f7c570fa1c141483dae7f"
locfile="check-builtin/array/../array.why"
loclnum="4" loccnumb="7" loccnume="9"
sum="4b45d6270f4a53daefb6fce54b8ebff7"
proved="true"
expanded="true"
shape="ainfix =agetasetV2V1V0V1V0FF">
<proof
prover="z3-2"
prover="3"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="cvc3-2.2"
prover="2"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="alt-ergo"
prover="1"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="spass"
prover="0"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="G2"
sum="2416a5181e1123834c475dca4280126f"
locfile="check-builtin/array/../array.why"
loclnum="6" loccnumb="7" loccnume="9"
sum="6ccca0aeacb41ec5118c79435eb055a1"
proved="true"
expanded="true"
shape="ainfix =agetasetV5V0V4V3V1Iainfix =agetV5V3V1Iainfix =V3V0NFF">
<proof
prover="z3-2"
prover="3"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="cvc3-2.2"
prover="2"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="alt-ergo"
prover="1"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="spass"
prover="0"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="G3"
sum="0e53b3897988fa72f807a146e9cf9620"
locfile="check-builtin/array/../array.why"
loclnum="10" loccnumb="7" loccnume="9"
sum="6108a9e01a2539ed185406b5ade7ca86"
proved="true"
expanded="true"
shape="ainfix =agetasetV2c1V1c0V0Iainfix =agetV2c0V0FF">
<proof
prover="z3-2"
prover="3"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="cvc3-2.2"
prover="2"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
obsolete="false"
archived="false">
<result status="valid" time="0.14"/>
</proof>
<proof
prover="alt-ergo"
prover="1"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="spass"
prover="0"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.14"/>
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="G4"
sum="31901caf34b2cb9e49a702d11f0840fb"
locfile="check-builtin/array/../array.why"
loclnum="13" loccnumb="7" loccnume="9"
sum="34fa3208c06f03a03e0897d791b6fa13"
proved="true"
expanded="true"
shape="ainfix =agetasetasetV2c1V1c0V0c1V1FF">
<proof
prover="z3-2"
prover="3"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="cvc3-2.2"
prover="2"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
obsolete="false"
archived="false">
<result status="valid" time="0.22"/>
</proof>
<proof
prover="alt-ergo"
prover="1"
timelimit="10"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="spass"
prover="0"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.23"/>
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
......
examples/check-builtin/bool/why3session.xml
View file @ 9b17d241
......@@ -32,7 +32,7 @@
name="G1"
locfile="check-builtin/bool/../bool.why"
loclnum="4" loccnumb="11" loccnume="13"
sum="1f30b23be48217e149fb64c21f9f9378"
sum="ca83f9c0bba83999ea519362a0f979d3"
proved="true"
expanded="true"
shape="ainfix =aTrueaFalseN">
......@@ -69,7 +69,7 @@
name="G2"
locfile="check-builtin/bool/../bool.why"
loclnum="5" loccnumb="11" loccnume="13"
sum="a7ef2d89ff85180057fa7183acf6c6d2"
sum="5f38ad601b7696e2fe3ba2f557f615e0"
proved="true"
expanded="true"
shape="ainfix =V0aFalseOainfix =V0aTrueF">
......@@ -85,7 +85,7 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
......@@ -106,7 +106,7 @@
name="G3"
locfile="check-builtin/bool/../bool.why"
loclnum="6" loccnumb="11" loccnume="13"
sum="dd23e4302e39a1d20bc5a55f4bb3c2ff"
sum="0787a194d06b1338870206245188cc68"
proved="true"
expanded="true"